of_stalkMap — Mathlib

English

A morphism is flat if and only if all stalk maps are flat ring homomorphisms.

Русский

Морфизм плоский тогда и только тогда, когда все stalk map-ы плоские как кольцевые гомоморфизмы.

LaTeX

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

Lean4

theorem of_stalkMap (H : ∀ x, (f.stalkMap x).hom.Flat) : Flat f :=
  HasRingHomProperty.of_stalkMap RingHom.Flat.ofLocalizationPrime H

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