Documentation

TauCeti.AlgebraicTopology.Singular.Cubical.Normalization

The normalization of cubical chains #

For a finite set S of coordinates, let ζ_S : Iⁿ → Iⁿ set the coordinates in S to 0. The normalization of a singular n-cube c is the signed sum

normalize c = Σ_S (-1) ^ |S| (c ∘ ζ_S),

that is, the image of c under the product of the commuting projections 1 - ζ_i. It is natural in the space, it vanishes on degenerate cubes (CubicalChain.normalize_eq_zero_of_mem_degenerate), and it differs from the identity by a degenerate chain (CubicalChain.normalize_sub_mem_degenerate): every term with S ≠ ∅ does not depend on the coordinates in S. So it induces a natural section NormalizedCubicalChain.toCubicalChain of the quotient map from unnormalized to normalized chains.

Through this section, the normalized cubical n-chains are naturally a retract of the free module on the singular n-cubes, that is, on the continuous maps from the model Iⁿ. This is the form in which the method of acyclic models applies to them.

Main definitions #

Main results #

References #

source
def TauCeti.SingularCube.zeroOn {n : ℕ} (S : Finset (Fin n)) :
C(Fin n → ↑unitInterval, Fin n → ↑unitInterval)

The map of the cube Iⁿ setting the coordinates in S to 0.

Instances For
    source
    @[simp]
    theorem TauCeti.SingularCube.zeroOn_apply {n : ℕ} (S : Finset (Fin n)) (x : Fin n → ↑unitInterval) (j : Fin n) :
    (zeroOn S) x j = if j ∈ S then 0 else x j
    source
    @[simp]
    theorem TauCeti.SingularCube.zeroOn_empty {n : ℕ} :
    zeroOn ∅ = ContinuousMap.id (Fin n → ↑unitInterval)
    source
    theorem TauCeti.SingularCube.isDegenerateAt_comp_zeroOn {X : Type u_1} [TopologicalSpace X] {n : ℕ} (c : SingularCube X n) {S : Finset (Fin n)} {j : Fin n} (hj : j ∈ S) :
    IsDegenerateAt (ContinuousMap.comp c (zeroOn S)) j

    A cube composed with ζ_S does not depend on the coordinates in S.

    source
    theorem TauCeti.SingularCube.comp_zeroOn_insert {X : Type u_1} [TopologicalSpace X] {n : ℕ} {c : SingularCube X n} {j : Fin n} (h : c.IsDegenerateAt j) (S : Finset (Fin n)) :
    ContinuousMap.comp c (zeroOn (insert j S)) = ContinuousMap.comp c (zeroOn S)

    Setting one more coordinate, on which the cube does not depend, to 0 does not change the cube.

    source
    noncomputable def TauCeti.CubicalChain.normalize {X : Type u_1} [TopologicalSpace X] (R : Type u_3) [Ring R] (n : ℕ) :
    CubicalChain X R n →ₗ[R] CubicalChain X R n

    The normalization of cubical chains: a cube c is sent to Σ_S (-1) ^ |S| (c ∘ ζ_S), where ζ_S sets the coordinates in S to 0.

    Instances For
      source
      @[simp]
      theorem TauCeti.CubicalChain.normalize_single {X : Type u_1} [TopologicalSpace X] (R : Type u_3) [Ring R] {n : ℕ} (c : SingularCube X n) (a : R) :
      (normalize R n) (Finsupp.single c a) = ∑ S : Finset (Fin n), (-1) ^ S.card • Finsupp.single (ContinuousMap.comp c (SingularCube.zeroOn S)) a
      source
      theorem TauCeti.CubicalChain.map_normalize {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_3) [Ring R] (f : C(X, Y)) {n : ℕ} (g : CubicalChain X R n) :
      (map R f n) ((normalize R n) g) = (normalize R n) ((map R f n) g)

      Normalization is natural.

      source
      theorem TauCeti.CubicalChain.normalize_single_eq_zero_of_isDegenerateAt {X : Type u_1} [TopologicalSpace X] (R : Type u_3) [Ring R] {n : ℕ} {c : SingularCube X n} {j : Fin n} (h : c.IsDegenerateAt j) (a : R) :
      (normalize R n) (Finsupp.single c a) = 0

      Normalization kills a cube which does not depend on one of its coordinates: the terms for S and for S with that coordinate added or removed cancel.

      source
      theorem TauCeti.CubicalChain.normalize_eq_zero_of_mem_degenerate {X : Type u_1} [TopologicalSpace X] (R : Type u_3) [Ring R] {n : ℕ} {f : CubicalChain X R n} (hf : f ∈ degenerate X R n) :
      (normalize R n) f = 0

      Normalization kills degenerate chains.

      source
      theorem TauCeti.CubicalChain.normalize_sub_mem_degenerate {X : Type u_1} [TopologicalSpace X] (R : Type u_3) [Ring R] {n : ℕ} (f : CubicalChain X R n) :
      (normalize R n) f - f ∈ degenerate X R n

      Normalization is the identity up to a degenerate chain: every term with S ≠ ∅ does not depend on the coordinates in S.

      source
      noncomputable def TauCeti.NormalizedCubicalChain.toCubicalChain (X : Type u_1) [TopologicalSpace X] (R : Type u_3) [Ring R] (n : ℕ) :
      NormalizedCubicalChain X R n →ₗ[R] CubicalChain X R n

      The natural section of the quotient map from unnormalized to normalized cubical chains, induced by the normalization.

      Instances For
        source
        @[simp]
        theorem TauCeti.NormalizedCubicalChain.toCubicalChain_mk {X : Type u_1} [TopologicalSpace X] (R : Type u_3) [Ring R] {n : ℕ} (f : CubicalChain X R n) :
        (toCubicalChain X R n) (Submodule.Quotient.mk f) = (CubicalChain.normalize R n) f
        source
        @[simp]
        theorem TauCeti.NormalizedCubicalChain.mk_toCubicalChain {X : Type u_1} [TopologicalSpace X] (R : Type u_3) [Ring R] {n : ℕ} (f : NormalizedCubicalChain X R n) :
        Submodule.Quotient.mk ((toCubicalChain X R n) f) = f

        The section is a section of the quotient map.

        source
        theorem TauCeti.NormalizedCubicalChain.toCubicalChain_map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (R : Type u_3) [Ring R] (f : C(X, Y)) {n : ℕ} (g : NormalizedCubicalChain X R n) :
        (toCubicalChain Y R n) ((map R f n) g) = (CubicalChain.map R f n) ((toCubicalChain X R n) g)

        The section is natural.

        source
        theorem TauCeti.NormalizedCubicalChain.sum_toCubicalChain {X : Type u_1} [TopologicalSpace X] (R : Type u_3) [Ring R] {n : ℕ} (f : NormalizedCubicalChain X R n) :
        (Finsupp.sum ((toCubicalChain X R n) f) fun (c : SingularCube X n) (a : R) => a • ofCube X R c) = f

        A normalized chain is the combination of the classes of the cubes of its normalization.

        source
        instance TauCeti.NormalizedCubicalChain.instProjective {X : Type u_1} [TopologicalSpace X] (R : Type u_3) [Ring R] (n : ℕ) :
        Module.Projective R (NormalizedCubicalChain X R n)

        The normalized cubical chains are a projective module: they are a retract of the free module on the cubes, through the section toCubicalChain of the quotient map.