d_comp_eq_zero_iff — Mathlib

English

Relation between previous/next degree morphisms after extending along an embedding, yielding predictable differential behavior.

Русский

Связь между дифференциалами на предшествующей и следующей степенях после расширения вдоль вложения.

LaTeX

$$$K.d\\ i j \\;\\Rightarrow\\; (K.extend e).d i' j' \\text{ via } extendXIso$$$

Lean4

theorem d_comp_eq_zero_iff ⦃W : C⦄ (φ : K.X j ⟶ W) :
    K.d i j ≫ φ = 0 ↔ (K.extend e).d i' j' ≫ (K.extendXIso e hj').hom ≫ φ = 0 :=
  by
  by_cases hij : c.Rel i j
  · have hi' : e.f i = i' := by rw [← hi', ← hj', c'.prev_eq' (e.rel hij)]
    rw [K.extend_d_eq e hi' hj', assoc, assoc, Iso.inv_hom_id_assoc, ← cancel_epi (K.extendXIso e hi').hom, comp_zero]
  · simp only [K.shape _ _ hij, zero_comp, true_iff]
    rw [K.extend_d_to_eq_zero e i' j' j hj', zero_comp]
    rw [hi]
    exact hij

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