English
The quotient of a finitely presented algebra by a finitely generated ideal is finitely presented.
Русский
Картинка: фактор-пространство над finitely presented algebra по FG идеалу снова finitely presented.
LaTeX
$$$\\forall I \\text{ FG } I \\subset A,\\; \\text{FinitePresentation } R (A/I)$$$
Lean4
/-- The quotient of a finitely presented algebra by a finitely generated ideal is finitely
presented. -/
protected theorem quotient {I : Ideal A} (h : I.FG) [FinitePresentation R A] : FinitePresentation R (A ⧸ I) where
out := by
obtain ⟨n, f, hf⟩ := FinitePresentation.out (R := R) (A := A)
refine ⟨n, (Ideal.Quotient.mkₐ R I).comp f, ?_, ?_⟩
· exact (Ideal.Quotient.mkₐ_surjective R I).comp hf.1
· refine Ideal.fg_ker_comp _ _ hf.2 ?_ hf.1
simp [h]
