feat(category_theory/extensive): Define extensive categories (#17318)

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Author: erdOne

docs/references.bib

@@ -404,6 +404,21 @@ @Book{            calugareanu
   doi           = {10.1007/978-94-015-9588-9}
 }
 
+@Article{         CARBONI1993145,
+  author        = {Aurelio Carboni and Stephen Lack and R.F.C. Walters},
+  doi           = {https://doi.org/10.1016/0022-4049(93)90035-R},
+  issn          = {0022-4049},
+  journal       = {Journal of Pure and Applied Algebra},
+  number        = {2},
+  pages         = {145-158},
+  title         = {Introduction to extensive and distributive categories},
+  url           = {https://www.sciencedirect.com/science/article/pii/002240499390035R},
+  volume        = {84},
+  year          = {1993},
+  bdsk-url-1    = {https://www.sciencedirect.com/science/article/pii/002240499390035R},
+  bdsk-url-2    = {https://doi.org/10.1016/0022-4049(93)90035-R}
+}
+
 @Article{         carneiro2015arithmetic,
   title         = {Arithmetic in Metamath, Case Study: Bertrand's Postulate},
   author        = {Carneiro, Mario},

src/category_theory/extensive.lean

@@ -0,0 +1,338 @@
+/-
+Copyright (c) 2022 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import category_theory.limits.shapes.comm_sq
+import category_theory.limits.shapes.strict_initial
+import category_theory.limits.shapes.types
+import topology.category.Top.limits
+
+/-!
+
+# Extensive categories
+
+## Main definitions
+- `category_theory.is_van_kampen_colimit`: A (colimit) cocone over a diagram `F : J ⥤ C` is van
+  Kampen if for every cocone `c'` over the pullback of the diagram `F' : J ⥤ C'`,
+  `c'` is colimiting iff `c'` is the pullback of `c`.
+- `category_theory.finitary_extensive`: A category is (finitary) extensive if it has finite
+  coproducts, and binary coproducts are van Kampen.
+
+## Main Results
+- `category_theory.has_strict_initial_objects_of_finitary_extensive`: The initial object
+  in extensive categories is strict.
+- `category_theory.finitary_extensive.mono_inr_of_is_colimit`: Coproduct injections are monic in
+  extensive categories.
+- `category_theory.binary_cofan.is_pullback_initial_to_of_is_van_kampen`: In extensive categories,
+  sums are disjoint, i.e. the pullback of `X ⟶ X ⨿ Y` and `Y ⟶ X ⨿ Y` is the initial object.
+- `category_theory.types.finitary_extensive`: The category of types is extensive.
+
+## TODO
+
+Show that the following are finitary extensive:
+- `Top`
+- functor categories into extensive categories
+- the categories of sheaves over a site
+- `Scheme`
+- `AffineScheme` (`CommRingᵒᵖ`)
+
+## References
+- https://ncatlab.org/nlab/show/extensive+category
+- [Carboni et al, Introduction to extensive and distributive categories][CARBONI1993145]
+
+-/
+
+open category_theory.limits
+
+namespace category_theory
+
+universes v' u' v u
+
+variables {J : Type v'} [category.{u'} J] {C : Type u} [category.{v} C]
+
+/-- A natural transformation is equifibered if every commutative square of the following form is
+a pullback.
+```
+F(X) → F(Y)
+ ↓      ↓
+G(X) → G(Y)
+```
+-/
+def nat_trans.equifibered {F G : J ⥤ C} (α : F ⟶ G) : Prop :=
+∀ ⦃i j : J⦄ (f : i ⟶ j), is_pullback (F.map f) (α.app i) (α.app j) (G.map f)
+
+lemma nat_trans.equifibered_of_is_iso {F G : J ⥤ C} (α : F ⟶ G) [is_iso α] : α.equifibered :=
+λ _ _ f, is_pullback.of_vert_is_iso ⟨nat_trans.naturality _ f⟩
+
+lemma nat_trans.equifibered.comp {F G H : J ⥤ C} {α : F ⟶ G} {β : G ⟶ H}
+  (hα : α.equifibered) (hβ : β.equifibered) : (α ≫ β).equifibered :=
+λ i j f, (hα f).paste_vert (hβ f)
+
+/-- A (colimit) cocone over a diagram `F : J ⥤ C` is universal if it is stable under pullbacks. -/
+def is_universal_colimit {F : J ⥤ C} (c : cocone F) : Prop :=
+∀ ⦃F' : J ⥤ C⦄ (c' : cocone F') (α : F' ⟶ F) (f : c'.X ⟶ c.X)
+  (h : α ≫ c.ι = c'.ι ≫ (functor.const J).map f) (hα : α.equifibered),
+  (∀ j : J, is_pullback (c'.ι.app j) (α.app j) f (c.ι.app j)) → nonempty (is_colimit c')
+
+/-- A (colimit) cocone over a diagram `F : J ⥤ C` is van Kampen if for every cocone `c'` over the
+pullback of the diagram `F' : J ⥤ C'`, `c'` is colimiting iff `c'` is the pullback of `c`.
+
+TODO: Show that this is iff the functor `C ⥤ Catᵒᵖ` sending `x` to `C/x` preserves it.
+TODO: Show that this is iff the inclusion functor `C ⥤ Span(C)` preserves it.
+-/
+def is_van_kampen_colimit {F : J ⥤ C} (c : cocone F) : Prop :=
+∀ ⦃F' : J ⥤ C⦄ (c' : cocone F') (α : F' ⟶ F) (f : c'.X ⟶ c.X)
+  (h : α ≫ c.ι = c'.ι ≫ (functor.const J).map f) (hα : α.equifibered),
+  nonempty (is_colimit c') ↔ ∀ j : J, is_pullback (c'.ι.app j) (α.app j) f (c.ι.app j)
+
+lemma is_van_kampen_colimit.is_universal {F : J ⥤ C} {c : cocone F} (H : is_van_kampen_colimit c) :
+  is_universal_colimit c :=
+λ _ c' α f h hα, (H c' α f h hα).mpr
+
+/-- A van Kampen colimit is a colimit. -/
+noncomputable
+def is_van_kampen_colimit.is_colimit {F : J ⥤ C} {c : cocone F} (h : is_van_kampen_colimit c) :
+  is_colimit c :=
+begin
+  refine ((h c (𝟙 F) (𝟙 c.X : _) (by rw [functor.map_id, category.comp_id, category.id_comp])
+    (nat_trans.equifibered_of_is_iso _)).mpr $ λ j, _).some,
+  haveI : is_iso (𝟙 c.X) := infer_instance,
+  exact is_pullback.of_vert_is_iso ⟨by erw [nat_trans.id_app, category.comp_id, category.id_comp]⟩,
+end
+
+lemma is_initial.is_van_kampen_colimit [has_strict_initial_objects C] {X : C} (h : is_initial X) :
+  is_van_kampen_colimit (as_empty_cocone X) :=
+begin
+  intros F' c' α f hf hα,
+  have : F' = functor.empty C := by apply functor.hext; rintro ⟨⟨⟩⟩,
+  subst this,
+  haveI := h.is_iso_to f,
+  refine ⟨by rintro _ ⟨⟨⟩⟩, λ _,
+    ⟨is_colimit.of_iso_colimit h (cocones.ext (as_iso f).symm $ by rintro ⟨⟨⟩⟩)⟩⟩
+end
+
+section extensive
+
+variables {X Y : C}
+
+/--
+A category is (finitary) extensive if it has finite coproducts,
+and binary coproducts are van Kampen.
+
+TODO: Show that this is iff all finite coproducts are van Kampen. -/
+class finitary_extensive (C : Type u) [category.{v} C] : Prop :=
+[has_finite_coproducts : has_finite_coproducts C]
+(van_kampen' : ∀ {X Y : C} (c : binary_cofan X Y), is_colimit c → is_van_kampen_colimit c)
+
+attribute [priority 100, instance] finitary_extensive.has_finite_coproducts
+
+lemma finitary_extensive.van_kampen [finitary_extensive C] {F : discrete walking_pair ⥤ C}
+  (c : cocone F) (hc : is_colimit c) : is_van_kampen_colimit c :=
+begin
+  let X := F.obj ⟨walking_pair.left⟩, let Y := F.obj ⟨walking_pair.right⟩,
+  have : F = pair X Y,
+  { apply functor.hext, { rintros ⟨⟨⟩⟩; refl }, { rintros ⟨⟨⟩⟩ ⟨j⟩ ⟨⟨rfl : _ = j⟩⟩; simpa } },
+  clear_value X Y, subst this,
+  exact finitary_extensive.van_kampen' c hc
+end
+
+lemma map_pair_equifibered {F F' : discrete walking_pair ⥤ C} (α : F ⟶ F') : α.equifibered :=
+begin
+  rintros ⟨⟨⟩⟩ ⟨j⟩ ⟨⟨rfl : _ = j⟩⟩,
+  all_goals { dsimp, simp only [discrete.functor_map_id],
+    exact is_pullback.of_horiz_is_iso ⟨by simp only [category.comp_id, category.id_comp]⟩ }
+end
+
+lemma binary_cofan.is_van_kampen_iff (c : binary_cofan X Y) :
+  is_van_kampen_colimit c ↔
+  ∀ {X' Y' : C} (c' : binary_cofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y)
+    (f : c'.X ⟶ c.X) (hαX : αX ≫ c.inl = c'.inl ≫ f) (hαY : αY ≫ c.inr = c'.inr ≫ f),
+    nonempty (is_colimit c') ↔ is_pullback c'.inl αX f c.inl ∧ is_pullback c'.inr αY f c.inr :=
+begin
+  split,
+  { introv H hαX hαY,
+    rw H c' (map_pair αX αY) f (by ext ⟨⟨⟩⟩; dsimp; assumption) (map_pair_equifibered _),
+    split, { intro H, exact ⟨H _, H _⟩ }, { rintros H ⟨⟨⟩⟩, exacts [H.1, H.2] } },
+  { introv H F' hα h,
+    let X' := F'.obj ⟨walking_pair.left⟩, let Y' := F'.obj ⟨walking_pair.right⟩,
+    have : F' = pair X' Y',
+    { apply functor.hext, { rintros ⟨⟨⟩⟩; refl }, { rintros ⟨⟨⟩⟩ ⟨j⟩ ⟨⟨rfl : _ = j⟩⟩; simpa } },
+    clear_value X' Y', subst this, change binary_cofan X' Y' at c',
+    rw H c' _ _ _ (nat_trans.congr_app hα ⟨walking_pair.left⟩)
+      (nat_trans.congr_app hα ⟨walking_pair.right⟩),
+    split, { rintros H ⟨⟨⟩⟩, exacts [H.1, H.2] }, { intro H, exact ⟨H _, H _⟩ } }
+end
+
+lemma binary_cofan.is_van_kampen_mk {X Y : C} (c : binary_cofan X Y)
+  (cofans : ∀ (X Y : C), binary_cofan X Y) (colimits : ∀ X Y, is_colimit (cofans X Y))
+  (cones : ∀ {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z), pullback_cone f g)
+  (limits : ∀ {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z),  is_limit (cones f g))
+  (h₁ : ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').X ⟶ c.X)
+    (hαX : αX ≫ c.inl = (cofans X' Y').inl ≫ f) (hαY : αY ≫ c.inr = (cofans X' Y').inr ≫ f),
+    is_pullback (cofans X' Y').inl αX f c.inl ∧ is_pullback (cofans X' Y').inr αY f c.inr)
+  (h₂ : ∀ {Z : C} (f : Z ⟶ c.X),
+    is_colimit (binary_cofan.mk (cones f c.inl).fst (cones f c.inr).fst)) :
+  is_van_kampen_colimit c :=
+begin
+  rw binary_cofan.is_van_kampen_iff,
+  introv hX hY,
+  split,
+  { rintros ⟨h⟩,
+    let e := h.cocone_point_unique_up_to_iso (colimits _ _),
+    obtain ⟨hl, hr⟩ := h₁ αX αY (e.inv ≫ f) (by simp [hX]) (by simp [hY]),
+    split,
+    { rw [← category.id_comp αX, ← iso.hom_inv_id_assoc e f],
+      have : c'.inl ≫ e.hom = 𝟙 X' ≫ (cofans X' Y').inl := by { dsimp, simp },
+      haveI : is_iso (𝟙 X') := infer_instance,
+      exact (is_pullback.of_vert_is_iso ⟨this⟩).paste_vert hl },
+    { rw [← category.id_comp αY, ← iso.hom_inv_id_assoc e f],
+      have : c'.inr ≫ e.hom = 𝟙 Y' ≫ (cofans X' Y').inr := by { dsimp, simp },
+      haveI : is_iso (𝟙 Y') := infer_instance,
+      exact (is_pullback.of_vert_is_iso ⟨this⟩).paste_vert hr } },
+  { rintro ⟨H₁, H₂⟩,
+    refine ⟨is_colimit.of_iso_colimit _ $ (iso_binary_cofan_mk _).symm⟩,
+    let e₁ : X' ≅ _ := H₁.is_limit.cone_point_unique_up_to_iso (limits _ _),
+    let e₂ : Y' ≅ _ := H₂.is_limit.cone_point_unique_up_to_iso (limits _ _),
+    have he₁ : c'.inl = e₁.hom ≫ (cones f c.inl).fst := by simp,
+    have he₂ : c'.inr = e₂.hom ≫ (cones f c.inr).fst := by simp,
+    rw [he₁, he₂],
+    apply binary_cofan.is_colimit_comp_right_iso (binary_cofan.mk _ _),
+    apply binary_cofan.is_colimit_comp_left_iso (binary_cofan.mk _ _),
+    exact h₂ f }
+end
+.
+lemma binary_cofan.mono_inr_of_is_van_kampen [has_initial C] {X Y : C} {c : binary_cofan X Y}
+  (h : is_van_kampen_colimit c) : mono c.inr :=
+begin
+  refine pullback_cone.mono_of_is_limit_mk_id_id _ (is_pullback.is_limit _),
+  refine (h (binary_cofan.mk (initial.to Y) (𝟙 Y))
+    (map_pair (initial.to X) (𝟙 Y)) c.inr _ (map_pair_equifibered _)).mp ⟨_⟩ ⟨walking_pair.right⟩,
+  { ext ⟨⟨⟩⟩; dsimp; simp },
+  { exact ((binary_cofan.is_colimit_iff_is_iso_inr initial_is_initial _).mpr
+      (by { dsimp, apply_instance })).some }
+end
+
+lemma finitary_extensive.mono_inr_of_is_colimit [finitary_extensive C]
+  {c : binary_cofan X Y} (hc : is_colimit c) : mono c.inr :=
+binary_cofan.mono_inr_of_is_van_kampen (finitary_extensive.van_kampen c hc)
+
+lemma finitary_extensive.mono_inl_of_is_colimit [finitary_extensive C]
+  {c : binary_cofan X Y} (hc : is_colimit c) : mono c.inl :=
+finitary_extensive.mono_inr_of_is_colimit (binary_cofan.is_colimit_flip hc)
+
+instance [finitary_extensive C] (X Y : C) : mono (coprod.inl : X ⟶ X ⨿ Y) :=
+(finitary_extensive.mono_inl_of_is_colimit (coprod_is_coprod X Y) : _)
+
+instance [finitary_extensive C] (X Y : C) : mono (coprod.inr : Y ⟶ X ⨿ Y) :=
+(finitary_extensive.mono_inr_of_is_colimit (coprod_is_coprod X Y) : _)
+
+lemma binary_cofan.is_pullback_initial_to_of_is_van_kampen [has_initial C]
+  {c : binary_cofan X Y}
+  (h : is_van_kampen_colimit c) : is_pullback (initial.to _) (initial.to _) c.inl c.inr :=
+begin
+  refine ((h (binary_cofan.mk (initial.to Y) (𝟙 Y)) (map_pair (initial.to X) (𝟙 Y)) c.inr _
+    (map_pair_equifibered _)).mp ⟨_⟩ ⟨walking_pair.left⟩).flip,
+  { ext ⟨⟨⟩⟩; dsimp; simp },
+  { exact ((binary_cofan.is_colimit_iff_is_iso_inr initial_is_initial _).mpr
+      (by { dsimp, apply_instance })).some }
+end
+
+lemma finitary_extensive.is_pullback_initial_to_binary_cofan [finitary_extensive C]
+  {c : binary_cofan X Y} (hc : is_colimit c) :
+  is_pullback (initial.to _) (initial.to _) c.inl c.inr :=
+binary_cofan.is_pullback_initial_to_of_is_van_kampen (finitary_extensive.van_kampen c hc)
+
+lemma has_strict_initial_of_is_universal [has_initial C]
+  (H : is_universal_colimit (binary_cofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))) :
+  has_strict_initial_objects C :=
+has_strict_initial_objects_of_initial_is_strict
+begin
+  intros A f,
+  suffices : is_colimit (binary_cofan.mk (𝟙 A) (𝟙 A)),
+  { obtain ⟨l, h₁, h₂⟩ := limits.binary_cofan.is_colimit.desc' this (f ≫ initial.to A) (𝟙 A),
+    rcases (category.id_comp _).symm.trans h₂ with rfl,
+    exact ⟨⟨_, ((category.id_comp _).symm.trans h₁).symm, initial_is_initial.hom_ext _ _⟩⟩ },
+  refine (H (binary_cofan.mk (𝟙 _) (𝟙 _)) (map_pair f f) f (by ext ⟨⟨⟩⟩; dsimp; simp)
+    (map_pair_equifibered _) _).some,
+  rintro ⟨⟨⟩⟩; dsimp;
+    exact is_pullback.of_horiz_is_iso ⟨(category.id_comp _).trans (category.comp_id _).symm⟩
+end
+
+@[priority 100]
+instance has_strict_initial_objects_of_finitary_extensive [finitary_extensive C] :
+  has_strict_initial_objects C :=
+has_strict_initial_of_is_universal (finitary_extensive.van_kampen _
+  ((binary_cofan.is_colimit_iff_is_iso_inr initial_is_initial _).mpr
+    (by { dsimp, apply_instance })).some).is_universal
+
+lemma finitary_extensive_iff_of_is_terminal (C : Type u) [category.{v} C] [has_finite_coproducts C]
+  (T : C) (HT : is_terminal T) (c₀ : binary_cofan T T) (hc₀ : is_colimit c₀) :
+  finitary_extensive C ↔ is_van_kampen_colimit c₀ :=
+begin
+  refine ⟨λ H, H.2 c₀ hc₀, λ H, _⟩,
+  constructor,
+  simp_rw binary_cofan.is_van_kampen_iff at H ⊢,
+  intros X Y c hc X' Y' c' αX αY f hX hY,
+  obtain ⟨d, hd, hd'⟩ := limits.binary_cofan.is_colimit.desc' hc
+    (HT.from _ ≫ c₀.inl) (HT.from _ ≫ c₀.inr),
+  rw H c' (αX ≫ HT.from _) (αY ≫ HT.from _) (f ≫ d)
+    (by rw [← reassoc_of hX, hd, category.assoc])
+    (by rw [← reassoc_of hY, hd', category.assoc]),
+  obtain ⟨hl, hr⟩ := (H c (HT.from _) (HT.from _) d hd.symm hd'.symm).mp ⟨hc⟩,
+  rw [hl.paste_vert_iff hX.symm, hr.paste_vert_iff hY.symm]
+end
+
+instance types.finitary_extensive : finitary_extensive (Type u) :=
+begin
+  rw [finitary_extensive_iff_of_is_terminal (Type u) punit types.is_terminal_punit _
+    (types.binary_coproduct_colimit _ _)],
+  apply binary_cofan.is_van_kampen_mk _ _ (λ X Y, types.binary_coproduct_colimit X Y) _
+    (λ X Y Z f g, (limits.types.pullback_limit_cone f g).2),
+  { intros,
+    split,
+    { refine ⟨⟨hαX.symm⟩, ⟨pullback_cone.is_limit_aux' _ _⟩⟩,
+      intro s,
+      have : ∀ x, ∃! y, s.fst x = sum.inl y,
+      { intro x,
+        cases h : s.fst x,
+        { simp_rw sum.inl_injective.eq_iff, exact exists_unique_eq' },
+        { apply_fun f at h,
+          cases ((congr_fun s.condition x).symm.trans h).trans (congr_fun hαY val : _).symm } },
+      delta exists_unique at this,
+      choose l hl hl',
+      exact ⟨l, (funext hl).symm, types.is_terminal_punit.hom_ext _ _,
+        λ l' h₁ h₂, funext $ λ x, hl' x (l' x) (congr_fun h₁ x).symm⟩ },
+    { refine ⟨⟨hαY.symm⟩, ⟨pullback_cone.is_limit_aux' _ _⟩⟩,
+      intro s, dsimp,
+      have : ∀ x, ∃! y, s.fst x = sum.inr y,
+      { intro x,
+        cases h : s.fst x,
+        { apply_fun f at h,
+          cases ((congr_fun s.condition x).symm.trans h).trans (congr_fun hαX val : _).symm },
+        { simp_rw sum.inr_injective.eq_iff, exact exists_unique_eq' } },
+      delta exists_unique at this,
+      choose l hl hl',
+      exact ⟨l, (funext hl).symm, types.is_terminal_punit.hom_ext _ _,
+        λ l' h₁ h₂, funext $ λ x, hl' x (l' x) (congr_fun h₁ x).symm⟩ } },
+  { intros Z f,
+    dsimp [limits.types.binary_coproduct_cocone],
+    delta types.pullback_obj,
+    have : ∀ x, f x = sum.inl punit.star ∨ f x = sum.inr punit.star,
+    { intro x, rcases f x with (⟨⟨⟩⟩|⟨⟨⟩⟩), exacts [or.inl rfl, or.inr rfl] },
+    let eX : {p : Z × punit // f p.fst = sum.inl p.snd} ≃ {x : Z // f x = sum.inl punit.star } :=
+      ⟨λ p, ⟨p.1.1, by convert p.2⟩, λ x, ⟨⟨_, _⟩, x.2⟩, λ _, by ext; refl, λ _, by ext; refl⟩,
+    let eY : {p : Z × punit // f p.fst = sum.inr p.snd} ≃ {x : Z // f x = sum.inr punit.star } :=
+      ⟨λ p, ⟨p.1.1, p.2.trans (congr_arg sum.inr $ subsingleton.elim _ _)⟩,
+        λ x, ⟨⟨_, _⟩, x.2⟩, λ _, by ext; refl, λ _, by ext; refl⟩,
+    fapply binary_cofan.is_colimit_mk,
+    { exact λ s x, dite _ (λ h, s.inl $ eX.symm ⟨x, h⟩)
+        (λ h, s.inr $ eY.symm ⟨x, (this x).resolve_left h⟩) },
+    { intro s, ext ⟨⟨x, ⟨⟩⟩, _⟩, dsimp, split_ifs; refl },
+    { intro s, ext ⟨⟨x, ⟨⟩⟩, hx⟩, dsimp, split_ifs, { cases h.symm.trans hx }, { refl } },
+    { intros s m e₁ e₂, ext x, split_ifs, { rw ← e₁, refl }, { rw ← e₂, refl } } }
+end
+
+end extensive
+
+end category_theory