Normalized cubical chains

The degenerate chains D_n(X; R) are the span of the degenerate singular n-cubes inside the unnormalized cubical chains. They form a subcomplex: on a cube c degenerate at the coordinate i, the two i-terms of ∂ c cancel, because the two i-faces of c coincide (face_eq_of_isDegenerateAt), and every other term is a degenerate cube (isDegenerate_face_of_ne). The normalized cubical chains C^□_n(X; R) are the quotient CubicalChain X R n ⧸ D_n, with the induced boundary, and they are the cubical singular chains of Massey, Singular Homology Theory, Chapter II.

Degenerate cubes are preserved by composition with a continuous map, so the push-forward descends to the quotient and the normalized chains are functorial. An injective continuous map also reflects degeneracy, so its push-forward on normalized chains is injective, and even has a left inverse.

Main definitions

• TauCeti.CubicalChain.degenerate X R n: the submodule spanned by the degenerate n-cubes.
• TauCeti.NormalizedCubicalChain X R n: the normalized cubical n-chains.
• TauCeti.NormalizedCubicalChain.boundary X R n: the induced boundary.
• TauCeti.NormalizedCubicalChain.map R f n: the push-forward along a continuous map.
• TauCeti.NormalizedCubicalChain.cast R h: reindexing along an equality of dimensions.
• TauCeti.NormalizedCubicalChain.desc g hg: the linear map determined by its values on cubes, vanishing on the degenerate ones.

Main results

• TauCeti.CubicalChain.degenerate_def, TauCeti.CubicalChain.degenerate_induction: the degenerate chains as a span, and induction on them.
• TauCeti.CubicalChain.boundary_mem_degenerate: the boundary of a degenerate chain is degenerate.
• TauCeti.CubicalChain.degenerate_zero: there are no degenerate 0-chains.
• TauCeti.NormalizedCubicalChain.boundary_boundary: ∂ ∘ ∂ = 0 on normalized chains.
• TauCeti.NormalizedCubicalChain.map_boundary: the boundary is natural.
• TauCeti.NormalizedCubicalChain.map_injective: injective continuous maps induce injective push-forwards, including all subspace inclusions.
• TauCeti.NormalizedCubicalChain.exists_comp_map_eq_id: the push-forward along an injective continuous map has a left inverse.

References

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

noncomputable def TauCeti.CubicalChain.degenerate (X : Type u_1) [TopologicalSpace X] (R : Type u_4) [Semiring R] (n : ℕ) : Submodule R (CubicalChain X R n)

The degenerate n-chains: the span of the degenerate singular n-cubes.

theorem TauCeti.CubicalChain.degenerate_def (X : Type u_1) [TopologicalSpace X] (R : Type u_4) [Semiring R] (n : ℕ) : degenerate X R n = Submodule.span R {f : SingularCube X n →₀ R | ∃ (c : SingularCube X n), c.IsDegenerate ∧ f = Finsupp.single c 1}

The degenerate n-chains are the span of the chains of the degenerate n-cubes.

theorem TauCeti.CubicalChain.degenerate_eq_supported {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Semiring R] (n : ℕ) : degenerate X R n = Finsupp.supported R R {c : SingularCube X n | c.IsDegenerate}

Degenerate chains are precisely the chains supported on degenerate cubes.

@[simp]

theorem TauCeti.CubicalChain.mem_degenerate_iff {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Semiring R] {n : ℕ} (g : CubicalChain X R n) : g ∈ degenerate X R n ↔ ∀ (c : SingularCube X n), ¬c.IsDegenerate → g c = 0

A chain is degenerate exactly when its coefficient at every nondegenerate cube vanishes.

theorem TauCeti.CubicalChain.degenerate_induction {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Semiring R] {n : ℕ} {P : CubicalChain X R n → Prop} (zero : P 0) (hsingle : ∀ (c : SingularCube X n), c.IsDegenerate → P (Finsupp.single c 1)) (hadd : ∀ (f g : CubicalChain X R n), P f → P g → P (f + g)) (hsmul : ∀ (r : R) (f : CubicalChain X R n), P f → P (r • f)) {g : CubicalChain X R n} (hg : g ∈ degenerate X R n) : P g

Induction on degenerate chains: a property of chains which holds for 0 and for the chain of each degenerate cube, and is stable under sums and scalar multiples, holds for every degenerate chain.

theorem TauCeti.CubicalChain.single_mem_degenerate {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Semiring R] {n : ℕ} {c : SingularCube X n} (hc : c.IsDegenerate) (a : R) : Finsupp.single c a ∈ degenerate X R n

@[simp]

theorem TauCeti.CubicalChain.degenerate_zero {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Semiring R] : degenerate X R 0 = ⊥

There are no degenerate 0-chains: a 0-cube is a point.

theorem TauCeti.CubicalChain.lmapDomain_mem_degenerate {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_4) [Semiring R] {n m : ℕ} {φ : SingularCube X n → SingularCube Y m} (hφ : ∀ (c : SingularCube X n), c.IsDegenerate → (φ c).IsDegenerate) {g : CubicalChain X R n} (hg : g ∈ degenerate X R n) : (Finsupp.lmapDomain R R φ) g ∈ degenerate Y R m

A map of singular cubes sending degenerate cubes to degenerate cubes preserves the degenerate chains.

theorem TauCeti.CubicalChain.map_mem_degenerate {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_4) [Semiring R] (f : C(X, Y)) {n : ℕ} {g : CubicalChain X R n} (hg : g ∈ degenerate X R n) : (map R f n) g ∈ degenerate Y R n

The push-forward of a degenerate chain is degenerate.

theorem TauCeti.CubicalChain.map_mem_degenerate_iff_of_injective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_4) [Semiring R] (f : C(X, Y)) (hf : Function.Injective ⇑f) {n : ℕ} (g : CubicalChain X R n) : (map R f n) g ∈ degenerate Y R n ↔ g ∈ degenerate X R n

Pushing forward along an injective continuous map reflects degenerate chains.

theorem TauCeti.CubicalChain.cast_mem_degenerate {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Semiring R] {n m : ℕ} (h : n = m) {f : CubicalChain X R n} (hf : f ∈ degenerate X R n) : (cast R h) f ∈ degenerate X R m

Reindexing preserves degenerate chains.

theorem TauCeti.CubicalChain.boundary_single_mem_degenerate {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Ring R] {n : ℕ} {c : SingularCube X (n + 1)} (hc : c.IsDegenerate) : (boundary X R n) (Finsupp.single c 1) ∈ degenerate X R n

The boundary of a degenerate cube is a degenerate chain: the two terms of the degenerate coordinate cancel, and every other face is degenerate.

theorem TauCeti.CubicalChain.boundary_mem_degenerate {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Ring R] {n : ℕ} {f : CubicalChain X R (n + 1)} (hf : f ∈ degenerate X R (n + 1)) : (boundary X R n) f ∈ degenerate X R n

The degenerate chains form a subcomplex.

@[reducible, inline]

abbrev TauCeti.NormalizedCubicalChain (X : Type u_4) [TopologicalSpace X] (R : Type u_5) [Ring R] (n : ℕ) : Type (max (max u_4 u_5) u_5 u_4)

The normalized cubical n-chains of X with coefficients in R: the unnormalized chains modulo the degenerate ones.

noncomputable def TauCeti.NormalizedCubicalChain.ofCube (X : Type u_1) [TopologicalSpace X] (R : Type u_4) [Ring R] {n : ℕ} (c : SingularCube X n) : NormalizedCubicalChain X R n

The class of a singular cube in the normalized chains.

theorem TauCeti.NormalizedCubicalChain.ofCube_def {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Ring R] {n : ℕ} (c : SingularCube X n) : ofCube X R c = Submodule.Quotient.mk (Finsupp.single c 1)

theorem TauCeti.NormalizedCubicalChain.linearMap_ext {X : Type u_1} [TopologicalSpace X] {R : Type u_4} [Ring R] {N : Type u_5} [AddCommGroup N] [Module R N] {n : ℕ} {f g : NormalizedCubicalChain X R n →ₗ[R] N} (h : ∀ (c : SingularCube X n), f (ofCube X R c) = g (ofCube X R c)) : f = g

Two linear maps out of the normalized n-chains agree if they agree on cubes.

theorem TauCeti.NormalizedCubicalChain.induction_on {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Ring R] {n : ℕ} {P : NormalizedCubicalChain X R n → Prop} (g : NormalizedCubicalChain X R n) (zero : P 0) (add : ∀ (a b : NormalizedCubicalChain X R n), P a → P b → P (a + b)) (smul : ∀ (r : R) (a : NormalizedCubicalChain X R n), P a → P (r • a)) (ofCube : ∀ (c : SingularCube X n), P (ofCube X R c)) : P g

Induction on normalized chains: a property of normalized chains which holds for 0 and for the class of each cube, and is stable under sums and scalar multiples, holds for every normalized chain.

@[simp]

theorem TauCeti.NormalizedCubicalChain.ofCube_eq_zero {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Ring R] {n : ℕ} {c : SingularCube X n} (hc : c.IsDegenerate) : ofCube X R c = 0

noncomputable def TauCeti.NormalizedCubicalChain.desc {X : Type u_1} [TopologicalSpace X] {R : Type u_4} [Ring R] {N : Type u_5} [AddCommGroup N] [Module R N] {n : ℕ} (g : SingularCube X n → N) (hg : ∀ (c : SingularCube X n), c.IsDegenerate → g c = 0) : NormalizedCubicalChain X R n →ₗ[R] N

The linear map out of the normalized n-chains determined by its values on cubes, which must vanish on the degenerate cubes.

@[simp]

theorem TauCeti.NormalizedCubicalChain.desc_ofCube {X : Type u_1} [TopologicalSpace X] {R : Type u_4} [Ring R] {N : Type u_5} [AddCommGroup N] [Module R N] {n : ℕ} (g : SingularCube X n → N) (hg : ∀ (c : SingularCube X n), c.IsDegenerate → g c = 0) (c : SingularCube X n) : (desc g hg) (ofCube X R c) = g c

noncomputable def TauCeti.NormalizedCubicalChain.boundary (X : Type u_1) [TopologicalSpace X] (R : Type u_4) [Ring R] (n : ℕ) : NormalizedCubicalChain X R (n + 1) →ₗ[R] NormalizedCubicalChain X R n

The boundary of normalized cubical chains, induced by the boundary of the unnormalized ones.

@[simp]

theorem TauCeti.NormalizedCubicalChain.boundary_mk {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Ring R] {n : ℕ} (f : CubicalChain X R (n + 1)) : (boundary X R n) (Submodule.Quotient.mk f) = Submodule.Quotient.mk ((CubicalChain.boundary X R n) f)

theorem TauCeti.NormalizedCubicalChain.boundary_boundary {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Ring R] (n : ℕ) : boundary X R n ∘ₗ boundary X R (n + 1) = 0

The boundary of a boundary vanishes.

@[simp]

theorem TauCeti.NormalizedCubicalChain.boundary_ofCube {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Ring R] {n : ℕ} (c : SingularCube X (n + 1)) : (boundary X R n) (ofCube X R c) = ∑ i : Fin (n + 1), (-1) ^ ↑i • (ofCube X R (SingularCube.face i 0 c) - ofCube X R (SingularCube.face i 1 c))

The boundary of the class of a cube is the signed sum of the classes of its faces.

noncomputable def TauCeti.NormalizedCubicalChain.map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_4) [Ring R] (f : C(X, Y)) (n : ℕ) : NormalizedCubicalChain X R n →ₗ[R] NormalizedCubicalChain Y R n

Normalized cubical chains pushed forward along a continuous map.

@[simp]

theorem TauCeti.NormalizedCubicalChain.map_mk {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_4) [Ring R] (f : C(X, Y)) {n : ℕ} (g : CubicalChain X R n) : (map R f n) (Submodule.Quotient.mk g) = Submodule.Quotient.mk ((CubicalChain.map R f n) g)

@[simp]

theorem TauCeti.NormalizedCubicalChain.map_ofCube {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_4) [Ring R] (f : C(X, Y)) {n : ℕ} (c : SingularCube X n) : (map R f n) (ofCube X R c) = ofCube Y R (f.comp c)

The push-forward of the class of a cube is the class of the composed cube.

@[simp]

theorem TauCeti.NormalizedCubicalChain.map_id {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Ring R] (n : ℕ) : map R (ContinuousMap.id X) n = LinearMap.id

theorem TauCeti.NormalizedCubicalChain.map_comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (R : Type u_4) [Ring R] (g : C(Y, Z)) (f : C(X, Y)) (n : ℕ) : map R (g.comp f) n = map R g n ∘ₗ map R f n

theorem TauCeti.NormalizedCubicalChain.map_injective {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_4) [Ring R] (f : C(X, Y)) (hf : Function.Injective ⇑f) (n : ℕ) : Function.Injective ⇑(map R f n)

Normalization preserves injectivity of a map of spaces. No embedding hypothesis is needed.

theorem TauCeti.NormalizedCubicalChain.ofCube_mem_range_map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_4) [Ring R] {f : C(X, Y)} (hf : Topology.IsInducing ⇑f) {n : ℕ} {c : SingularCube Y n} (hc : Set.range ⇑c ⊆ Set.range ⇑f) : ofCube Y R c ∈ (map R f n).range

A cube with values in the range of an inducing map f lifts through f, so its class is a push-forward along f.

theorem TauCeti.NormalizedCubicalChain.exists_comp_map_eq_id {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_4) [Ring R] {f : C(X, Y)} (hf : Function.Injective ⇑f) (n : ℕ) : ∃ (r : NormalizedCubicalChain Y R n →ₗ[R] NormalizedCubicalChain X R n), r ∘ₗ map R f n = LinearMap.id

The push-forward of normalized chains along an injective continuous map has a left inverse.

theorem TauCeti.NormalizedCubicalChain.map_boundary {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_4) [Ring R] (f : C(X, Y)) (n : ℕ) : map R f n ∘ₗ boundary X R n = boundary Y R n ∘ₗ map R f (n + 1)

The boundary is natural.

noncomputable def TauCeti.NormalizedCubicalChain.cast {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Ring R] {n m : ℕ} (h : n = m) : NormalizedCubicalChain X R n →ₗ[R] NormalizedCubicalChain X R m

Reindex normalized chains along an equality of dimensions.

@[simp]

theorem TauCeti.NormalizedCubicalChain.cast_mk {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Ring R] {n m : ℕ} (h : n = m) (f : CubicalChain X R n) : (cast R h) (Submodule.Quotient.mk f) = Submodule.Quotient.mk ((CubicalChain.cast R h) f)

@[simp]

theorem TauCeti.NormalizedCubicalChain.cast_cast {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Ring R] {n m k : ℕ} (h : n = m) (h' : m = k) (c : NormalizedCubicalChain X R n) : (cast R h') ((cast R h) c) = (cast R ⋯) c

Reindexing along successive dimension equalities is reindexing along their composite.

@[simp]

theorem TauCeti.NormalizedCubicalChain.cast_rfl {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Ring R] {n : ℕ} (c : NormalizedCubicalChain X R n) : (cast R ⋯) c = c

Reindexing along rfl is the identity.

theorem TauCeti.NormalizedCubicalChain.map_cast {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_4) [Ring R] (f : C(X, Y)) {n m : ℕ} (h : n = m) (c : NormalizedCubicalChain X R n) : (map R f m) ((cast R h) c) = (cast R h) ((map R f n) c)

Reindexing commutes with the push-forward.

theorem TauCeti.NormalizedCubicalChain.boundary_cast {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Ring R] {n m : ℕ} (h : n = m) (c : NormalizedCubicalChain X R (n + 1)) : (boundary X R m) ((cast R ⋯) c) = (cast R h) ((boundary X R n) c)

Reindexing commutes with the boundary.

theorem TauCeti.NormalizedCubicalChain.cast_injective {X : Type u_1} [TopologicalSpace X] (R : Type u_4) [Ring R] {n m : ℕ} (h : n = m) : Function.Injective ⇑(cast R h)

Reindexing is injective.

theorem TauCeti.NormalizedCubicalChain.heq_of_cast_eq {X : Type u_1} [TopologicalSpace X] {R : Type u_4} [Ring R] {n m : ℕ} (h : n = m) {x : NormalizedCubicalChain X R n} {y : NormalizedCubicalChain X R m} (hxy : (cast R h) x = y) : x ≍ y

Equal after reindexing implies heterogeneously equal.

@[simp]

theorem TauCeti.NormalizedCubicalChain.map_const_succ {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_4) [Ring R] (y : Y) (n : ℕ) : map R (ContinuousMap.const X y) (n + 1) = 0

A constant map induces zero on positive-dimensional normalized cubical chains.