uliftFunctor_preservesLimitsOfSize

English

The universe-lift functor preserves limits of arbitrary size: for any diagram K, Ulift(lim K) ≅ lim(Ulift ∘ K).

Русский

Функтор подъёма вселенной сохраняет пределы произвольного размера: для любой диаграммы K Ulift(lim K) ≅ lim(Ulift ∘ K).

LaTeX

$$$\forall J [\text{Category } J], \forall K : J \to \mathrm{CommGrpCat},\; \mathrm{Ulift}(\varprojlim J K) \cong \varprojlim J (\mathrm{Ulift} \circ K)$$$

Lean4

/-- The universe lift for commutative groups preserves limits of arbitrary size.
-/
@[to_additive /-- The universe lift functor for commutative additive groups preserves limits of
      arbitrary size. -/
    ]
noncomputable instance uliftFunctor_preservesLimitsOfSize : PreservesLimitsOfSize.{w', w} uliftFunctor.{v, u} where

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