English
Preserving colimits of shape J is transferred along an equivalence J ≌ J': if F preserves shape J, it preserves shape J'.
Русский
Сохранение колимитов по форме J переносится через эквивалентность форм J ≌ J': если F сохраняет колимиты по форме J, он сохраняет их и по форме J'.
LaTeX
$$$ (e : J \\simeq J') \\ [PreservesColimitsOfShape J\\, F] \\Rightarrow PreservesColimitsOfShape J'\\, F. $$$
Lean4
/-- Transfer preservation of colimits along an equivalence in the shape. -/
theorem preservesColimitsOfShape_of_equiv {J' : Type w₂} [Category.{w₂'} J'] (e : J ≌ J') (F : C ⥤ D)
[PreservesColimitsOfShape J F] : PreservesColimitsOfShape J' F where
preservesColimit
{K} :=
{
preserves := fun {c} t =>
⟨by
let equ := e.invFunIdAssoc (K ⋙ F)
have := (isColimitOfPreserves F (t.whiskerEquivalence e)).whiskerEquivalence e.symm
apply ((IsColimit.precomposeInvEquiv equ _).symm this).ofIsoColimit
refine Cocones.ext (Iso.refl _) fun j => ?_
simp [equ, ← Functor.map_comp]⟩ }
