homotopyPToId_eventually_constant

English

Let X be a simplicial object in a preadditive category. For natural numbers n and q with n < q, the n-th component of the homotopy from P to Id does not depend on q once q is large enough; i.e., for q > n, the (n, n+1) component of the homotopy from X to Id stabilizes: (homotopyPToId X (q+1)).hom n (n+1) = (homotopyPToId X q).hom n (n+1).

Русский

Пусть X — симплициальный объект в абелевой/покрывающейся категории. Для натуральных чисел n и q с n < q компонентом (?) гомотопии от P к Id на уровне (n, n+1) является независимый от q при sufficiently large q: если q > n, то (homotopyPToId X (q+1)).hom n (n+1) = (homotopyPToId X q).hom n (n+1).

LaTeX

$$$\text{Пусть } X\text{ — симпликсиальный объект в приближённой абелевой/препредопределённой категории. Тогда для всех } n,q\text{ с } n

Lean4

theorem homotopyPToId_eventually_constant {q n : ℕ} (hqn : n < q) :
    ((homotopyPToId X (q + 1)).hom n (n + 1) : X _⦋n⦌ ⟶ X _⦋n + 1⦌) = (homotopyPToId X q).hom n (n + 1) := by
  simp only [homotopyHσToZero, AlternatingFaceMapComplex.obj_X, Homotopy.trans_hom, Homotopy.ofEq_hom, Pi.zero_apply,
    Homotopy.add_hom, Homotopy.compLeft_hom, add_zero, Homotopy.nullHomotopy'_hom, ComplexShape.down_Rel,
    hσ'_eq_zero hqn (c_mk (n + 1) n rfl), dite_eq_ite, ite_self, comp_zero, zero_add, homotopyPToId]

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