English
If X is an augmented simplicial object with an extra degeneracy in a preadditive category with zero object, then the augmentation on the alternating face map complex is a homotopy equivalence.
Русский
Если X — дополненный симплициальный объект в прeддитивной категории с нулевым объектом, и у него есть дополнительное развёртывание, то дополнение на комплексах чередующихся лиц является гомотопической эквивалентностью.
LaTeX
$$$\text{homotopyEquiv}(\mathrm{AlternatingFaceMapComplex}(\mathrm{drop}(X))) \simeq (\mathrm{ChainComplex})_{single_0}(\mathrm{point}(X))$$$
Lean4
/-- If `C` is a preadditive category and `X` is an augmented simplicial object
in `C` that has an extra degeneracy, then the augmentation on the alternating
face map complex of `X` is a homotopy equivalence. -/
noncomputable def homotopyEquiv [Preadditive C] [HasZeroObject C] {X : SimplicialObject.Augmented C}
(ed : ExtraDegeneracy X) :
HomotopyEquiv (AlgebraicTopology.AlternatingFaceMapComplex.obj (drop.obj X))
((ChainComplex.single₀ C).obj (point.obj X))
where
hom := AlternatingFaceMapComplex.ε.app X
inv := (ChainComplex.fromSingle₀Equiv _ _).symm (by exact ed.s')
homotopyInvHomId :=
Homotopy.ofEq
(by
ext
dsimp
erw [AlternatingFaceMapComplex.ε_app_f_zero, ChainComplex.fromSingle₀Equiv_symm_apply_f_zero, s'_comp_ε]
rfl)
homotopyHomInvId :=
{ hom i := Pi.single (i + 1) (-ed.s i)
zero i j hij := Pi.single_eq_of_ne (Ne.symm hij) _
comm
i := by
cases i with
| zero =>
rw [Homotopy.prevD_chainComplex, Homotopy.dNext_zero_chainComplex, zero_add]
dsimp
erw [ChainComplex.fromSingle₀Equiv_symm_apply_f_zero]
simp only [AlternatingFaceMapComplex.obj_d_eq]
rw [Fin.sum_univ_two]
simp [s_comp_δ₀, s₀_comp_δ₁]
| succ i =>
rw [Homotopy.prevD_chainComplex, Homotopy.dNext_succ_chainComplex]
simp [Fin.sum_univ_succ (n := i + 2), s_comp_δ₀, Preadditive.sum_comp, Preadditive.comp_sum, s_comp_δ,
pow_succ] }
