English
Given a morphism φ: K → L and a map k: L.X i → A with certain compatibility conditions (j, hj, hk), the induced opcycles map intertwines with the descOpcycles maps: opcyclesMap φ i ≫ L.descOpcycles k j hj hk = K.descOpcycles (φ.f i ≫ k) j hj.
Русский
При наличии морфизма φ: K → L и отображения k: L.X i → A с определёнными условиями совместимости, полученные отображения opcycles и descOpcycles взаимно согласованы: opcyclesMap φ i ≫ L.descOpcycles k j hj hk = K.descOpcycles (φ.f i ≫ k) j hj.
LaTeX
$$$$ opcyclesMap(\varphi,i) \;\circ\; L.descOpcycles(k,j, hj,hk) = K.descOpcycles( (\varphi.f i) \circ k , j, hj ) $$$$
Lean4
@[reassoc (attr := simp)]
theorem opcyclesMap_comp_descOpcycles {A : C} (k : L.X i ⟶ A) (j : ι) (hj : c.prev i = j) (hk : L.d j i ≫ k = 0)
(φ : K ⟶ L) :
opcyclesMap φ i ≫ L.descOpcycles k j hj hk =
K.descOpcycles (φ.f i ≫ k) j hj (by rw [← φ.comm_assoc, hk, comp_zero]) :=
by simp only [← cancel_epi (K.pOpcycles i), p_opcyclesMap_assoc, p_descOpcycles]
