Locally constant multiplication on singular chains

A locally constant natural-number-valued function acts on singular chains by multiplying each simplex by its value at any point of that simplex. The value is independent of the point, since a simplex is connected. The action commutes with the boundary and with continuous maps when the functions are pulled back. On a connected subspace it is ordinary multiplication by one natural number.

This is the chain operation needed to express the transfer formula for coverings of variable degree. We use Mathlib's coproduct presentation SSet.isColimitChainComplexXCofan and its alternating boundary formula. See Hatcher, Algebraic Topology, Section 3.G, for transfer.

noncomputable def TauCeti.singularChainLocallyConstantNsmul {B : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (R : C) (d : LocallyConstant ↑B ℕ) : (TopCat.toSSet.obj B).chainComplex R ⟶ (TopCat.toSSet.obj B).chainComplex R

Multiplication on singular chains by a locally constant natural-number-valued function. On a singular simplex it multiplies by the value at the initial vertex.

theorem TauCeti.ιChainComplex_singularChainLocallyConstantNsmul_f {B : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (R : C) (d : LocallyConstant ↑B ℕ) {n : ℕ} (σ : (TopCat.toSSet.obj B).obj (Opposite.op { len := n })) (x : ↑(SimplexCategory.toTop.{w}.obj { len := n })) : CategoryTheory.CategoryStruct.comp ((TopCat.toSSet.obj B).ιChainComplex σ) ((singularChainLocallyConstantNsmul R d).f n) = d ((TopCat.simplexMap σ) x) • (TopCat.toSSet.obj B).ιChainComplex σ

On the summand of a simplex, locally constant multiplication is multiplication by its value at any chosen point of the simplex.

theorem TauCeti.ιChainComplex_singularChainLocallyConstantNsmul_f_assoc {B : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (R : C) (d : LocallyConstant ↑B ℕ) {n : ℕ} (σ : (TopCat.toSSet.obj B).obj (Opposite.op { len := n })) (x : ↑(SimplexCategory.toTop.{w}.obj { len := n })) {Z : C} (h : ((TopCat.toSSet.obj B).chainComplex R).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp ((TopCat.toSSet.obj B).ιChainComplex σ) (CategoryTheory.CategoryStruct.comp ((singularChainLocallyConstantNsmul R d).f n) h) = CategoryTheory.CategoryStruct.comp (d ((TopCat.simplexMap σ) x) • (TopCat.toSSet.obj B).ιChainComplex σ) h

On the summand of a simplex, locally constant multiplication is multiplication by its value at any chosen point of the simplex.

@[simp]

theorem TauCeti.ιChainComplex_singularChainLocallyConstantNsmul_f_initial {B : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (R : C) (d : LocallyConstant ↑B ℕ) {n : ℕ} (σ : (TopCat.toSSet.obj B).obj (Opposite.op { len := n })) : CategoryTheory.CategoryStruct.comp ((TopCat.toSSet.obj B).ιChainComplex σ) ((singularChainLocallyConstantNsmul R d).f n) = d ((TopCat.simplexMap σ) (Opposite.unop (Opposite.op { len := n })).toTopInitialVertex) • (TopCat.toSSet.obj B).ιChainComplex σ

The canonical computation rule uses the initial vertex.

@[simp]

theorem TauCeti.ιChainComplex_singularChainLocallyConstantNsmul_f_initial_assoc {B : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (R : C) (d : LocallyConstant ↑B ℕ) {n : ℕ} (σ : (TopCat.toSSet.obj B).obj (Opposite.op { len := n })) {Z : C} (h : ((TopCat.toSSet.obj B).chainComplex R).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp ((TopCat.toSSet.obj B).ιChainComplex σ) (CategoryTheory.CategoryStruct.comp ((singularChainLocallyConstantNsmul R d).f n) h) = CategoryTheory.CategoryStruct.comp (d ((TopCat.simplexMap σ) { len := n }.toTopInitialVertex) • (TopCat.toSSet.obj B).ιChainComplex σ) h

The canonical computation rule uses the initial vertex.

@[simp]

theorem TauCeti.singularChainLocallyConstantNsmul_const {B : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (R : C) (d : ℕ) : singularChainLocallyConstantNsmul R (LocallyConstant.const (↑B) d) = d • CategoryTheory.CategoryStruct.id ((TopCat.toSSet.obj B).chainComplex R)

A constant function acts by ordinary multiplication on the whole chain complex.

theorem TauCeti.singularChainLocallyConstantNsmul_naturality {B Y : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (R : C) (f : Y ⟶ B) (d : LocallyConstant ↑B ℕ) : CategoryTheory.CategoryStruct.comp (singularChainLocallyConstantNsmul R (LocallyConstant.comap (TopCat.Hom.hom f) d)) (SSet.chainComplexMap (TopCat.toSSet.map f) R) = CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (TopCat.toSSet.map f) R) (singularChainLocallyConstantNsmul R d)

Locally constant multiplication commutes with push-forward after pulling back the function along the continuous map.

theorem TauCeti.singularChainLocallyConstantNsmul_naturality_assoc {B Y : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (R : C) (f : Y ⟶ B) (d : LocallyConstant ↑B ℕ) {Z : ChainComplex C ℕ} (h : (TopCat.toSSet.obj B).chainComplex R ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularChainLocallyConstantNsmul R (LocallyConstant.comap (TopCat.Hom.hom f) d)) (CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (TopCat.toSSet.map f) R) h) = CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (TopCat.toSSet.map f) R) (CategoryTheory.CategoryStruct.comp (singularChainLocallyConstantNsmul R d) h)

Locally constant multiplication commutes with push-forward after pulling back the function along the continuous map.

theorem TauCeti.chainComplexMap_comp_singularChainLocallyConstantNsmul {B Y : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (R : C) [PreconnectedSpace ↑Y] (f : Y ⟶ B) (d : LocallyConstant ↑B ℕ) (y : ↑Y) : CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (TopCat.toSSet.map f) R) (singularChainLocallyConstantNsmul R d) = d ((CategoryTheory.ConcreteCategory.hom f) y) • SSet.chainComplexMap (TopCat.toSSet.map f) R

On the image of a map from a preconnected space, locally constant multiplication is the scalar given by its value at any point of that space.

theorem TauCeti.chainComplexMap_comp_singularChainLocallyConstantNsmul_assoc {B Y : TopCat} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (R : C) [PreconnectedSpace ↑Y] (f : Y ⟶ B) (d : LocallyConstant ↑B ℕ) (y : ↑Y) {Z : ChainComplex C ℕ} (h : (TopCat.toSSet.obj B).chainComplex R ⟶ Z) : CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (TopCat.toSSet.map f) R) (CategoryTheory.CategoryStruct.comp (singularChainLocallyConstantNsmul R d) h) = CategoryTheory.CategoryStruct.comp (d ((CategoryTheory.ConcreteCategory.hom f) y) • SSet.chainComplexMap (TopCat.toSSet.map f) R) h

On the image of a map from a preconnected space, locally constant multiplication is the scalar given by its value at any point of that space.