English
If F ≅ G is a natural isomorphism and F preserves the limit for K, then G preserves the limit for K; i.e., preservation transfers along a natural isomorphism.
Русский
Если F ≅ G — натуральный изоморфизм и F сохраняет предел для K, тогда G сохраняет предел для K; то есть сохранение переносится вдоль натуралного изоморфизма.
LaTeX
$$$$\big( F \cong G \big) \Rightarrow (\mathrm{PreservesLimit}(K,F) \Rightarrow \mathrm{PreservesLimit}(K,G)).$$$$
Lean4
/-- Transfer preservation of limits along a natural isomorphism in the diagram. -/
theorem preservesLimit_of_iso_diagram {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂) [PreservesLimit K₁ F] :
PreservesLimit K₂ F where
preserves {c}
t :=
⟨by
apply IsLimit.postcomposeInvEquiv (Functor.isoWhiskerRight h F :) _ _
have := (IsLimit.postcomposeInvEquiv h c).symm t
apply IsLimit.ofIsoLimit (isLimitOfPreserves F this)
exact Cones.ext (Iso.refl _)⟩
