feat(algebraic_geometry): LocallyRingedSpace has coproducts. (#10665)

Author: erdOne

src/algebraic_geometry/locally_ringed_space/has_colimits.lean

@@ -0,0 +1,111 @@
+/-
+Copyright (c) 2021 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import algebraic_geometry.locally_ringed_space
+import algebra.category.CommRing.constructions
+import algebraic_geometry.open_immersion
+import category_theory.limits.constructions.limits_of_products_and_equalizers
+
+/-!
+# Colimits of LocallyRingedSpace
+
+We construct the explict coproducts of `LocallyRingedSpace`.
+
+## TODO
+
+Construct the explict coequalizers of `LocallyRingedSpace`.
+It then follows that `LocallyRingedSpace` has all colimits, and
+`forget_to_SheafedSpace` preserves them.
+
+-/
+
+namespace algebraic_geometry
+
+universes v u
+
+open category_theory category_theory.limits opposite
+
+namespace SheafedSpace
+
+variables {C : Type u} [category.{v} C] [has_limits C]
+variables {J : Type v} [category.{v} J] (F : J ⥤ SheafedSpace C)
+
+lemma is_colimit_exists_rep {c : cocone F} (hc : is_colimit c) (x : c.X) :
+  ∃ (i : J) (y : F.obj i), (c.ι.app i).base y = x :=
+concrete.is_colimit_exists_rep (F ⋙ SheafedSpace.forget _)
+  (is_colimit_of_preserves (SheafedSpace.forget _) hc) x
+
+lemma colimit_exists_rep (x : colimit F) :
+  ∃ (i : J) (y : F.obj i), (colimit.ι F i).base y = x :=
+concrete.is_colimit_exists_rep (F ⋙ SheafedSpace.forget _)
+  (is_colimit_of_preserves (SheafedSpace.forget _) (colimit.is_colimit F)) x
+
+instance {X Y : SheafedSpace C} (f g : X ⟶ Y) : epi (coequalizer.π f g).base :=
+begin
+  erw ← (show _ = (coequalizer.π f g).base, from
+    ι_comp_coequalizer_comparison f g (SheafedSpace.forget C)),
+  rw ← preserves_coequalizer.iso_hom,
+  apply epi_comp
+end
+
+end SheafedSpace
+
+namespace LocallyRingedSpace
+
+section has_coproducts
+
+variables {ι : Type u} (F : discrete ι ⥤ LocallyRingedSpace.{u})
+
+/-- The explicit coproduct for `F : discrete ι ⥤ LocallyRingedSpace`. -/
+noncomputable
+def coproduct : LocallyRingedSpace :=
+{ to_SheafedSpace := colimit (F ⋙ forget_to_SheafedSpace : _),
+  local_ring := λ x, begin
+    obtain ⟨i, y, ⟨⟩⟩ := SheafedSpace.colimit_exists_rep (F ⋙ forget_to_SheafedSpace) x,
+    haveI : _root_.local_ring (((F ⋙ forget_to_SheafedSpace).obj i).to_PresheafedSpace.stalk y) :=
+      (F.obj i).local_ring _,
+    exact (as_iso (PresheafedSpace.stalk_map (colimit.ι (F ⋙ forget_to_SheafedSpace) i : _) y)
+      ).symm.CommRing_iso_to_ring_equiv.local_ring
+  end }
+
+/-- The explicit coproduct cofan for `F : discrete ι ⥤ LocallyRingedSpace`. -/
+noncomputable
+def coproduct_cofan : cocone F :=
+{ X := coproduct F,
+  ι := { app := λ j, ⟨colimit.ι (F ⋙ forget_to_SheafedSpace) j, infer_instance⟩ } }
+
+/-- The explicit coproduct cofan constructed in `coproduct_cofan` is indeed a colimit. -/
+noncomputable
+def coproduct_cofan_is_colimit : is_colimit (coproduct_cofan F) :=
+{ desc := λ s, ⟨colimit.desc (F ⋙ forget_to_SheafedSpace) (forget_to_SheafedSpace.map_cocone s),
+  begin
+    intro x,
+    obtain ⟨i, y, ⟨⟩⟩ := SheafedSpace.colimit_exists_rep (F ⋙ forget_to_SheafedSpace) x,
+    have := PresheafedSpace.stalk_map.comp (colimit.ι (F ⋙ forget_to_SheafedSpace) i : _)
+      (colimit.desc (F ⋙ forget_to_SheafedSpace) (forget_to_SheafedSpace.map_cocone s)) y,
+    rw ← is_iso.comp_inv_eq at this,
+    erw [← this, PresheafedSpace.stalk_map.congr_hom _ _
+      (colimit.ι_desc (forget_to_SheafedSpace.map_cocone s) i : _)],
+    haveI : is_local_ring_hom (PresheafedSpace.stalk_map
+      ((forget_to_SheafedSpace.map_cocone s).ι.app i) y) := (s.ι.app i).2 y,
+    apply_instance
+  end⟩,
+  fac' := λ s j, subtype.eq (colimit.ι_desc _ _),
+  uniq' := λ s f h, subtype.eq (is_colimit.uniq _ (forget_to_SheafedSpace.map_cocone s) f.1
+    (λ j, congr_arg subtype.val (h j))) }
+
+instance : has_coproducts LocallyRingedSpace.{u} :=
+λ ι, ⟨λ F, ⟨⟨⟨_, coproduct_cofan_is_colimit F⟩⟩⟩⟩
+
+noncomputable
+instance (J : Type*) : preserves_colimits_of_shape (discrete J) forget_to_SheafedSpace :=
+⟨λ G, preserves_colimit_of_preserves_colimit_cocone (coproduct_cofan_is_colimit G)
+  ((colimit.is_colimit _).of_iso_colimit (cocones.ext (iso.refl _) (λ j, category.comp_id _)))⟩
+
+end has_coproducts
+
+end LocallyRingedSpace
+
+end algebraic_geometry

src/algebraic_geometry/open_immersion.lean

@@ -8,6 +8,7 @@ import category_theory.limits.shapes.binary_products
 import category_theory.limits.preserves.shapes.pullbacks
 import topology.sheaves.functors
 import algebraic_geometry.Scheme
+import category_theory.limits.shapes.strict_initial
 
 /-!
 # Open immersions of structured spaces
@@ -519,4 +520,80 @@ end pullback
 
 end PresheafedSpace.is_open_immersion
 
+namespace SheafedSpace.is_open_immersion
+
+section prod
+
+variables [has_limits C] {ι : Type v} (F : discrete ι ⥤ SheafedSpace C) [has_colimit F] (i : ι)
+
+lemma sigma_ι_open_embedding : open_embedding (colimit.ι F i).base :=
+begin
+  rw ← (show _ = (colimit.ι F i).base,
+    from ι_preserves_colimits_iso_inv (SheafedSpace.forget C) F i),
+  have : _ = _ ≫ colimit.ι (discrete.functor (F ⋙ SheafedSpace.forget C).obj) i :=
+    has_colimit.iso_of_nat_iso_ι_hom discrete.nat_iso_functor i,
+  rw ← iso.eq_comp_inv at this,
+  rw this,
+  have : colimit.ι _ _ ≫ _ = _ := Top.sigma_iso_sigma_hom_ι (F ⋙ SheafedSpace.forget C).obj i,
+  rw ← iso.eq_comp_inv at this,
+  rw this,
+  simp_rw [← category.assoc, Top.open_embedding_iff_comp_is_iso,
+    Top.open_embedding_iff_is_iso_comp],
+  exact open_embedding_sigma_mk
+end
+
+lemma image_preimage_is_empty (j : ι) (h : i ≠ j) (U : opens (F.obj i)) :
+  (opens.map (colimit.ι (F ⋙ SheafedSpace.forget_to_PresheafedSpace) j).base).obj
+    ((opens.map (preserves_colimit_iso SheafedSpace.forget_to_PresheafedSpace F).inv.base).obj
+    ((sigma_ι_open_embedding F i).is_open_map.functor.obj U)) = ∅ :=
+begin
+  ext,
+  apply iff_false_intro,
+  rintro ⟨y, hy, eq⟩,
+  replace eq := concrete_category.congr_arg
+    (preserves_colimit_iso (SheafedSpace.forget C) F ≪≫
+      has_colimit.iso_of_nat_iso discrete.nat_iso_functor ≪≫ Top.sigma_iso_sigma _).hom eq,
+  simp_rw [category_theory.iso.trans_hom, ← Top.comp_app, ← PresheafedSpace.comp_base] at eq,
+  rw ι_preserves_colimits_iso_inv at eq,
+  change ((SheafedSpace.forget C).map (colimit.ι F i) ≫ _) y =
+    ((SheafedSpace.forget C).map (colimit.ι F j) ≫ _) x at eq,
+  rw [ι_preserves_colimits_iso_hom_assoc, ι_preserves_colimits_iso_hom_assoc,
+    has_colimit.iso_of_nat_iso_ι_hom_assoc, has_colimit.iso_of_nat_iso_ι_hom_assoc,
+    Top.sigma_iso_sigma_hom_ι, Top.sigma_iso_sigma_hom_ι] at eq,
+  exact h (congr_arg sigma.fst eq)
+end
+
+instance sigma_ι_is_open_immersion [has_strict_terminal_objects C] :
+  SheafedSpace.is_open_immersion (colimit.ι F i) :=
+{ base_open := sigma_ι_open_embedding F i,
+  c_iso := λ U, begin
+    have e : colimit.ι F i = _ :=
+      (ι_preserves_colimits_iso_inv SheafedSpace.forget_to_PresheafedSpace F i).symm,
+    have H : open_embedding (colimit.ι (F ⋙ SheafedSpace.forget_to_PresheafedSpace) i ≫
+      (preserves_colimit_iso SheafedSpace.forget_to_PresheafedSpace F).inv).base :=
+      e ▸ sigma_ι_open_embedding F i,
+    suffices : is_iso ((colimit.ι (F ⋙ SheafedSpace.forget_to_PresheafedSpace) i ≫
+      (preserves_colimit_iso SheafedSpace.forget_to_PresheafedSpace F).inv).c.app
+        (op (H.is_open_map.functor.obj U))),
+    { convert this },
+    rw [PresheafedSpace.comp_c_app,
+      ← PresheafedSpace.colimit_presheaf_obj_iso_componentwise_limit_hom_π],
+    suffices : is_iso (limit.π (PresheafedSpace.componentwise_diagram
+      (F ⋙ SheafedSpace.forget_to_PresheafedSpace)
+      ((opens.map (preserves_colimit_iso SheafedSpace.forget_to_PresheafedSpace F).inv.base).obj
+      (unop $ op $ H.is_open_map.functor.obj U))) (op i)),
+    { resetI, apply_instance },
+    apply limit_π_is_iso_of_is_strict_terminal,
+    intros j hj,
+    induction j using opposite.rec,
+    dsimp,
+    convert (F.obj j).sheaf.is_terminal_of_empty,
+    convert image_preimage_is_empty F i j (λ h, hj (congr_arg op h.symm)) U,
+    exact (congr_arg PresheafedSpace.hom.base e).symm
+  end }
+
+end prod
+
+end SheafedSpace.is_open_immersion
+
 end algebraic_geometry

src/algebraic_geometry/sheafed_space.lean

@@ -149,6 +149,10 @@ instance [has_limits C] : creates_colimits (forget_to_PresheafedSpace : SheafedS
 instance [has_limits C] : has_colimits (SheafedSpace C) :=
 has_colimits_of_has_colimits_creates_colimits forget_to_PresheafedSpace
 
+noncomputable
+ instance [has_limits C] : preserves_colimits (forget C) :=
+ limits.comp_preserves_colimits forget_to_PresheafedSpace (PresheafedSpace.forget C)
+
 end SheafedSpace
 
 end algebraic_geometry

src/topology/category/Top/basic.lean

@@ -79,4 +79,20 @@ by { ext, refl }
 @[simp] lemma of_homeo_of_iso {X Y : Top.{u}} (f : X ≅ Y) : iso_of_homeo (homeo_of_iso f) = f :=
 by { ext, refl }
 
+@[simp]
+lemma open_embedding_iff_comp_is_iso {X Y Z : Top} (f : X ⟶ Y) (g : Y ⟶ Z) [is_iso g] :
+  open_embedding (f ≫ g) ↔ open_embedding f :=
+open_embedding_iff_open_embedding_compose f (Top.homeo_of_iso (as_iso g)).open_embedding
+
+@[simp]
+lemma open_embedding_iff_is_iso_comp {X Y Z : Top} (f : X ⟶ Y) (g : Y ⟶ Z) [is_iso f] :
+  open_embedding (f ≫ g) ↔ open_embedding g :=
+begin
+  split,
+  { intro h,
+    convert h.comp (Top.homeo_of_iso (as_iso f).symm).open_embedding,
+    exact congr_arg _ (is_iso.inv_hom_id_assoc f g).symm },
+  { exact λ h, h.comp (Top.homeo_of_iso (as_iso f)).open_embedding }
+end
+
 end Top

src/topology/maps.lean

@@ -423,6 +423,22 @@ lemma open_embedding.comp {g : β → γ} {f : α → β}
   (hg : open_embedding g) (hf : open_embedding f) : open_embedding (g ∘ f) :=
 ⟨hg.1.comp hf.1, (hg.is_open_map.comp hf.is_open_map).is_open_range⟩
 
+lemma open_embedding_of_open_embedding_compose {α β γ : Type*} [topological_space α]
+  [topological_space β] [topological_space γ] (f : α → β) {g : β → γ} (hg : open_embedding g)
+    (h : open_embedding (g ∘ f)) : open_embedding f :=
+begin
+  have hf := hg.to_embedding.continuous_iff.mpr h.continuous,
+  split,
+  { exact embedding_of_embedding_compose hf hg.continuous h.to_embedding },
+  { rw [hg.open_iff_image_open, ← set.image_univ, ← set.image_comp, ← h.open_iff_image_open],
+    exact is_open_univ }
+end
+
+lemma open_embedding_iff_open_embedding_compose {α β γ : Type*} [topological_space α]
+  [topological_space β] [topological_space γ] (f : α → β) {g : β → γ} (hg : open_embedding g) :
+    open_embedding (g ∘ f) ↔ open_embedding f :=
+⟨open_embedding_of_open_embedding_compose f hg, hg.comp⟩
+
 end open_embedding
 
 section closed_embedding