English
If f: A →ₐ[R] B is surjective, then the kernel is FG provided A and B are finitely presented in the appropriate sense.
Русский
Если f: A →ₐ[R] B сюръективно, ядро FG при условии конечной презентации A и B.
LaTeX
$$$\\forall f : A \\to B,\\; Surjective f \\Rightarrow (\\ker f).FG$ при предположении конечной презентации$$
Lean4
/-- If `f : A →ₐ[R] B` is a surjection between finitely-presented `R`-algebras, then the kernel of
`f` is finitely generated. -/
theorem ker_fG_of_surjective (f : A →ₐ[R] B) (hf : Function.Surjective f) [FinitePresentation R A]
[FinitePresentation R B] : (RingHom.ker f.toRingHom).FG :=
by
obtain ⟨n, g, hg, _⟩ := FinitePresentation.out (R := R) (A := A)
convert (ker_fg_of_mvPolynomial (f.comp g) (hf.comp hg)).map g.toRingHom
simp_rw [RingHom.ker_eq_comap_bot, AlgHom.toRingHom_eq_coe, AlgHom.comp_toRingHom]
rw [← Ideal.comap_comap, Ideal.map_comap_of_surjective (g : MvPolynomial (Fin n) R →+* A) hg]
