singleObjCyclesSelfIso_inv_iCycles

English

For any C and X with hf, the zero-th component of the inverse image equals f.

Русский

Для любых C и X с hf нулевая компонента образа через обратное отобразение равна f.

LaTeX

$$$((\\mathrm{fromSingle}_0^{\\mathrm{Equiv}} C X)^{-1} \\langle f, hf \\rangle)_0 = f$$$

Lean4

@[reassoc (attr := simp)]
theorem singleObjCyclesSelfIso_inv_iCycles :
    (singleObjCyclesSelfIso _ _ _).inv ≫ ((single C c j).obj A).iCycles j = (singleObjXSelf c j A).inv := by
  simp [singleObjCyclesSelfIso]

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