comp — Mathlib

English

If g and f are finitely presented ring homomorphisms, then their composition g ∘ f is finitely presented.

Русский

Если гомоморфизмы кольца f: A→B и g: B→C являются конечнопредставимыми, то их композиция g∘f: A→C также конечнопредставима.

LaTeX

$$$\\text{If } f:A\\to B \\text{ and } g:B\\to C \\text{ are finitely presented, then } g\\circ f:A\\to C \\text{ is finitely presented.}$$$

Lean4

theorem comp {g : B →+* C} {f : A →+* B} (hg : g.FinitePresentation) (hf : f.FinitePresentation) :
    (g.comp f).FinitePresentation := by
  algebraize [f, g, g.comp f]
  exact Algebra.FinitePresentation.trans A B C

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