Singular chains with coefficients in a ring, on elements

For a ring k, the simplicial singular chain complex with coefficients in k is the complex of k-modules whose n-chains are the formal k-combinations of singular n-simplices. This file gives the element-level interface to it: the chain simplexChain σ a of a simplex with a coefficient, the extensionality of linear maps out of the chains (and, for integer coefficients, of additive maps), the linear map with prescribed values on simplices, the push-forward and the boundary of a simplex, the chains of points and paths (TauCeti.pointChain, TauCeti.pathChain), and the augmentation, the sum of the coefficients of a 0-chain, natural and vanishing on boundaries.

Main definitions

• TauCeti.singularChains k: the simplicial singular chain complex functor with coefficients in the ring k.
• TauCeti.simplexChain σ a: the chain of a singular simplex σ with coefficient a.
• TauCeti.chainsDesc f: the linear map out of the singular n-chains with the given values on singular simplices.
• TauCeti.singularAugment k X: the augmentation of the simplicial singular chains.
• ContinuousMap.singularHomologyMap: the induced linear map on singular homology.
• TauCeti.singularChainsAugmentation k X: the augmentation, as a chain map to k in degree 0.

Main results

• TauCeti.singularChains_linearMap_ext, TauCeti.singularChains_addMonoidHom_ext: linear maps, and additive maps out of the chains with integer coefficients, are determined on simplices.
• TauCeti.singularChains_d_simplexChain: the boundary of a simplex.
• TauCeti.singularAugment_map, TauCeti.singularAugment_d: the augmentation is natural and vanishes on boundaries.

@[reducible, inline]

noncomputable abbrev TauCeti.singularChains (k : Type u) [Ring k] : CategoryTheory.Functor TopCat (ChainComplex (ModuleCat k) ℕ)

The simplicial singular chain complex functor with coefficients in the ring k.

@[reducible, inline]

noncomputable abbrev TauCeti.simplexChain {k : Type u} [Ring k] {X : TopCat} {n : ℕ} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) (a : k) : ↑(((singularChains k).obj X).X n)

The chain of a singular simplex, with coefficient a.

theorem TauCeti.singularChains_linearMap_ext {k : Type u} [Ring k] {X : TopCat} {n : ℕ} {V : Type u} [AddCommGroup V] [Module k V] {L L' : ↑(((singularChains k).obj X).X n) →ₗ[k] V} (h : ∀ (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })), L (simplexChain σ 1) = L' (simplexChain σ 1)) : L = L'

Linear maps out of simplicial singular chains agree when they agree on simplices.

theorem TauCeti.simplexChain_eq_smul {k : Type u} [Ring k] {X : TopCat} {n : ℕ} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) (a : k) : simplexChain σ a = a • simplexChain σ 1

The chain of a simplex with coefficient a is a times the chain of the simplex.

theorem TauCeti.singularChains_map_f_simplexChain {k : Type u} [Ring k] {X Y : TopCat} (f : X ⟶ Y) {n : ℕ} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) (a : k) : (CategoryTheory.ConcreteCategory.hom (((singularChains k).map f).f n)) (simplexChain σ a) = simplexChain ((CategoryTheory.ConcreteCategory.hom ((TopCat.toSSet.map f).app (Opposite.op { len := n }))) σ) a

Pushing the chain of a simplex forward along a continuous map gives the chain of the pushed-forward simplex, with the same coefficient.

noncomputable def TauCeti.chainsDesc {k : Type u} [Ring k] {X : TopCat} {n : ℕ} {V : Type u} [AddCommGroup V] [Module k V] (f : (TopCat.toSSet.obj X).obj (Opposite.op { len := n }) → V) : ↑(((singularChains k).obj X).X n) →ₗ[k] V

The linear map out of the singular n-chains with the given values on singular simplices.

@[simp]

theorem TauCeti.chainsDesc_simplexChain {k : Type u} [Ring k] {X : TopCat} {n : ℕ} {V : Type u} [AddCommGroup V] [Module k V] (f : (TopCat.toSSet.obj X).obj (Opposite.op { len := n }) → V) (s : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) (a : k) : (chainsDesc f) (simplexChain s a) = a • f s

The linear map with given values on simplices takes the chain of a simplex with coefficient a to a times the value on the simplex.

theorem TauCeti.chainsDesc_simplexChain_one {k : Type u} [Ring k] {X : TopCat} {n : ℕ} {V : Type u} [AddCommGroup V] [Module k V] (f : (TopCat.toSSet.obj X).obj (Opposite.op { len := n }) → V) (s : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) : (chainsDesc f) (simplexChain s 1) = f s

The linear map with given values on simplices takes the chain of a simplex to the value on the simplex.

theorem TauCeti.singularChains_addMonoidHom_ext {X : TopCat} {n : ℕ} {V : Type} [AddCommGroup V] {f g : ↑(((singularChains ℤ).obj X).X n) →+ V} (h : ∀ (s : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })), f (simplexChain s 1) = g (simplexChain s 1)) : f = g

Additive maps out of the singular chains with integer coefficients agree when they agree on simplices.

noncomputable def TauCeti.singularAugment (k : Type u) [Ring k] (X : TopCat) : ↑(((singularChains k).obj X).X 0) →ₗ[k] k

The augmentation of the simplicial singular chains: the sum of the coefficients.

@[simp]

theorem TauCeti.singularAugment_simplexChain {k : Type u} [Ring k] (X : TopCat) (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := 0 })) (a : k) : (singularAugment k X) (simplexChain σ a) = a

The augmentation of the chain of a 0-simplex with coefficient a is a.

theorem TauCeti.singularAugment_map {k : Type u} [Ring k] {X Y : TopCat} (f : X ⟶ Y) (x : ↑(((singularChains k).obj X).X 0)) : (singularAugment k Y) ((CategoryTheory.ConcreteCategory.hom (((singularChains k).map f).f 0)) x) = (singularAugment k X) x

The augmentation of the simplicial singular chains is natural.

@[simp]

theorem TauCeti.singularChains_d_simplexChain {k : Type u} [Ring k] {X : TopCat} {n : ℕ} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n + 1 })) (a : k) : (CategoryTheory.ConcreteCategory.hom (((singularChains k).obj X).d (n + 1) n)) (simplexChain σ a) = ∑ i : Fin (n + 2), (-1) ^ ↑i • simplexChain ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (TopCat.toSSet.obj X) i)) σ) a

The boundary of a singular simplex is the alternating sum of its faces.

@[simp]

theorem TauCeti.singularAugment_d {k : Type u} [Ring k] (X : TopCat) (x : ↑(((singularChains k).obj X).X 1)) : (singularAugment k X) ((CategoryTheory.ConcreteCategory.hom (((singularChains k).obj X).d 1 0)) x) = 0

The augmentation of the simplicial singular chains vanishes on boundaries.

noncomputable def TauCeti.singularChainsAugmentation (k : Type u) [Ring k] (X : TopCat) : (singularChains k).obj X ⟶ (ChainComplex.single₀ (ModuleCat k)).obj ↧k

The augmentation of the simplicial singular chains, as a chain map to the coefficient ring placed in degree 0.

@[simp]

theorem TauCeti.singularChainsAugmentation_f_zero (k : Type u) [Ring k] (X : TopCat) : (singularChainsAugmentation k X).f 0 = ModuleCat.ofHom (singularAugment k X)

In degree 0 the augmentation chain map is the augmentation.

@[reducible, inline]

noncomputable abbrev TauCeti.pointChain (k : Type u) [Ring k] {X : TopCat} (p : ↑X) : ↑(((singularChains k).obj X).X 0)

The chain of the singular 0-simplex at a point.

@[reducible, inline]

noncomputable abbrev TauCeti.pathChain (k : Type u) [Ring k] {X : TopCat} (g : C(↑unitInterval, ↑X)) : ↑(((singularChains k).obj X).X 1)

The chain of the singular 1-simplex of a map from the unit interval (TauCeti.TopCat.simplex₁).

theorem TauCeti.singularChains_d_pathChain {k : Type u} [Ring k] {X : TopCat} (g : C(↑unitInterval, ↑X)) : (CategoryTheory.ConcreteCategory.hom (((singularChains k).obj X).d 1 0)) (pathChain k g) = pointChain k (g 1) - pointChain k (g 0)

The boundary of the chain of a path is the difference of the chains of its endpoints.

theorem TauCeti.singularChains_map_f_pathChain {k : Type u} [Ring k] {X Y : TopCat} (f : X ⟶ Y) (g : C(↑unitInterval, ↑X)) : (CategoryTheory.ConcreteCategory.hom (((singularChains k).map f).f 1)) (pathChain k g) = pathChain k ((CategoryTheory.ConcreteCategory.hom f).comp g)

Pushing the chain of a path forward along a continuous map gives the chain of the composite.

@[reducible, inline]

noncomputable abbrev ContinuousMap.singularHomologyMap (k : Type u) [Ring k] (n : ℕ) {Y Z : Type u} [TopologicalSpace Y] [TopologicalSpace Z] (g : C(Y, Z)) : ↑(HomologicalComplex.homology ((TauCeti.singularChains k).obj ↧Y) n) →ₗ[k] ↑(HomologicalComplex.homology ((TauCeti.singularChains k).obj ↧Z) n)

The map induced on degree-n singular homology with coefficients in k by a continuous map.

@[simp]

theorem ContinuousMap.singularHomologyMap_id {k : Type u} [Ring k] {n : ℕ} {Y : Type u} [TopologicalSpace Y] (x : ↑(HomologicalComplex.homology ((TauCeti.singularChains k).obj ↧Y) n)) : (singularHomologyMap k n (ContinuousMap.id Y)) x = x

The identity map induces the identity on singular homology.

theorem ContinuousMap.singularHomologyMap_comp {k : Type u} [Ring k] {n : ℕ} {Y Z W : Type u} [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W] (g : C(Z, W)) (g' : C(Y, Z)) (x : ↑(HomologicalComplex.homology ((TauCeti.singularChains k).obj ↧Y) n)) : (singularHomologyMap k n (g.comp g')) x = (singularHomologyMap k n g) ((singularHomologyMap k n g') x)

Singular homology respects composition of continuous maps.