instIsStableUnderCompositionSchemeLocallyOfFinitePresentation

English

LocallyOfFinitePresentation is stable under composition of morphisms.

Русский

LocallyOfFinitePresentation устойчива относительно композиции морфизмов.

LaTeX

$$$\text{LocallyOfFinitePresentation}(f) \land \text{LocallyOfFinitePresentation}(g) \Rightarrow \text{LocallyOfFinitePresentation}(f \circ g).$$$

Lean4

instance : MorphismProperty.IsStableUnderComposition @LocallyOfFinitePresentation :=
  HasRingHomProperty.stableUnderComposition RingHom.finitePresentation_stableUnderComposition

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