homologyι_descOpcycles_eq_zero_of_boundary

English

For k: K.X i → A and j, with hi, given hx: k = d i i' ≫ x, we have K.homologyι i ≫ K.descOpcycles k j hi (by rw ...) = 0.

Русский

Для k, являющегося границей, композиция гомологического отображения с descOpcycles равна нулю.

LaTeX

$$$K.homology\iota i \circ K.descOpcycles(k,j,hj, ) = 0$$$

Lean4

@[reassoc]
theorem homologyι_descOpcycles_eq_zero_of_boundary {A : C} (k : K.X i ⟶ A) (j : ι) (hj : c.prev i = j) {i' : ι}
    (x : K.X i' ⟶ A) (hx : k = K.d i i' ≫ x) :
    K.homologyι i ≫ K.descOpcycles k j hj (by rw [hx, K.d_comp_d_assoc, zero_comp]) = 0 :=
  by
  by_cases h : c.Rel i i'
  · obtain rfl := c.next_eq' h
    exact (K.sc i).homologyι_descOpcycles_eq_zero_of_boundary _ x hx
  · have : K.descOpcycles k j hj (by rw [hx, K.d_comp_d_assoc, zero_comp]) = 0 :=
      by
      rw [K.shape _ _ h, zero_comp] at hx
      rw [← cancel_epi (K.pOpcycles i), comp_zero, p_descOpcycles, hx]
    rw [this, comp_zero]

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