From d568375c5456705286ca42fb2eb9aaa84c559f02 Mon Sep 17 00:00:00 2001 From: Andrew Yang Date: Wed, 24 Jul 2024 06:00:36 +0800 Subject: [PATCH 1/4] =?UTF-8?q?refactor(AlgebraicGeometry):=20Introduce=20?= =?UTF-8?q?`Scheme.toSpec=CE=93`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/AlgebraicGeometry/AffineScheme.lean | 25 +++---- .../GammaSpecAdjunction.lean | 66 ++++++++++--------- Mathlib/AlgebraicGeometry/Pullbacks.lean | 4 +- 3 files changed, 50 insertions(+), 45 deletions(-) diff --git a/Mathlib/AlgebraicGeometry/AffineScheme.lean b/Mathlib/AlgebraicGeometry/AffineScheme.lean index dcbd2c259a492..1a69332850544 100644 --- a/Mathlib/AlgebraicGeometry/AffineScheme.lean +++ b/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 @@ -354,10 +356,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] @@ -649,7 +650,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 diff --git a/Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean b/Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean index 7180e550a04f1..e91bf2784771c 100644 --- a/Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean +++ b/Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean @@ -420,14 +420,12 @@ 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 +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 := @@ -439,56 +437,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. -/ diff --git a/Mathlib/AlgebraicGeometry/Pullbacks.lean b/Mathlib/AlgebraicGeometry/Pullbacks.lean index c6a2251ef7e71..746b620e01e1b 100644 --- a/Mathlib/AlgebraicGeometry/Pullbacks.lean +++ b/Mathlib/AlgebraicGeometry/Pullbacks.lean @@ -462,8 +462,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`. -/ From 6c86c0bc5721691885e6720755d7a11960843346 Mon Sep 17 00:00:00 2001 From: Andrew Yang <36414270+erdOne@users.noreply.github.com> Date: Wed, 24 Jul 2024 11:43:29 +0800 Subject: [PATCH 2/4] Update GammaSpecAdjunction.lean --- Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean b/Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean index e91bf2784771c..dc04f7ca83068 100644 --- a/Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean +++ b/Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean @@ -420,6 +420,7 @@ theorem adjunction_counit_app' {R : CommRingCatᵒᵖ} : theorem adjunction_counit_app {R : CommRingCatᵒᵖ} : ΓSpec.adjunction.counit.app R = (Scheme.ΓSpecIso (unop R)).inv.op := 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 From 61d9df585a85bd4dbc5a038846551735d195ecaf Mon Sep 17 00:00:00 2001 From: Andrew Yang Date: Thu, 3 Oct 2024 16:16:48 +0100 Subject: [PATCH 3/4] fix --- Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean b/Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean index 83373737cbce2..fc114dd60f6a8 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean @@ -353,7 +353,7 @@ 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 _ _ @@ -361,8 +361,6 @@ theorem isIso_ΓSpec_adjunction_unit_app_basicOpen {X : Scheme} [CompactSpace X] · 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 From eb1d5a54304de66748b65f7962d2b345bed3151c Mon Sep 17 00:00:00 2001 From: Andrew Yang Date: Thu, 3 Oct 2024 16:20:40 +0100 Subject: [PATCH 4/4] fix --- Mathlib/AlgebraicGeometry/Morphisms/Affine.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/AlgebraicGeometry/Morphisms/Affine.lean b/Mathlib/AlgebraicGeometry/Morphisms/Affine.lean index 9cf21c35955ab..c990b0ee818d7 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/Affine.lean +++ b/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]