instIsStableUnderCompositionScheme

Mathlib.AlgebraicGeometry.Morphisms.Flat

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Flat.instIsStableUnderCompositionScheme

English

Flat morphisms are closed under composition.

Русский

Морфизмы, плоские, замкнуты по композиции.

LaTeX

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

Lean4

instance : MorphismProperty.IsStableUnderComposition @Flat :=
  HasRingHomProperty.stableUnderComposition RingHom.Flat.stableUnderComposition

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru