uliftFunctor_preservesLimitsOfShape

English

For a fixed shape J, the universe-lift functor preserves limits of shape J: Ulift(lim_J K) ≅ lim_J (Ulift ∘ K) for all K : J ⥤ CommGrpCat.

Русский

Для фиксированной формы J функтор подъёма вселенной сохраняет пределы формы J: Ulift(lim_J K) ≅ lim_J (Ulift ∘ K) для всех K : J ⥤ CommGrpCat.

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

@[to_additive]
noncomputable instance uliftFunctor_preservesLimitsOfShape {J : Type w} [Category.{w'} J] :
    PreservesLimitsOfShape J uliftFunctor.{v, u} where

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