singleMapHomologicalComplex_inv_app_self

English

For each j, the f-component of the inverse at X is given by composing the homomorphism of the self-isomorphism of the object X with the map induced by F on the inverse of the self-map.

Русский

Для каждого j компонента f в обратном отображении на X задаётся композиция гомоморфизма самосвязи объекта X с отображением, индуцированным F на обратное отображение self-map.

LaTeX

$$$((\mathrm{singleMapHomologicalComplex} F \ c \ j).\mathrm{inv}.\mathrm{app} \ X).f_j = (\mathrm{singleObjXSelf} \ c \ j \ (F.\mathrm{obj} X)).hom \circ F( (\mathrm{singleObjXSelf} \ c \ j \ X).inv ).$$$

Lean4

@[simp]
theorem singleMapHomologicalComplex_inv_app_self (j : ι) (X : W₁) :
    ((singleMapHomologicalComplex F c j).inv.app X).f j =
      (singleObjXSelf c j (F.obj X)).hom ≫ F.map (singleObjXSelf c j X).inv :=
  by simp [singleMapHomologicalComplex, singleObjXSelf, singleObjXIsoOfEq, eqToHom_map]

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