comp_homEquiv_symm — Mathlib

English

For a representable by F with position Y, and for X,X', an element x in F.obj(op X') and a morphism f: X ⟶ X', one has f ≫ e.homEquiv.symm(x) = e.homEquiv.symm(F.map f.op (x)).

Русский

Для F, допускающего представление в Y, при X, X' и x ∈ F.obj(op X'), а также f: X ⟶ X', выполняется равенство f ∘ e.homEquiv.symm(x) = e.homEquiv.symm(F.map f.op(x)).

LaTeX

$$$ f \; \gg e.homEquiv.symm x = e.homEquiv.symm (F.map f.op x)$$$

Lean4

theorem comp_homEquiv_symm {F : Cᵒᵖ ⥤ Type v} {Y : C} (e : F.RepresentableBy Y) {X X' : C} (x : F.obj (op X'))
    (f : X ⟶ X') : f ≫ e.homEquiv.symm x = e.homEquiv.symm (F.map f.op x) :=
  e.homEquiv.injective (by simp [homEquiv_comp])

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