liftCycles_i — Mathlib

English

For a fixed i, and any k: A → K.X_i with certain vanishing d_i j, the equality (K.liftCycles k j hj hk) ≫ K.iCycles i = k holds.

Русский

Для фиксированного i и любого k: A → K.X_i с условием, что d_i j = 0, выполняется равенство (K.liftCycles k j hj hk) ≫ K.iCycles i = k.

LaTeX

$$$K.liftCycles k j hj hk \;\; \Rightarrow \; K.liftCycles k j hj hk \;\circ K.iCycles i = k$$$

Lean4

@[reassoc (attr := simp)]
theorem liftCycles_i {A : C} (k : A ⟶ K.X i) (j : ι) (hj : c.next i = j) (hk : k ≫ K.d i j = 0) :
    K.liftCycles k j hj hk ≫ K.iCycles i = k :=
  by
  dsimp [liftCycles, iCycles]
  simp

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