homEquiv_eq — Mathlib

English

Extensionality for representable objects: equality of homEquiv at identity implies equality of the representable data.

Русский

Расширенная эквивалентность для представимых объектов: равенство h omEquiv на единичном морфизме имплицирует равенство представляемой информации.

LaTeX

$$ext {F : C^{op} ⥤ Type v} {X} {e e' : F.RepresentableBy X} (h : e.homEquiv (1_X) = e'.homEquiv (1_X)) : e = e'$$

Lean4

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

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