R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
f✝ : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f✝ = 0
inst✝ : Algebra R S
f : R[X]
ϕ : AdjoinRoot f →ₐ[R] S
⊢ AlgHom.equalizer ϕ (liftHom f (↑ϕ (root f)) (_ : ↑(aeval (↑ϕ (root f))) f = 0)) = ⊤
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
f✝ : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f✝ = 0
inst✝ : Algebra R S
f : R[X]
ϕ : AdjoinRoot f →ₐ[R] S
⊢ liftHom f (↑ϕ (root f)) (_ : ↑(aeval (↑ϕ (root f))) f = 0) = ϕ
suffices ϕ.equalizer (liftHom f (ϕ (root f)) (aeval_algHom_eq_zero f ϕ)) = ⊤ by
  exact (AlgHom.ext fun x => (SetLike.ext_iff.mp this x).mpr Algebra.mem_top).symm
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
f✝ : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f✝ = 0
inst✝ : Algebra R S
f : R[X]
ϕ : AdjoinRoot f →ₐ[R] S
⊢ root f ∈ ↑(AlgHom.equalizer ϕ (liftHom f (↑ϕ (root f)) (_ : ↑(aeval (↑ϕ (root f))) f = 0)))
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
f✝ : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f✝ = 0
inst✝ : Algebra R S
f : R[X]
ϕ : AdjoinRoot f →ₐ[R] S
⊢ AlgHom.equalizer ϕ (liftHom f (↑ϕ (root f)) (_ : ↑(aeval (↑ϕ (root f))) f = 0)) = ⊤
rw [eq_top_iff, ← adjoinRoot_eq_top, Algebra.adjoin_le_iff, Set.singleton_subset_iff]
no goals
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
f✝ : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f✝ = 0
inst✝ : Algebra R S
f : R[X]
ϕ : AdjoinRoot f →ₐ[R] S
⊢ root f ∈ ↑(AlgHom.equalizer ϕ (liftHom f (↑ϕ (root f)) (_ : ↑(aeval (↑ϕ (root f))) f = 0)))
exact (@lift_root _ _ _ _ _ _ _ (aeval_algHom_eq_zero f ϕ)).symm
no goals
R : Type u
S : Type v
K : Type w
inst✝² : CommRing R
f✝ : R[X]
inst✝¹ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f✝ = 0
inst✝ : Algebra R S
f : R[X]
ϕ : AdjoinRoot f →ₐ[R] S
this : AlgHom.equalizer ϕ (liftHom f (↑ϕ (root f)) (_ : ↑(aeval (↑ϕ (root f))) f = 0)) = ⊤
⊢ liftHom f (↑ϕ (root f)) (_ : ↑(aeval (↑ϕ (root f))) f = 0) = ϕ
exact (AlgHom.ext fun x => (SetLike.ext_iff.mp this x).mpr Algebra.mem_top).symm