English
Let C and D be categories and J, J′ be small categories connected by an equivalence e : J ≃ J′. Let F: C ⟶ D be a functor. If F reflects colimits of shape J, then F also reflects colimits of shape J′.
Русский
Пусть C и D — категории, J и J′ — малые категории, связанные эквивалентностью e: J ≃ J′. Пусть F: C ⟶ D — функтор. Если F отражает колимиты формы J, то он отражает колимиты формы J′.
LaTeX
$$$\\forall \\; C \\; D \\; J \\; J' ,\\; e:\\, J \\simeq J' ,\\; F:\\, C \\to D:\\ ReflectsColimitsOfShape(J,F) \\Rightarrow ReflectsColimitsOfShape(J',F) ,$$$
Lean4
/-- Transfer reflection of colimits along an equivalence in the shape. -/
theorem reflectsColimitsOfShape_of_equiv {J' : Type w₂} [Category.{w₂'} J'] (e : J ≌ J') (F : C ⥤ D)
[ReflectsColimitsOfShape J F] : ReflectsColimitsOfShape J' F where
reflectsColimit :=
{
reflects := fun {c} t =>
⟨by
apply IsColimit.ofWhiskerEquivalence e
apply isColimitOfReflects F
apply IsColimit.ofIsoColimit _ (Functor.mapCoconeWhisker _).symm
exact IsColimit.whiskerEquivalence t _⟩ }
