feat(algebraic_geometry): Define open_covers of Schemes. (#10931)

Co-authored-by: Johan Commelin <johan@commelin.net>

src/algebra/category/CommRing/instances.lean

@@ -0,0 +1,21 @@
+/-
+Copyright (c) 2021 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import algebra.category.CommRing.basic
+import ring_theory.localization
+
+/-!
+# Ring-theoretic results in terms of categorical languages
+-/
+
+open category_theory
+
+instance localization_unit_is_iso (R : CommRing) :
+  is_iso (CommRing.of_hom $ algebra_map R (localization.away (1 : R))) :=
+is_iso.of_iso (is_localization.at_one R (localization.away (1 : R))).to_ring_equiv.to_CommRing_iso
+
+instance localization_unit_is_iso' (R : CommRing) :
+  @is_iso CommRing _ R _ (CommRing.of_hom $ algebra_map R (localization.away (1 : R))) :=
+by { cases R, exact localization_unit_is_iso _ }

src/algebraic_geometry/Scheme.lean

@@ -54,6 +54,16 @@ induced_category.category Scheme.to_LocallyRingedSpace
 /-- The structure sheaf of a Scheme. -/
 protected abbreviation sheaf (X : Scheme) := X.to_SheafedSpace.sheaf
 
+/-- The forgetful functor from `Scheme` to `LocallyRingedSpace`. -/
+@[simps, derive[full, faithful]]
+def forget_to_LocallyRingedSpace : Scheme ⥤ LocallyRingedSpace :=
+  induced_functor _
+
+/-- The forgetful functor from `Scheme` to `Top`. -/
+@[simps]
+def forget_to_Top : Scheme ⥤ Top :=
+  Scheme.forget_to_LocallyRingedSpace ⋙ LocallyRingedSpace.forget_to_Top
+
 /--
 The spectrum of a commutative ring, as a scheme.
 -/

src/algebraic_geometry/locally_ringed_space.lean

@@ -121,12 +121,17 @@ instance : category LocallyRingedSpace :=
   assoc' := by { intros, ext1, simp, }, }.
 
 /-- The forgetful functor from `LocallyRingedSpace` to `SheafedSpace CommRing`. -/
-def forget_to_SheafedSpace : LocallyRingedSpace ⥤ SheafedSpace CommRing :=
+@[simps] def forget_to_SheafedSpace : LocallyRingedSpace ⥤ SheafedSpace CommRing :=
 { obj := λ X, X.to_SheafedSpace,
   map := λ X Y f, f.1, }
 
 instance : faithful forget_to_SheafedSpace := {}
 
+/-- The forgetful functor from `LocallyRingedSpace` to `Top`. -/
+@[simps]
+def forget_to_Top : LocallyRingedSpace ⥤ Top :=
+forget_to_SheafedSpace ⋙ SheafedSpace.forget _
+
 @[simp] lemma comp_val {X Y Z : LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z) :
   (f ≫ g).val = f.val ≫ g.val := rfl
 

src/algebraic_geometry/open_immersion.lean

@@ -9,6 +9,7 @@ import category_theory.limits.preserves.shapes.pullbacks
 import topology.sheaves.functors
 import algebraic_geometry.Scheme
 import category_theory.limits.shapes.strict_initial
+import algebra.category.CommRing.instances
 
 /-!
 # Open immersions of structured spaces
@@ -974,7 +975,7 @@ begin
   apply_with limits.comp_preserves_limit { instances := ff },
   apply_instance,
   apply preserves_limit_of_iso_diagram _ (diagram_iso_cospan.{u} _).symm,
-  dsimp,
+  dsimp [SheafedSpace.forget_to_PresheafedSpace, -subtype.val_eq_coe],
   apply_instance,
 end
 
@@ -1062,4 +1063,148 @@ end pullback
 
 end LocallyRingedSpace.is_open_immersion
 
+lemma is_open_immersion.open_range {X Y : Scheme} (f : X ⟶ Y) [H : is_open_immersion f] :
+  is_open (set.range f.1.base) := H.base_open.open_range
+
+section open_cover
+
+namespace Scheme
+
+/-- An open cover of `X` consists of a family of open immersions into `X`,
+and for each `x : X` an open immersion (indexed by `f x`) that covers `x`.
+
+This is merely a coverage in the Zariski pretopology, and it would be optimal
+if we could reuse the existing API about pretopologies, However, the definitions of sieves and
+grothendieck topologies uses `Prop`s, so that the actual open sets and immersions are hard to
+obtain. Also, since such a coverage in the pretopology usually contains a proper class of
+immersions, it is quite hard to glue them, reason about finite covers, etc.
+-/
+-- TODO: provide API to and from a presieve.
+structure open_cover (X : Scheme.{u}) :=
+(J : Type v)
+(obj : Π (j : J), Scheme)
+(map : Π (j : J), obj j ⟶ X)
+(f : X.carrier → J)
+(covers : ∀ x, x ∈ set.range ((map (f x)).1.base))
+(is_open : ∀ x, is_open_immersion (map x) . tactic.apply_instance)
+
+attribute [instance] open_cover.is_open
+
+variables {X Y Z : Scheme.{u}} (𝒰 : open_cover X) (f : X ⟶ Z) (g : Y ⟶ Z)
+variables [∀ x, has_pullback (𝒰.map x ≫ f) g]
+
+/-- The affine cover of a scheme. -/
+def affine_cover (X : Scheme) : open_cover X :=
+{ J := X.carrier,
+  obj := λ x, Spec.obj $ opposite.op (X.local_affine x).some_spec.some,
+  map := λ x, ((X.local_affine x).some_spec.some_spec.some.inv ≫
+    X.to_LocallyRingedSpace.of_restrict _ : _),
+  f := λ x, x,
+  is_open := λ x, begin
+    apply_with PresheafedSpace.is_open_immersion.comp { instances := ff },
+    apply_instance,
+    apply PresheafedSpace.is_open_immersion.of_restrict,
+  end,
+  covers :=
+  begin
+    intro x,
+    erw coe_comp,
+    rw [set.range_comp, set.range_iff_surjective.mpr, set.image_univ],
+    erw subtype.range_coe_subtype,
+    exact (X.local_affine x).some.2,
+    rw ← Top.epi_iff_surjective,
+    change epi ((SheafedSpace.forget _).map (LocallyRingedSpace.forget_to_SheafedSpace.map _)),
+    apply_instance
+  end }
+
+instance : inhabited X.open_cover := ⟨X.affine_cover⟩
+
+/-- Given an open cover `{ Uᵢ }` of `X`, and for each `Uᵢ` an open cover, we may combine these
+open covers to form an open cover of `X`.  -/
+def open_cover.bind (f : Π (x : 𝒰.J), open_cover (𝒰.obj x)) : open_cover X :=
+{ J := Σ (i : 𝒰.J), (f i).J,
+  obj := λ x, (f x.1).obj x.2,
+  map := λ x, (f x.1).map x.2 ≫ 𝒰.map x.1,
+  f := λ x, ⟨_, (f _).f (𝒰.covers x).some⟩,
+  covers := λ x,
+  begin
+    let y := (𝒰.covers x).some,
+    have hy : (𝒰.map (𝒰.f x)).val.base y = x := (𝒰.covers x).some_spec,
+    rcases (f (𝒰.f x)).covers y with ⟨z, hz⟩,
+    change x ∈ set.range (((f (𝒰.f x)).map ((f (𝒰.f x)).f y) ≫ 𝒰.map (𝒰.f x)).1.base),
+    use z,
+    erw comp_apply,
+    rw [hz, hy],
+  end }
+
+local attribute [reducible] CommRing.of CommRing.of_hom
+
+instance val_base_is_iso {X Y : Scheme} (f : X ⟶ Y) [is_iso f] : is_iso f.1.base :=
+Scheme.forget_to_Top.map_is_iso f
+
+instance basic_open_is_open_immersion {R : CommRing} (f : R) :
+algebraic_geometry.is_open_immersion (Scheme.Spec.map (CommRing.of_hom
+  (algebra_map R (localization.away f))).op) :=
+begin
+  apply_with SheafedSpace.is_open_immersion.of_stalk_iso { instances := ff },
+  any_goals { apply_instance },
+  any_goals { apply_instance },
+  exact (prime_spectrum.localization_away_open_embedding (localization.away f) f : _),
+  intro x,
+  exact Spec_map_localization_is_iso R (submonoid.powers f) x,
+end
+
+/-- The basic open sets form an affine open cover of `Spec R`. -/
+def affine_basis_cover_of_affine (R : CommRing) : open_cover (Spec.obj (opposite.op R)) :=
+{ J := R,
+  obj := λ r, Spec.obj (opposite.op $ CommRing.of $ localization.away r),
+  map := λ r, Spec.map (quiver.hom.op (algebra_map R (localization.away r) : _)),
+  f := λ x, 1,
+  covers := λ r,
+  begin
+    rw set.range_iff_surjective.mpr ((Top.epi_iff_surjective _).mp _),
+    { exact trivial },
+    { apply_instance }
+  end,
+  is_open := λ x, algebraic_geometry.Scheme.basic_open_is_open_immersion x }
+
+/-- We may bind the basic open sets of an open affine cover to form a affine cover that is also
+a basis. -/
+def affine_basis_cover (X : Scheme) : open_cover X :=
+X.affine_cover.bind (λ x, affine_basis_cover_of_affine _)
+
+lemma affine_basis_cover_map_range (X : Scheme)
+  (x : X.carrier) (r : (X.local_affine x).some_spec.some) :
+  set.range (X.affine_basis_cover.map ⟨x, r⟩).1.base =
+    (X.affine_cover.map x).1.base '' (prime_spectrum.basic_open r).1 :=
+begin
+  erw [coe_comp, set.range_comp],
+  congr,
+  exact (prime_spectrum.localization_away_comap_range (localization.away r) r : _)
+end
+
+lemma affine_basis_cover_is_basis (X : Scheme) :
+  topological_space.is_topological_basis
+    { x : set X.carrier | ∃ a : X.affine_basis_cover.J, x =
+      set.range ((X.affine_basis_cover.map a).1.base) } :=
+begin
+  apply topological_space.is_topological_basis_of_open_of_nhds,
+  { rintros _ ⟨a, rfl⟩,
+    exact is_open_immersion.open_range (X.affine_basis_cover.map a) },
+  { rintros a U haU hU,
+    rcases X.affine_cover.covers a with ⟨x, e⟩,
+    let U' := (X.affine_cover.map (X.affine_cover.f a)).1.base ⁻¹' U,
+    have hxU' : x ∈ U' := by { rw ← e at haU, exact haU },
+    rcases prime_spectrum.is_basis_basic_opens.exists_subset_of_mem_open hxU'
+      ((X.affine_cover.map (X.affine_cover.f a)).1.base.continuous_to_fun.is_open_preimage _ hU)
+      with ⟨_,⟨_,⟨s,rfl⟩,rfl⟩,hxV,hVU⟩,
+    refine ⟨_,⟨⟨_,s⟩,rfl⟩,_,_⟩; erw affine_basis_cover_map_range,
+    { exact ⟨x,hxV,e⟩ },
+    { rw set.image_subset_iff, exact hVU } }
+end
+
+end Scheme
+
+end open_cover
+
 end algebraic_geometry