diff --git a/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean b/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean index f3fa7a4fbdf4a..26c8303a68816 100644 --- a/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean +++ b/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean @@ -647,6 +647,10 @@ theorem closedPoint_mem_iff (U : TopologicalSpace.Opens <| PrimeSpectrum R) : · rintro rfl trivial +lemma closed_point_mem_iff {U : TopologicalSpace.Opens (PrimeSpectrum R)} : + closedPoint R ∈ U ↔ U = ⊤ := + ⟨(eq_top_iff.mpr fun x _ ↦ (specializes_closedPoint x).mem_open U.2 ·), (· ▸ trivial)⟩ + @[simp] theorem PrimeSpectrum.comap_residue (T : Type u) [CommRing T] [LocalRing T] (x : PrimeSpectrum (ResidueField T)) : PrimeSpectrum.comap (residue T) x = closedPoint T := by diff --git a/Mathlib/AlgebraicGeometry/Scheme.lean b/Mathlib/AlgebraicGeometry/Scheme.lean index 3a705c863a6a4..546fea88d15d5 100644 --- a/Mathlib/AlgebraicGeometry/Scheme.lean +++ b/Mathlib/AlgebraicGeometry/Scheme.lean @@ -709,4 +709,15 @@ end Scheme end Stalks +section LocalRing + +open LocalRing + +@[simp] +lemma Spec_closedPoint {R S : CommRingCat} [LocalRing R] [LocalRing S] + {f : R ⟶ S} [IsLocalRingHom f] : (Spec.map f).base (closedPoint S) = closedPoint R := + LocalRing.comap_closedPoint f + +end LocalRing + end AlgebraicGeometry diff --git a/Mathlib/AlgebraicGeometry/Stalk.lean b/Mathlib/AlgebraicGeometry/Stalk.lean index 8865ed5e23d8f..c5d01c4906552 100644 --- a/Mathlib/AlgebraicGeometry/Stalk.lean +++ b/Mathlib/AlgebraicGeometry/Stalk.lean @@ -8,14 +8,25 @@ import Mathlib.AlgebraicGeometry.AffineScheme /-! # Stalks of a Scheme -Given a scheme `X` and a point `x : X`, `AlgebraicGeometry.Scheme.fromSpecStalk X x` is the -canonical scheme morphism from `Spec(O_x)` to `X`. This is helpful for constructing the canonical -map from the spectrum of the residue field of a point to the original scheme. +## Main definitions and results + +- `AlgebraicGeometry.Scheme.fromSpecStalk`: The canonical morphism `Spec 𝒪_{X, x} ⟶ X`. +- `AlgebraicGeometry.Scheme.range_fromSpecStalk`: The range of the map `Spec 𝒪_{X, x} ⟶ X` is + exactly the `y`s that specialize to `x`. +- `AlgebraicGeometry.SpecToEquivOfLocalRing`: + Given a local ring `R` and scheme `X`, morphisms `Spec R ⟶ X` corresponds to pairs + `(x, f)` where `x : X` and `f : 𝒪_{X, x} ⟶ R` is a local ring homomorphism. -/ namespace AlgebraicGeometry -open CategoryTheory Opposite TopologicalSpace +open CategoryTheory Opposite TopologicalSpace LocalRing + +universe u + +variable {X Y : Scheme.{u}} (f : X ⟶ Y) {U V : X.Opens} (hU : IsAffineOpen U) (hV : IsAffineOpen V) + +section fromSpecStalk /-- A morphism from `Spec(O_x)` to `X`, which is defined with the help of an affine open @@ -30,8 +41,7 @@ noncomputable def IsAffineOpen.fromSpecStalk The morphism from `Spec(O_x)` to `X` given by `IsAffineOpen.fromSpec` does not depend on the affine open neighborhood of `x` we choose. -/ -theorem IsAffineOpen.fromSpecStalk_eq {X : Scheme} (x : X) {U V : X.Opens} - (hU : IsAffineOpen U) (hV : IsAffineOpen V) (hxU : x ∈ U) (hxV : x ∈ V) : +theorem IsAffineOpen.fromSpecStalk_eq (x : X) (hxU : x ∈ U) (hxV : x ∈ V) : hU.fromSpecStalk hxU = hV.fromSpecStalk hxV := by obtain ⟨U', h₁, h₂, h₃ : U' ≤ U ⊓ V⟩ := Opens.isBasis_iff_nbhd.mp (isBasis_affine_open X) (show x ∈ U ⊓ V from ⟨hxU, hxV⟩) @@ -51,12 +61,254 @@ theorem IsAffineOpen.fromSpecStalk_eq {X : Scheme} (x : X) {U V : X.Opens} If `x` is a point of `X`, this is the canonical morphism from `Spec(O_x)` to `X`. -/ noncomputable def Scheme.fromSpecStalk (X : Scheme) (x : X) : - Scheme.Spec.obj (op (X.presheaf.stalk x)) ⟶ X := + Spec (X.presheaf.stalk x) ⟶ X := (isAffineOpen_opensRange (X.affineOpenCover.map x)).fromSpecStalk (X.affineOpenCover.covers x) @[simp] -theorem IsAffineOpen.fromSpecStalk_eq_fromSpecStalk - {X : Scheme} {U : X.Opens} (hU : IsAffineOpen U) {x : X} (hxU : x ∈ U) : +theorem IsAffineOpen.fromSpecStalk_eq_fromSpecStalk {x : X} (hxU : x ∈ U) : hU.fromSpecStalk hxU = X.fromSpecStalk x := fromSpecStalk_eq .. +lemma IsAffineOpen.fromSpecStalk_closedPoint {U : Opens X} (hU : IsAffineOpen U) + {x : X} (hxU : x ∈ U) : + (hU.fromSpecStalk hxU).base (closedPoint (X.presheaf.stalk x)) = x := by + rw [IsAffineOpen.fromSpecStalk, Scheme.comp_base_apply] + rw [← hU.primeIdealOf_eq_map_closedPoint ⟨x, hxU⟩, hU.fromSpec_primeIdealOf ⟨x, hxU⟩] + +namespace Scheme + +@[simp] +lemma fromSpecStalk_closedPoint {x : X} : + (X.fromSpecStalk x).base (closedPoint (X.presheaf.stalk x)) = x := + IsAffineOpen.fromSpecStalk_closedPoint _ _ + +lemma fromSpecStalk_app {x : X} (hxU : x ∈ U) : + (X.fromSpecStalk x).app U = + X.presheaf.germ U x hxU ≫ + (ΓSpecIso (X.presheaf.stalk x)).inv ≫ + (Spec (X.presheaf.stalk x)).presheaf.map (homOfLE le_top).op := by + obtain ⟨_, ⟨V : X.Opens, hV, rfl⟩, hxV, hVU⟩ := (isBasis_affine_open X).exists_subset_of_mem_open + hxU U.2 + rw [← hV.fromSpecStalk_eq_fromSpecStalk hxV, IsAffineOpen.fromSpecStalk, Scheme.comp_app, + hV.fromSpec_app_of_le _ hVU, ← X.presheaf.germ_res (homOfLE hVU) x hxV] + simp [Category.assoc, ← ΓSpecIso_inv_naturality_assoc] + +@[reassoc] +lemma Spec_map_stalkSpecializes_fromSpecStalk {x y : X} (h : x ⤳ y) : + Spec.map (X.presheaf.stalkSpecializes h) ≫ X.fromSpecStalk y = X.fromSpecStalk x := by + obtain ⟨_, ⟨U, hU, rfl⟩, hyU, -⟩ := + (isBasis_affine_open X).exists_subset_of_mem_open (Set.mem_univ y) isOpen_univ + have hxU : x ∈ U := h.mem_open U.2 hyU + rw [← hU.fromSpecStalk_eq_fromSpecStalk hyU, ← hU.fromSpecStalk_eq_fromSpecStalk hxU, + IsAffineOpen.fromSpecStalk, IsAffineOpen.fromSpecStalk, ← Category.assoc, ← Spec.map_comp, + TopCat.Presheaf.germ_stalkSpecializes] + +@[reassoc (attr := simp)] +lemma Spec_map_stalkMap_fromSpecStalk {x} : + Spec.map (f.stalkMap x) ≫ Y.fromSpecStalk _ = X.fromSpecStalk x ≫ f := by + obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ := (isBasis_affine_open Y).exists_subset_of_mem_open + (Set.mem_univ (f.base x)) isOpen_univ + obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ := (isBasis_affine_open X).exists_subset_of_mem_open + hxU (f ⁻¹ᵁ U).2 + rw [← hU.fromSpecStalk_eq_fromSpecStalk hxU, ← hV.fromSpecStalk_eq_fromSpecStalk hxV, + IsAffineOpen.fromSpecStalk, ← Spec.map_comp_assoc, Scheme.stalkMap_germ f _ x hxU, + IsAffineOpen.fromSpecStalk, Spec.map_comp_assoc, ← X.presheaf.germ_res (homOfLE hVU) x hxV, + Spec.map_comp_assoc, Category.assoc, ← Spec.map_comp_assoc (f.app _), + Hom.app_eq_appLE, Hom.appLE_map, IsAffineOpen.Spec_map_appLE_fromSpec] + +lemma Spec_fromSpecStalk (R : CommRingCat) (x) : + (Spec R).fromSpecStalk x = + Spec.map ((ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial) := by + rw [← (isAffineOpen_top (Spec R)).fromSpecStalk_eq_fromSpecStalk (x := x) trivial, + IsAffineOpen.fromSpecStalk, IsAffineOpen.fromSpec_top, isoSpec_Spec_inv, + ← Spec.map_comp] + +-- This is not a simp lemma to respect the abstraction boundaries +/-- A variant of `Spec_fromSpecStalk` that breaks abstraction boundaries. -/ +lemma Spec_fromSpecStalk' (R : CommRingCat) (x) : + (Spec R).fromSpecStalk x = Spec.map (StructureSheaf.toStalk R _) := + Spec_fromSpecStalk _ _ + +@[stacks 01J7] +lemma range_fromSpecStalk {x : X} : + Set.range (X.fromSpecStalk x).base = { y | y ⤳ x } := by + ext y + constructor + · rintro ⟨y, rfl⟩ + exact ((LocalRing.specializes_closedPoint y).map (X.fromSpecStalk x).base.2).trans + (specializes_of_eq fromSpecStalk_closedPoint) + · rintro (hy : y ⤳ x) + have := fromSpecStalk_closedPoint (x := y) + rw [← Spec_map_stalkSpecializes_fromSpecStalk hy] at this + exact ⟨_, this⟩ + +end Scheme + +end fromSpecStalk + +variable (R : CommRingCat.{u}) [LocalRing R] + +section stalkClosedPointIso + +/-- For a local ring `(R, 𝔪)`, +this is the isomorphism between the stalk of `Spec R` at `𝔪` and `R`. -/ +noncomputable +def stalkClosedPointIso : + (Spec R).presheaf.stalk (closedPoint R) ≅ R := + StructureSheaf.stalkIso _ _ ≪≫ (IsLocalization.atUnits R + (closedPoint R).asIdeal.primeCompl fun _ ↦ not_not.mp).toRingEquiv.toCommRingCatIso.symm + +lemma stalkClosedPointIso_inv : + (stalkClosedPointIso R).inv = StructureSheaf.toStalk R _ := by + ext x + exact StructureSheaf.localizationToStalk_of _ _ _ + +lemma ΓSpecIso_hom_stalkClosedPointIso_inv : + (Scheme.ΓSpecIso R).hom ≫ (stalkClosedPointIso R).inv = + (Spec R).presheaf.germ ⊤ (closedPoint _) trivial := by + rw [stalkClosedPointIso_inv, ← Iso.eq_inv_comp] + rfl + +@[reassoc (attr := simp)] +lemma germ_stalkClosedPointIso_hom : + (Spec R).presheaf.germ ⊤ (closedPoint _) trivial ≫ (stalkClosedPointIso R).hom = + (Scheme.ΓSpecIso R).hom := by + rw [← ΓSpecIso_hom_stalkClosedPointIso_inv, Category.assoc, Iso.inv_hom_id, Category.comp_id] + +lemma Spec_stalkClosedPointIso : + Spec.map (stalkClosedPointIso R).inv = (Spec R).fromSpecStalk (closedPoint R) := by + rw [stalkClosedPointIso_inv, Scheme.Spec_fromSpecStalk'] + +end stalkClosedPointIso + +section stalkClosedPointTo + +variable {R} (f : Spec R ⟶ X) + + +namespace Scheme + +/-- +Given a local ring `(R, 𝔪)` and a morphism `f : Spec R ⟶ X`, +they induce a (local) ring homomorphism `φ : 𝒪_{X, f 𝔪} ⟶ R`. + +This is inverse to `φ ↦ Spec.map φ ≫ X.fromSpecStalk (f 𝔪)`. See `SpecToEquivOfLocalRing`. +-/ +noncomputable +def stalkClosedPointTo : + X.presheaf.stalk (f.base (closedPoint R)) ⟶ R := + f.stalkMap (closedPoint R) ≫ (stalkClosedPointIso R).hom + +instance isLocalRingHom_stalkClosedPointTo : + IsLocalRingHom (stalkClosedPointTo f) := by + apply (config := { allowSynthFailures := true }) RingHom.isLocalRingHom_comp + · apply isLocalRingHom_of_iso + · apply f.prop + +lemma preimage_eq_top_of_closedPoint_mem + {U : Opens X} (hU : f.base (closedPoint R) ∈ U) : f ⁻¹ᵁ U = ⊤ := + LocalRing.closed_point_mem_iff.mp hU + +lemma stalkClosedPointTo_comp (g : X ⟶ Y) : + stalkClosedPointTo (f ≫ g) = g.stalkMap _ ≫ stalkClosedPointTo f := by + rw [stalkClosedPointTo, Scheme.stalkMap_comp] + exact Category.assoc _ _ _ + +lemma germ_stalkClosedPointTo_Spec {R S : CommRingCat} [LocalRing S] (φ : R ⟶ S): + (Spec R).presheaf.germ ⊤ _ trivial ≫ stalkClosedPointTo (Spec.map φ) = + (ΓSpecIso R).hom ≫ φ := by + rw [stalkClosedPointTo, Scheme.stalkMap_germ_assoc, ← Iso.inv_comp_eq, + ← ΓSpecIso_inv_naturality_assoc] + simp_rw [Opens.map_top] + rw [germ_stalkClosedPointIso_hom, Iso.inv_hom_id, Category.comp_id] + +@[reassoc] +lemma germ_stalkClosedPointTo (U : Opens X) (hU : f.base (closedPoint R) ∈ U) : + X.presheaf.germ U _ hU ≫ stalkClosedPointTo f = f.app U ≫ + ((Spec R).presheaf.mapIso (eqToIso (preimage_eq_top_of_closedPoint_mem f hU).symm).op ≪≫ + ΓSpecIso R).hom := by + rw [stalkClosedPointTo, Scheme.stalkMap_germ_assoc, Iso.trans_hom] + congr 1 + rw [← Iso.eq_comp_inv, Category.assoc, ΓSpecIso_hom_stalkClosedPointIso_inv] + simp only [TopCat.Presheaf.pushforward_obj_obj, Functor.mapIso_hom, Iso.op_hom, eqToIso.hom, + TopCat.Presheaf.germ_res] + +@[reassoc] +lemma germ_stalkClosedPointTo_Spec_fromSpecStalk + {x : X} (f : X.presheaf.stalk x ⟶ R) [IsLocalRingHom f] (U : Opens X) (hU) : + X.presheaf.germ U _ hU ≫ stalkClosedPointTo (Spec.map f ≫ X.fromSpecStalk x) = + X.presheaf.germ U x (by simpa using hU) ≫ f := by + have : (Spec.map f ≫ X.fromSpecStalk x).base (closedPoint R) = x := by + rw [comp_base_apply, Spec_closedPoint, fromSpecStalk_closedPoint] + have : x ∈ U := this ▸ hU + simp only [TopCat.Presheaf.stalkCongr_hom, TopCat.Presheaf.germ_stalkSpecializes_assoc, + germ_stalkClosedPointTo, comp_app, + fromSpecStalk_app (X := X) (x := x) this, Category.assoc, Iso.trans_hom, + Functor.mapIso_hom, Hom.naturality_assoc, ← Functor.map_comp_assoc, + (Spec.map f).app_eq_appLE, Hom.appLE_map_assoc, Hom.map_appLE_assoc] + simp_rw [← Opens.map_top (Spec.map f).base] + rw [← (Spec.map f).app_eq_appLE, ΓSpecIso_naturality, Iso.inv_hom_id_assoc] + +lemma stalkClosedPointTo_fromSpecStalk (x : X) : + stalkClosedPointTo (X.fromSpecStalk x) = + (X.presheaf.stalkCongr (by rw [fromSpecStalk_closedPoint]; rfl)).hom := by + refine TopCat.Presheaf.stalk_hom_ext _ fun U hxU ↦ ?_ + simp only [TopCat.Presheaf.stalkCongr_hom, TopCat.Presheaf.germ_stalkSpecializes, id_eq] + have : X.fromSpecStalk x = Spec.map (𝟙 (X.presheaf.stalk x)) ≫ X.fromSpecStalk x := by simp + convert germ_stalkClosedPointTo_Spec_fromSpecStalk (𝟙 (X.presheaf.stalk x)) U hxU + +@[reassoc] +lemma Spec_stalkClosedPointTo_fromSpecStalk : + Spec.map (stalkClosedPointTo f) ≫ X.fromSpecStalk _ = f := by + obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ := (isBasis_affine_open X).exists_subset_of_mem_open + (Set.mem_univ (f.base (closedPoint R))) isOpen_univ + have := IsAffineOpen.Spec_map_appLE_fromSpec f hU (isAffineOpen_top _) + (preimage_eq_top_of_closedPoint_mem f hxU).ge + rw [IsAffineOpen.fromSpec_top, Iso.eq_inv_comp, isoSpec_Spec_hom] at this + rw [← hU.fromSpecStalk_eq_fromSpecStalk hxU, IsAffineOpen.fromSpecStalk, ← Spec.map_comp_assoc, + germ_stalkClosedPointTo] + simpa only [Iso.trans_hom, Functor.mapIso_hom, Iso.op_hom, Category.assoc, + Hom.app_eq_appLE, Hom.appLE_map_assoc, Spec.map_comp_assoc] + +end Scheme + +end stalkClosedPointTo + +variable {R} + +omit [LocalRing R] in +/-- useful lemma for applications of `SpecToEquivOfLocalRing` -/ +lemma SpecToEquivOfLocalRing_eq_iff + {f₁ f₂ : Σ x, { f : X.presheaf.stalk x ⟶ R // IsLocalRingHom f }} : + f₁ = f₂ ↔ ∃ h₁ : f₁.1 = f₂.1, f₁.2.1 = + (X.presheaf.stalkCongr (by rw [h₁]; rfl)).hom ≫ f₂.2.1 := by + constructor + · rintro rfl; simp + · obtain ⟨x₁, ⟨f₁, h₁⟩⟩ := f₁ + obtain ⟨x₂, ⟨f₂, h₂⟩⟩ := f₂ + rintro ⟨rfl : x₁ = x₂, e : f₁ = _⟩ + simp [e] + +variable (X R) + +/-- +Given a local ring `R` and scheme `X`, morphisms `Spec R ⟶ X` corresponds to pairs +`(x, f)` where `x : X` and `f : 𝒪_{X, x} ⟶ R` is a local ring homomorphism. +-/ +@[simps] +noncomputable +def SpecToEquivOfLocalRing : + (Spec R ⟶ X) ≃ Σ x, { f : X.presheaf.stalk x ⟶ R // IsLocalRingHom f } where + toFun f := ⟨f.base (closedPoint R), Scheme.stalkClosedPointTo f, inferInstance⟩ + invFun xf := Spec.map xf.2.1 ≫ X.fromSpecStalk xf.1 + left_inv := Scheme.Spec_stalkClosedPointTo_fromSpecStalk + right_inv xf := by + obtain ⟨x, ⟨f, hf⟩⟩ := xf + symm + refine SpecToEquivOfLocalRing_eq_iff.mpr ⟨?_, ?_⟩ + · simp only [Scheme.comp_coeBase, TopCat.coe_comp, Function.comp_apply, Spec_closedPoint, + Scheme.fromSpecStalk_closedPoint] + · refine TopCat.Presheaf.stalk_hom_ext _ fun U hxU ↦ ?_ + simp only [Scheme.germ_stalkClosedPointTo_Spec_fromSpecStalk, + TopCat.Presheaf.stalkCongr_hom, TopCat.Presheaf.germ_stalkSpecializes_assoc] + end AlgebraicGeometry