forget_isCorepresentable — Mathlib

English

The forgetful functor GrpCat → Type is corepresentable by the same representing object as for groups, i.e. there is a natural isomorphism coyoneda at op(of ULift(ℤ)) ≅ forget GrpCat.

Русский

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

LaTeX

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

Lean4

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

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