uliftFunctor_preservesLimit — Mathlib

English

The ulift functor preserves limits of a given shape.

Русский

Функтор подъёма вселенной сохраняет пределы заданной формы.

LaTeX

$$$\\text{uliftFunctorPreservesLimit}$$$

Lean4

@[to_additive]
noncomputable instance uliftFunctor_preservesLimit {J : Type w} [Category.{w'} J] (K : J ⥤ GrpCat.{u}) :
    PreservesLimit K uliftFunctor.{v, u} where
  preserves
    lc :=
    ⟨isLimitOfReflects (forget GrpCat.{max u v})
        (isLimitOfPreserves CategoryTheory.uliftFunctor (isLimitOfPreserves (forget GrpCat) lc))⟩

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