coyonedaObjIsoForget — Mathlib

English

The forgetful functor AddGrpCat → Type is corepresentable by ULift(ℤ) in additive form, i.e. there is a natural isomorphism between coyoneda at op(of ULift(ℤ)) and forget on AddGrpCat.

Русский

Забывающий функтор AddGrpCat → Type корепрезентируем объектом ULift(ℤ); существует естественная изоморми́змa coyoneda(op(of ULift(ℤ))) ≅ forget AddGrpCat.

LaTeX

$$$ \\mathrm{coyoneda}\\big(\\mathrm{op}(\\mathrm{of}(\\mathrm{ULift}(\\mathbb{Z})))\\big) \\cong \\mathrm{forget}\\, \\mathrm{AddGrpCat} $$$

Lean4

/-- The forget functor `AddGrpCat.{u} ⥤ Type u` is corepresentable. -/
def coyonedaObjIsoForget : coyoneda.obj (op (of (ULift.{u} ℤ))) ≅ forget AddGrpCat.{u} :=
  NatIso.ofComponents fun M ↦ (ConcreteCategory.homEquiv.trans (uliftZMultiplesHom M.carrier).symm).toIso

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