descOpcycles_comp — Mathlib

English

descOpcycles is functorial in the right argument: (k ≫ α) adjust, giving equality with a new hk; specifically K.descOpcycles k j hj hk ≫ α = K.descOpcycles (k ≫ α) j hj (by rw ...).

Русский

DescOpcycles естественно по правому аргументу: (k ∘ α) дает эквивалентное выражение для новой hk.

LaTeX

$$$K.descOpcycles(k,j,hj,hk) \circ \alpha = K.descOpcycles(k \circ \alpha, j, hj, hk')$$$

Lean4

@[reassoc]
theorem descOpcycles_comp {A A' : C} (k : K.X i ⟶ A) (j : ι) (hj : c.prev i = j) (hk : K.d j i ≫ k = 0) (α : A ⟶ A') :
    K.descOpcycles k j hj hk ≫ α = K.descOpcycles (k ≫ α) j hj (by rw [reassoc_of% hk, zero_comp]) := by
  simp only [← cancel_epi (K.pOpcycles i), p_descOpcycles_assoc, p_descOpcycles]

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