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_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

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

@[instance 100]

instance AlgebraicGeometry.Flat.instOfSubsingletonCarrierCarrierCommRingCatOfIsIntegral {X Y : Scheme} (f : X ⟶ Y) [Subsingleton ↥Y] [IsIntegral Y] : Flat f

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

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

Sections of fibered products

Suppose we are given the following cartesian square:

Y --g-→ X
|       |
iY      iX
↓       |
T --f-→ S

Let Uₛ be an open of S, Uₓ and Uₜ be opens of X and T mapping into Uₛ. There is a canonical map Γ(X, Uₓ) ⊗[Γ(S, Uₛ)] Γ(T, Uₜ) ⟶ Γ(X ×ₛ T, pr₁ ⁻¹ Uₓ ∩ pr₂ ⁻¹ Uₜ).

We show that this map is

1. isIso_pushoutSection_of_isAffineOpen: bijective when Uₛ, Uₜ, and Uₓ are all affine.
2. mono_pushoutSection_of_isCompact_of_flat_right: injective when Uₛ, Uₜ are affine, Uₓ is compact, and f is flat.
3. isIso_pushoutSection_of_isQuasiSeparated_of_flat_right: bijective when Uₛ, Uₜ are affine, Uₓ is qcqs, and f is flat.
4. mono_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat: injective when Uₛ is affine, Uₜ is compact, Uₓ is qcqs, f is flat, and Γ(T, Uₜ) is flat over Γ(S, Uₛ) (typically true when S = Spec k.)
5. isIso_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat: bijective when Uₛ is affine, Uₜ and Uₓ are qcqs, f is flat, and Γ(T, Uₜ) is flat over Γ(S, Uₛ) (typically true when S = Spec k.)

@[reducible, inline]

abbrev AlgebraicGeometry.pushoutSection {X Y S T : Scheme} {f : T ⟶ S} {g : Y ⟶ X} {iX : X ⟶ S} {iY : Y ⟶ T} (H : CategoryTheory.IsPullback g iY iX f) {US : S.Opens} {UT : T.Opens} {UX : X.Opens} (hUST : UT ≤ (TopologicalSpace.Opens.map f.base).obj US) (hUSX : UX ≤ (TopologicalSpace.Opens.map iX.base).obj US) {UY : Y.Opens} (hUY : UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT) : CategoryTheory.Limits.pushout (Scheme.Hom.appLE iX US UX hUSX) (Scheme.Hom.appLE f US UT hUST) ⟶ Y.presheaf.obj (Opposite.op UY)

The canonical map Γ(X, Uₓ) ⊗[Γ(S, Uₛ)] Γ(T, Uₜ) ⟶ Γ(X ×ₛ T, pr₁ ⁻¹ Uₓ ∩ pr₂ ⁻¹ Uₜ). This is an isomorphism under various circumstances.

theorem AlgebraicGeometry.isIso_pushoutSection_iff {X Y S T : Scheme} {f : T ⟶ S} {g : Y ⟶ X} {iX : X ⟶ S} {iY : Y ⟶ T} (H : CategoryTheory.IsPullback g iY iX f) {US : S.Opens} {UT : T.Opens} {UX : X.Opens} (hUST : UT ≤ (TopologicalSpace.Opens.map f.base).obj US) (hUSX : UX ≤ (TopologicalSpace.Opens.map iX.base).obj US) {UY : Y.Opens} (hUY : UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT) : CategoryTheory.IsIso (pushoutSection H hUST hUSX hUY) ↔ CategoryTheory.IsPushout (Scheme.Hom.appLE iX US UX hUSX) (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE g UX UY ⋯) (Scheme.Hom.appLE iY UT UY ⋯)

theorem AlgebraicGeometry.isIso_pushoutSection_of_isAffineOpen {X Y S T : Scheme} {f : T ⟶ S} {g : Y ⟶ X} {iX : X ⟶ S} {iY : Y ⟶ T} (H : CategoryTheory.IsPullback g iY iX f) {US : S.Opens} {UT : T.Opens} {UX : X.Opens} (hUST : UT ≤ (TopologicalSpace.Opens.map f.base).obj US) (hUSX : UX ≤ (TopologicalSpace.Opens.map iX.base).obj US) {UY : Y.Opens} (hUY : UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT) (hUS : IsAffineOpen US) (hUT : IsAffineOpen UT) (hUX : IsAffineOpen UX) : CategoryTheory.IsIso (pushoutSection H hUST hUSX hUY)

theorem AlgebraicGeometry.mono_pushoutSection_of_iSup_eq {X Y S T : Scheme} {f : T ⟶ S} {g : Y ⟶ X} {iX : X ⟶ S} {iY : Y ⟶ T} (H : CategoryTheory.IsPullback g iY iX f) {US : S.Opens} {UT : T.Opens} {UX : X.Opens} (hUST : UT ≤ (TopologicalSpace.Opens.map f.base).obj US) (hUSX : UX ≤ (TopologicalSpace.Opens.map iX.base).obj US) {UY : Y.Opens} (hUY : UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT) {ι : Type u_1} [Finite ι] (VX : ι → X.Opens) (hVU : iSup VX = UX) (hV : ∀ (i : ι), CategoryTheory.Mono (pushoutSection H hUST ⋯ ⋯)) (hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat) : CategoryTheory.Mono (pushoutSection H hUST hUSX hUY)

theorem AlgebraicGeometry.isIso_pushoutSection_of_iSup_eq {X Y S T : Scheme} {f : T ⟶ S} {g : Y ⟶ X} {iX : X ⟶ S} {iY : Y ⟶ T} (H : CategoryTheory.IsPullback g iY iX f) {US : S.Opens} {UT : T.Opens} {UX : X.Opens} (hUST : UT ≤ (TopologicalSpace.Opens.map f.base).obj US) (hUSX : UX ≤ (TopologicalSpace.Opens.map iX.base).obj US) {UY : Y.Opens} (hUY : UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT) {ι : Type u} [Finite ι] (VX : ι → X.Opens) (hVU : iSup VX = UX) (hV : ∀ (i : ι), CategoryTheory.IsIso (pushoutSection H hUST ⋯ ⋯)) (hV' : ∀ (i j : ι), CategoryTheory.Mono (pushoutSection H hUST ⋯ ⋯)) (hT : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat) : CategoryTheory.IsIso (pushoutSection H hUST hUSX hUY)

theorem AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_right {X Y S T : Scheme} {f : T ⟶ S} {g : Y ⟶ X} {iX : X ⟶ S} {iY : Y ⟶ T} (H : CategoryTheory.IsPullback g iY iX f) {US : S.Opens} {UT : T.Opens} {UX : X.Opens} (hUST : UT ≤ (TopologicalSpace.Opens.map f.base).obj US) (hUSX : UX ≤ (TopologicalSpace.Opens.map iX.base).obj US) {UY : Y.Opens} (hUY : UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT) [Flat f] (hUS : IsAffineOpen US) (hUT : IsAffineOpen UT) (hUX : IsCompact ↑UX) : CategoryTheory.Mono (pushoutSection H hUST hUSX hUY)

theorem AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_left {X Y S T : Scheme} {f : T ⟶ S} {g : Y ⟶ X} {iX : X ⟶ S} {iY : Y ⟶ T} (H : CategoryTheory.IsPullback g iY iX f) {US : S.Opens} {UT : T.Opens} {UX : X.Opens} (hUST : UT ≤ (TopologicalSpace.Opens.map f.base).obj US) (hUSX : UX ≤ (TopologicalSpace.Opens.map iX.base).obj US) {UY : Y.Opens} (hUY : UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT) [Flat iX] (hUS : IsAffineOpen US) (hUX : IsAffineOpen UX) (hUT : IsCompact ↑UT) : CategoryTheory.Mono (pushoutSection H hUST hUSX hUY)

theorem AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_right {X Y S T : Scheme} {f : T ⟶ S} {g : Y ⟶ X} {iX : X ⟶ S} {iY : Y ⟶ T} (H : CategoryTheory.IsPullback g iY iX f) {US : S.Opens} {UT : T.Opens} {UX : X.Opens} (hUST : UT ≤ (TopologicalSpace.Opens.map f.base).obj US) (hUSX : UX ≤ (TopologicalSpace.Opens.map iX.base).obj US) {UY : Y.Opens} (hUY : UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT) [Flat f] (hUS : IsAffineOpen US) (hUT : IsAffineOpen UT) (hUX : IsCompact ↑UX) (hUX' : IsQuasiSeparated ↑UX) : CategoryTheory.IsIso (pushoutSection H hUST hUSX hUY)

theorem AlgebraicGeometry.isIso_pushoutSection_of_isQuasiSeparated_of_flat_left {X Y S T : Scheme} {f : T ⟶ S} {g : Y ⟶ X} {iX : X ⟶ S} {iY : Y ⟶ T} (H : CategoryTheory.IsPullback g iY iX f) {US : S.Opens} {UT : T.Opens} {UX : X.Opens} (hUST : UT ≤ (TopologicalSpace.Opens.map f.base).obj US) (hUSX : UX ≤ (TopologicalSpace.Opens.map iX.base).obj US) {UY : Y.Opens} (hUY : UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT) [Flat iX] (hUS : IsAffineOpen US) (hUX : IsAffineOpen UX) (hUT : IsCompact ↑UT) (hUT' : IsQuasiSeparated ↑UT) : CategoryTheory.IsIso (pushoutSection H hUST hUSX hUY)

theorem AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_left_of_ringHomFlat {X Y S T : Scheme} {f : T ⟶ S} {g : Y ⟶ X} {iX : X ⟶ S} {iY : Y ⟶ T} (H : CategoryTheory.IsPullback g iY iX f) {US : S.Opens} {UT : T.Opens} {UX : X.Opens} (hUST : UT ≤ (TopologicalSpace.Opens.map f.base).obj US) (hUSX : UX ≤ (TopologicalSpace.Opens.map iX.base).obj US) {UY : Y.Opens} (hUY : UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT) [Flat iX] (hUS : IsAffineOpen US) (hUT : IsCompact ↑UT) (hUX : IsCompact ↑UX) (hf : (CommRingCat.Hom.hom (Scheme.Hom.appLE f US UT hUST)).Flat) : CategoryTheory.Mono (pushoutSection H hUST hUSX hUY)

theorem AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat {X Y S T : Scheme} {f : T ⟶ S} {g : Y ⟶ X} {iX : X ⟶ S} {iY : Y ⟶ T} (H : CategoryTheory.IsPullback g iY iX f) {US : S.Opens} {UT : T.Opens} {UX : X.Opens} (hUST : UT ≤ (TopologicalSpace.Opens.map f.base).obj US) (hUSX : UX ≤ (TopologicalSpace.Opens.map iX.base).obj US) {UY : Y.Opens} (hUY : UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT) [Flat f] (hUS : IsAffineOpen US) (hUT : IsCompact ↑UT) (hUX : IsCompact ↑UX) (hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat) : CategoryTheory.Mono (pushoutSection H hUST hUSX hUY)

theorem AlgebraicGeometry.isIso_pushoutSection_of_isCompact_of_flat_right_of_ringHomFlat {X Y S T : Scheme} {f : T ⟶ S} {g : Y ⟶ X} {iX : X ⟶ S} {iY : Y ⟶ T} (H : CategoryTheory.IsPullback g iY iX f) {US : S.Opens} {UT : T.Opens} {UX : X.Opens} (hUST : UT ≤ (TopologicalSpace.Opens.map f.base).obj US) (hUSX : UX ≤ (TopologicalSpace.Opens.map iX.base).obj US) {UY : Y.Opens} (hUY : UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT) [Flat f] (hUS : IsAffineOpen US) (hUT : IsCompact ↑UT) (hUT' : IsQuasiSeparated ↑UT) (hUX : IsCompact ↑UX) (hUX' : IsQuasiSeparated ↑UX) (hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat) : CategoryTheory.IsIso (pushoutSection H hUST hUSX hUY)