rightHomologyι_descOpcycles_π_eq_zero_of_boundary

English

If k = S.g ≫ x for some x, then rightHomologyι ≫ descOpcycles k = 0.

Русский

Если k = S.g ∘ x для некоторого x, то rightHomologyι ∘ descOpcycles k = 0.

LaTeX

$$$\\mathrm{rightHomology\\}\\iota \\; \\circ \\; \\mathrm{descOpcycles}\\ k = 0$$$

Lean4

@[reassoc]
theorem rightHomologyι_descOpcycles_π_eq_zero_of_boundary (x : S.X₃ ⟶ A) (hx : k = S.g ≫ x) :
    S.rightHomologyι ≫ S.descOpcycles k (by rw [hx, S.zero_assoc, zero_comp]) = 0 :=
  RightHomologyData.ι_descQ_eq_zero_of_boundary _ k x hx

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