Flat morphisms

A morphism of schemes f : X ⟶ Y is flat if for each affine U ⊆ Y and V ⊆ f ⁻¹' U, the induced map Γ(Y, U) ⟶ Γ(X, V) is flat. This is equivalent to asking that all stalk maps are flat (see AlgebraicGeometry.Flat.iff_flat_stalkMap).

We show that this property is local, and are stable under compositions and base change.

class AlgebraicGeometry.Flat {X Y : Scheme} (f : X ⟶ Y) : Prop

A morphism of schemes f : X ⟶ Y is flat if for each affine U ⊆ Y and V ⊆ f ⁻¹' U, the induced map Γ(Y, U) ⟶ Γ(X, V) is flat. This is equivalent to asking that all stalk maps are flat (see AlgebraicGeometry.Flat.iff_flat_stalkMap).

• flat_of_affine_subset (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U) : (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e)).Flat

theorem AlgebraicGeometry.flat_iff {X Y : Scheme} (f : X ⟶ Y) : Flat f ↔ ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e)).Flat

instance AlgebraicGeometry.Flat.instHasRingHomPropertyFlat : HasRingHomProperty @Flat fun {R S : Type u_1} [CommRing R] [CommRing S] => RingHom.Flat

@[instance 900]

instance AlgebraicGeometry.Flat.instOfIsOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : Flat f

instance AlgebraicGeometry.Flat.instIsStableUnderCompositionScheme : CategoryTheory.MorphismProperty.IsStableUnderComposition @Flat

instance AlgebraicGeometry.Flat.comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [hf : Flat f] [hg : Flat g] : Flat (CategoryTheory.CategoryStruct.comp f g)

instance AlgebraicGeometry.Flat.instIsMultiplicativeScheme : CategoryTheory.MorphismProperty.IsMultiplicative @Flat

instance AlgebraicGeometry.Flat.isStableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @Flat

instance AlgebraicGeometry.Flat.instFstScheme {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [Flat g] : Flat (CategoryTheory.Limits.pullback.fst f g)

instance AlgebraicGeometry.Flat.instSndScheme {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [Flat f] : Flat (CategoryTheory.Limits.pullback.snd f g)

instance AlgebraicGeometry.Flat.instMorphismRestrict {X Y : Scheme} (f : X ⟶ Y) (V : Y.Opens) [Flat f] : Flat (f ∣_ V)

instance AlgebraicGeometry.Flat.instResLE {X Y : Scheme} (f : X ⟶ Y) (U : X.Opens) (V : Y.Opens) (e : U ≤ (TopologicalSpace.Opens.map f.base).obj V) [Flat f] : Flat (Scheme.Hom.resLE f V U e)

theorem AlgebraicGeometry.Flat.of_stalkMap {X Y : Scheme} (f : X ⟶ Y) (H : ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat) : Flat f

theorem AlgebraicGeometry.Flat.stalkMap {X Y : Scheme} (f : X ⟶ Y) [Flat f] (x : ↥X) : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat

theorem AlgebraicGeometry.Flat.iff_flat_stalkMap {X Y : Scheme} (f : X ⟶ Y) : Flat f ↔ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat

instance AlgebraicGeometry.Flat.instDescScheme {X : Scheme} {ι : Type v} [Small.{u, v} ι] {Y : ι → Scheme} {f : (i : ι) → Y i ⟶ X} [∀ (i : ι), Flat (f i)] : Flat (CategoryTheory.Limits.Sigma.desc f)

theorem AlgebraicGeometry.Flat.isQuotientMap_of_surjective {X Y : Scheme} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] : Topology.IsQuotientMap ⇑(CategoryTheory.ConcreteCategory.hom f.base)

A surjective, quasi-compact, flat morphism is a quotient map.

theorem AlgebraicGeometry.Flat.epi_of_flat_of_surjective {X Y : Scheme} (f : X ⟶ Y) [Flat f] [Surjective f] : CategoryTheory.Epi f

A flat surjective morphism of schemes is an epimorphism in the category of schemes.