liftCycles_homologyπ_eq_zero_of_boundary

English

If k: A → K.X_i is a boundary, i.e. k = x ≫ K.d i' i, then K.liftCycles k j hj (by ...) ≫ K.homologyπ i = 0.

Русский

Если k является границей, то образ поднятой цикла по гомологическим данным исчезает в гомологии: K.liftCycles k j hj (предел) ≫ K.homologyπ i = 0.

LaTeX

$$$K.liftCycles(k,j,hj,hk) \circ K.homology\pi i = 0$$$

Lean4

@[reassoc]
theorem liftCycles_homologyπ_eq_zero_of_boundary {A : C} (k : A ⟶ K.X i) (j : ι) (hj : c.next i = j) {i' : ι}
    (x : A ⟶ K.X i') (hx : k = x ≫ K.d i' i) :
    K.liftCycles k j hj (by rw [hx, assoc, K.d_comp_d, comp_zero]) ≫ K.homologyπ i = 0 :=
  by
  by_cases h : c.Rel i' i
  · obtain rfl := c.prev_eq' h
    exact (K.sc i).liftCycles_homologyπ_eq_zero_of_boundary _ x hx
  · have : liftCycles K k j hj (by rw [hx, assoc, K.d_comp_d, comp_zero]) = 0 :=
      by
      rw [K.shape _ _ h, comp_zero] at hx
      rw [← cancel_mono (K.iCycles i), zero_comp, liftCycles_i, hx]
    rw [this, zero_comp]

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