pOpcycles_restrictionOpcyclesIso_inv

English

If K has homology at j′, then the restricted complex K.restriction e has homology at j.

Русский

Если у K есть гомология в позиции j′, то ограниченное по e K.restriction имеет гомологию в позиции j.

LaTeX

$$$$ [K.HasHomology j'] \Rightarrow (K.restriction e).HasHomology j $$$$

Lean4

@[reassoc (attr := simp)]
theorem pOpcycles_restrictionOpcyclesIso_inv :
    K.pOpcycles j' ≫ (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').inv =
      (K.restrictionXIso e hj').inv ≫ (K.restriction e).pOpcycles j :=
  by simp [restrictionOpcyclesIso]

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