unitAuxAuxAux — Mathlib

English

Intermediate stage providing an isomorphism between YonedaCollection (restrictedYonedaObj η) X and F.obj (op X).

Русский

Промежуточная стадия, задающая изоморфизм между YonedaCollection (restrictedYonedaObj η) X и F.obj (op X).

LaTeX

$$$$ \operatorname{YonedaCollection}(\operatorname{restrictedYonedaObj}\eta)X \cong F(\operatorname{op}X) $$$$

Lean4

/-- Intermediate stage of assembling the unit. -/
@[simps]
def unitAuxAuxAux {F : Cᵒᵖ ⥤ Type v} (η : F ⟶ A) (X : C) : YonedaCollection (restrictedYonedaObj η) X ≅ F.obj (op X)
    where
  hom := unitForward η X
  inv := unitBackward η X
  hom_inv_id := unitBackward_unitForward η X
  inv_hom_id := unitForward_unitBackward η X

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