instFaithfulUliftFunctor — Mathlib

English

Let C be the category of commutative groups. The universe-lift functor on C is faithful: for any objects A,B in C, the map Hom(A,B) → Hom(U(A), U(B)) is injective, i.e., f ≠ g implies Ulift(f) ≠ Ulift(g).

Русский

Пусть C — категория коммутативных групп. Функтор подстановки вселенной на C является верным: для любых объектов A,B отображение Hom(A,B) → Hom(U(A), U(B)) инъективно, то есть f ≠ g ⇒ Ulift(f) ≠ Ulift(g).

LaTeX

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

Lean4

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

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