Documentation

TauCeti.Topology.CWComplex.Classical.Map

Cellular maps of relative CW complexes #

A cellular map preserves the skeletal filtration of a relative CW complex. This condition ensures that the map restricts to each skeleton and to each consecutive skeletal pair, the restrictions used to act on cellular chains.

The mathematical source is Hatcher, Algebraic Topology, Section 2.2.

source
@[reducible, inline]
abbrev TauCeti.IsCellular {X Y : Type w} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] {D : Set X} {E : Set Y} (C : Set X) [Topology.RelCWComplex C D] (C' : Set Y) [Topology.RelCWComplex C' E] (f : ↧↑C ⟶ ↧↑C') :
Prop

A map of relative CW complexes is cellular if it preserves every stage of the skeletal filtration. In particular, it sends the base (stage zero) into the target base.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem TauCeti.isCellular_id {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] :
    IsCellular C C (CategoryTheory.CategoryStruct.id ↧↑C)

    The identity map preserves every skeleton.

    source
    theorem TauCeti.IsCellular.comp {X Y Z : Type w} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] [TopologicalSpace Z] [T2Space Z] {D : Set X} {E : Set Y} {F : Set Z} (C : Set X) [Topology.RelCWComplex C D] (C' : Set Y) [Topology.RelCWComplex C' E] {C'' : Set Z} [Topology.RelCWComplex C'' F] {f : ↧↑C ⟶ ↧↑C'} {g : ↧↑C' ⟶ ↧↑C''} (hf : IsCellular C C' f) (hg : IsCellular C' C'' g) :
    IsCellular C C'' (CategoryTheory.CategoryStruct.comp f g)

    The composite of cellular maps is cellular.

    source
    def TauCeti.skeletonMap {X Y : Type w} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] {D : Set X} {E : Set Y} (C : Set X) [Topology.RelCWComplex C D] (C' : Set Y) [Topology.RelCWComplex C' E] {f : ↧↑C ⟶ ↧↑C'} (hf : IsCellular C C' f) (n : ℕ) :
    skeletonObj C n ⟶ skeletonObj C' n

    The restriction of a cellular map to the n-th stage of the skeletal filtration.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.skeletonMap_apply {X Y : Type w} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] {D : Set X} {E : Set Y} (C : Set X) [Topology.RelCWComplex C D] (C' : Set Y) [Topology.RelCWComplex C' E] {f : ↧↑C ⟶ ↧↑C'} (hf : IsCellular C C' f) (n : ℕ) (x : ↑(skeletonObj C n)) :
      (TopCat.Hom.hom (skeletonMap C C' hf n)).toFun x = ⟨↑((CategoryTheory.ConcreteCategory.hom f) ⟨↑x, ⋯⟩), ⋯⟩

      On points, the restriction to a skeleton agrees with the original cellular map.

      source
      theorem TauCeti.skeletonMap_comp_inclusion {X Y : Type w} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] {D : Set X} {E : Set Y} (C : Set X) [Topology.RelCWComplex C D] (C' : Set Y) [Topology.RelCWComplex C' E] {f : ↧↑C ⟶ ↧↑C'} (hf : IsCellular C C' f) {n m : ℕ} (h : n ≤ m) :
      CategoryTheory.CategoryStruct.comp (skeletonMap C C' hf n) (TopCat.ofHom (ContinuousMap.inclusion ⋯)) = CategoryTheory.CategoryStruct.comp (TopCat.ofHom (ContinuousMap.inclusion ⋯)) (skeletonMap C C' hf m)

      Restriction of a cellular map commutes with inclusions of skeleta.

      source
      theorem TauCeti.skeletonMap_comp_inclusion_assoc {X Y : Type w} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] {D : Set X} {E : Set Y} (C : Set X) [Topology.RelCWComplex C D] (C' : Set Y) [Topology.RelCWComplex C' E] {f : ↧↑C ⟶ ↧↑C'} (hf : IsCellular C C' f) {n m : ℕ} (h : n ≤ m) {Z : TopCat} (h✝ : ↧↑↑(Topology.RelCWComplex.skeletonLT C' ↑m) ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (skeletonMap C C' hf n) (CategoryTheory.CategoryStruct.comp (TopCat.ofHom (ContinuousMap.inclusion ⋯)) h✝) = CategoryTheory.CategoryStruct.comp (TopCat.ofHom (ContinuousMap.inclusion ⋯)) (CategoryTheory.CategoryStruct.comp (skeletonMap C C' hf m) h✝)

      Restriction of a cellular map commutes with inclusions of skeleta.

      source
      theorem TauCeti.skeletonMap_comp_inclusion_complex {X Y : Type w} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] {D : Set X} {E : Set Y} (C : Set X) [Topology.RelCWComplex C D] (C' : Set Y) [Topology.RelCWComplex C' E] {f : ↧↑C ⟶ ↧↑C'} (hf : IsCellular C C' f) (n : ℕ) :
      CategoryTheory.CategoryStruct.comp (skeletonMap C C' hf n) (TopCat.ofHom (ContinuousMap.inclusion ⋯)) = CategoryTheory.CategoryStruct.comp (TopCat.ofHom (ContinuousMap.inclusion ⋯)) f

      Restriction of a cellular map commutes with inclusion of a skeleton into the complex.

      source
      theorem TauCeti.skeletonMap_comp_inclusion_complex_assoc {X Y : Type w} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] {D : Set X} {E : Set Y} (C : Set X) [Topology.RelCWComplex C D] (C' : Set Y) [Topology.RelCWComplex C' E] {f : ↧↑C ⟶ ↧↑C'} (hf : IsCellular C C' f) (n : ℕ) {Z : TopCat} (h : ↧↑C' ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (skeletonMap C C' hf n) (CategoryTheory.CategoryStruct.comp (TopCat.ofHom (ContinuousMap.inclusion ⋯)) h) = CategoryTheory.CategoryStruct.comp (TopCat.ofHom (ContinuousMap.inclusion ⋯)) (CategoryTheory.CategoryStruct.comp f h)

      Restriction of a cellular map commutes with inclusion of a skeleton into the complex.

      source
      @[simp]
      theorem TauCeti.skeletonMap_id {X : Type w} [TopologicalSpace X] [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] (n : ℕ) :
      skeletonMap C C ⋯ n = CategoryTheory.CategoryStruct.id (skeletonObj C n)

      Restriction of the identity map to a skeleton is the identity.

      source
      theorem TauCeti.skeletonMap_comp {X Y Z : Type w} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] [TopologicalSpace Z] [T2Space Z] {D : Set X} {E : Set Y} {F : Set Z} (C : Set X) [Topology.RelCWComplex C D] (C' : Set Y) [Topology.RelCWComplex C' E] {f : ↧↑C ⟶ ↧↑C'} (hf : IsCellular C C' f) (C'' : Set Z) [Topology.RelCWComplex C'' F] {g : ↧↑C' ⟶ ↧↑C''} (hg : IsCellular C' C'' g) (n : ℕ) :
      skeletonMap C C'' ⋯ n = CategoryTheory.CategoryStruct.comp (skeletonMap C C' hf n) (skeletonMap C' C'' hg n)

      Restriction to a skeleton respects composition of cellular maps.

      source
      theorem TauCeti.skeletonMap_comp_assoc {X Y Z : Type w} [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] [TopologicalSpace Z] [T2Space Z] {D : Set X} {E : Set Y} {F : Set Z} (C : Set X) [Topology.RelCWComplex C D] (C' : Set Y) [Topology.RelCWComplex C' E] {f : ↧↑C ⟶ ↧↑C'} (hf : IsCellular C C' f) (C'' : Set Z) [Topology.RelCWComplex C'' F] {g : ↧↑C' ⟶ ↧↑C''} (hg : IsCellular C' C'' g) (n : ℕ) {Z✝ : TopCat} (h : skeletonObj C'' n ⟶ Z✝) :
      CategoryTheory.CategoryStruct.comp (skeletonMap C C'' ⋯ n) h = CategoryTheory.CategoryStruct.comp (skeletonMap C C' hf n) (CategoryTheory.CategoryStruct.comp (skeletonMap C' C'' hg n) h)

      Restriction to a skeleton respects composition of cellular maps.