Documentation

TauCeti.AlgebraicTopology.Cellular.SkeletonNeighborhood

The skeletal pair and the skeleton with the cell cores removed #

For a relative CW complex, the skeletal pair (Xⁿ, Xⁿ⁻¹) — in Tau Ceti's indexing TauCeti.skeletonPair C n, with ambient space skeletonLT C (n + 1) — includes into the pair TauCeti.skeletonNeighborhoodPair C n, whose subspace TauCeti.skeletonNeighborhood C n is Xⁿ with the inner half of every open n-cell removed. The endpoint TauCeti.skeletonNeighborhoodEndpoint of the radial deformation TauCeti.skeletonNeighborhoodHomotopy is a homotopy inverse of this inclusion of pairs, the deformation itself supplying both homotopies, so the inclusion induces isomorphisms on relative singular homology in every degree. In particular the cellular chain group Hₙ(Xⁿ, Xⁿ⁻¹) is the relative homology of (Xⁿ, TauCeti.skeletonNeighborhood C n).

The point of the replacement is excision: unlike Xⁿ⁻¹, the subspace TauCeti.skeletonNeighborhood C n contains Xⁿ⁻¹ in its interior (TauCeti.skeletonLT_subset_interior_skeletonNeighborhood), so Xⁿ⁻¹ can be excised from the new pair, leaving the open n-cells relative to their outer halves.

Main results #

References #

source
@[reducible, inline]
abbrev TauCeti.skeletonNeighborhoodPair {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) :
TopPair

The pair (Xⁿ, TauCeti.skeletonNeighborhood C n): the n-skeleton skeletonLT C (n + 1) relative to its subset obtained by removing the inner half of every open n-cell.

Equations
Instances For
    source
    def TauCeti.skeletonPairToNeighborhood {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) :
    skeletonPair C n ⟶ skeletonNeighborhoodPair C n

    The inclusion of the skeletal pair (Xⁿ, Xⁿ⁻¹) into (Xⁿ, TauCeti.skeletonNeighborhood C n).

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.skeletonPairToNeighborhood_fst_apply {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) (x : ↑TopPair.fst) :
      (CategoryTheory.ConcreteCategory.hom (TopPair.Hom.fst (skeletonPairToNeighborhood C n))) x = x
      source
      @[simp]
      theorem TauCeti.skeletonPairToNeighborhood_snd_apply {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) (x : ↑TopPair.snd) :
      ↑((CategoryTheory.ConcreteCategory.hom (TopPair.Hom.snd (skeletonPairToNeighborhood C n))) x) = ↑x
      source
      noncomputable def TauCeti.skeletonNeighborhoodToPair {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) :
      skeletonNeighborhoodPair C n ⟶ skeletonPair C n

      The radial deformation retraction, as a map of pairs (Xⁿ, TauCeti.skeletonNeighborhood C n) ⟶ (Xⁿ, Xⁿ⁻¹); it is a homotopy inverse of TauCeti.skeletonPairToNeighborhood.

      Equations
      Instances For
        source
        noncomputable def TauCeti.skeletonPairToNeighborhoodHomotopy {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) :
        TopPair.Homotopy (CategoryTheory.CategoryStruct.comp (skeletonPairToNeighborhood C n) (skeletonNeighborhoodToPair C n)) (CategoryTheory.CategoryStruct.id (skeletonPair C n))

        The inclusion followed by the inverse is homotopic to the identity on the skeletal pair.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def TauCeti.skeletonNeighborhoodToPairHomotopy {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) :
          TopPair.Homotopy (CategoryTheory.CategoryStruct.comp (skeletonNeighborhoodToPair C n) (skeletonPairToNeighborhood C n)) (CategoryTheory.CategoryStruct.id (skeletonNeighborhoodPair C n))

          The inverse followed by the inclusion is homotopic to the identity on the neighborhood pair.

          Equations
          Instances For
            source
            theorem TauCeti.isIso_singularHomologyMap_skeletonPairToNeighborhood {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Preadditive A] [CategoryTheory.CategoryWithHomology A] (R : A) (n k : ℕ) :
            CategoryTheory.IsIso (TopPair.singularHomologyMap (skeletonPairToNeighborhood C n) R k)

            The inclusion (Xⁿ, Xⁿ⁻¹) ⟶ (Xⁿ, TauCeti.skeletonNeighborhood C n) induces isomorphisms on relative singular homology in every degree.

            source
            noncomputable def TauCeti.cellularChainGroupIsoNeighborhood {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) :
            cellularChainGroup C R n ≅ (skeletonNeighborhoodPair C n).singularHomology R n

            The cellular chain group Hₙ(Xⁿ, Xⁿ⁻¹) is the relative singular homology of the pair (Xⁿ, TauCeti.skeletonNeighborhood C n), through TauCeti.skeletonPairToNeighborhood.

            Equations
            Instances For
              source
              @[simp]
              theorem TauCeti.cellularChainGroupIsoNeighborhood_hom {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) :
              (cellularChainGroupIsoNeighborhood C R n).hom = TopPair.singularHomologyMap (skeletonPairToNeighborhood C n) R n