English
If J ≌ J' is an equivalence of categories, then W.colimitsOfShape J and W.colimitsOfShape J' coincide.
Русский
Если J и J' эквивалентны категориям, то W.colimitsOfShape J и W.colimitsOfShape J' совпадают.
LaTeX
$$W.colimitsOfShape J = W.colimitsOfShape J'$$
Lean4
theorem colimitsOfShape_le_of_final {J' : Type*} [Category J'] (F : J ⥤ J') [F.Final] :
W.colimitsOfShape J' ≤ W.colimitsOfShape J :=
by
intro _ _ _ ⟨X₁, X₂, c₁, c₂, h₁, h₂, f, hf⟩
have h₁' : IsColimit (c₁.whisker F) := (Functor.Final.isColimitWhiskerEquiv F c₁).symm h₁
have h₂' : IsColimit (c₂.whisker F) := (Functor.Final.isColimitWhiskerEquiv F c₂).symm h₂
have :
h₁.desc (Cocone.mk c₂.pt (f ≫ c₂.ι)) = h₁'.desc (Cocone.mk c₂.pt (Functor.whiskerLeft _ f ≫ (c₂.whisker F).ι)) :=
h₁'.hom_ext
(fun j ↦ by
have := h₁'.fac (Cocone.mk c₂.pt (Functor.whiskerLeft F f ≫ Functor.whiskerLeft F c₂.ι)) j
dsimp at this ⊢
simp [this])
rw [this]
exact ⟨_, _, _, _, h₁', h₂', _, fun _ ↦ hf _⟩
