English
If f: A →ₐ[R] B is surjective with fg kernel and A is finitely presented, then B is finitely presented.
Русский
Если f: A →ₐ[R] B сюръективно, ядро которого FG, и A имеет конечную презентацию, тогда B имеет конечную презентацию.
LaTeX
$$$f: A \\to B\\quad f \\text{ surjective},\\ ker(f)\\text{ FG},\\ A\\text{ finitely presented }\\Rightarrow B\\text{ finitely presented}$$$
Lean4
/-- If `f : A →ₐ[R] B` is surjective with finitely generated kernel and `A` is finitely presented,
then so is `B`. -/
theorem of_surjective {f : A →ₐ[R] B} (hf : Function.Surjective f) (hker : (RingHom.ker f.toRingHom).FG)
[FinitePresentation R A] : FinitePresentation R B :=
letI : FinitePresentation R (A ⧸ RingHom.ker f) := FinitePresentation.quotient hker
equiv (Ideal.quotientKerAlgEquivOfSurjective hf)
