instFstScheme

Mathlib.AlgebraicGeometry.Morphisms.Flat

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

English

If g: Y → S is flat, then the first projection of a pullback is flat.

Русский

Если g: Y → S плоский, то первая проекция в тягодном витке (pullback) плоская.

LaTeX

$$$\\text{Flat}(g) \\Rightarrow \\text{Flat}(\\text{pullback.fst } f \\; g)$$$

Lean4

instance {X Y Z : Scheme.{u}} (f : X ⟶ Z) (g : Y ⟶ Z) [Flat g] : Flat (pullback.fst f g) :=
  MorphismProperty.pullback_fst _ _ inferInstance

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

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

Разделы

Аффилиация

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