Theorem: DividedPowers.isDPMorphism.comp (DividedPowers/DPMorphism.lean)

State before:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
⊢ hJ.isDPMorphism hK g → hI.isDPMorphism hJ f → hI.isDPMorphism hK h
Tactic:
intro hg hf
State after:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
⊢ hI.isDPMorphism hK h

State before:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
⊢ hI.isDPMorphism hK h
Tactic:
rw [← hcomp]
State after:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
⊢ hI.isDPMorphism hK (g.comp f)

State before:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
⊢ hI.isDPMorphism hK (g.comp f)
Tactic:
constructor
State after:
case left
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
⊢ Ideal.map (g.comp f) I ≤ K

case right
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
⊢ ∀ (n : ℕ), ∀ a ∈ I, hK.dpow n ((g.comp f) a) = (g.comp f) (hI.dpow n a)

State before:
case left
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
⊢ Ideal.map (g.comp f) I ≤ K
Tactic:
apply le_trans _ hg.1
State after:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
⊢ Ideal.map (g.comp f) I ≤ Ideal.map g J

State before:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
⊢ Ideal.map (g.comp f) I ≤ Ideal.map g J
Tactic:
rw [← Ideal.map_map]
State after:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
⊢ Ideal.map g (Ideal.map f I) ≤ Ideal.map g J

State before:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
⊢ Ideal.map g (Ideal.map f I) ≤ Ideal.map g J
Tactic:
exact Ideal.map_mono hf.1
State after:
no goals

State before:
case right
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
⊢ ∀ (n : ℕ), ∀ a ∈ I, hK.dpow n ((g.comp f) a) = (g.comp f) (hI.dpow n a)
Tactic:
intro n a ha
State after:
case right
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
n : ℕ
a : A
ha : a ∈ I
⊢ hK.dpow n ((g.comp f) a) = (g.comp f) (hI.dpow n a)

State before:
case right
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
n : ℕ
a : A
ha : a ∈ I
⊢ hK.dpow n ((g.comp f) a) = (g.comp f) (hI.dpow n a)
Tactic:
simp only [RingHom.coe_comp, Function.comp_apply]
State after:
case right
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
n : ℕ
a : A
ha : a ∈ I
⊢ hK.dpow n (g (f a)) = g (f (hI.dpow n a))

State before:
case right
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
n : ℕ
a : A
ha : a ∈ I
⊢ hK.dpow n (g (f a)) = g (f (hI.dpow n a))
Tactic:
rw [← hf.2 n a ha]
State after:
case right
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
n : ℕ
a : A
ha : a ∈ I
⊢ hK.dpow n (g (f a)) = g (hJ.dpow n (f a))

State before:
case right
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
n : ℕ
a : A
ha : a ∈ I
⊢ hK.dpow n (g (f a)) = g (hJ.dpow n (f a))
Tactic:
rw [hg.2]
State after:
case right.a
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
n : ℕ
a : A
ha : a ∈ I
⊢ f a ∈ J

State before:
case right.a
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
n : ℕ
a : A
ha : a ∈ I
⊢ f a ∈ J
Tactic:
apply hf.1
State after:
case right.a.a
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
n : ℕ
a : A
ha : a ∈ I
⊢ f a ∈ Ideal.map f I

State before:
case right.a.a
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
n : ℕ
a : A
ha : a ∈ I
⊢ f a ∈ Ideal.map f I
Tactic:
exact Ideal.mem_map_of_mem f ha
State after:
no goals