Merge branch 'master' into YK-isO-TVS

Mathlib.lean

@@ -3622,6 +3622,7 @@ import Mathlib.Order.Bounded
 import Mathlib.Order.BoundedOrder
 import Mathlib.Order.Bounds.Basic
 import Mathlib.Order.Bounds.Defs
+import Mathlib.Order.Bounds.Image
 import Mathlib.Order.Bounds.OrderIso
 import Mathlib.Order.Category.BddDistLat
 import Mathlib.Order.Category.BddLat
@@ -4553,6 +4554,7 @@ import Mathlib.Topology.Algebra.Module.Determinant
 import Mathlib.Topology.Algebra.Module.FiniteDimension
 import Mathlib.Topology.Algebra.Module.LinearPMap
 import Mathlib.Topology.Algebra.Module.LocallyConvex
+import Mathlib.Topology.Algebra.Module.ModuleTopology
 import Mathlib.Topology.Algebra.Module.Multilinear.Basic
 import Mathlib.Topology.Algebra.Module.Multilinear.Bounded
 import Mathlib.Topology.Algebra.Module.Multilinear.Topology

Mathlib/Algebra/BigOperators/Group/Finset.lean

@@ -1611,13 +1611,13 @@ theorem dvd_prod_of_mem (f : α → β) {a : α} {s : Finset α} (ha : a ∈ s)
 /-- A product can be partitioned into a product of products, each equivalent under a setoid. -/
 @[to_additive "A sum can be partitioned into a sum of sums, each equivalent under a setoid."]
 theorem prod_partition (R : Setoid α) [DecidableRel R.r] :
-    ∏ x ∈ s, f x = ∏ xbar ∈ s.image Quotient.mk'', ∏ y ∈ s.filter (⟦·⟧ = xbar), f y := by
+    ∏ x ∈ s, f x = ∏ xbar ∈ s.image (Quotient.mk _), ∏ y ∈ s.filter (⟦·⟧ = xbar), f y := by
   refine (Finset.prod_image' f fun x _hx => ?_).symm
   rfl
 
 /-- If we can partition a product into subsets that cancel out, then the whole product cancels. -/
 @[to_additive "If we can partition a sum into subsets that cancel out, then the whole sum cancels."]
-theorem prod_cancels_of_partition_cancels (R : Setoid α) [DecidableRel R.r]
+theorem prod_cancels_of_partition_cancels (R : Setoid α) [DecidableRel R]
     (h : ∀ x ∈ s, ∏ a ∈ s.filter fun y => R y x, f a = 1) : ∏ x ∈ s, f x = 1 := by
   rw [prod_partition R, ← Finset.prod_eq_one]
   intro xbar xbar_in_s

Mathlib/Algebra/CharZero/Quotient.lean

@@ -51,11 +51,11 @@ namespace QuotientAddGroup
 
 theorem zmultiples_zsmul_eq_zsmul_iff {ψ θ : R ⧸ AddSubgroup.zmultiples p} {z : ℤ} (hz : z ≠ 0) :
     z • ψ = z • θ ↔ ∃ k : Fin z.natAbs, ψ = θ + ((k : ℕ) • (p / z) : R) := by
-  induction ψ using Quotient.inductionOn'
-  induction θ using Quotient.inductionOn'
+  induction ψ using Quotient.inductionOn
+  induction θ using Quotient.inductionOn
   -- Porting note: Introduced Zp notation to shorten lines
   let Zp := AddSubgroup.zmultiples p
-  have : (Quotient.mk'' : R → R ⧸ Zp) = ((↑) : R → R ⧸ Zp) := rfl
+  have : (Quotient.mk _ : R → R ⧸ Zp) = ((↑) : R → R ⧸ Zp) := rfl
   simp only [this]
   simp_rw [← QuotientAddGroup.mk_zsmul, ← QuotientAddGroup.mk_add,
     QuotientAddGroup.eq_iff_sub_mem, ← smul_sub, ← sub_sub]

Mathlib/AlgebraicGeometry/Modules/Tilde.lean

@@ -22,6 +22,8 @@ such that `M^~(U)` is the set of dependent functions that are locally fractions.
 
 * `ModuleCat.tildeInType` : `M^~` as a sheaf of types groups.
 * `ModuleCat.tilde` : `M^~` as a sheaf of `𝒪_{Spec R}`-modules.
+* `ModuleCat.tilde.stalkIso`: The isomorphism of `R`-modules from the stalk of `M^~` at `x` to
+the localization of `M` at the prime ideal corresponding to `x`.
 
 ## Technical note
 
@@ -252,6 +254,144 @@ noncomputable def localizationToStalk (x : PrimeSpectrum.Top R) :
     (TopCat.Presheaf.stalk (tildeInModuleCat M) x) :=
   LocalizedModule.lift _ (toStalk M x) <| isUnit_toStalk M x
 
+
+/-- The ring homomorphism that takes a section of the structure sheaf of `R` on the open set `U`,
+implemented as a subtype of dependent functions to localizations at prime ideals, and evaluates
+the section on the point corresponding to a given prime ideal. -/
+def openToLocalization (U : Opens (PrimeSpectrum R)) (x : PrimeSpectrum R) (hx : x ∈ U) :
+    (tildeInModuleCat M).obj (op U) ⟶
+    ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M) where
+  toFun s := (s.1 ⟨x, hx⟩ : _)
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
+
+/--
+The morphism of `R`-modules from the stalk of `M^~` at `x` to the localization of `M` at the
+prime ideal of `R` corresponding to `x`.
+-/
+noncomputable def stalkToFiberLinearMap (x : PrimeSpectrum.Top R) :
+    (tildeInModuleCat M).stalk  x ⟶
+    ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M) :=
+  Limits.colimit.desc ((OpenNhds.inclusion x).op ⋙ (tildeInModuleCat M))
+    { pt := _
+      ι :=
+      { app := fun U => openToLocalization M ((OpenNhds.inclusion _).obj U.unop) x U.unop.2 } }
+
+@[simp]
+theorem germ_comp_stalkToFiberLinearMap (U : Opens (PrimeSpectrum.Top R)) (x) (hx : x ∈ U) :
+    (tildeInModuleCat M).germ U x hx ≫ stalkToFiberLinearMap M x =
+    openToLocalization M U x hx :=
+  Limits.colimit.ι_desc _ _
+
+@[simp]
+theorem stalkToFiberLinearMap_germ (U : Opens (PrimeSpectrum.Top R)) (x : PrimeSpectrum.Top R)
+    (hx : x ∈ U) (s : (tildeInModuleCat M).1.obj (op U)) :
+    stalkToFiberLinearMap M x
+      (TopCat.Presheaf.germ (tildeInModuleCat M) U x hx s) = (s.1 ⟨x, hx⟩ : _) :=
+  DFunLike.ext_iff.1 (germ_comp_stalkToFiberLinearMap M U x hx) s
+
+@[reassoc (attr := simp), elementwise (attr := simp)]
+theorem toOpen_germ (U : Opens (PrimeSpectrum.Top R)) (x) (hx : x ∈ U) :
+    toOpen M U ≫ M.tildeInModuleCat.germ U x hx = toStalk M x := by
+  rw [← toOpen_res M ⊤ U (homOfLE le_top : U ⟶ ⊤), Category.assoc, Presheaf.germ_res]; rfl
+
+@[reassoc (attr := simp)]
+theorem toStalk_comp_stalkToFiberLinearMap (x : PrimeSpectrum.Top R) :
+    toStalk M x ≫ stalkToFiberLinearMap M x =
+    LocalizedModule.mkLinearMap x.asIdeal.primeCompl M := by
+  rw [toStalk, Category.assoc, germ_comp_stalkToFiberLinearMap]; rfl
+
+theorem stalkToFiberLinearMap_toStalk (x : PrimeSpectrum.Top R) (m : M) :
+    (stalkToFiberLinearMap M x) (toStalk M x m) =
+    LocalizedModule.mk m 1 :=
+  LinearMap.ext_iff.1 (toStalk_comp_stalkToFiberLinearMap M x) _
+
+/--
+If `U` is an open subset of `Spec R`, `m` is an element of `M` and `r` is an element of `R`
+that is invertible on `U` (i.e. does not belong to any prime ideal corresponding to a point
+in `U`), this is `m / r` seen as a section of `M^~` over `U`.
+-/
+def const (m : M) (r : R) (U : Opens (PrimeSpectrum.Top R))
+    (hu : ∀ x ∈ U, r ∈ (x : PrimeSpectrum.Top R).asIdeal.primeCompl) :
+    (tildeInModuleCat M).obj (op U) :=
+  ⟨fun x => LocalizedModule.mk m ⟨r, hu x x.2⟩, fun x =>
+    ⟨U, x.2, 𝟙 _, m, r, fun y => ⟨hu _ y.2, by
+      simpa only [LocalizedModule.mkLinearMap_apply, LocalizedModule.smul'_mk,
+        LocalizedModule.mk_eq] using ⟨1, by simp⟩⟩⟩⟩
+
+@[simp]
+theorem const_apply (m : M) (r : R) (U : Opens (PrimeSpectrum.Top R))
+    (hu : ∀ x ∈ U, r ∈ (x : PrimeSpectrum.Top R).asIdeal.primeCompl) (x : U) :
+    (const M m r U hu).1 x = LocalizedModule.mk m ⟨r, hu x x.2⟩ :=
+  rfl
+
+theorem exists_const (U) (s : (tildeInModuleCat M).obj (op U)) (x : PrimeSpectrum.Top R)
+    (hx : x ∈ U) :
+    ∃ (V : Opens (PrimeSpectrum.Top R)) (_ : x ∈ V) (i : V ⟶ U) (f : M) (g : R) (hg : _),
+      const M f g V hg = (tildeInModuleCat M).map i.op s :=
+  let ⟨V, hxV, iVU, f, g, hfg⟩ := s.2 ⟨x, hx⟩
+  ⟨V, hxV, iVU, f, g, fun y hyV => (hfg ⟨y, hyV⟩).1, Subtype.eq <| funext fun y => by
+    obtain ⟨h1, (h2 : g • s.1 ⟨y, _⟩ = LocalizedModule.mk f 1)⟩ := hfg y
+    exact show LocalizedModule.mk f ⟨g, by exact h1⟩ = s.1 (iVU y) by
+      set x := s.1 (iVU y); change g • x = _ at h2; clear_value x
+      induction x using LocalizedModule.induction_on with
+      | h a b =>
+        rw [LocalizedModule.smul'_mk, LocalizedModule.mk_eq] at h2
+        obtain ⟨c, hc⟩ := h2
+        exact LocalizedModule.mk_eq.mpr ⟨c, by simpa using hc.symm⟩⟩
+
+@[simp]
+theorem res_const (f : M) (g : R) (U hu V hv i) :
+    (tildeInModuleCat M).map i (const M f g U hu) = const M f g V hv :=
+  rfl
+
+@[simp]
+theorem localizationToStalk_mk (x : PrimeSpectrum.Top R) (f : M) (s : x.asIdeal.primeCompl) :
+    localizationToStalk M x (LocalizedModule.mk f s) =
+      (tildeInModuleCat M).germ (PrimeSpectrum.basicOpen (s : R)) x s.2
+        (const M f s (PrimeSpectrum.basicOpen s) fun _ => id) :=
+  (Module.End_isUnit_iff _ |>.1 (isUnit_toStalk M x s)).injective <| by
+  erw [← LinearMap.mul_apply]
+  simp only [IsUnit.mul_val_inv, LinearMap.one_apply, Module.algebraMap_end_apply]
+  show (M.tildeInModuleCat.germ ⊤ x ⟨⟩) ((toOpen M ⊤) f) = _
+  rw [← map_smul]
+  fapply TopCat.Presheaf.germ_ext (W := PrimeSpectrum.basicOpen s.1) (hxW := s.2)
+  · exact homOfLE le_top
+  · exact 𝟙 _
+  refine Subtype.eq <| funext fun y => show LocalizedModule.mk f 1 = _ from ?_
+  show LocalizedModule.mk f 1 = s.1 • LocalizedModule.mk f _
+  rw [LocalizedModule.smul'_mk, LocalizedModule.mk_eq]
+  exact ⟨1, by simp⟩
+
+/--
+The isomorphism of `R`-modules from the stalk of `M^~` at `x` to the localization of `M` at the
+prime ideal corresponding to `x`.
+-/
+@[simps]
+noncomputable def stalkIso (x : PrimeSpectrum.Top R) :
+    TopCat.Presheaf.stalk (tildeInModuleCat M) x ≅
+    ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M) where
+  hom := stalkToFiberLinearMap M x
+  inv := localizationToStalk M x
+  hom_inv_id := TopCat.Presheaf.stalk_hom_ext _ fun U hxU ↦ ext _ fun s ↦ by
+    show localizationToStalk M x (stalkToFiberLinearMap M x (M.tildeInModuleCat.germ U x hxU s)) =
+      M.tildeInModuleCat.germ U x hxU s
+    rw [stalkToFiberLinearMap_germ]
+    obtain ⟨V, hxV, iVU, f, g, (hg : V ≤ PrimeSpectrum.basicOpen _), hs⟩ :=
+      exists_const _ _ s x hxU
+    rw [← res_apply M U V iVU s ⟨x, hxV⟩, ← hs, const_apply, localizationToStalk_mk]
+    exact (tildeInModuleCat M).germ_ext V hxV (homOfLE hg) iVU <| hs ▸ rfl
+  inv_hom_id := by ext x; exact x.induction_on (fun _ _ => by simp)
+
+instance (x : PrimeSpectrum.Top R) :
+    IsLocalizedModule x.asIdeal.primeCompl (toStalk M x) := by
+  convert IsLocalizedModule.of_linearEquiv
+    (hf := localizedModuleIsLocalizedModule (M := M) x.asIdeal.primeCompl)
+    (e := (stalkIso M x).symm.toLinearEquiv)
+  simp only [of_coe, show (stalkIso M x).symm.toLinearEquiv.toLinearMap = (stalkIso M x).inv by rfl,
+    stalkIso_inv]
+  erw [LocalizedModule.lift_comp]
+
 end Tilde
 
 end ModuleCat

Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

@@ -3,12 +3,10 @@ Copyright (c) 2023 Jonas van der Schaaf. All rights reserved.
 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.Preimmersion
 import Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
 import Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
 import Mathlib.AlgebraicGeometry.Morphisms.FiniteType
 import Mathlib.AlgebraicGeometry.ResidueField
-import Mathlib.RingTheory.RingHom.Surjective
 
 /-!
 
@@ -134,6 +132,10 @@ theorem of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsClosedImmersion
     simp_rw [Scheme.stalkMap_comp] at h
     exact Function.Surjective.of_comp h
 
+instance Spec_map_residue {X : Scheme.{u}} (x) : IsClosedImmersion (Spec.map (X.residue x)) :=
+  IsClosedImmersion.spec_of_surjective (X.residue x)
+    Ideal.Quotient.mk_surjective
+
 instance {X Y : Scheme} (f : X ⟶ Y) [IsClosedImmersion f] : QuasiCompact f where
   isCompact_preimage _ _ hU' := base_closed.isCompact_preimage hU'
 

Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean

@@ -5,6 +5,7 @@ Authors: Andrew Yang
 -/
 import Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
 import Mathlib.RingTheory.RingHom.Surjective
+import Mathlib.RingTheory.SurjectiveOnStalks
 
 /-!
 
@@ -95,6 +96,32 @@ 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⟩
 
+lemma Spec_map_iff {R S : CommRingCat.{u}} (f : R ⟶ S) :
+    IsPreimmersion (Spec.map f) ↔ Embedding (PrimeSpectrum.comap f) ∧ f.SurjectiveOnStalks := by
+  haveI : (RingHom.toMorphismProperty <| fun f ↦ Function.Surjective f).RespectsIso := by
+    rw [← RingHom.toMorphismProperty_respectsIso_iff]
+    exact RingHom.surjective_respectsIso
+  refine ⟨fun ⟨h₁, h₂⟩ ↦ ⟨h₁, ?_⟩, fun ⟨h₁, h₂⟩ ↦ ⟨h₁, fun (x : PrimeSpectrum S) ↦ ?_⟩⟩
+  · intro p hp
+    let e := Scheme.arrowStalkMapSpecIso f ⟨p, hp⟩
+    apply ((RingHom.toMorphismProperty <| fun f ↦ Function.Surjective f).arrow_mk_iso_iff e).mp
+    exact h₂ ⟨p, hp⟩
+  · let e := Scheme.arrowStalkMapSpecIso f x
+    apply ((RingHom.toMorphismProperty <| fun f ↦ Function.Surjective f).arrow_mk_iso_iff e).mpr
+    exact h₂ x.asIdeal x.isPrime
+
+lemma mk_Spec_map {R S : CommRingCat.{u}} {f : R ⟶ S}
+    (h₁ : Embedding (PrimeSpectrum.comap f)) (h₂ : f.SurjectiveOnStalks) :
+    IsPreimmersion (Spec.map f) :=
+  (Spec_map_iff f).mpr ⟨h₁, h₂⟩
+
+lemma of_isLocalization {R S : Type u} [CommRing R] (M : Submonoid R) [CommRing S]
+    [Algebra R S] [IsLocalization M S] :
+    IsPreimmersion (Spec.map (CommRingCat.ofHom <| algebraMap R S)) :=
+  IsPreimmersion.mk_Spec_map
+    (PrimeSpectrum.localization_comap_embedding (R := R) S M)
+    (RingHom.surjectiveOnStalks_of_isLocalization (M := M) S)
+
 end IsPreimmersion
 
 end AlgebraicGeometry