inclusionOfMooreComplexMap — Mathlib

English

There is a canonical inclusion map from the normalized Moore complex of a simplicial object into the alternating face map complex, for each X.

Русский

Существуют канонические включения от нормализованного Moore-цепочного комплекса к иначе сформированному массиву чётной/чередующейся структуры для каждого X.

LaTeX

$$$\text{inclusionOfMooreComplexMap} : (\text{normalizedMooreComplex } A).\mathrm{obj}\; X \longrightarrow (\text{alternatingFaceMapComplex } A).\mathrm{obj}\; X$$$

Lean4

/-- The inclusion map of the Moore complex in the alternating face map complex -/
def inclusionOfMooreComplexMap (X : SimplicialObject A) :
    (normalizedMooreComplex A).obj X ⟶ (alternatingFaceMapComplex A).obj X :=
  by
  dsimp only [normalizedMooreComplex, NormalizedMooreComplex.obj, alternatingFaceMapComplex,
    AlternatingFaceMapComplex.obj]
  apply
    ChainComplex.ofHom _ _ _ _ _ _
      (fun n => (NormalizedMooreComplex.objX X n).arrow)
        /- we have to show the compatibility of the differentials on the alternating
                   face map complex with those defined on the normalized Moore complex:
                   we first get rid of the terms of the alternating sum that are obviously
                   zero on the normalized_Moore_complex -/

  intro i
  simp only [AlternatingFaceMapComplex.objD, comp_sum]
  rw [Fin.sum_univ_succ, Fintype.sum_eq_zero]
  swap
  · intro j
    rw [NormalizedMooreComplex.objX_add_one, comp_zsmul, ←
      factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ _ (Finset.mem_univ j)), Category.assoc,
      kernelSubobject_arrow_comp, comp_zero, smul_zero]
      -- finally, we study the remaining term which is induced by X.δ 0

  rw [add_zero, Fin.val_zero, pow_zero, one_zsmul]
  dsimp [NormalizedMooreComplex.objD, NormalizedMooreComplex.objX]
  cases i <;> simp

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