liftCycles_homologyπ_eq_zero_of_boundary

English

If S has homology and a morphism k factors through boundary data with a boundary relation hx, then lifting cycles followed by the homology projection gives zero.

Русский

Если S имеет гомологию и отображение k факторизуется через граничные данные с соотношением, то подъём циклов, за которым следует гомологический проекции, даёт ноль.

LaTeX

$$S.liftCycles(k, (by rw [hx, assoc, S.zero, comp_zero])) ≫ S.homologyπ = 0$$

Lean4

theorem liftCycles_homologyπ_eq_zero_of_boundary [S.HasHomology] (k : A ⟶ S.X₂) (x : A ⟶ S.X₁) (hx : k = x ≫ S.f) :
    S.liftCycles k (by rw [hx, assoc, S.zero, comp_zero]) ≫ S.homologyπ = 0 :=
  by
  dsimp only [homologyπ]
  rw [S.liftCycles_leftHomologyπ_eq_zero_of_boundary_assoc k x hx, zero_comp]

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