Simplicial cochains as functions on simplices

For a ring k and a k-module M, evaluation on the unit chain of each simplex identifies Hom_k(C_n(K; k), M) with functions from the n-simplices of K to M. This identification is integral-linear, including for noncommutative rings. The cochain differential becomes the alternating sum of values on faces, and pullback becomes precomposition on simplices.

The construction uses Mathlib's SSet.isColimitChainComplexXCofan and Cofan.IsColimit.desc, the coproduct universal property also used by TauCeti.chainsDesc. These coordinates allow comparison of coefficient rings without changing cochain values. Over a commutative ring they are k-linear (TauCeti.cochainValuesLinearEquiv).

References

• A. Hatcher, Algebraic Topology, Section 3.1.

noncomputable def TauCeti.cochainValuesEquiv (k : Type w) [Ring k] (M : ModuleCat k) (K : SSet) (n : ℕ) : ((K.chainComplex ↧k).X n ⟶ M) ≃ₗ[ℤ] K.obj (Opposite.op { len := n }) → ↑M

Evaluation on unit simplex chains identifies simplicial cochains with functions on simplices, as modules over the integers.

@[simp]

theorem TauCeti.cochainValuesEquiv_apply (k : Type w) [Ring k] (M : ModuleCat k) (K : SSet) (n : ℕ) (φ : (K.chainComplex ↧k).X n ⟶ M) (σ : K.obj (Opposite.op { len := n })) : (cochainValuesEquiv k M K n) φ σ = (CategoryTheory.ConcreteCategory.hom φ) ((CategoryTheory.ConcreteCategory.hom (K.ιChainComplex σ)) 1)

The value coordinate of a cochain is its value on the unit chain of the simplex.

@[simp]

theorem TauCeti.cochainValuesEquiv_symm_apply (k : Type w) [Ring k] (M : ModuleCat k) (K : SSet) (n : ℕ) (v : K.obj (Opposite.op { len := n }) → ↑M) (σ : K.obj (Opposite.op { len := n })) (a : k) : (CategoryTheory.ConcreteCategory.hom ((cochainValuesEquiv k M K n).symm v)) ((CategoryTheory.ConcreteCategory.hom (K.ιChainComplex σ)) a) = a • v σ

The cochain with prescribed values evaluates a simplex with coefficient a to a times its prescribed value.

theorem TauCeti.cochainValuesEquiv_d (k : Type w) [Ring k] (M : ModuleCat k) (K : SSet) (n : ℕ) (φ : (K.chainComplex ↧k).X n ⟶ M) (σ : K.obj (Opposite.op { len := n + 1 })) : (cochainValuesEquiv k M K (n + 1)) (CategoryTheory.CategoryStruct.comp ((K.chainComplex ↧k).d (n + 1) n) φ) σ = ∑ i : Fin (n + 2), (-1) ^ ↑i • (cochainValuesEquiv k M K n) φ ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ K i)) σ)

The cochain differential, in simplex coordinates, is the alternating sum over faces.

theorem TauCeti.cochainValuesEquiv_chainComplexMap (k : Type w) [Ring k] (M : ModuleCat k) (K : SSet) {L : SSet} (f : K ⟶ L) (n : ℕ) (φ : (L.chainComplex ↧k).X n ⟶ M) (σ : K.obj (Opposite.op { len := n })) : (cochainValuesEquiv k M K n) (CategoryTheory.CategoryStruct.comp ((SSet.chainComplexMap f ↧k).f n) φ) σ = (cochainValuesEquiv k M L n) φ ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op { len := n }))) σ)

Pullback of cochains is precomposition of their value functions with the simplicial map.

noncomputable def TauCeti.cochainValuesLinearEquiv (k : Type w) [CommRing k] (M : ModuleCat k) (K : SSet) (n : ℕ) : ((K.chainComplex ↧k).X n ⟶ M) ≃ₗ[k] K.obj (Opposite.op { len := n }) → ↑M

For a commutative ring k, the identification TauCeti.cochainValuesEquiv of cochains with functions on simplices is k-linear.

@[simp]

theorem TauCeti.coe_cochainValuesLinearEquiv (k : Type w) [CommRing k] (M : ModuleCat k) (K : SSet) (n : ℕ) : ⇑(cochainValuesLinearEquiv k M K n) = ⇑(cochainValuesEquiv k M K n)

@[simp]

theorem TauCeti.coe_cochainValuesLinearEquiv_symm (k : Type w) [CommRing k] (M : ModuleCat k) (K : SSet) (n : ℕ) : ⇑(cochainValuesLinearEquiv k M K n).symm = ⇑(cochainValuesEquiv k M K n).symm

theorem TauCeti.cochainValuesEquiv_linearYonedaObj_d (k : Type w) [CommRing k] (M : ModuleCat k) (K : SSet) (n : ℕ) (φ : ↑(((K.chainComplex ↧k).linearYonedaObj k M).X n)) (σ : K.obj (Opposite.op { len := n + 1 })) : (cochainValuesEquiv k M K (n + 1)) ((CategoryTheory.ConcreteCategory.hom (((K.chainComplex ↧k).linearYonedaObj k M).d n (n + 1))) φ) σ = ∑ i : Fin (n + 2), (-1) ^ ↑i • (cochainValuesEquiv k M K n) φ ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ K i)) σ)

The values of the coboundary of a cochain in Hom(C(K; k), M) are alternating sums of its values on faces.