liftCycles_comp_cyclesMap — Mathlib

English

For any k: A → K.X i and φ: K → L, the lifting of cycles commutes with cycles maps up to φ: K.liftCycles k j hj hk ≫ cyclesMap φ i = L.liftCycles (k ≫ φ.f i) j hj (compatibility).

Русский

Для любого k: A → K.X i и φ: K → L подстановка подъема циклов коммутирует с отображением циклов: K.liftCycles k j hj hk ≫ cyclesMap φ i = L.liftCycles (k ≫ φ.f i) j hj.

LaTeX

$$$$ K.liftCycles(k,j,hj,hk) \;\circ\; cyclesMap(\varphi,i) = L.liftCycles(k \circ \varphi.f i, j, hj) $$$$

Lean4

@[reassoc (attr := simp)]
theorem liftCycles_comp_cyclesMap {A : C} (k : A ⟶ K.X i) (j : ι) (hj : c.next i = j) (hk : k ≫ K.d i j = 0)
    (φ : K ⟶ L) :
    K.liftCycles k j hj hk ≫ cyclesMap φ i =
      L.liftCycles (k ≫ φ.f i) j hj (by rw [assoc, φ.comm, reassoc_of% hk, zero_comp]) :=
  by simp only [← cancel_mono (L.iCycles i), assoc, cyclesMap_i, liftCycles_i_assoc, liftCycles_i]

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