|
| 1 | +/- |
| 2 | +Copyright (c) 2025 Christian Merten. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Christian Merten |
| 5 | +-/ |
| 6 | +import Mathlib.CategoryTheory.Limits.Connected |
| 7 | +import Mathlib.CategoryTheory.Presentable.Finite |
| 8 | + |
| 9 | +/-! |
| 10 | +# (Co)limit presentations |
| 11 | +
|
| 12 | +Let `J` and `C` be categories and `X : C`. We define type `ColimitPresentation J X` that contains |
| 13 | +the data of objects `Dⱼ` and natural maps `sⱼ : Dⱼ ⟶ X` that make `X` the colimit of the `Dⱼ`. |
| 14 | +
|
| 15 | +## Main definitions: |
| 16 | +
|
| 17 | +- `CategoryTheory.Limits.ColimitPresentation`: A colimit presentation of `X` over `J` is a diagram |
| 18 | + `{Dᵢ}` in `C` and natural maps `sᵢ : Dᵢ ⟶ X` making `X` into the colimit of the `Dᵢ`. |
| 19 | +- `CategoryTheory.Limits.ColimitPresentation.bind`: Given a colimit presentation of `X` and |
| 20 | + colimit presentations of the components, this is the colimit presentation over the sigma type. |
| 21 | +
|
| 22 | +## TODOs: |
| 23 | +
|
| 24 | +- Dualise to obtain `LimitPresentation`. |
| 25 | +- Refactor `TransfiniteCompositionOfShape` so that it extends `ColimitPresentation`. |
| 26 | +-/ |
| 27 | + |
| 28 | +universe s t w v u |
| 29 | + |
| 30 | +namespace CategoryTheory.Limits |
| 31 | + |
| 32 | +variable {C : Type u} [Category.{v} C] |
| 33 | + |
| 34 | +/-- A colimit presentation of `X` over `J` is a diagram `{Dᵢ}` in `C` and natural maps |
| 35 | +`sᵢ : Dᵢ ⟶ X` making `X` into the colimit of the `Dᵢ`. -/ |
| 36 | +structure ColimitPresentation (J : Type w) [Category.{t} J] (X : C) where |
| 37 | + /-- The diagram `{Dᵢ}`. -/ |
| 38 | + diag : J ⥤ C |
| 39 | + /-- The natural maps `sᵢ : Dᵢ ⟶ X`. -/ |
| 40 | + ι : diag ⟶ (Functor.const J).obj X |
| 41 | + /-- `X` is the colimit of the `Dᵢ` via `sᵢ`. -/ |
| 42 | + isColimit : IsColimit (Cocone.mk _ ι) |
| 43 | + |
| 44 | +variable {J : Type w} [Category.{t} J] {X : C} |
| 45 | + |
| 46 | +namespace ColimitPresentation |
| 47 | + |
| 48 | +initialize_simps_projections ColimitPresentation (-isColimit) |
| 49 | + |
| 50 | +/-- The cocone associated to a colimit presentation. -/ |
| 51 | +abbrev cocone (pres : ColimitPresentation J X) : Cocone pres.diag := |
| 52 | + Cocone.mk _ pres.ι |
| 53 | + |
| 54 | +/-- The canonical colimit presentation of any object over a point. -/ |
| 55 | +@[simps] |
| 56 | +noncomputable |
| 57 | +def self (X : C) : ColimitPresentation PUnit.{s + 1} X where |
| 58 | + diag := (Functor.const _).obj X |
| 59 | + ι := 𝟙 _ |
| 60 | + isColimit := isColimitConstCocone _ _ |
| 61 | + |
| 62 | +/-- If `F` preserves colimits of shape `J`, it maps colimit presentations of `X` to |
| 63 | +colimit presentations of `F(X)`. -/ |
| 64 | +@[simps] |
| 65 | +noncomputable |
| 66 | +def map (P : ColimitPresentation J X) {D : Type*} [Category D] (F : C ⥤ D) |
| 67 | + [PreservesColimitsOfShape J F] : ColimitPresentation J (F.obj X) where |
| 68 | + diag := P.diag ⋙ F |
| 69 | + ι := Functor.whiskerRight P.ι F ≫ (F.constComp _ _).hom |
| 70 | + isColimit := (isColimitOfPreserves F P.isColimit).ofIsoColimit (Cocones.ext (.refl _) (by simp)) |
| 71 | + |
| 72 | +/-- Map a colimit presentation under an isomorphism. -/ |
| 73 | +@[simps] |
| 74 | +def ofIso (P : ColimitPresentation J X) {Y : C} (e : X ≅ Y) : ColimitPresentation J Y where |
| 75 | + diag := P.diag |
| 76 | + ι := P.ι ≫ (Functor.const J).map e.hom |
| 77 | + isColimit := P.isColimit.ofIsoColimit (Cocones.ext e fun _ ↦ rfl) |
| 78 | + |
| 79 | +section |
| 80 | + |
| 81 | +variable {J : Type*} {I : J → Type*} [Category J] [∀ j, Category (I j)] |
| 82 | + {D : J ⥤ C} {P : ∀ j, ColimitPresentation (I j) (D.obj j)} |
| 83 | + |
| 84 | +set_option linter.unusedVariables false in |
| 85 | +/-- The type underlying the category used in the construction of the composition |
| 86 | +of colimit presentations. This is simply `Σ j, I j` but with a different category structure. -/ |
| 87 | +@[nolint unusedArguments] |
| 88 | +def Total (P : ∀ j, ColimitPresentation (I j) (D.obj j)) : Type _ := |
| 89 | + Σ j, I j |
| 90 | + |
| 91 | +variable (P) in |
| 92 | +/-- Constructor for `Total` to guide type checking. -/ |
| 93 | +abbrev Total.mk (i : J) (k : I i) : Total P := ⟨i, k⟩ |
| 94 | + |
| 95 | +/-- Morphisms in the `Total` category. -/ |
| 96 | +@[ext] |
| 97 | +structure Total.Hom (k l : Total P) where |
| 98 | + /-- The underlying morphism in the first component. -/ |
| 99 | + base : k.1 ⟶ l.1 |
| 100 | + /-- A morphism in `C`. -/ |
| 101 | + hom : (P k.1).diag.obj k.2 ⟶ (P l.1).diag.obj l.2 |
| 102 | + w : (P k.1).ι.app k.2 ≫ D.map base = hom ≫ (P l.1).ι.app l.2 := by cat_disch |
| 103 | + |
| 104 | +attribute [reassoc] Total.Hom.w |
| 105 | + |
| 106 | +/-- Composition of morphisms in the `Total` category. -/ |
| 107 | +@[simps] |
| 108 | +def Total.Hom.comp {k l m : Total P} (f : k.Hom l) (g : l.Hom m) : k.Hom m where |
| 109 | + base := f.base ≫ g.base |
| 110 | + hom := f.hom ≫ g.hom |
| 111 | + w := by |
| 112 | + simp only [Functor.const_obj_obj, Functor.map_comp, Category.assoc] |
| 113 | + rw [f.w_assoc, g.w] |
| 114 | + |
| 115 | +@[simps! id_base id_hom comp_base comp_hom] |
| 116 | +instance : Category (Total P) where |
| 117 | + Hom := Total.Hom |
| 118 | + id _ := { base := 𝟙 _, hom := 𝟙 _ } |
| 119 | + comp := Total.Hom.comp |
| 120 | + |
| 121 | +section Small |
| 122 | + |
| 123 | +variable {J : Type w} {I : J → Type w} [SmallCategory J] [∀ j, SmallCategory (I j)] |
| 124 | + {D : J ⥤ C} {P : ∀ j, ColimitPresentation (I j) (D.obj j)} |
| 125 | + |
| 126 | +lemma Total.exists_hom_of_hom {j j' : J} (i : I j) (u : j ⟶ j') |
| 127 | + [IsFiltered (I j')] [IsFinitelyPresentable.{w} ((P j).diag.obj i)] : |
| 128 | + ∃ (i' : I j') (f : Total.mk P j i ⟶ Total.mk P j' i'), f.base = u := by |
| 129 | + obtain ⟨i', q, hq⟩ := IsFinitelyPresentable.exists_hom_of_isColimit (P j').isColimit |
| 130 | + ((P j).ι.app i ≫ D.map u) |
| 131 | + use i', { base := u, hom := q, w := by simp [← hq] } |
| 132 | + |
| 133 | +instance [IsFiltered J] [∀ j, IsFiltered (I j)] : Nonempty (Total P) := by |
| 134 | + obtain ⟨j⟩ : Nonempty J := IsFiltered.nonempty |
| 135 | + obtain ⟨i⟩ : Nonempty (I j) := IsFiltered.nonempty |
| 136 | + exact ⟨⟨j, i⟩⟩ |
| 137 | + |
| 138 | +instance [IsFiltered J] [∀ j, IsFiltered (I j)] |
| 139 | + [∀ j i, IsFinitelyPresentable.{w} ((P j).diag.obj i)] : |
| 140 | + IsFiltered (Total P) where |
| 141 | + cocone_objs k l := by |
| 142 | + let a := IsFiltered.max k.1 l.1 |
| 143 | + obtain ⟨a', f, hf⟩ := Total.exists_hom_of_hom (P := P) k.2 (IsFiltered.leftToMax k.1 l.1) |
| 144 | + obtain ⟨b', g, hg⟩ := Total.exists_hom_of_hom (P := P) l.2 (IsFiltered.rightToMax k.1 l.1) |
| 145 | + refine ⟨⟨a, IsFiltered.max a' b'⟩, ?_, ?_, trivial⟩ |
| 146 | + · exact f ≫ { base := 𝟙 _, hom := (P _).diag.map (IsFiltered.leftToMax _ _) } |
| 147 | + · exact g ≫ { base := 𝟙 _, hom := (P _).diag.map (IsFiltered.rightToMax _ _) } |
| 148 | + cocone_maps {k l} f g := by |
| 149 | + let a := IsFiltered.coeq f.base g.base |
| 150 | + obtain ⟨a', u, hu⟩ := Total.exists_hom_of_hom (P := P) l.2 (IsFiltered.coeqHom f.base g.base) |
| 151 | + have : (f.hom ≫ u.hom) ≫ (P _).ι.app _ = (g.hom ≫ u.hom) ≫ (P _).ι.app _ := by |
| 152 | + simp only [Category.assoc, Functor.const_obj_obj, ← u.w, ← f.w_assoc, ← g.w_assoc] |
| 153 | + rw [← Functor.map_comp, hu, IsFiltered.coeq_condition f.base g.base] |
| 154 | + simp |
| 155 | + obtain ⟨j, p, q, hpq⟩ := IsFinitelyPresentable.exists_eq_of_isColimit (P _).isColimit _ _ this |
| 156 | + dsimp at p q |
| 157 | + refine ⟨⟨a, IsFiltered.coeq p q⟩, |
| 158 | + u ≫ { base := 𝟙 _, hom := (P _).diag.map (p ≫ IsFiltered.coeqHom p q) }, ?_⟩ |
| 159 | + apply Total.Hom.ext |
| 160 | + · simp [hu, IsFiltered.coeq_condition f.base g.base] |
| 161 | + · rw [Category.assoc] at hpq |
| 162 | + simp only [Functor.map_comp, comp_hom, reassoc_of% hpq] |
| 163 | + simp [← Functor.map_comp, ← IsFiltered.coeq_condition] |
| 164 | + |
| 165 | +/-- If `P` is a colimit presentation over `J` of `X` and for every `j` we are given a colimit |
| 166 | +presentation `Qⱼ` over `I j` of the `P.diag.obj j`, this is the refined colimit presentation of `X` |
| 167 | +over `Total Q`. -/ |
| 168 | +@[simps] |
| 169 | +def bind {X : C} (P : ColimitPresentation J X) (Q : ∀ j, ColimitPresentation (I j) (P.diag.obj j)) |
| 170 | + [∀ j, IsFiltered (I j)] [∀ j i, IsFinitelyPresentable.{w} ((Q j).diag.obj i)] : |
| 171 | + ColimitPresentation (Total Q) X where |
| 172 | + diag.obj k := (Q k.1).diag.obj k.2 |
| 173 | + diag.map {k l} f := f.hom |
| 174 | + ι.app k := (Q k.1).ι.app k.2 ≫ P.ι.app k.1 |
| 175 | + ι.naturality {k l} u := by simp [← u.w_assoc] |
| 176 | + isColimit.desc c := P.isColimit.desc |
| 177 | + { pt := c.pt |
| 178 | + ι.app j := (Q j).isColimit.desc |
| 179 | + { pt := c.pt |
| 180 | + ι.app i := c.ι.app ⟨j, i⟩ |
| 181 | + ι.naturality {i i'} u := by |
| 182 | + let v : Total.mk Q j i ⟶ .mk _ j i' := { base := 𝟙 _, hom := (Q _).diag.map u } |
| 183 | + simpa using c.ι.naturality v } |
| 184 | + ι.naturality {j j'} u := by |
| 185 | + refine (Q j).isColimit.hom_ext fun i ↦ ?_ |
| 186 | + simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.comp_id, |
| 187 | + (Q j).isColimit.fac] |
| 188 | + obtain ⟨i', hom, rfl⟩ := Total.exists_hom_of_hom (P := Q) i u |
| 189 | + rw [reassoc_of% hom.w, (Q j').isColimit.fac] |
| 190 | + simpa using c.ι.naturality hom } |
| 191 | + isColimit.fac := fun c ⟨j, i⟩ ↦ by simp [P.isColimit.fac, (Q j).isColimit.fac] |
| 192 | + isColimit.uniq c m hm := by |
| 193 | + refine P.isColimit.hom_ext fun j ↦ ?_ |
| 194 | + simp only [Functor.const_obj_obj, P.isColimit.fac] |
| 195 | + refine (Q j).isColimit.hom_ext fun i ↦ ?_ |
| 196 | + simpa [(Q j).isColimit.fac] using hm (.mk _ j i) |
| 197 | + |
| 198 | +end Small |
| 199 | + |
| 200 | +end |
| 201 | + |
| 202 | +end CategoryTheory.Limits.ColimitPresentation |
0 commit comments