homologyι_descOpcycles_eq_zero_of_boundary

English

If hx: k = S.g ≫ x, then the composition of homologyι with the boundary-desc map descOpcycles applied to k equals zero.

Русский

Если k = S.g ≫ x, то композиция гомологииι с отображением descOpcycles на k равна нулю.

LaTeX

$$S.homologyι ≫ S.descOpcycles k (by rw [hx, S.zero_assoc, zero_comp]) = 0$$

Lean4

@[reassoc]
theorem homologyι_descOpcycles_eq_zero_of_boundary [S.HasHomology] (k : S.X₂ ⟶ A) (x : S.X₃ ⟶ A) (hx : k = S.g ≫ x) :
    S.homologyι ≫ S.descOpcycles k (by rw [hx, S.zero_assoc, zero_comp]) = 0 :=
  by
  dsimp only [homologyι]
  rw [assoc, S.rightHomologyι_descOpcycles_π_eq_zero_of_boundary k x hx, comp_zero]

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