chore(AlgebraicGeometry): refactor structureSheaf (leanprover-community#35090)

We redefine `structureSheaf` to unify its construction with `tilde`.

Author: erdOne

Mathlib/Algebra/Category/Ring/FilteredColimits.lean

@@ -295,6 +295,14 @@ instance forget₂SemiRing_preservesFilteredColimits :
           (SemiRingCat.FilteredColimits.colimitCoconeIsColimit
             (F ⋙ forget₂ RingCat SemiRingCat.{u})) }
 
+instance : Limits.PreservesFilteredColimits (forget₂ RingCat AddCommGrpCat.{u}) where
+  preserves_filtered_colimits _ :=
+    { preservesColimit := fun {F} =>
+        Limits.preservesColimit_of_preserves_colimit_cocone
+          (RingCat.FilteredColimits.colimitCoconeIsColimit.{u, u} F)
+          (AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit
+            (F ⋙ forget₂ RingCat AddCommGrpCat.{u})) }
+
 instance forget_preservesFilteredColimits : PreservesFilteredColimits (forget RingCat.{u}) :=
   Limits.comp_preservesFilteredColimits (forget₂ RingCat SemiRingCat) (forget SemiRingCat.{u})
 

Mathlib/AlgebraicGeometry/AffineScheme.lean

@@ -622,7 +622,7 @@ theorem exists_basicOpen_le {V : X.Opens} (x : V) (h : ↑x ∈ U) :
 
 noncomputable
 instance {R : CommRingCat} {U} : Algebra R Γ(Spec R, U) :=
-  ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.map (homOfLE le_top).op).hom.toAlgebra
+  inferInstanceAs (Algebra R ((Spec.structureSheaf R).presheaf.obj _))
 
 @[simp]
 lemma algebraMap_Spec_obj {R : CommRingCat} {U} : algebraMap R Γ(Spec R, U) =
@@ -653,13 +653,13 @@ theorem isLocalization_basicOpen :
     (IsLocalization.isLocalization_iff_of_ringEquiv (Submonoid.powers f)
       (asIso <| basicOpenSectionsToAffine hU f).commRingCatIsoToRingEquiv).mpr
   convert StructureSheaf.IsLocalization.to_basicOpen _ f using 1
-  -- Porting note: more hand holding is required here, the next 3 lines were not necessary
+  apply Algebra.algebra_ext
+  intro _
   congr 1
   dsimp [CommRingCat.ofHom, RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp,
     basicOpenSectionsToAffine]
   rw [hU.fromSpec.naturality_assoc, hU.fromSpec_app_self]
-  simp only [Category.assoc, ← Functor.map_comp, ← op_comp]
-  exact CommRingCat.hom_ext_iff.mp (StructureSheaf.toOpen_res _ _ _ _)
+  rfl
 
 instance _root_.AlgebraicGeometry.isLocalization_away_of_isAffine
     [IsAffine X] (r : Γ(X, ⊤)) :
@@ -1219,22 +1219,44 @@ end Factorization
 
 section Stalks
 
+variable {R S : CommRingCat.{u}} (f : R ⟶ S) (p : PrimeSpectrum S) (x : PrimeSpectrum R)
+
+variable (R) (x : PrimeSpectrum R) in
+/-- The stalk of `Spec R` at `x` is isomorphic to `Rₚ`,
+where `p` is the prime corresponding to `x`. -/
+noncomputable
+def Spec.stalkIso : (Spec R).presheaf.stalk x ≅ .of (Localization.AtPrime x.asIdeal) :=
+  (StructureSheaf.stalkIso ..).toCommRingCatIso.symm
+
+@[reassoc (attr := simp)]
+lemma Spec.algebraMap_stalkIso_inv :
+    CommRingCat.ofHom (algebraMap R _) ≫ (stalkIso R x).inv =
+      (Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial := by
+  ext s : 2
+  exact (IsLocalization.algEquiv _ ((structureSheaf R).presheaf.stalk _) _).symm.commutes s
+
+@[reassoc (attr := simp)]
+lemma Spec.germ_stalkMapIso_hom :
+    (Spec R).presheaf.germ ⊤ _ trivial ≫ (stalkIso R x).hom =
+      (Scheme.ΓSpecIso R).hom ≫ CommRingCat.ofHom (algebraMap R _) := by
+  simp [← Iso.inv_comp_eq, ← Spec.algebraMap_stalkIso_inv_assoc]
+
 /-- Variant of `AlgebraicGeometry.localRingHom_comp_stalkIso` for `Spec.map`. -/
 @[elementwise]
 lemma Scheme.localRingHom_comp_stalkIso {R S : CommRingCat.{u}} (f : R ⟶ S) (p : PrimeSpectrum S) :
-    (StructureSheaf.stalkIso R (PrimeSpectrum.comap f.hom p)).hom ≫
+    (Spec.stalkIso R (p.comap f.hom)).hom ≫
       (CommRingCat.ofHom <| Localization.localRingHom
         (PrimeSpectrum.comap f.hom p).asIdeal p.asIdeal f.hom rfl) ≫
-      (StructureSheaf.stalkIso S p).inv = (Spec.map f).stalkMap p :=
+      (Spec.stalkIso S p).inv = (Spec.map f).stalkMap p :=
   AlgebraicGeometry.localRingHom_comp_stalkIso f p
 
 /-- Given a morphism of rings `f : R ⟶ S`, the stalk map of `Spec S ⟶ Spec R` at
 a prime of `S` is isomorphic to the localized ring homomorphism. -/
 def Scheme.arrowStalkMapSpecIso {R S : CommRingCat.{u}} (f : R ⟶ S) (p : PrimeSpectrum S) :
     Arrow.mk ((Spec.map f).stalkMap p) ≅ Arrow.mk (CommRingCat.ofHom <| Localization.localRingHom
       (p.comap f.hom).asIdeal p.asIdeal f.hom rfl) := Arrow.isoMk
-  (StructureSheaf.stalkIso R (PrimeSpectrum.comap f.hom p))
-  (StructureSheaf.stalkIso S p) <| by
+  (Spec.stalkIso R (p.comap f.hom))
+  (Spec.stalkIso S p) <| by
     rw [← Scheme.localRingHom_comp_stalkIso]
     simp
 

Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

@@ -140,7 +140,8 @@ theorem toΓSpecCApp_iff
     (f :
       (structureSheaf <| Γ.obj <| op X).val.obj (op <| basicOpen r) ⟶
         X.presheaf.obj (op <| X.toΓSpecMapBasicOpen r)) :
-    toOpen _ (basicOpen r) ≫ f = X.toToΓSpecMapBasicOpen r ↔ f = X.toΓSpecCApp r := by
+    CommRingCat.ofHom (algebraMap (Γ.obj (op X)) _) ≫ f = X.toToΓSpecMapBasicOpen r ↔
+      f = X.toΓSpecCApp r := by
   have loc_inst := IsLocalization.to_basicOpen (Γ.obj (op X)) r
   refine ConcreteCategory.ext_iff.trans ?_
   rw [← @IsLocalization.Away.lift_comp _ _ _ _ _ _ _ r loc_inst _
@@ -151,7 +152,8 @@ theorem toΓSpecCApp_iff
     exact IsLocalization.ringHom_ext (Submonoid.powers r) h
   apply congr_arg
 
-theorem toΓSpecCApp_spec : toOpen _ (basicOpen r) ≫ X.toΓSpecCApp r = X.toToΓSpecMapBasicOpen r :=
+theorem toΓSpecCApp_spec :
+    CommRingCat.ofHom (algebraMap (Γ.obj (op X)) _) ≫ X.toΓSpecCApp r = X.toToΓSpecMapBasicOpen r :=
   (X.toΓSpecCApp_iff r _).2 rfl
 
 /-- The sheaf hom on all basic opens, commuting with restrictions. -/
@@ -163,7 +165,9 @@ def toΓSpecCBasicOpens :
   naturality r s f := by
     apply (StructureSheaf.to_basicOpen_epi (Γ.obj (op X)) r.unop).1
     simp only [← Category.assoc]
-    rw [X.toΓSpecCApp_spec r.unop]
+    rw [show algebraMap (Γ.obj (op X)) ((structureSheaf (Γ.obj (op X))).val.obj _) = algebraMap _
+      ((structureSheafInType (Γ.obj (op X)) (Γ.obj (op X))).val.obj _) from rfl,
+      X.toΓSpecCApp_spec r.unop]
     convert X.toΓSpecCApp_spec s.unop
     symm
     apply X.presheaf.map_comp
@@ -182,7 +186,8 @@ theorem toΓSpecSheafedSpace_app_eq :
   apply TopCat.Sheaf.extend_hom_app _ _ _
 
 @[reassoc] theorem toΓSpecSheafedSpace_app_spec (r : Γ.obj (op X)) :
-    toOpen (Γ.obj (op X)) (basicOpen r) ≫ X.toΓSpecSheafedSpace.hom.c.app (op (basicOpen r)) =
+    CommRingCat.ofHom (algebraMap (Γ.obj (op X)) _) ≫
+        X.toΓSpecSheafedSpace.hom.c.app (op (basicOpen r)) =
       X.toToΓSpecMapBasicOpen r :=
   (X.toΓSpecSheafedSpace_app_eq r).symm ▸ X.toΓSpecCApp_spec r
 
@@ -191,8 +196,8 @@ stalks (in `Spec Γ(X)` and in `X`). -/
 theorem toStalk_stalkMap_toΓSpec (x : X) :
     toStalk _ _ ≫ X.toΓSpecSheafedSpace.hom.stalkMap x = X.presheaf.Γgerm x := by
   rw [PresheafedSpace.Hom.stalkMap,
-    ← toOpen_germ _ (basicOpen (1 : Γ.obj (op X))) _ (by rw [basicOpen_one]; trivial),
-    ← Category.assoc, Category.assoc (toOpen _ _), stalkFunctor_map_germ, ← Category.assoc,
+    ← algebraMap_germ (basicOpen (1 : Γ.obj (op X))) _ (by rw [basicOpen_one]; trivial),
+    ← Category.assoc, Category.assoc (CommRingCat.ofHom _), stalkFunctor_map_germ, ← Category.assoc,
     X.toΓSpecSheafedSpace_app_eq, X.toΓSpecCApp_spec, Γgerm]
   erw [← stalkPushforward_germ _ _ X.presheaf ⊤]
   congr 1
@@ -244,7 +249,7 @@ theorem comp_ring_hom_ext {X : LocallyRingedSpace.{u}} {R : CommRingCat.{u}} {f
     (h :
       ∀ r : R,
         f ≫ X.presheaf.map (homOfLE le_top : (Opens.map β.base).obj (basicOpen r) ⟶ _).op =
-          toOpen R (basicOpen r) ≫ β.c.app (op (basicOpen r))) :
+          CommRingCat.ofHom (algebraMap _ _) ≫ β.c.app (op (basicOpen r))) :
     X.toΓSpec ≫ Spec.locallyRingedSpaceMap f = β := by
   refine LocallyRingedSpace.forgetToSheafedSpace.map_injective
     (Spec.basicOpen_hom_ext w ?_)
@@ -258,10 +263,11 @@ theorem comp_ring_hom_ext {X : LocallyRingedSpace.{u}} {R : CommRingCat.{u}} {f
 /-- `toSpecΓ _` is an isomorphism so these are mutually two-sided inverses. -/
 theorem Γ_Spec_left_triangle : toSpecΓ (Γ.obj (op X)) ≫ X.toΓSpec.c.app (op ⊤) = 𝟙 _ := by
   unfold toSpecΓ
-  rw [← toOpen_res _ (basicOpen (1 : Γ.obj (op X))) ⊤ (eqToHom basicOpen_one.symm),
-    Category.assoc, NatTrans.naturality, ← Category.assoc]
-  erw [X.toΓSpecSheafedSpace_app_spec 1, ← Functor.map_comp]
-  convert eqToHom_map X.presheaf _; rfl
+  have := X.toΓSpecSheafedSpace_app_spec 1
+  unfold toToΓSpecMapBasicOpen toΓSpecMapBasicOpen at this
+  rw! [basicOpen_one] at this
+  convert this
+  exact (X.presheaf.map_id ..).symm
 
 end LocallyRingedSpace
 
@@ -303,7 +309,7 @@ theorem right_triangle (R : CommRingCat) :
     rw [← IsLocalization.AtPrime.to_map_mem_maximal_iff ((structureSheaf R).presheaf.stalk p)
         p.asIdeal x]
     rfl
-  · intro r; apply toOpen_res
+  · intro r; rfl
 
 /-- The adjunction `Γ ⊣ Spec` from `CommRingᵒᵖ` to `LocallyRingedSpace`. -/
 @[simps]
@@ -323,23 +329,26 @@ def locallyRingedSpaceAdjunction : Γ.rightOp ⊣ Spec.toLocallyRingedSpace.{u}
       Spec.toLocallyRingedSpace_map, Quiver.Hom.unop_op]
     exact right_triangle R.unop
 
-/-- `@[simp]`-normal form of `locallyRingedSpaceAdjunction_counit_app`. -/
-@[simp]
+
 lemma toSpecΓ_unop (R : CommRingCatᵒᵖ) :
-    AlgebraicGeometry.toSpecΓ (Opposite.unop R) = toOpen R.unop ⊤ := rfl
+    AlgebraicGeometry.toSpecΓ (Opposite.unop R) = CommRingCat.ofHom (algebraMap _ _) := rfl
 
 /-- `@[simp]`-normal form of `locallyRingedSpaceAdjunction_counit_app'`. -/
 @[simp]
 lemma toSpecΓ_of (R : Type u) [CommRing R] :
-    AlgebraicGeometry.toSpecΓ (CommRingCat.of R) = toOpen R ⊤ := rfl
+    AlgebraicGeometry.toSpecΓ (CommRingCat.of R) = CommRingCat.ofHom (algebraMap _ _) := rfl
 
 lemma locallyRingedSpaceAdjunction_counit_app (R : CommRingCatᵒᵖ) :
     locallyRingedSpaceAdjunction.counit.app R =
-      (toOpen R.unop ⊤).op := rfl
+      (CommRingCat.ofHom (algebraMap _ _)).op := rfl
 
 lemma locallyRingedSpaceAdjunction_counit_app' (R : Type u) [CommRing R] :
     locallyRingedSpaceAdjunction.counit.app (op <| CommRingCat.of R) =
-      (toOpen R ⊤).op := rfl
+      (CommRingCat.ofHom (algebraMap _ _)).op := rfl
+
+lemma unop_locallyRingedSpaceAdjunction_counit_app' (R : Type u) [CommRing R] :
+    (locallyRingedSpaceAdjunction.counit.app (op <| CommRingCat.of R)).unop =
+      (CommRingCat.ofHom (algebraMap _ _)) := rfl
 
 lemma locallyRingedSpaceAdjunction_homEquiv_apply
     {X : LocallyRingedSpace} {R : CommRingCatᵒᵖ}
@@ -356,16 +365,16 @@ lemma locallyRingedSpaceAdjunction_homEquiv_apply'
 lemma toOpen_comp_locallyRingedSpaceAdjunction_homEquiv_app
     {X : LocallyRingedSpace} {R : Type u} [CommRing R]
     (f : Γ.rightOp.obj X ⟶ op (CommRingCat.of R)) (U) :
-    StructureSheaf.toOpen R U.unop ≫
+    CommRingCat.ofHom (algebraMap R _) ≫
       (locallyRingedSpaceAdjunction.homEquiv X (op <| CommRingCat.of R) f).c.app U =
     f.unop ≫ X.presheaf.map (homOfLE le_top).op := by
-  rw [← StructureSheaf.toOpen_res _ _ _ (homOfLE le_top), Category.assoc,
+  dsimp
+  rw [← StructureSheaf.algebraMap_self_map _ U _ (homOfLE le_top).op, Category.assoc,
     NatTrans.naturality _ (homOfLE (le_top (a := U.unop))).op,
-    show (toOpen R ⊤) = (toOpen R ⊤).op.unop from rfl,
-    ← locallyRingedSpaceAdjunction_counit_app']
+    ← unop_locallyRingedSpaceAdjunction_counit_app']
   simp_rw [← Γ_map_op]
-  rw [← Γ.rightOp_map_unop, ← Category.assoc, ← unop_comp, ← Adjunction.homEquiv_counit,
-    Equiv.symm_apply_apply]
+  rw [← Γ.rightOp_map_unop, ← Category.assoc, ← unop_comp]
+  erw [← Adjunction.homEquiv_counit, Equiv.symm_apply_apply]
   rfl
 
 /-- The adjunction `Γ ⊣ Spec` from `CommRingᵒᵖ` to `Scheme`. -/
@@ -459,19 +468,6 @@ lemma Scheme.toSpecΓ_preimage_basicOpen (X : Scheme.{u}) (r : Γ(X, ⊤)) :
   rw [Scheme.toSpecΓ_appTop]
   exact Iso.inv_hom_id_apply (C := CommRingCat) _ _
 
--- Warning: this LHS of this lemma breaks the structure-sheaf abstraction.
-@[reassoc (attr := simp)]
-theorem toOpen_toSpecΓ_app {X : Scheme.{u}} (U) :
-    StructureSheaf.toOpen _ _ ≫ X.toSpecΓ.app U =
-      X.presheaf.map (homOfLE (by exact le_top)).op := by
-  rw [← StructureSheaf.toOpen_res _ _ _ (homOfLE le_top), Category.assoc,
-    NatTrans.naturality _ (homOfLE (le_top (a := U))).op]
-  change (ΓSpec.adjunction.counit.app (Scheme.Γ.rightOp.obj X)).unop ≫
-    (Scheme.Γ.rightOp.map (ΓSpec.adjunction.unit.app X)).unop ≫ _ = _
-  rw [← Category.assoc, ← unop_comp, ΓSpec.adjunction.left_triangle_components]
-  dsimp
-  exact Category.id_comp _
-
 lemma ΓSpecIso_inv_ΓSpec_adjunction_homEquiv {X : Scheme.{u}} {B : CommRingCat} (φ : B ⟶ Γ(X, ⊤)) :
     (Scheme.ΓSpecIso B).inv ≫ ((ΓSpec.adjunction.homEquiv X (op B)) φ.op).appTop = φ := by
   simp only [Adjunction.homEquiv_apply, Scheme.Spec_map, Opens.map_top, Scheme.Hom.comp_app]

Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean

@@ -42,6 +42,7 @@ variable {X : Scheme.{u}}
 variable (I : IdealSheafData X)
 
 /-- `Spec (𝒪ₓ(U)/I(U))`, the object to be glued into the closed subscheme. -/
+noncomputable
 def glueDataObj (U : X.affineOpens) : Scheme :=
   Spec <| .of <| Γ(X, U) ⧸ I.ideal U