English
If J ≃ J' is an equivalence of shapes and F preserves limits of shape J, then F preserves limits of shape J'.
Русский
Если J ≃ J' — эквивалентность форм диаграмм и F сохраняет пределы формы J, тогда F сохраняет пределы формы J'.
LaTeX
$$$$e: J \simeq J' \Rightarrow (\mathrm{PreservesLimitsOfShape}(J,F) \Rightarrow \mathrm{PreservesLimitsOfShape}(J',F)).$$$$
Lean4
/-- Transfer preservation of limits along an equivalence in the shape. -/
theorem preservesLimitsOfShape_of_equiv {J' : Type w₂} [Category.{w₂'} J'] (e : J ≌ J') (F : C ⥤ D)
[PreservesLimitsOfShape J F] : PreservesLimitsOfShape J' F where
preservesLimit
{K} :=
{
preserves := fun {c} t =>
⟨by
let equ := e.invFunIdAssoc (K ⋙ F)
have := (isLimitOfPreserves F (t.whiskerEquivalence e)).whiskerEquivalence e.symm
apply ((IsLimit.postcomposeHomEquiv equ _).symm this).ofIsoLimit
refine Cones.ext (Iso.refl _) fun j => ?_
simp [equ, ← Functor.map_comp]⟩ }
