alternatingFaceMapComplexConst — Mathlib

English

Odd-case iCycles map is zero when composed with ψ.

Русский

Нечётный случай: iCycles-компонента композиция с ψ равна нулю.

LaTeX

$$$((\mathrm{alternatingConst}\; A\; hOdd\; hEven\; hc).iCycles\, j)\;\circ ψ = 0$$$

Lean4

/-- The alternating face complex of the constant complex is the alternating constant complex. -/
noncomputable def alternatingFaceMapComplexConst :
    Functor.const _ ⋙ alternatingFaceMapComplex C ≅ ChainComplex.alternatingConst :=
  NatIso.ofComponents
    (fun X ↦
      HomologicalComplex.Hom.isoOfComponents (fun _ ↦ Iso.refl _) <|
        by
        rintro _ i rfl
        simp [SimplicialObject.δ, ← Finset.sum_smul, Fin.sum_neg_one_pow, Nat.even_add_one, -Nat.not_even_iff_odd])
    (by intros; ext; simp)

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