homEquiv_symm_comp — Mathlib

English

For a representable by e with Y and f: X ⟶ Y, the value of e.homEquiv on f equals F.map f.op applied to e.homEquiv(id_Y).

Русский

Для представления e с Y и f: X ⟶ Y значение e.homEquiv на f равно F.map f.op применённому к e.homEquiv(id_Y).

LaTeX

$$e.homEquiv f = F.map f.op (e.homEquiv (id_Y))$$

Lean4

theorem homEquiv_symm_comp {F : C ⥤ Type v} {X : C} (e : F.CorepresentableBy X) {Y Y' : C} (y : F.obj Y) (g : Y ⟶ Y') :
    e.homEquiv.symm y ≫ g = e.homEquiv.symm (F.map g y) :=
  e.homEquiv.injective (by simp [homEquiv_comp])

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