Theorem: DividedPowers.Quotient.OfSurjective.isDPMorphism (DividedPowers/SubDPIdeal.lean)

State before:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
⊢ hI.isDPMorphism (dividedPowers hI hf hIf) f
Tactic:
constructor
State after:
case left
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
⊢ Ideal.map f I ≤ Ideal.map f I

case right
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
⊢ ∀ (n : ℕ), ∀ a ∈ I, (dividedPowers hI hf hIf).dpow n (f a) = f (hI.dpow n a)

State before:
case left
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
⊢ Ideal.map f I ≤ Ideal.map f I

case right
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
⊢ ∀ (n : ℕ), ∀ a ∈ I, (dividedPowers hI hf hIf).dpow n (f a) = f (hI.dpow n a)
Tactic:
exact le_refl (Ideal.map f I)
State after:
case right
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
⊢ ∀ (n : ℕ), ∀ a ∈ I, (dividedPowers hI hf hIf).dpow n (f a) = f (hI.dpow n a)

State before:
case right
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
⊢ ∀ (n : ℕ), ∀ a ∈ I, (dividedPowers hI hf hIf).dpow n (f a) = f (hI.dpow n a)
Tactic:
intro n a ha
State after:
case right
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
⊢ (dividedPowers hI hf hIf).dpow n (f a) = f (hI.dpow n a)

State before:
case right
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
f : A →+* B
hf : Function.Surjective ⇑f
hIf : hI.isSubDPIdeal (RingHom.ker f ⊓ I)
n : ℕ
a : A
ha : a ∈ I
⊢ (dividedPowers hI hf hIf).dpow n (f a) = f (hI.dpow n a)
Tactic:
rw [dpow_apply hI hf hIf ha]
State after:
no goals