Theorem: DividedPowers.le_equalizer_of_dp_morphism (DividedPowers/SubDPIdeal.lean)

State before:
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
⊢ Ideal.map f I ≤ hK.dpEqualizer hK'
Tactic:
rw [Ideal.map]
State after:
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
⊢ Ideal.span (⇑f '' ↑I) ≤ hK.dpEqualizer hK'

State before:
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
⊢ Ideal.span (⇑f '' ↑I) ≤ hK.dpEqualizer hK'
Tactic:
rw [Ideal.span_le]
State after:
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
⊢ ⇑f '' ↑I ⊆ ↑(hK.dpEqualizer hK')

State before:
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
⊢ ⇑f '' ↑I ⊆ ↑(hK.dpEqualizer hK')
Tactic:
rintro b ⟨a, ha, rfl⟩
State after:
case intro.intro
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ ↑I
⊢ f a ∈ ↑(hK.dpEqualizer hK')

State before:
case intro.intro
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ ↑I
⊢ f a ∈ ↑(hK.dpEqualizer hK')
Tactic:
simp only [SetLike.mem_coe] at ha ⊢
State after:
case intro.intro
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ I
⊢ f a ∈ hK.dpEqualizer hK'

State before:
case intro.intro
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ I
⊢ f a ∈ hK.dpEqualizer hK'
Tactic:
rw [mem_dpEqualizer_iff]
State after:
case intro.intro
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ I
⊢ f a ∈ K ∧ ∀ (n : ℕ), hK.dpow n (f a) = hK'.dpow n (f a)

State before:
case intro.intro
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ I
⊢ f a ∈ K ∧ ∀ (n : ℕ), hK.dpow n (f a) = hK'.dpow n (f a)
Tactic:
constructor
State after:
case intro.intro.left
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ I
⊢ f a ∈ K

case intro.intro.right
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ I
⊢ ∀ (n : ℕ), hK.dpow n (f a) = hK'.dpow n (f a)

State before:
case intro.intro.left
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ I
⊢ f a ∈ K

case intro.intro.right
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ I
⊢ ∀ (n : ℕ), hK.dpow n (f a) = hK'.dpow n (f a)
Tactic:
apply hI_le_K
State after:
case intro.intro.left.a
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ I
⊢ f a ∈ Ideal.map f I

case intro.intro.right
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ I
⊢ ∀ (n : ℕ), hK.dpow n (f a) = hK'.dpow n (f a)

State before:
case intro.intro.left.a
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ I
⊢ f a ∈ Ideal.map f I

case intro.intro.right
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ I
⊢ ∀ (n : ℕ), hK.dpow n (f a) = hK'.dpow n (f a)
Tactic:
exact Ideal.mem_map_of_mem f ha
State after:
case intro.intro.right
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ I
⊢ ∀ (n : ℕ), hK.dpow n (f a) = hK'.dpow n (f a)

State before:
case intro.intro.right
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : hI.isDPMorphism hK f
hIK' : hI.isDPMorphism hK' f
a : A
ha : a ∈ I
⊢ ∀ (n : ℕ), hK.dpow n (f a) = hK'.dpow n (f a)
Tactic:
simp only [isDPMorphism, Ideal.map_id, RingHom.id_apply] at hIK hIK'
State after:
case intro.intro.right
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : Ideal.map f I ≤ K ∧ ∀ (n : ℕ), ∀ a ∈ I, hK.dpow n (f a) = f (hI.dpow n a)
hIK' : Ideal.map f I ≤ K ∧ ∀ (n : ℕ), ∀ a ∈ I, hK'.dpow n (f a) = f (hI.dpow n a)
a : A
ha : a ∈ I
⊢ ∀ (n : ℕ), hK.dpow n (f a) = hK'.dpow n (f a)

State before:
case intro.intro.right
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : Ideal.map f I ≤ K ∧ ∀ (n : ℕ), ∀ a ∈ I, hK.dpow n (f a) = f (hI.dpow n a)
hIK' : Ideal.map f I ≤ K ∧ ∀ (n : ℕ), ∀ a ∈ I, hK'.dpow n (f a) = f (hI.dpow n a)
a : A
ha : a ∈ I
⊢ ∀ (n : ℕ), hK.dpow n (f a) = hK'.dpow n (f a)
Tactic:
intro n
State after:
case intro.intro.right
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : Ideal.map f I ≤ K ∧ ∀ (n : ℕ), ∀ a ∈ I, hK.dpow n (f a) = f (hI.dpow n a)
hIK' : Ideal.map f I ≤ K ∧ ∀ (n : ℕ), ∀ a ∈ I, hK'.dpow n (f a) = f (hI.dpow n a)
a : A
ha : a ∈ I
n : ℕ
⊢ hK.dpow n (f a) = hK'.dpow n (f a)

State before:
case intro.intro.right
A✝ : Type ?u.88948
inst✝² : CommSemiring A✝
I✝ : Ideal A✝
hI✝ : DividedPowers I✝
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommSemiring B
f : A →+* B
K : Ideal B
hI_le_K : Ideal.map f I ≤ K
hK hK' : DividedPowers K
hIK : Ideal.map f I ≤ K ∧ ∀ (n : ℕ), ∀ a ∈ I, hK.dpow n (f a) = f (hI.dpow n a)
hIK' : Ideal.map f I ≤ K ∧ ∀ (n : ℕ), ∀ a ∈ I, hK'.dpow n (f a) = f (hI.dpow n a)
a : A
ha : a ∈ I
n : ℕ
⊢ hK.dpow n (f a) = hK'.dpow n (f a)
Tactic:
rw [hIK.2 n a ha, hIK'.2 n a ha]
State after:
no goals