case intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Surjective ↑f
hRB : FinitePresentation R B
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] A
hg : Surjective ↑g
right✝ : Ideal.FG (RingHom.ker ↑g)
⊢ Ideal.FG (RingHom.ker ↑f)
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Surjective ↑f
hRA : FinitePresentation R A
hRB : FinitePresentation R B
⊢ Ideal.FG (RingHom.ker ↑f)
obtain ⟨n, g, hg, _⟩ := hRA
case h.e'_3
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Surjective ↑f
hRB : FinitePresentation R B
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] A
hg : Surjective ↑g
right✝ : Ideal.FG (RingHom.ker ↑g)
⊢ RingHom.ker ↑f = Ideal.map (↑g) (RingHom.ker ↑(AlgHom.comp f g))
case intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Surjective ↑f
hRB : FinitePresentation R B
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] A
hg : Surjective ↑g
right✝ : Ideal.FG (RingHom.ker ↑g)
⊢ Ideal.FG (RingHom.ker ↑f)
convert (ker_fg_of_mvPolynomial (f.comp g) (hf.comp hg) hRB).map g.toRingHom
case h.e'_3
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Surjective ↑f
hRB : FinitePresentation R B
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] A
hg : Surjective ↑g
right✝ : Ideal.FG (RingHom.ker ↑g)
⊢ Ideal.comap ↑f ⊥ = Ideal.map (↑g) (Ideal.comap (RingHom.comp ↑f ↑g) ⊥)
case h.e'_3
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Surjective ↑f
hRB : FinitePresentation R B
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] A
hg : Surjective ↑g
right✝ : Ideal.FG (RingHom.ker ↑g)
⊢ RingHom.ker ↑f = Ideal.map (↑g) (RingHom.ker ↑(AlgHom.comp f g))
simp_rw [RingHom.ker_eq_comap_bot, AlgHom.toRingHom_eq_coe, AlgHom.comp_toRingHom]
no goals
case h.e'_3
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Surjective ↑f
hRB : FinitePresentation R B
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] A
hg : Surjective ↑g
right✝ : Ideal.FG (RingHom.ker ↑g)
⊢ Ideal.comap ↑f ⊥ = Ideal.map (↑g) (Ideal.comap (RingHom.comp ↑f ↑g) ⊥)
rw [← Ideal.comap_comap, Ideal.map_comap_of_surjective (g : MvPolynomial (Fin n) R →+* A) hg]