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.
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
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),
(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
theorem
AlgebraicGeometry.Flat.of_stalkMap
{X Y : Scheme}
(f : X ⟶ Y)
(H : ∀ (x : ↑↑X.toPresheafedSpace), (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.toPresheafedSpace)
: