[Merged by Bors] - refactor(AlgebraicGeometry): Introduce Scheme.toSpecΓ

Mathlib/AlgebraicGeometry/AffineScheme.lean

@@ -52,24 +52,26 @@ deriving Category
 
 /-- A Scheme is affine if the canonical map `X ⟶ Spec Γ(X)` is an isomorphism. -/
 class IsAffine (X : Scheme) : Prop where
-  affine : IsIso (ΓSpec.adjunction.unit.app X)
+  affine : IsIso X.toSpecΓ
 
 attribute [instance] IsAffine.affine
 
+instance (X : Scheme.{u}) [IsAffine X] : IsIso (ΓSpec.adjunction.unit.app X) := @IsAffine.affine X _
+
 /-- The canonical isomorphism `X ≅ Spec Γ(X)` for an affine scheme. -/
 @[simps! (config := .lemmasOnly) hom]
 def Scheme.isoSpec (X : Scheme) [IsAffine X] : X ≅ Spec Γ(X, ⊤) :=
-  asIso (ΓSpec.adjunction.unit.app X)
+  asIso X.toSpecΓ
 
 @[reassoc]
 theorem Scheme.isoSpec_hom_naturality {X Y : Scheme} [IsAffine X] [IsAffine Y] (f : X ⟶ Y) :
     X.isoSpec.hom ≫ Spec.map (f.app ⊤) = f ≫ Y.isoSpec.hom := by
-  simp only [isoSpec, asIso_hom, ΓSpec.adjunction_unit_naturality]
+  simp only [isoSpec, asIso_hom, Scheme.toSpecΓ_naturality]
 
 @[reassoc]
 theorem Scheme.isoSpec_inv_naturality {X Y : Scheme} [IsAffine X] [IsAffine Y] (f : X ⟶ Y) :
     Spec.map (f.app ⊤) ≫ Y.isoSpec.inv = X.isoSpec.inv ≫ f := by
-  rw [Iso.eq_inv_comp, isoSpec, asIso_hom, ← ΓSpec.adjunction_unit_naturality_assoc, isoSpec,
+  rw [Iso.eq_inv_comp, isoSpec, asIso_hom, ← Scheme.toSpecΓ_naturality_assoc, isoSpec,
     asIso_inv, IsIso.hom_inv_id, Category.comp_id]
 
 /-- Construct an affine scheme from a scheme and the information that it is affine.
@@ -228,7 +230,7 @@ theorem iSup_affineOpens_eq_top (X : Scheme) : ⨆ i : X.affineOpens, (i : X.Ope
 theorem Scheme.map_PrimeSpectrum_basicOpen_of_affine
     (X : Scheme) [IsAffine X] (f : Scheme.Γ.obj (op X)) :
     X.isoSpec.hom ⁻¹ᵁ PrimeSpectrum.basicOpen f = X.basicOpen f :=
-  ΓSpec.adjunction_unit_map_basicOpen _ _
+  Scheme.toSpecΓ_preimage_basicOpen _ _
 
 theorem isBasis_basicOpen (X : Scheme) [IsAffine X] :
     Opens.IsBasis (Set.range (X.basicOpen : Γ(X, ⊤) → X.Opens)) := by
@@ -240,10 +242,10 @@ theorem isBasis_basicOpen (X : Scheme) [IsAffine X] :
   constructor
   · rintro ⟨_, ⟨x, rfl⟩, rfl⟩
     refine ⟨_, ⟨_, ⟨x, rfl⟩, rfl⟩, ?_⟩
-    exact congr_arg Opens.carrier (ΓSpec.adjunction_unit_map_basicOpen _ _)
+    exact congr_arg Opens.carrier (Scheme.toSpecΓ_preimage_basicOpen _ _)
   · rintro ⟨_, ⟨_, ⟨x, rfl⟩, rfl⟩, rfl⟩
     refine ⟨_, ⟨x, rfl⟩, ?_⟩
-    exact congr_arg Opens.carrier (ΓSpec.adjunction_unit_map_basicOpen _ _).symm
+    exact congr_arg Opens.carrier (Scheme.toSpecΓ_preimage_basicOpen _ _).symm
 
 namespace IsAffineOpen
 
@@ -356,10 +358,9 @@ theorem SpecΓIdentity_hom_app_fromSpec :
     (Scheme.ΓSpecIso Γ(X, U)).hom ≫ hU.fromSpec.app U =
       (Spec Γ(X, U)).presheaf.map (eqToHom hU.fromSpec_preimage_self).op := by
   simp only [fromSpec, Scheme.isoSpec, asIso_inv, Scheme.comp_coeBase, Opens.map_comp_obj,
-    ΓSpecIso_obj_hom, Scheme.Opens.topIso_inv, Opens.map_top, Functor.id_obj, Functor.comp_obj,
-    Functor.rightOp_obj, Scheme.Γ_obj, unop_op, Scheme.Spec_obj, Scheme.Opens.topIso_hom,
-    Scheme.comp_app, Scheme.Opens.ι_app_self, Category.assoc, ← Functor.map_comp_assoc, ← op_comp,
-    eqToHom_trans, Scheme.Opens.eq_presheaf_map_eqToHom, Scheme.Hom.naturality_assoc,
+    ΓSpecIso_obj_hom, Scheme.Opens.topIso_inv, Opens.map_top, Scheme.Opens.topIso_hom,
+    Scheme.comp_app, Scheme.Opens.ι_app_self, unop_op, Category.assoc, ← Functor.map_comp_assoc, ←
+    op_comp, eqToHom_trans, Scheme.Opens.eq_presheaf_map_eqToHom, Scheme.Hom.naturality_assoc,
     Scheme.inv_app_top, IsIso.hom_inv_id_assoc]
   simp only [eqToHom_op, eqToHom_map, Spec.map_eqToHom, eqToHom_unop,
     Scheme.Spec_map_presheaf_map_eqToHom, eqToHom_trans]
@@ -683,7 +684,7 @@ section ZeroLocus
 /-- On a locally ringed space `X`, the preimage of the zero locus of the prime spectrum
 of `Γ(X, ⊤)` under `toΓSpecFun` agrees with the associated zero locus on `X`. -/
 lemma Scheme.toΓSpec_preimage_zeroLocus_eq {X : Scheme.{u}} (s : Set Γ(X, ⊤)) :
-    (ΓSpec.adjunction.unit.app X).val.base ⁻¹' PrimeSpectrum.zeroLocus s = X.zeroLocus s :=
+    X.toSpecΓ.val.base ⁻¹' PrimeSpectrum.zeroLocus s = X.zeroLocus s :=
   LocallyRingedSpace.toΓSpec_preimage_zeroLocus_eq s
 
 open ConcreteCategory

Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

@@ -403,14 +403,13 @@ theorem adjunction_counit_app' {R : CommRingCatᵒᵖ} :
 theorem adjunction_counit_app {R : CommRingCatᵒᵖ} :
     ΓSpec.adjunction.counit.app R = (Scheme.ΓSpecIso (unop R)).inv.op := rfl
 
--- This is not a simp lemma to respect the abstraction
-theorem adjunction_unit_app {X : Scheme} :
-    ΓSpec.adjunction.unit.app X = locallyRingedSpaceAdjunction.unit.app X.1 := rfl
+/-- The canonical map `X ⟶ Spec Γ(X, ⊤)`. This is the unit of the `Γ-Spec` adjunction. -/
+def _root_.AlgebraicGeometry.Scheme.toSpecΓ (X : Scheme.{u}) : X ⟶ Spec Γ(X, ⊤) :=
+  ΓSpec.adjunction.unit.app X
 
-@[reassoc (attr := simp)]
-theorem adjunction_unit_naturality {X Y : Scheme.{u}} (f : X ⟶ Y) :
-    f ≫ ΓSpec.adjunction.unit.app Y = ΓSpec.adjunction.unit.app X ≫ Spec.map (f.app ⊤) :=
-  ΓSpec.adjunction.unit.naturality f
+@[simp]
+theorem adjunction_unit_app {X : Scheme} :
+    ΓSpec.adjunction.unit.app X = X.toSpecΓ := rfl
 
 instance isIso_locallyRingedSpaceAdjunction_counit :
     IsIso.{u + 1, u + 1} locallyRingedSpaceAdjunction.counit :=
@@ -422,56 +421,62 @@ instance isIso_adjunction_counit : IsIso ΓSpec.adjunction.counit := by
   rw [adjunction_counit_app]
   infer_instance
 
+end ΓSpec
+
+@[reassoc (attr := simp)]
+theorem Scheme.toSpecΓ_naturality {X Y : Scheme.{u}} (f : X ⟶ Y) :
+    f ≫ Y.toSpecΓ = X.toSpecΓ ≫ Spec.map (f.app ⊤) :=
+  ΓSpec.adjunction.unit.naturality f
+
 @[simp]
-theorem adjunction_unit_app_app_top (X : Scheme.{u}) :
-    (ΓSpec.adjunction.unit.app X).app ⊤ = (Scheme.ΓSpecIso Γ(X, ⊤)).hom := by
+theorem Scheme.toSpecΓ_app_top (X : Scheme.{u}) :
+    X.toSpecΓ.app ⊤ = (Scheme.ΓSpecIso Γ(X, ⊤)).hom := by
   have := ΓSpec.adjunction.left_triangle_components X
   dsimp at this
   rw [← IsIso.eq_comp_inv] at this
-  simp only [adjunction_counit_app, Functor.id_obj, Functor.comp_obj, Functor.rightOp_obj,
+  simp only [ΓSpec.adjunction_counit_app, Functor.id_obj, Functor.comp_obj, Functor.rightOp_obj,
     Scheme.Γ_obj, Category.id_comp] at this
   rw [← Quiver.Hom.op_inj.eq_iff, this, ← op_inv, IsIso.Iso.inv_inv]
 
 @[simp]
 theorem SpecMap_ΓSpecIso_hom (R : CommRingCat.{u}) :
-    Spec.map ((Scheme.ΓSpecIso R).hom) = adjunction.unit.app (Spec R) := by
+    Spec.map ((Scheme.ΓSpecIso R).hom) = (Spec R).toSpecΓ := by
   have := ΓSpec.adjunction.right_triangle_components (op R)
   dsimp at this
   rwa [← IsIso.eq_comp_inv, Category.id_comp, ← Spec.map_inv, IsIso.Iso.inv_inv, eq_comm] at this
 
-lemma adjunction_unit_map_basicOpen (X : Scheme.{u}) (r : Γ(X, ⊤)) :
-    (ΓSpec.adjunction.unit.app X ⁻¹ᵁ (PrimeSpectrum.basicOpen r)) = X.basicOpen r := by
-  rw [← basicOpen_eq_of_affine]
-  erw [Scheme.preimage_basicOpen]
+lemma Scheme.toSpecΓ_preimage_basicOpen (X : Scheme.{u}) (r : Γ(X, ⊤)) :
+    X.toSpecΓ ⁻¹ᵁ (PrimeSpectrum.basicOpen r) = X.basicOpen r := by
+  rw [← basicOpen_eq_of_affine, Scheme.preimage_basicOpen]
   congr
-  rw [ΓSpec.adjunction_unit_app_app_top]
+  rw [Scheme.toSpecΓ_app_top]
   exact Iso.inv_hom_id_apply _ _
 
-theorem toOpen_unit_app_val_c_app {X : Scheme.{u}} (U) :
-    StructureSheaf.toOpen _ _ ≫ (ΓSpec.adjunction.unit.app X).val.c.app U =
+-- 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.unop))).op]
+    NatTrans.naturality _ (homOfLE (le_top (a := U))).op]
   show (Γ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 _
 
--- Warning: this LHS of this lemma breaks the structure-sheaf abstraction.
-@[reassoc (attr := simp)]
-theorem toOpen_unit_app_val_c_app' {X : Scheme.{u}} (U : Opens (PrimeSpectrum Γ(X, ⊤))) :
-    toOpen Γ(X, ⊤) U ≫ (adjunction.unit.app X).app U =
-      X.presheaf.map (homOfLE (by exact le_top)).op :=
-  ΓSpec.toOpen_unit_app_val_c_app (op U)
-
-end ΓSpec
-
 theorem ΓSpecIso_obj_hom {X : Scheme.{u}} (U : X.Opens) :
     (Scheme.ΓSpecIso Γ(X, U)).hom = (Spec.map U.topIso.inv).app ⊤ ≫
-      (ΓSpec.adjunction.unit.app U).app ⊤ ≫ U.topIso.hom := by
-  rw [ΓSpec.adjunction_unit_app_app_top] -- why can't simp find this
-  simp
+      U.toScheme.toSpecΓ.app ⊤ ≫ U.topIso.hom := by simp
+
+@[deprecated (since := "2024-07-24")]
+alias ΓSpec.adjunction_unit_naturality := Scheme.toSpecΓ_naturality
+@[deprecated (since := "2024-07-24")]
+alias ΓSpec.adjunction_unit_naturality_assoc := Scheme.toSpecΓ_naturality_assoc
+@[deprecated (since := "2024-07-24")]
+alias ΓSpec.adjunction_unit_app_app_top := Scheme.toSpecΓ_app_top
+@[deprecated (since := "2024-07-24")]
+alias ΓSpec.adjunction_unit_map_basicOpen := Scheme.toSpecΓ_preimage_basicOpen
 
 /-! Immediate consequences of the adjunction. -/
 

Mathlib/AlgebraicGeometry/Morphisms/Affine.lean

@@ -122,8 +122,7 @@ lemma isAffine_of_isAffineOpen_basicOpen (s : Set Γ(X, ⊤))
     simp only [← basicOpen_eq_of_affine]
     exact (isAffineOpen_top (Scheme.Spec.obj (op _))).basicOpen _
   · rw [PrimeSpectrum.iSup_basicOpen_eq_top_iff, Subtype.range_coe_subtype, Set.setOf_mem_eq, hs]
-  · show IsAffineOpen (ΓSpec.adjunction.unit.app X ⁻¹ᵁ PrimeSpectrum.basicOpen i.1)
-    rw [ΓSpec.adjunction_unit_map_basicOpen]
+  · rw [Scheme.toSpecΓ_preimage_basicOpen]
     exact hs₂ _ i.2
   · simp only [Functor.comp_obj, Functor.rightOp_obj, Scheme.Γ_obj, Scheme.Spec_obj, id_eq,
       eq_mpr_eq_cast, Functor.id_obj, Opens.map_top, morphismRestrict_app]

Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

@@ -353,16 +353,14 @@ theorem isIso_ΓSpec_adjunction_unit_app_basicOpen {X : Scheme} [CompactSpace X]
     [QuasiSeparatedSpace X] (f : X.presheaf.obj (op ⊤)) :
     IsIso ((ΓSpec.adjunction.unit.app X).val.c.app (op (PrimeSpectrum.basicOpen f))) := by
   refine @IsIso.of_isIso_comp_right _ _ _ _ _ _ (X.presheaf.map
-    (eqToHom (ΓSpec.adjunction_unit_map_basicOpen _ _).symm).op) _ ?_
+    (eqToHom (Scheme.toSpecΓ_preimage_basicOpen _ _).symm).op) _ ?_
   rw [ConcreteCategory.isIso_iff_bijective, CommRingCat.forget_map]
   apply (config := { allowSynthFailures := true }) IsLocalization.bijective
   · exact StructureSheaf.IsLocalization.to_basicOpen _ _
   · refine is_localization_basicOpen_of_qcqs ?_ ?_ _
     · exact isCompact_univ
     · exact isQuasiSeparated_univ
   · rw [← CommRingCat.comp_eq_ring_hom_comp]
-    simp [RingHom.algebraMap_toAlgebra]
-    rw [ΓSpec.toOpen_unit_app_val_c_app'_assoc, ← Functor.map_comp]
-    rfl
+    simp [RingHom.algebraMap_toAlgebra, ← Functor.map_comp]
 
 end AlgebraicGeometry

Mathlib/AlgebraicGeometry/Pullbacks.lean

@@ -453,8 +453,8 @@ instance isAffine_of_isAffine_isAffine_isAffine {X Y Z : Scheme}
     IsAffine (pullback f g) :=
   isAffine_of_isIso
     (pullback.map f g (Spec.map (Γ.map f.op)) (Spec.map (Γ.map g.op))
-        (ΓSpec.adjunction.unit.app X) (ΓSpec.adjunction.unit.app Y) (ΓSpec.adjunction.unit.app Z)
-        (ΓSpec.adjunction.unit.naturality f) (ΓSpec.adjunction.unit.naturality g) ≫
+        X.toSpecΓ Y.toSpecΓ Z.toSpecΓ
+        (Scheme.toSpecΓ_naturality f) (Scheme.toSpecΓ_naturality g) ≫
       (PreservesPullback.iso Scheme.Spec _ _).inv)
 
 /-- Given an open cover `{ Xᵢ }` of `X`, then `X ×[Z] Y` is covered by `Xᵢ ×[Z] Y`. -/