liftCycles_leftHomologyπ_eq_zero_of_boundary

English

If k = boundary, then liftCycles k hk ≫ leftHomologyπ = 0.

Русский

Если k является границей, то liftCycles k hk ≫ leftHomologyπ = 0.

LaTeX

$$$S.liftCycles\,k\,hk \circ S.leftHomology\pi = 0$$$

Lean4

@[reassoc]
theorem liftCycles_leftHomologyπ_eq_zero_of_boundary (x : A ⟶ S.X₁) (hx : k = x ≫ S.f) :
    S.liftCycles k (by rw [hx, assoc, S.zero, comp_zero]) ≫ S.leftHomologyπ = 0 :=
  LeftHomologyData.liftK_π_eq_zero_of_boundary _ k x hx

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