comp_d_eq_zero_iff — Mathlib

English

Equivalence of zero-condition for extended differential composed with a map in the extended complex when considering predecessors and successors.

Русский

Эквивалентность условия нулевого состава расширенного дифференциала с картой в расширенном комплексе, с учётом предшествующих и последующих.

LaTeX

$$$\\text{comp\\_d\\_eq\\_zero\\_iff}$$$

Lean4

theorem comp_d_eq_zero_iff ⦃W : C⦄ (φ : W ⟶ K.X j) :
    φ ≫ K.d j k = 0 ↔ φ ≫ (K.extendXIso e hj').inv ≫ (K.extend e).d j' k' = 0 :=
  by
  by_cases hjk : c.Rel j k
  · have hk' : e.f k = k' := by rw [← hk', ← hj', c'.next_eq' (e.rel hjk)]
    rw [K.extend_d_eq e hj' hk', Iso.inv_hom_id_assoc, ← cancel_mono (K.extendXIso e hk').inv, zero_comp, assoc]
  · simp only [K.shape _ _ hjk, comp_zero, true_iff]
    rw [K.extend_d_from_eq_zero e j' k' j hj', comp_zero, comp_zero]
    rw [hk]
    exact hjk

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