English
Let J be a small category and F : J ⥤ Type be a diagram of types. If c is a colimit cocone for F, and for every j there is an equivalence e_j : G.obj j ≃ F.obj j compatible with maps F.map and G.map, then precomposing c with e yields a colimit cocone for G.
Русский
Пусть J — малая категория и F : J ⥤ Type — диаграмма типов. Если c — колимитный кокон для F, и для каждого j существует эквивалентность e_j : G.obj j ≃ F.obj j, совместимая с отображениями F.map и G.map, тогда c, скорректированный через e, образует колимитный кокон для G.
LaTeX
$$$\\text{IsColimitCore}(c) \\Rightarrow \\text{IsColimitCore}\\bigl(c.\\text{precompose}(\\{e_j\\},\\ \\text{naturality})\\bigr)$$$
Lean4
/-- A colimit cocone for `F : J ⥤ Type w₀` induces a colimit cocone
for `G : J ⥤ Type w₉'` when we have a natural equivalence `G.obj j ≃ F.obj j`
for all `j : J`. -/
def precompose (hc : IsColimitCore.{w₂} c) {G : J ⥤ Type w₀'} (e : ∀ j, G.obj j ≃ F.obj j)
(naturality : ∀ {j j'} (f : j ⟶ j'), e j' ∘ G.map f = F.map f ∘ e j) :
IsColimitCore.{w₂} (c.precompose _ naturality)
where
desc c' := hc.desc (c'.precompose _ (FunctorToTypes.naturality_symm e naturality))
fac c'
j := by
rw [precompose_ι, ← Function.comp_assoc, hc.fac, precompose_ι, Function.comp_assoc, Equiv.symm_comp_self,
Function.comp_id]
funext {T f g}
h :=
hc.funext
(fun j ↦ by
ext x
obtain ⟨y, rfl⟩ := (e j).surjective x
exact congr_fun (h j) y)
