preservesLimitsOfSize_of_univLE — Mathlib

English

If K1 ≅ K2 are diagram shapes and F preserves the limit for K1, then F preserves the limit for K2.

Русский

Если K1 ≅ K2 — изоморфия диаграмм и F сохраняет предел для K1, то F сохраняет предел для K2.

LaTeX

$$$$K_1 \cong K_2 \Rightarrow (\mathrm{PreservesLimit}(K_1,F) \Rightarrow \mathrm{PreservesLimit}(K_2,F)).$$$$

Lean4

/-- A functor preserving larger limits also preserves smaller limits. -/
theorem preservesLimitsOfSize_of_univLE (F : C ⥤ D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}]
    [PreservesLimitsOfSize.{w', w₂'} F] : PreservesLimitsOfSize.{w, w₂} F where
  preservesLimitsOfShape
    {J} := preservesLimitsOfShape_of_equiv ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm F

Похожие утверждения