essImage_yonedaMon — Mathlib

English

The essImage of the Yoneda Mon object functor coincides with the preimage under forgetful functor of representable functors.

Русский

EssImage у Yoneda Mon совпадает с предобразом под забывчивым функтором от представимых функторов.

LaTeX

$$$\\yonedaMon.essImage = (\\cdot \\circ \\mathrm{forget}_{MonCat})^{-1}'(\\{\\text{IsRepresentable}\})$$$

Lean4

theorem essImage_yonedaMon : yonedaMon (C := C).essImage = (· ⋙ forget _) ⁻¹' setOf Functor.IsRepresentable :=
  by
  ext F
  constructor
  · rintro ⟨M, ⟨α⟩⟩
    exact ⟨M.X, ⟨Functor.representableByEquiv.symm (Functor.isoWhiskerRight α (forget _))⟩⟩
  · rintro ⟨X, ⟨e⟩⟩
    letI := MonObj.ofRepresentableBy X F e
    exact ⟨Mon.mk X, ⟨yonedaMonObjIsoOfRepresentableBy X F e⟩⟩

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