descOpcycles_comp — Mathlib

English

For φ, h, the relation (ofEpiOfIsIsoOfMono' φ h).g' = h.g' ≫ φ.τ3 holds.

Русский

Для φ и h выполняется равенство (ofEpiOfIsIsoOfMono' φ h).g' = h.g' ≫ φ.τ3.

LaTeX

$$$(\\mathrm{ofEpiOfIsIsoOfMono'}\\ φ\\ h).g' = h.g' \\circ φ.τ_3$$$

Lean4

@[reassoc]
theorem descOpcycles_comp {A' : C} (α : A ⟶ A') :
    S.descOpcycles k hk ≫ α = S.descOpcycles (k ≫ α) (by rw [reassoc_of% hk, zero_comp]) := by
  simp only [← cancel_epi S.pOpcycles, p_descOpcycles_assoc, p_descOpcycles]

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