forget_isCorepresentable — Mathlib

English

The forgetful functor CommGrpCat → Type is corepresentable by ULift(ℤ) in multiplicative form, i.e. coyoneda at op(of ULift(Multiplicative ℤ)) is isomorphic to forget.

Русский

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

LaTeX

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

Lean4

instance forget_isCorepresentable : (forget CommGrpCat.{u}).IsCorepresentable :=
  Functor.IsCorepresentable.mk' CommGrpCat.coyonedaObjIsoForget

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