feat(algebraic_geometry): Define the category of AffineSchemes (#11326

)

src/algebraic_geometry/AffineScheme.lean

@@ -0,0 +1,139 @@
+/-
+Copyright (c) 2022 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import algebraic_geometry.Gamma_Spec_adjunction
+import algebraic_geometry.open_immersion
+import category_theory.limits.opposites
+
+/-!
+# Affine schemes
+
+We define the category of `AffineScheme`s as the essential image of `Spec`.
+We also define predicates about affine schemes and affine open sets.
+
+## Main definitions
+
+* `algebraic_geometry.AffineScheme`: The category of affine schemes.
+* `algebraic_geometry.is_affine`: A scheme is affine if the canonical map `X ⟶ Spec Γ(X)` is an
+  isomorphism.
+* `algebraic_geometry.Scheme.iso_Spec`: The canonical isomorphism `X ≅ Spec Γ(X)` for an affine
+  scheme.
+* `algebraic_geometry.AffineScheme.equiv_CommRing`: The equivalence of categories
+  `AffineScheme ≌ CommRingᵒᵖ` given by `AffineScheme.Spec : CommRingᵒᵖ ⥤ AffineScheme` and
+  `AffineScheme.Γ : AffineSchemeᵒᵖ ⥤ CommRing`.
+* `algebraic_geometry.is_affine_open`: An open subset of a scheme is affine if the open subscheme is
+  affine.
+
+-/
+
+noncomputable theory
+
+open category_theory category_theory.limits opposite topological_space
+
+universe u
+
+namespace algebraic_geometry
+
+/-- The category of affine schemes -/
+def AffineScheme := Scheme.Spec.ess_image
+
+/-- A Scheme is affine if the canonical map `X ⟶ Spec Γ(X)` is an isomorphism. -/
+class is_affine (X : Scheme) : Prop :=
+(affine : is_iso (Γ_Spec.adjunction.unit.app X))
+
+attribute [instance] is_affine.affine
+
+/-- The canonical isomorphism `X ≅ Spec Γ(X)` for an affine scheme. -/
+def Scheme.iso_Spec (X : Scheme) [is_affine X] :
+  X ≅ Scheme.Spec.obj (op $ Scheme.Γ.obj $ op X) :=
+as_iso (Γ_Spec.adjunction.unit.app X)
+
+lemma mem_AffineScheme (X : Scheme) : X ∈ AffineScheme ↔ is_affine X :=
+⟨λ h, ⟨functor.ess_image.unit_is_iso h⟩, λ h, @@mem_ess_image_of_unit_is_iso _ _ _ X h.1⟩
+
+instance is_affine_AffineScheme (X : AffineScheme.{u}) : is_affine (X : Scheme.{u}) :=
+(mem_AffineScheme _).mp X.prop
+
+instance Spec_is_affine (R : CommRingᵒᵖ) : is_affine (Scheme.Spec.obj R) :=
+(mem_AffineScheme _).mp (Scheme.Spec.obj_mem_ess_image R)
+
+lemma is_affine_of_iso {X Y : Scheme} (f : X ⟶ Y) [is_iso f] [h : is_affine Y] :
+  is_affine X :=
+by { rw [← mem_AffineScheme] at h ⊢, exact functor.ess_image.of_iso (as_iso f).symm h }
+
+namespace AffineScheme
+
+/-- The `Spec` functor into the category of affine schemes. -/
+@[derive [full, faithful, ess_surj], simps]
+def Spec : CommRingᵒᵖ ⥤ AffineScheme := Scheme.Spec.to_ess_image
+
+/-- The forgetful functor `AffineScheme ⥤ Scheme`. -/
+@[derive [full, faithful], simps]
+def forget_to_Scheme : AffineScheme ⥤ Scheme := Scheme.Spec.ess_image_inclusion
+
+/-- The global section functor of an affine scheme. -/
+def Γ : AffineSchemeᵒᵖ ⥤ CommRing := forget_to_Scheme.op ⋙ Scheme.Γ
+
+/-- The category of affine schemes is equivalent to the category of commutative rings. -/
+def equiv_CommRing : AffineScheme ≌ CommRingᵒᵖ :=
+equiv_ess_image_of_reflective.symm
+
+instance Γ_is_equiv : is_equivalence Γ.{u} :=
+begin
+  haveI : is_equivalence Γ.{u}.right_op.op := is_equivalence.of_equivalence equiv_CommRing.op,
+  exact (functor.is_equivalence_trans Γ.{u}.right_op.op (op_op_equivalence _).functor : _),
+end
+
+instance : has_colimits AffineScheme.{u} :=
+begin
+  haveI := adjunction.has_limits_of_equivalence.{u} Γ.{u},
+  haveI : has_colimits AffineScheme.{u} ᵒᵖᵒᵖ := has_colimits_op_of_has_limits,
+  exactI adjunction.has_colimits_of_equivalence.{u} (op_op_equivalence AffineScheme.{u}).inverse
+end
+
+instance : has_limits AffineScheme.{u} :=
+begin
+  haveI := adjunction.has_colimits_of_equivalence Γ.{u},
+  haveI : has_limits AffineScheme.{u} ᵒᵖᵒᵖ := limits.has_limits_op_of_has_colimits,
+  exactI adjunction.has_limits_of_equivalence (op_op_equivalence AffineScheme.{u}).inverse
+end
+
+end AffineScheme
+
+/-- An open subset of a scheme is affine if the open subscheme is affine. -/
+def is_affine_open {X : Scheme} (U : opens X.carrier) : Prop :=
+is_affine (X.restrict U.open_embedding)
+
+lemma range_is_affine_open_of_open_immersion {X Y : Scheme} [is_affine X] (f : X ⟶ Y)
+  [H : is_open_immersion f] : is_affine_open ⟨set.range f.1.base, H.base_open.open_range⟩ :=
+begin
+  refine is_affine_of_iso (is_open_immersion.iso_of_range_eq f (Y.of_restrict _) _).inv,
+  exact subtype.range_coe.symm,
+  apply_instance
+end
+
+lemma top_is_affine_open (X : Scheme) [is_affine X] : is_affine_open (⊤ : opens X.carrier) :=
+begin
+  convert range_is_affine_open_of_open_immersion (𝟙 X),
+  ext1,
+  exact set.range_id.symm
+end
+
+instance Scheme.affine_basis_cover_is_affine (X : Scheme) (i : X.affine_basis_cover.J) :
+  is_affine (X.affine_basis_cover.obj i) :=
+algebraic_geometry.Spec_is_affine _
+
+lemma is_basis_affine_open (X : Scheme) :
+  opens.is_basis { U : opens X.carrier | is_affine_open U } :=
+begin
+  rw opens.is_basis_iff_nbhd,
+  rintros U x (hU : x ∈ (U : set X.carrier)),
+  obtain ⟨S, hS, hxS, hSU⟩ := X.affine_basis_cover_is_basis.exists_subset_of_mem_open hU U.prop,
+  refine ⟨⟨S, X.affine_basis_cover_is_basis.is_open hS⟩, _, hxS, hSU⟩,
+  rcases hS with ⟨i, rfl⟩,
+  exact range_is_affine_open_of_open_immersion _,
+end
+
+end algebraic_geometry

src/algebraic_geometry/Gamma_Spec_adjunction.lean

@@ -5,7 +5,7 @@ Authors: Junyan Xu
 -/
 import algebraic_geometry.Scheme
 import category_theory.adjunction.limits
-import category_theory.adjunction.fully_faithful
+import category_theory.adjunction.reflective
 
 /-!
 # Adjunction between `Γ` and `Spec`
@@ -362,4 +362,10 @@ R_faithful_of_counit_is_iso Γ_Spec.LocallyRingedSpace_adjunction
 instance Spec.faithful : faithful Scheme.Spec :=
 R_faithful_of_counit_is_iso Γ_Spec.adjunction
 
+instance : is_right_adjoint Spec.to_LocallyRingedSpace := ⟨_, Γ_Spec.LocallyRingedSpace_adjunction⟩
+instance : is_right_adjoint Scheme.Spec := ⟨_, Γ_Spec.adjunction⟩
+
+instance : reflective Spec.to_LocallyRingedSpace := ⟨⟩
+instance Spec.reflective : reflective Scheme.Spec := ⟨⟩
+
 end algebraic_geometry

src/algebraic_geometry/open_immersion.lean

@@ -1297,6 +1297,23 @@ end to_Scheme
 
 end PresheafedSpace.is_open_immersion
 
+/-- The restriction of a Scheme along an open embedding. -/
+@[simps]
+def Scheme.restrict {U : Top} (X : Scheme) {f : U ⟶ Top.of X.carrier} (h : open_embedding f) :
+  Scheme :=
+{ to_PresheafedSpace := X.to_PresheafedSpace.restrict h,
+  ..(PresheafedSpace.is_open_immersion.to_Scheme X (X.to_PresheafedSpace.of_restrict h)) }
+
+/-- The canonical map from the restriction to the supspace. -/
+@[simps]
+def Scheme.of_restrict {U : Top} (X : Scheme) {f : U ⟶ Top.of X.carrier} (h : open_embedding f) :
+  X.restrict h ⟶ X :=
+X.to_LocallyRingedSpace.of_restrict h
+
+instance is_open_immersion.of_restrict {U : Top} (X : Scheme) {f : U ⟶ Top.of X.carrier}
+  (h : open_embedding f) : is_open_immersion (X.of_restrict h) :=
+show PresheafedSpace.is_open_immersion (X.to_PresheafedSpace.of_restrict h), by apply_instance
+
 namespace is_open_immersion
 
 variables {X Y Z : Scheme.{u}} (f : X ⟶ Z) (g : Y ⟶ Z)
@@ -1307,6 +1324,10 @@ instance of_is_iso [is_iso g] :
   is_open_immersion g := @@LocallyRingedSpace.is_open_immersion.of_is_iso _
 (show is_iso ((induced_functor _).map g), by apply_instance)
 
+/-- A open immersion induces an isomorphism from the domain onto the image -/
+def iso_restrict : X ≅ (Z.restrict H.base_open : _) :=
+⟨H.iso_restrict.hom, H.iso_restrict.inv, H.iso_restrict.hom_inv_id, H.iso_restrict.inv_hom_id⟩
+
 include H
 
 local notation `forget` := Scheme.forget_to_LocallyRingedSpace
@@ -1405,6 +1426,31 @@ end
 instance forget_to_Top_preserves_of_right :
   preserves_limit (cospan g f) Scheme.forget_to_Top := preserves_pullback_symmetry _ _ _
 
+/--
+The universal property of open immersions:
+For an open immersion `f : X ⟶ Z`, given any morphism of schemes `g : Y ⟶ Z` whose topological
+image is contained in the image of `f`, we can lift this morphism to a unique `Y ⟶ X` that
+commutes with these maps.
+-/
+def lift (H' : set.range g.1.base ⊆ set.range f.1.base) : Y ⟶ X :=
+LocallyRingedSpace.is_open_immersion.lift f g H'
+
+@[simp, reassoc] lemma lift_fac (H' : set.range g.1.base ⊆ set.range f.1.base) :
+  lift f g H' ≫ f = g :=
+LocallyRingedSpace.is_open_immersion.lift_fac f g H'
+
+lemma lift_uniq (H' : set.range g.1.base ⊆ set.range f.1.base) (l : Y ⟶ X)
+  (hl : l ≫ f = g) : l = lift f g H' :=
+LocallyRingedSpace.is_open_immersion.lift_uniq f g H' l hl
+
+/-- Two open immersions with equal range is isomorphic. -/
+@[simps] def iso_of_range_eq [is_open_immersion g] (e : set.range f.1.base = set.range g.1.base) :
+  X ≅ Y :=
+{ hom := lift g f (le_of_eq e),
+  inv := lift f g (le_of_eq e.symm),
+  hom_inv_id' := by { rw ← cancel_mono f, simp },
+  inv_hom_id' := by { rw ← cancel_mono g, simp } }
+
 end is_open_immersion
 
 end algebraic_geometry

src/category_theory/adjunction/reflective.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
 import category_theory.adjunction.fully_faithful
+import category_theory.reflects_isomorphisms
 import category_theory.epi_mono
 
 /-!
@@ -152,4 +153,20 @@ lemma unit_comp_partial_bijective_natural [reflective i] (A : C) {B B' : C} (h :
   (unit_comp_partial_bijective A hB') (f ≫ h) = unit_comp_partial_bijective A hB f ≫ h :=
 by rw [←equiv.eq_symm_apply, unit_comp_partial_bijective_symm_natural A h, equiv.symm_apply_apply]
 
+/-- If `i : D ⥤ C` is reflective, the inverse functor of `i ≌ F.ess_image` can be explicitly
+defined by the reflector. -/
+@[simps]
+def equiv_ess_image_of_reflective [reflective i] : D ≌ i.ess_image :=
+{ functor := i.to_ess_image,
+  inverse := i.ess_image_inclusion ⋙ (left_adjoint i : _),
+  unit_iso := nat_iso.of_components (λ X, (as_iso $ (of_right_adjoint i).counit.app X).symm)
+    (by { intros X Y f, dsimp, simp only [is_iso.eq_inv_comp, is_iso.comp_inv_eq, category.assoc],
+      exact ((of_right_adjoint i).counit.naturality _).symm }),
+  counit_iso := nat_iso.of_components
+    (λ X, by { refine (iso.symm $ as_iso _), exact (of_right_adjoint i).unit.app X,
+      apply_with (is_iso_of_reflects_iso _ i.ess_image_inclusion) { instances := ff },
+      exact functor.ess_image.unit_is_iso X.prop })
+    (by { intros X Y f, dsimp, simp only [is_iso.eq_inv_comp, is_iso.comp_inv_eq, category.assoc],
+      exact ((of_right_adjoint i).unit.naturality f).symm }) }
+
 end category_theory