essImage_yonedaGrp — Mathlib

English

The essential image of yonedaGrp coincides with the preimage under forgetful functor of the representable functors.

Русский

Необходимое изображение yonedaGrp совпадает с предобразом по забыванию от представимых функторов.

LaTeX

$$$yonedaGrp.essImage = (\cdot \downarrow \forget GrpCat)^{-1}(\{\text{IsRepresentable}\})$$$

Lean4

theorem essImage_yonedaGrp : yonedaGrp (C := C).essImage = (· ⋙ forget _) ⁻¹' setOf Functor.IsRepresentable :=
  by
  ext F
  constructor
  · rintro ⟨G, ⟨α⟩⟩
    exact ⟨G.X, ⟨Functor.representableByEquiv.symm (Functor.isoWhiskerRight α (forget _))⟩⟩
  · rintro ⟨X, ⟨e⟩⟩
    letI := GrpObj.ofRepresentableBy X F e
    exact ⟨⟨X⟩, ⟨yonedaGrpObjIsoOfRepresentableBy X F e⟩⟩

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