English
The universe-lift functor preserves limits of shape J: for any diagram K: J → CommGrpCat, Ulift(K) preserves the limit cone, i.e., Ulift(lim_J K) ≅ lim_J (Ulift ∘ K).
Русский
Функтор подъёма вселенной сохраняет пределы формы J: для любого диаграммы K: J → CommGrpCat, Ulift сохраняет предел, то есть Ulift(lim_J K) ≅ lim_J (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
@[to_additive]
noncomputable instance uliftFunctor_preservesLimit {J : Type w} [Category.{w'} J] (K : J ⥤ CommGrpCat.{u}) :
PreservesLimit K uliftFunctor.{v, u} where
preserves
lc :=
⟨isLimitOfReflects (forget CommGrpCat.{max u v})
(isLimitOfPreserves CategoryTheory.uliftFunctor (isLimitOfPreserves (forget CommGrpCat) lc))⟩
