comp_liftCycles — Mathlib

English

LiftCycles is natural in the right argument: for α: A' → A and k: A → K.X_i with hk, we have α ∘ K.liftCycles(k, j, hj, hk) = K.liftCycles(α ∘ k, j, hj, hk').

Русский

LiftCycles естественно относительно правого аргумента: для α: A' → A и k: A → K.X_i с hk мы имеем α ∘ K.liftCycles(k, j, hj, hk) = K.liftCycles(α ∘ k, j, hj, hk'), где hk' эквивалентно hk.

LaTeX

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

Lean4

@[reassoc]
theorem comp_liftCycles {A' A : C} (k : A ⟶ K.X i) (j : ι) (hj : c.next i = j) (hk : k ≫ K.d i j = 0) (α : A' ⟶ A) :
    α ≫ K.liftCycles k j hj hk = K.liftCycles (α ≫ k) j hj (by rw [assoc, hk, comp_zero]) := by
  simp only [← cancel_mono (K.iCycles i), assoc, liftCycles_i]

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