feat(AlgebraicGeometry): flat morphisms of schemes

Mathlib.lean

@@ -980,6 +980,7 @@ import Mathlib.AlgebraicGeometry.Morphisms.Etale
 import Mathlib.AlgebraicGeometry.Morphisms.Finite
 import Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
 import Mathlib.AlgebraicGeometry.Morphisms.FiniteType
+import Mathlib.AlgebraicGeometry.Morphisms.Flat
 import Mathlib.AlgebraicGeometry.Morphisms.Immersion
 import Mathlib.AlgebraicGeometry.Morphisms.Integral
 import Mathlib.AlgebraicGeometry.Morphisms.IsIso

Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

@@ -544,6 +544,13 @@ variable (φ) in
 @[simp] lemma Spec.preimage_map : Spec.preimage (Spec.map φ) = φ :=
   Spec.map_injective (Spec.map_preimage (Spec.map φ))
 
+/-- Useful for replacing `f` by `Spec.map φ` everywhere in proofs. -/
+lemma Spec.map_surjective {R S : CommRingCat} :
+    Function.Surjective (Spec.map : (R ⟶ S) → _) := by
+  intro f
+  use Spec.preimage f
+  simp
+
 /-- Spec is fully faithful -/
 @[simps]
 def Spec.homEquiv {R S : CommRingCat} : (Spec S ⟶ Spec R) ≃ (R ⟶ S) where

Mathlib/AlgebraicGeometry/Morphisms/Flat.lean

@@ -0,0 +1,74 @@
+/-
+Copyright (c) 2024 Christian Merten. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Merten
+-/
+import Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
+import Mathlib.RingTheory.RingHom.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.
+
+We show that this property is local, and are stable under compositions and base change.
+
+-/
+
+noncomputable section
+
+open CategoryTheory CategoryTheory.Limits Opposite TopologicalSpace
+
+universe v u
+
+namespace AlgebraicGeometry
+
+variable {X Y : Scheme.{u}} (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.
+-/
+@[mk_iff]
+class Flat (f : X ⟶ Y) : Prop where
+  flat_of_affine_subset :
+    ∀ (U : Y.affineOpens) (V : X.affineOpens) (e : V.1 ≤ f ⁻¹ᵁ U.1), (f.appLE U V e).hom.Flat
+
+namespace Flat
+
+instance : HasRingHomProperty @Flat RingHom.Flat where
+  isLocal_ringHomProperty := RingHom.Flat.propertyIsLocal
+  eq_affineLocally' := by
+    ext X Y f
+    rw [flat_iff, affineLocally_iff_affineOpens_le]
+
+instance (priority := 900) [IsOpenImmersion f] : Flat f :=
+  HasRingHomProperty.of_isOpenImmersion
+    RingHom.Flat.containsIdentities
+
+instance : MorphismProperty.IsStableUnderComposition @Flat :=
+  HasRingHomProperty.stableUnderComposition RingHom.Flat.stableUnderComposition
+
+instance comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
+    [hf : Flat f] [hg : Flat g] : Flat (f ≫ g) :=
+  MorphismProperty.comp_mem _ f g hf hg
+
+instance : MorphismProperty.IsMultiplicative @Flat where
+  id_mem _ := inferInstance
+
+instance isStableUnderBaseChange : MorphismProperty.IsStableUnderBaseChange @Flat :=
+  HasRingHomProperty.isStableUnderBaseChange RingHom.Flat.isStableUnderBaseChange
+
+lemma of_stalkMap (H : ∀ x, (f.stalkMap x).hom.Flat) : Flat f :=
+  HasRingHomProperty.of_stalkMap RingHom.Flat.ofLocalizationPrime H
+
+lemma stalkMap [Flat f] (x : X) : (f.stalkMap x).hom.Flat :=
+  HasRingHomProperty.stalkMap (P := @Flat)
+    (fun f hf J hJ ↦ hf.localRingHom J (J.comap f) rfl) ‹_› x
+
+lemma iff_flat_stalkMap : Flat f ↔ ∀ x, (f.stalkMap x).hom.Flat :=
+  ⟨fun _ ↦ stalkMap f, fun H ↦ of_stalkMap f H⟩
+
+end Flat
+
+end AlgebraicGeometry

Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

@@ -530,7 +530,8 @@ private lemma respects_isOpenImmersion_aux
       let f' : (V s).toScheme ⟶ U.ι ⁻¹ᵁ s := f ∣_ U.ι ⁻¹ᵁ s
       have hf' : P f' := IsLocalAtTarget.restrict hf _
       let e : (U.ι ⁻¹ᵁ s).toScheme ≅ s := IsOpenImmersion.isoOfRangeEq ((U.ι ⁻¹ᵁ s).ι ≫ U.ι) s.1.ι
-        (by simpa [Set.range_comp, Set.image_preimage_eq_iff, heq] using le_sSup s.2)
+        (by simpa only [Scheme.comp_coeBase, TopCat.coe_comp, Set.range_comp, Scheme.Opens.range_ι,
+          Opens.map_coe, Set.image_preimage_eq_iff, heq, Opens.coe_sSup] using le_sSup s.2)
       have heq : (V s).ι ≫ f ≫ U.ι = f' ≫ e.hom ≫ s.1.ι := by
         simp only [V, IsOpenImmersion.isoOfRangeEq_hom_fac, f', e, morphismRestrict_ι_assoc]
       rw [heq, ← Category.assoc]
@@ -633,6 +634,69 @@ lemma locally_of_iff (hQl : LocalizationAwayPreserves Q)
     ext X Y f
     rw [h, iff_exists_appLE_locally (P := affineLocally (Locally Q)) hQa.left hQa.respectsIso]
 
+/-- If `Q` is a property of ring maps that can be checked on prime ideals, the
+associated property of scheme morphisms can be checked on stalks. -/
+lemma of_stalkMap (hQ : OfLocalizationPrime Q) (H : ∀ x, Q (f.stalkMap x).hom) : P f := by
+  have hQi := (HasRingHomProperty.isLocal_ringHomProperty P).respectsIso
+  wlog hY : IsAffine Y generalizing X Y f
+  · rw [IsLocalAtTarget.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top _)]
+    intro U
+    refine this (fun x ↦ ?_) U.2
+    exact (hQi.arrow_mk_iso_iff (AlgebraicGeometry.morphismRestrictStalkMap f U x)).mpr (H x.val)
+  wlog hX : IsAffine X generalizing X f
+  · rw [IsLocalAtSource.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top _)]
+    intro U
+    refine this ?_ U.2
+    intro x
+    rw [Scheme.stalkMap_comp, CommRingCat.hom_comp, hQi.cancel_right_isIso]
+    exact H x.val
+  wlog hXY : ∃ R S, Y = Spec R ∧ X = Spec S generalizing X Y
+  · rw [← P.cancel_right_of_respectsIso (g := Y.isoSpec.hom)]
+    rw [← P.cancel_left_of_respectsIso (f := X.isoSpec.inv)]
+    refine this inferInstance (fun x ↦ ?_) inferInstance ?_
+    · rw [Scheme.stalkMap_comp, Scheme.stalkMap_comp, CommRingCat.hom_comp,
+        hQi.cancel_right_isIso, CommRingCat.hom_comp, hQi.cancel_left_isIso]
+      apply H
+    · use Γ(Y, ⊤), Γ(X, ⊤)
+  obtain ⟨R, S, rfl, rfl⟩ := hXY
+  obtain ⟨φ, rfl⟩ := Spec.map_surjective f
+  rw [Spec_iff (P := P)]
+  apply hQ
+  intro P hP
+  specialize H ⟨P, hP⟩
+  rwa [hQi.arrow_mk_iso_iff (Scheme.arrowStalkMapSpecIso φ _)] at H
+
+/-- Let `Q` be a property of ring maps that is stable under localization.
+Then if the associated property of scheme morphisms holds for `f`, `Q` holds on all stalks. -/
+lemma stalkMap
+      (hQ : ∀ {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (_ : Q f)
+        (J : Ideal S) (_ : J.IsPrime), Q (Localization.localRingHom _ J f rfl))
+      (hf : P f) (x : X) : Q (f.stalkMap x).hom := by
+  have hQi := (HasRingHomProperty.isLocal_ringHomProperty P).respectsIso
+  wlog h : IsAffine X ∧ IsAffine Y generalizing X Y f
+  · obtain ⟨U, hU, hfx, _⟩ := Opens.isBasis_iff_nbhd.mp (isBasis_affine_open Y)
+      (Opens.mem_top <| f.base x)
+    obtain ⟨V, hV, hx, e⟩ := Opens.isBasis_iff_nbhd.mp (isBasis_affine_open X)
+      (show x ∈ f ⁻¹ᵁ U from hfx)
+    rw [← hQi.arrow_mk_iso_iff (Scheme.Hom.resLEStalkMap f e ⟨x, hx⟩)]
+    exact this (IsLocalAtSource.resLE _ hf) _ ⟨hV, hU⟩
+  obtain ⟨hX, hY⟩ := h
+  wlog hXY : ∃ R S, Y = Spec R ∧ X = Spec S generalizing X Y
+  · have : Q ((X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom).stalkMap (X.isoSpec.hom.base x)).hom := by
+      refine this ?_ (X.isoSpec.hom.base x) inferInstance inferInstance ?_
+      · rwa [P.cancel_left_of_respectsIso, P.cancel_right_of_respectsIso]
+      · use Γ(Y, ⊤), Γ(X, ⊤)
+    rw [Scheme.stalkMap_comp, Scheme.stalkMap_comp, CommRingCat.hom_comp,
+      hQi.cancel_right_isIso, CommRingCat.hom_comp, hQi.cancel_left_isIso] at this
+    have heq : (X.isoSpec.inv.base (X.isoSpec.hom.base x)) = x := by simp
+    rwa [hQi.arrow_mk_iso_iff
+      (Scheme.arrowStalkMapIsoOfInseparable f <| Inseparable.of_eq heq)] at this
+  obtain ⟨R, S, rfl, rfl⟩ := hXY
+  obtain ⟨φ, rfl⟩ := Spec.map_surjective f
+  rw [hQi.arrow_mk_iso_iff (Scheme.arrowStalkMapSpecIso φ _)]
+  rw [Spec_iff (P := P)] at hf
+  apply hQ _ hf
+
 end HasRingHomProperty
 
 end AlgebraicGeometry

Mathlib/AlgebraicGeometry/Restrict.lean

@@ -47,9 +47,11 @@ def toScheme {X : Scheme.{u}} (U : X.Opens) : Scheme.{u} :=
 instance : CoeOut X.Opens Scheme := ⟨toScheme⟩
 
 /-- The restriction of a scheme to an open subset. -/
-@[simps! base_apply]
 def ι : ↑U ⟶ X := X.ofRestrict _
 
+@[simp]
+lemma ι_base_apply (x : U) : U.ι.base x = x.val := rfl
+
 instance : IsOpenImmersion U.ι := inferInstanceAs (IsOpenImmersion (X.ofRestrict _))
 
 @[simps! over] instance : U.toScheme.CanonicallyOver X where
@@ -147,6 +149,16 @@ lemma germ_stalkIso_inv {X : Scheme.{u}} (U : X.Opens) (V : U.toScheme.Opens) (x
       (U.stalkIso x).inv = U.toScheme.presheaf.germ V x hx :=
   PresheafedSpace.restrictStalkIso_inv_eq_germ X.toPresheafedSpace U.isOpenEmbedding V x hx
 
+lemma stalkIso_inv {X : Scheme.{u}} (U : X.Opens) (x : U) :
+    (U.stalkIso x).inv = U.ι.stalkMap x := by
+  rw [← Category.comp_id (U.stalkIso x).inv, Iso.inv_comp_eq]
+  apply TopCat.Presheaf.stalk_hom_ext
+  intro W hxW
+  simp only [Category.comp_id, U.germ_stalkIso_hom_assoc]
+  convert (Scheme.stalkMap_germ U.ι (U.ι ''ᵁ W) x ⟨_, hxW, rfl⟩).symm
+  refine (U.toScheme.presheaf.germ_res (homOfLE ?_) _ _).symm
+  exact (Set.preimage_image_eq _ Subtype.val_injective).le
+
 end Scheme.Opens
 
 /-- If `U` is a family of open sets that covers `X`, then `X.restrict U` forms an `X.open_cover`. -/
@@ -313,7 +325,8 @@ noncomputable
 def Scheme.restrictRestrictComm (X : Scheme.{u}) (U V : X.Opens) :
     (U.ι ⁻¹ᵁ V).toScheme ≅ V.ι ⁻¹ᵁ U :=
   IsOpenImmersion.isoOfRangeEq (Opens.ι _ ≫ U.ι) (Opens.ι _ ≫ V.ι) <| by
-    simp [Set.image_preimage_eq_inter_range, Set.inter_comm (U : Set X), Set.range_comp]
+    simp only [comp_coeBase, TopCat.coe_comp, Set.range_comp, Opens.range_ι, Opens.map_coe,
+      Set.image_preimage_eq_inter_range, Set.inter_comm (U : Set X)]
 
 /-- If `f : X ⟶ Y` is an open immersion, then for any `U : X.Opens`,
 we have the isomorphism `U ≅ f ''ᵁ U`. -/
@@ -705,6 +718,21 @@ lemma resLE_appLE {U : Y.Opens} {V : X.Opens} (e : V ≤ f ⁻¹ᵁ U)
   rw [← X.presheaf.map_comp, ← X.presheaf.map_comp]
   rfl
 
+@[simp]
+lemma coe_resLE_base (x : V) : ((f.resLE U V e).base x).val = f.base x := by
+  simp [resLE, morphismRestrict_base]
+
+/-- The stalk map of `f.resLE U V` at `x : V` is is the stalk map of `f` at `x`. -/
+def resLEStalkMap (x : V) :
+    Arrow.mk ((f.resLE U V e).stalkMap x) ≅ Arrow.mk (f.stalkMap x) :=
+  Arrow.isoMk (U.stalkIso _ ≪≫
+      (Y.presheaf.stalkCongr <| Inseparable.of_eq <| by simp)) (V.stalkIso x) <| by
+    dsimp
+    rw [Category.assoc, ← Iso.eq_inv_comp, ← Category.assoc, ← Iso.comp_inv_eq,
+      Opens.stalkIso_inv, Opens.stalkIso_inv, ← stalkMap_comp,
+      stalkMap_congr_hom _ _ (resLE_comp_ι f e), stalkMap_comp]
+    simp
+
 end Scheme.Hom
 
 /-- `f.resLE U V` induces `f.appLE U V` on global sections. -/

Mathlib/AlgebraicGeometry/Scheme.lean

@@ -761,6 +761,14 @@ lemma stalkMap_germ_apply (U : Y.Opens) (x : X) (hx : f.base x ∈ U) (y) :
       X.presheaf.germ (f ⁻¹ᵁ U) x hx (f.app U y) :=
   PresheafedSpace.stalkMap_germ_apply f.toPshHom U x hx y
 
+/-- If `x` and `y` are inseparable, the stalk maps are isomorphic. -/
+noncomputable def arrowStalkMapIsoOfInseparable {x y : X}
+    (h : Inseparable x y) : Arrow.mk (f.stalkMap x) ≅ Arrow.mk (f.stalkMap y) :=
+  Arrow.isoMk (Y.presheaf.stalkCongr <| h.map f.continuous) (X.presheaf.stalkCongr h) <| by
+    simp only [Arrow.mk_left, Arrow.mk_right, Functor.id_obj, TopCat.Presheaf.stalkCongr_hom,
+      Arrow.mk_hom]
+    rw [Scheme.stalkSpecializes_stalkMap]
+
 end Scheme
 
 end Stalks

Mathlib/RingTheory/RingHom/Flat.lean

@@ -88,4 +88,28 @@ lemma propertyIsLocal : PropertyIsLocal Flat where
     (stableUnderComposition.stableUnderCompositionWithLocalizationAway
       holdsForLocalizationAway).right
 
+lemma ofLocalizationPrime : OfLocalizationPrime Flat := by
+  introv R h
+  algebraize_only [f]
+  rw [RingHom.Flat]
+  apply Module.flat_of_isLocalized_maximal S S (fun P ↦ Localization.AtPrime P)
+    (fun P ↦ Algebra.linearMap S _)
+  intro P _
+  algebraize_only [Localization.localRingHom (Ideal.comap f P) P f rfl]
+  have : IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
+    .of_algebraMap_eq fun x ↦ (Localization.localRingHom_to_map _ _ _ rfl x).symm
+  replace h : Module.Flat (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) := h ..
+  exact Module.Flat.trans R (Localization.AtPrime <| Ideal.comap f P) (Localization.AtPrime P)
+
+lemma localRingHom {f : R →+* S} (hf : f.Flat)
+    (P : Ideal S) [P.IsPrime] (Q : Ideal R) [Q.IsPrime] (hQP : Q = Ideal.comap f P) :
+    (Localization.localRingHom Q P f hQP).Flat := by
+  subst hQP
+  algebraize [f, Localization.localRingHom (Ideal.comap f P) P f rfl]
+  have : IsScalarTower R (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P) :=
+    .of_algebraMap_eq fun x ↦ (Localization.localRingHom_to_map _ _ _ rfl x).symm
+  rw [RingHom.Flat, Module.flat_iff_of_isLocalization
+    (S := (Localization.AtPrime (Ideal.comap f P))) (p := (Ideal.comap f P).primeCompl)]
+  exact Module.Flat.trans R S (Localization.AtPrime P)
+
 end RingHom.Flat

Mathlib/RingTheory/RingHomProperties.lean

@@ -191,6 +191,16 @@ lemma toMorphismProperty_respectsIso_iff :
     exact MorphismProperty.RespectsIso.precomp (toMorphismProperty P)
       e.toCommRingCatIso.hom (CommRingCat.ofHom f)
 
+/-- Variant of `MorphismProperty.arrow_mk_iso_iff` specialized to morphism properties in
+`CommRingCat` given by ring hom properties. -/
+lemma RespectsIso.arrow_mk_iso_iff (hQ : RingHom.RespectsIso P) {A B A' B' : CommRingCat}
+    {f : A ⟶ B} {g : A' ⟶ B'} (e : Arrow.mk f ≅ Arrow.mk g) :
+    P f.hom ↔ P g.hom := by
+  have : (toMorphismProperty P).RespectsIso := by
+    rwa [← toMorphismProperty_respectsIso_iff]
+  change toMorphismProperty P _ ↔ toMorphismProperty P _
+  rw [MorphismProperty.arrow_mk_iso_iff (toMorphismProperty P) e]
+
 end ToMorphismProperty
 
 end RingHom