representableByEquiv — Mathlib

English

For a RepresentableBy object e of F with Y, and for X,X' in C, and x in F.obj(op X'), the relation f ≫ e.homEquiv.symm x = e.homEquiv.symm (F.map f.op x) holds for any morphism f: X ⟶ X'.

Русский

Для e: F.RepresentableBy Y над F, и любых X,X' в C, и x∈F.obj(op X'), верно f ≫ e.homEquiv.symm x = e.homEquiv.symm (F.map f.op x) для любого f: X ⟶ X'.

LaTeX

$$f ≫ e.homEquiv.symm x = e.homEquiv.symm (F.map f.op x)$$

Lean4

/-- The obvious bijection `F.RepresentableBy Y ≃ (yoneda.obj Y ≅ F)`
when `F : Cᵒᵖ ⥤ Type v₁` and `[Category.{v₁} C]`. -/
def representableByEquiv {F : Cᵒᵖ ⥤ Type v₁} {Y : C} : F.RepresentableBy Y ≃ (yoneda.obj Y ≅ F)
    where
  toFun
    r :=
    NatIso.ofComponents (fun _ ↦ r.homEquiv.toIso)
      (fun {X X'} f ↦ by
        ext g
        simp [r.homEquiv_comp])
  invFun
    e :=
    { homEquiv := (e.app _).toEquiv
      homEquiv_comp := fun {X X'} f g ↦ congr_fun (e.hom.naturality f.op) g }

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