The augmentation of cubical chains

The augmentation ε : C^□_0(X; R) → R sends every singular 0-cube, a point of X, to 1. It vanishes on boundaries: the boundary of a 1-cube, a path, is its end point minus its starting point. No 0-cube is degenerate, so the augmentation of the unnormalized chains descends to the normalized ones without any condition.

Main definitions

• TauCeti.CubicalChain.augment X R, TauCeti.NormalizedCubicalChain.augment X R: the augmentations.

Main results

• TauCeti.NormalizedCubicalChain.augment_boundary: ε ∘ ∂ = 0.
• TauCeti.NormalizedCubicalChain.augment_map: the augmentation is natural.

References

• W. S. Massey, Singular Homology Theory, GTM 70, Springer, 1980, Chapter II.

noncomputable def TauCeti.CubicalChain.augment (X : Type u_1) [TopologicalSpace X] (R : Type u_3) [Semiring R] : CubicalChain X R 0 →ₗ[R] R

The augmentation of the unnormalized 0-chains: the sum of the coefficients.

@[simp]

theorem TauCeti.CubicalChain.augment_single {X : Type u_1} [TopologicalSpace X] (R : Type u_3) [Semiring R] (c : SingularCube X 0) (a : R) : (augment X R) (Finsupp.single c a) = a

theorem TauCeti.CubicalChain.degenerate_le_ker_augment {X : Type u_1} [TopologicalSpace X] (R : Type u_3) [Semiring R] : degenerate X R 0 ≤ (augment X R).ker

theorem TauCeti.CubicalChain.augment_map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_3) [Semiring R] (f : C(X, Y)) : augment Y R ∘ₗ map R f 0 = augment X R

theorem TauCeti.CubicalChain.augment_boundary {X : Type u_1} [TopologicalSpace X] (R : Type u_3) [Ring R] : augment X R ∘ₗ boundary X R 0 = 0

The augmentation vanishes on boundaries: a path contributes its end point minus its starting point.

noncomputable def TauCeti.NormalizedCubicalChain.augment (X : Type u_1) [TopologicalSpace X] (R : Type u_3) [Ring R] : NormalizedCubicalChain X R 0 →ₗ[R] R

The augmentation of the normalized 0-chains.

@[simp]

theorem TauCeti.NormalizedCubicalChain.augment_mk {X : Type u_1} [TopologicalSpace X] (R : Type u_3) [Ring R] (f : CubicalChain X R 0) : (augment X R) (Submodule.Quotient.mk f) = (CubicalChain.augment X R) f

@[simp]

theorem TauCeti.NormalizedCubicalChain.augment_ofCube {X : Type u_1} [TopologicalSpace X] (R : Type u_3) [Ring R] (c : SingularCube X 0) : (augment X R) (ofCube X R c) = 1

theorem TauCeti.NormalizedCubicalChain.augment_boundary {X : Type u_1} [TopologicalSpace X] (R : Type u_3) [Ring R] : augment X R ∘ₗ boundary X R 0 = 0

The augmentation vanishes on boundaries.

theorem TauCeti.NormalizedCubicalChain.augment_map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_3) [Ring R] (f : C(X, Y)) : augment Y R ∘ₗ map R f 0 = augment X R

The augmentation is natural.

@[simp]

theorem TauCeti.NormalizedCubicalChain.map_const_zero {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_3) [Ring R] (y : Y) (c : NormalizedCubicalChain X R 0) : (map R (ContinuousMap.const X y) 0) c = (augment X R) c • ofCube Y R (SingularCube.point y)

On 0-chains, a constant map multiplies the class of its value by the augmentation.

theorem TauCeti.NormalizedCubicalChain.augment_surjective {X : Type u_1} [TopologicalSpace X] (R : Type u_3) [Ring R] (x : X) : Function.Surjective ⇑(augment X R)

The augmentation is surjective when a point of the space is given.