iff_flat_stalkMap

Mathlib.AlgebraicGeometry.Morphisms.Flat

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

English

Flat f is equivalent to all stalk maps being flat.

Русский

Flat f эквивалентно тому, что все stalk maps плоски.

LaTeX

$$$Flat(f) \\iff \\forall x, (f.stalkMap x).hom.Flat$$$

Lean4

theorem iff_flat_stalkMap : Flat f ↔ ∀ x, (f.stalkMap x).hom.Flat :=
  ⟨fun _ ↦ stalkMap f, fun H ↦ of_stalkMap f H⟩

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

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

Разделы

Аффилиация

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