singleObjCyclesSelfIso — Mathlib

English

The map component at degree zero of the single₀ map is exactly the original morphism f.

Русский

Компонента отображения в нулевой степени у single₀ map равна исходному морфизму f.

LaTeX

$$$(\\mathrm{single}_0 V).\\mathrm{map} f)_0 = f$$$

Lean4

/-- The canonical isomorphism `((single C c j).obj A).cycles j ≅ A` -/
noncomputable def singleObjCyclesSelfIso : ((single C c j).obj A).cycles j ≅ A :=
  ((single C c j).obj A).iCyclesIso j _ rfl rfl ≪≫ singleObjXSelf c j A

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