comp

Mathlib.AlgebraicGeometry.Morphisms.Flat

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

English

If f and g are flat, then their composition is flat.

Русский

Если f и g плоские, то их композиция плоская.

LaTeX

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

Lean4

instance comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [hf : Flat f] [hg : Flat g] : Flat (f ≫ g) :=
  MorphismProperty.comp_mem _ f g hf hg

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

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

Разделы

Аффилиация

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