comp — Mathlib

English

If f is finitely presented and g is surjective with a finitely generated kernel, then g ∘ f is finitely presented.

Русский

Если f конечнопредставим и g сюръективен с порожденным ядром, то композиция g∘f конечнопредставима.

LaTeX

$$$f.FinitePresentation \\land Surjective(g) \\land (\\ker g)\\ FG \\Rightarrow (g\\circ f).FinitePresentation$$$

Lean4

theorem comp {g : B →ₐ[R] C} {f : A →ₐ[R] B} (hg : g.FinitePresentation) (hf : f.FinitePresentation) :
    (g.comp f).FinitePresentation :=
  RingHom.FinitePresentation.comp hg hf

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