comp_eq_zero — Mathlib

English

If S is exact, then for any a, b with a ≫ g = 0 and f ≫ b = 0, we have a ≫ b = 0.

Русский

Если S точен, то для любых a, b с a ≫ g = 0 и f ≫ b = 0 выполняется a ≫ b = 0.

LaTeX

$$$ a \\!\\circ b = 0 \\quad \\text{under } a \\circ g = 0, \\; f \\circ b = 0 $$$

Lean4

@[reassoc]
theorem comp_eq_zero (h : S.Exact) {X Y : C} {a : X ⟶ S.X₂} (ha : a ≫ S.g = 0) {b : S.X₂ ⟶ Y} (hb : S.f ≫ b = 0) :
    a ≫ b = 0 := by
  have := h.hasHomology
  have eq := h
  rw [exact_iff_iCycles_pOpcycles_zero] at eq
  rw [← S.liftCycles_i a ha, ← S.p_descOpcycles b hb, assoc, reassoc_of% eq, zero_comp, comp_zero]

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