feat(AlgebraicGeometry): Define preimmersions. (#14748)

Author: erdOne

Mathlib.lean

@@ -808,6 +808,7 @@ import Mathlib.AlgebraicGeometry.Morphisms.Constructors
 import Mathlib.AlgebraicGeometry.Morphisms.FiniteType
 import Mathlib.AlgebraicGeometry.Morphisms.IsIso
 import Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
+import Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
 import Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
 import Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
 import Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

@@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Amelia Livingston, Christian Merten, Jonas van der Schaaf
 -/
 import Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
-import Mathlib.RingTheory.LocalProperties
-import Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
+import Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
 
 /-!
 
@@ -48,16 +47,24 @@ lemma closedEmbedding {X Y : Scheme} (f : X ⟶ Y)
     [IsClosedImmersion f] : ClosedEmbedding f.1.base :=
   IsClosedImmersion.base_closed
 
-lemma surjective_stalkMap {X Y : Scheme} (f : X ⟶ Y)
-    [IsClosedImmersion f] (x : X) : Function.Surjective (f.stalkMap x) :=
-  IsClosedImmersion.surj_on_stalks x
-
 lemma eq_inf : @IsClosedImmersion = (topologically ClosedEmbedding) ⊓
     stalkwise (fun f ↦ Function.Surjective f) := by
   ext X Y f
   rw [isClosedImmersion_iff]
   rfl
 
+lemma iff_isPreimmersion {X Y : Scheme} {f : X ⟶ Y} :
+    IsClosedImmersion f ↔ IsPreimmersion f ∧ IsClosed (Set.range f.1.base) := by
+  rw [and_comm, isClosedImmersion_iff, isPreimmersion_iff, ← and_assoc, closedEmbedding_iff,
+    @and_comm (Embedding _)]
+
+lemma of_isPreimmersion {X Y : Scheme} (f : X ⟶ Y) [IsPreimmersion f]
+    (hf : IsClosed (Set.range f.1.base)) : IsClosedImmersion f :=
+  iff_isPreimmersion.mpr ⟨‹_›, hf⟩
+
+instance (priority := 900) {X Y : Scheme} (f : X ⟶ Y) [IsClosedImmersion f] : IsPreimmersion f :=
+  (iff_isPreimmersion.mp ‹_›).1
+
 /-- Isomorphisms are closed immersions. -/
 instance {X Y : Scheme} (f : X ⟶ Y) [IsIso f] : IsClosedImmersion f where
   base_closed := Homeomorph.closedEmbedding <| TopCat.homeoOfIso (asIso f.1.base)
@@ -121,7 +128,7 @@ theorem of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsClosedImmersion
         ← Set.image_comp]
       exact ClosedEmbedding.isClosedMap h _ hZ
   surj_on_stalks x := by
-    have h := surjective_stalkMap (f ≫ g) x
+    have h := (f ≫ g).stalkMap_surjective x
     simp_rw [Scheme.comp_val, Scheme.stalkMap_comp] at h
     exact Function.Surjective.of_comp h
 
@@ -130,11 +137,6 @@ instance {X Y : Scheme} (f : X ⟶ Y) [IsClosedImmersion f] : QuasiCompact f whe
 
 end IsClosedImmersion
 
-/-- Being surjective on stalks is local at the target. -/
-instance isSurjectiveOnStalks_isLocalAtTarget : IsLocalAtTarget
-    (stalkwise (fun f ↦ Function.Surjective f)) :=
-  stalkwiseIsLocalAtTarget_of_respectsIso surjective_respectsIso
-
 /-- Being a closed immersion is local at the target. -/
 instance IsClosedImmersion.isLocalAtTarget : IsLocalAtTarget @IsClosedImmersion :=
   eq_inf ▸ inferInstance

Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean

@@ -0,0 +1,100 @@
+/-
+Copyright (c) 2024 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
+import Mathlib.RingTheory.LocalProperties
+
+/-!
+
+# Preimmersions of schemes
+
+A morphism of schemes `f : X ⟶ Y` is a preimmersion if the underlying map of topological spaces
+is an embedding and the induced morphisms of stalks are all surjective. This is not a concept seen
+in the literature but it is useful for generalizing results on immersions to other maps including
+`Spec 𝒪_{X, x} ⟶ X` and inclusions of fibers `κ(x) ×ₓ Y ⟶ Y`.
+
+## TODO
+
+* Show preimmersions are local at the target.
+* Show preimmersions are stable under pullback.
+* Show that `Spec f` is a preimmersion for `f : R ⟶ S` if every `s : S` is of the form `f a / f b`.
+
+-/
+
+universe v u
+
+open CategoryTheory
+
+namespace AlgebraicGeometry
+
+/-- A morphism of schemes `f : X ⟶ Y` is a preimmersion if the underlying map of
+topological spaces is an embedding and the induced morphisms of stalks are all surjective. -/
+@[mk_iff]
+class IsPreimmersion {X Y : Scheme} (f : X ⟶ Y) : Prop where
+  base_embedding : Embedding f.1.base
+  surj_on_stalks : ∀ x, Function.Surjective (f.stalkMap x)
+
+lemma Scheme.Hom.embedding {X Y : Scheme} (f : Hom X Y) [IsPreimmersion f] : Embedding f.1.base :=
+  IsPreimmersion.base_embedding
+
+lemma Scheme.Hom.stalkMap_surjective {X Y : Scheme} (f : Hom X Y) [IsPreimmersion f] (x) :
+    Function.Surjective (f.stalkMap x) :=
+  IsPreimmersion.surj_on_stalks x
+
+lemma isPreimmersion_eq_inf :
+    @IsPreimmersion = topologically Embedding ⊓ stalkwise (Function.Surjective ·) := by
+  ext
+  rw [isPreimmersion_iff]
+  rfl
+
+/-- Being surjective on stalks is local at the target. -/
+instance isSurjectiveOnStalks_isLocalAtTarget : IsLocalAtTarget
+    (stalkwise (Function.Surjective ·)) :=
+  stalkwiseIsLocalAtTarget_of_respectsIso surjective_respectsIso
+
+namespace IsPreimmersion
+
+instance : IsLocalAtTarget @IsPreimmersion :=
+  isPreimmersion_eq_inf ▸ inferInstance
+
+instance (priority := 900) {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f] : IsPreimmersion f where
+  base_embedding := f.openEmbedding.toEmbedding
+  surj_on_stalks _ := (ConcreteCategory.bijective_of_isIso _).2
+
+instance : MorphismProperty.IsMultiplicative @IsPreimmersion where
+  id_mem _ := inferInstance
+  comp_mem {X Y Z} f g hf hg := by
+    refine ⟨hg.base_embedding.comp hf.base_embedding, fun x ↦ ?_⟩
+    rw [Scheme.stalkMap_comp]
+    exact (hf.surj_on_stalks x).comp (hg.surj_on_stalks (f.1.1 x))
+
+instance comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsPreimmersion f]
+    [IsPreimmersion g] : IsPreimmersion (f ≫ g) :=
+  MorphismProperty.IsStableUnderComposition.comp_mem f g inferInstance inferInstance
+
+instance (priority := 900) {X Y} (f : X ⟶ Y) [IsPreimmersion f] : Mono f := by
+  refine (Scheme.forgetToLocallyRingedSpace ⋙
+    LocallyRingedSpace.forgetToSheafedSpace).mono_of_mono_map ?_
+  apply SheafedSpace.mono_of_base_injective_of_stalk_epi
+  · exact f.embedding.inj
+  · exact fun x ↦ ConcreteCategory.epi_of_surjective _ (f.stalkMap_surjective x)
+
+theorem of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsPreimmersion g]
+    [IsPreimmersion (f ≫ g)] : IsPreimmersion f where
+  base_embedding := by
+    have h := (f ≫ g).embedding
+    rwa [← g.embedding.of_comp_iff]
+  surj_on_stalks x := by
+    have h := (f ≫ g).stalkMap_surjective x
+    rw [Scheme.stalkMap_comp] at h
+    exact Function.Surjective.of_comp h
+
+theorem comp_iff {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsPreimmersion g] :
+    IsPreimmersion (f ≫ g) ↔ IsPreimmersion f :=
+  ⟨fun _ ↦ of_comp f g, fun _ ↦ inferInstance⟩
+
+end IsPreimmersion
+
+end AlgebraicGeometry

Mathlib/Geometry/RingedSpace/SheafedSpace.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
+import Mathlib.Geometry.RingedSpace.Stalks
 import Mathlib.Topology.Sheaves.Functors
 
 /-!
@@ -209,6 +210,39 @@ instance [HasLimits C] : HasColimits.{v} (SheafedSpace C) :=
 noncomputable instance [HasLimits C] : PreservesColimits (forget C) :=
   Limits.compPreservesColimits forgetToPresheafedSpace (PresheafedSpace.forget C)
 
+section ConcreteCategory
+
+variable [ConcreteCategory.{v} C] [HasColimits C] [HasLimits C]
+variable  [PreservesLimits (CategoryTheory.forget C)]
+variable [PreservesFilteredColimits (CategoryTheory.forget C)]
+variable [(CategoryTheory.forget C).ReflectsIsomorphisms]
+
+attribute [local instance] ConcreteCategory.instFunLike in
+lemma hom_stalk_ext {X Y : SheafedSpace C} (f g : X ⟶ Y) (h : f.base = g.base)
+    (h' : ∀ x, f.stalkMap x = (Y.presheaf.stalkCongr (h ▸ rfl)).hom ≫ g.stalkMap x) :
+    f = g := by
+  obtain ⟨f, fc⟩ := f
+  obtain ⟨g, gc⟩ := g
+  obtain rfl : f = g := h
+  congr
+  ext U s
+  refine section_ext X.sheaf _ _ _ fun x ↦ show X.presheaf.germ x _ = X.presheaf.germ x _ from ?_
+  erw [← PresheafedSpace.stalkMap_germ_apply ⟨f, fc⟩, ← PresheafedSpace.stalkMap_germ_apply ⟨f, gc⟩]
+  simp [h']
+
+lemma mono_of_base_injective_of_stalk_epi {X Y : SheafedSpace C} (f : X ⟶ Y)
+    (h₁ : Function.Injective f.base)
+    (h₂ : ∀ x, Epi (f.stalkMap x)) : Mono f := by
+  constructor
+  intro Z ⟨g, gc⟩ ⟨h, hc⟩ e
+  obtain rfl : g = h := ConcreteCategory.hom_ext _ _ fun x ↦ h₁ congr(($e).base x)
+  refine SheafedSpace.hom_stalk_ext ⟨g, gc⟩ ⟨g, hc⟩ rfl fun x ↦ ?_
+  rw [← cancel_epi (f.stalkMap (g x)), stalkCongr_hom, stalkSpecializes_refl, Category.id_comp,
+    ← PresheafedSpace.stalkMap.comp ⟨g, gc⟩ f, ← PresheafedSpace.stalkMap.comp ⟨g, hc⟩ f]
+  congr 1
+
+end ConcreteCategory
+
 end SheafedSpace
 
 end AlgebraicGeometry