of_surjective — Mathlib

English

If S is finitely presented over R and I is an ideal, then S/I is finitely presented over R.

Русский

Если S над R имеет конечную презентацию, то фактор-модуль S/I над R имеет конечную презентацию.

LaTeX

$$$[\\text{Algebra.FiniteType R S}] \\Rightarrow \\text{Algebra.FiniteType R (S/I)}$$$

Lean4

theorem of_surjective [FiniteType R A] (f : A →ₐ[R] B) (hf : Surjective f) : FiniteType R B :=
  ⟨by
    convert ‹FiniteType R A›.1.map f
    simpa only [map_top f, @eq_comm _ ⊤, eq_top_iff, AlgHom.mem_range] using hf⟩

Похожие утверждения