uliftFunctor_full — Mathlib

English

The ulift functor is full: every morphism between lifted objects arises from a morphism downstairs.

Русский

Усложняющий (ulift) функтор является полным: каждый морфизм между вознесёнными объектами поднимается из морфизма между исходными объектами.

LaTeX

$$$$ \text{uliftFunctor is Full}. $$$$

Lean4

instance uliftFunctor_full : (uliftFunctor.{v, u}).Full :=
  fullyFaithfulULiftFunctor.full

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