instFullUliftFunctor — Mathlib

English

Let C be the category of commutative additive groups. The universe-lift functor is full: every morphism Ulift(A) → Ulift(B) arises from a morphism A → B.

Русский

Пусть C — категория коммутативно-аддитивных групп. Функтор подстановки вселенной является полным: каждый морфизм Ulift(A) → Ulift(B) вытекает из морфизма A → B.

LaTeX

$$$\forall A,B : \text{CommGrpCat},\; \forall h : \mathrm{Hom}(\mathrm{Ulift} A, \mathrm{Ulift} B),\; \exists f : \mathrm{Hom}(A,B),\; \mathrm{Ulift}(f) = h$$$

Lean4

@[to_additive /-- The universe lift functor for commutative additive groups is full. -/
    ]
instance : uliftFunctor.{u, v}.Full :=
  uliftFunctorFullyFaithful.full

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