homEquiv_eq — Mathlib

English

For any X, the homEquiv evaluated at f equals F.map f.op applied to homEquiv at identity X.

Русский

Для любого X: X, значение homEquiv на f равно F.map f.op применённому к homEquiv(id_X).

LaTeX

$$e.homEquiv f = F.map f.op (e.homEquiv (id X))$$

Lean4

theorem homEquiv_eq {F : C ⥤ Type v} {X : C} (e : F.CorepresentableBy X) {Y : C} (f : X ⟶ Y) :
    e.homEquiv f = F.map f (e.homEquiv (𝟙 X)) := by conv_lhs => rw [← Category.id_comp f, e.homEquiv_comp]

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