Documentation

Mathlib.AlgebraicGeometry.Morphisms.Flat

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) :

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) : (Scheme.Hom.appLE f (↑U) (↑V) e).hom.Flat

Instances

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), (Scheme.Hom.appLE f (↑U) (↑V) e).hom.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] :

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

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

theorem AlgebraicGeometry.Flat.stalkMap {X Y : Scheme} (f : X ⟶ Y) [Flat f] (x : ↑↑X.toPresheafedSpace) :

(Scheme.Hom.stalkMap f x).hom.Flat

theorem AlgebraicGeometry.Flat.iff_flat_stalkMap {X Y : Scheme} (f : X ⟶ Y) :

Flat f ↔ ∀ (x : ↑↑X.toPresheafedSpace), (Scheme.Hom.stalkMap f x).hom.Flat