pOpcycles_opcyclesIsoSc'_hom — Mathlib

English

The inverse of opcycles-iso followed by fromOpcycles yields the corresponding fromOpcycles map.

Русский

Обратное изоморфирование opcycles, применённое к fromOpcycles, даёт соответствующее fromOpcycles.

LaTeX

$$$ (K.opcyclesIsoSc' i j k hi hk).inv \circ K.fromOpcycles j k = (K.sc' i j k).fromOpcycles $$$

Lean4

@[reassoc (attr := simp)]
theorem pOpcycles_opcyclesIsoSc'_hom : K.pOpcycles j ≫ (K.opcyclesIsoSc' i j k hi hk).hom = (K.sc' i j k).pOpcycles :=
  by
  dsimp [opcyclesIsoSc']
  erw [ShortComplex.p_opcyclesMap]
  apply id_comp

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