finitePresentation_stableUnderComposition

English

Being finitely presented is stable under composition of ring homomorphisms: if f and g are finitely presented, then g ∘ f is finitely presented.

Русский

Свойство конечного презентирования сохраняется при композиции: если f и g — конечнопредставляющие гомоморфизмы колец, то их композиция g ∘ f тоже конечнопредставлена.

LaTeX

$$$\text{If } f: R \to S$ and $g: S \to T$ are RingHom.FinitePresentation,\ then\ g \circ f: R \to T\ is\ RingHom.FinitePresentation.$$$

Lean4

/-- Being finitely-presented is stable under composition. -/
theorem finitePresentation_stableUnderComposition : StableUnderComposition @FinitePresentation :=
  by
  introv R hf hg
  exact hg.comp hf

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