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_appLE {U : Y.Opens} : IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Flat

Instances

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

Flat f ↔ ∀ {U : Y.Opens}, IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Flat

theorem AlgebraicGeometry.Scheme.Hom.flat_appLE {X Y : Scheme} (f : X ⟶ Y) [self : Flat f] {U : Y.Opens} :

IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), (CommRingCat.Hom.hom (appLE f U V e)).Flat

Alias of AlgebraicGeometry.Flat.flat_appLE.

@[deprecated AlgebraicGeometry.Scheme.Hom.flat_appLE (since := "2026-01-20")]

theorem AlgebraicGeometry.Flat.flat_of_affine_subset {X Y : Scheme} (f : X ⟶ Y) [self : Flat f] {U : Y.Opens} :

IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Flat

Alias of AlgebraicGeometry.Flat.flat_appLE.

Alias of AlgebraicGeometry.Flat.flat_appLE.

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

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

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.

theorem AlgebraicGeometry.Flat.flat_and_surjective_iff_faithfullyFlat_of_isAffine {X Y : Scheme} (f : X ⟶ Y) [IsAffine X] [IsAffine Y] :

Flat f ∧ Surjective f ↔ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).FaithfullyFlat

theorem AlgebraicGeometry.flat_and_surjective_SpecMap_iff {R S : CommRingCat} (f : R ⟶ S) :

Flat (Spec.map f) ∧ Surjective (Spec.map f) ↔ (CommRingCat.Hom.hom f).FaithfullyFlat