Cellular maps act on cellular chains #
A continuous map between the carriers of relative CW complexes is cellular when it carries each stage of the skeletal filtration into the stage of the same degree. It then induces maps of consecutive skeletal pairs. Naturality of the connecting morphism of a pair shows that these maps commute with the cellular differential, giving a chain map. Restrictions to skeleta relative to the base and the map of the whole base pairs commute with the skeletal inclusions. These are the maps used in the natural cellular–singular comparison. This construction keeps the maps of pairs visible, so the resulting chain map is induced by the original continuous map.
The mathematical source is Hatcher, Algebraic Topology, Section 2.2.
def
TauCeti.skeletonPairMap
{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 : ℕ)
:
The restrictions to two consecutive skeleta form a map of skeletal pairs.
Equations
- TauCeti.skeletonPairMap C C' hf n = TauCeti.TopTriple.innerPair.map (TauCeti.skeletonTripleMap✝ C C' hf n)
Instances For
@[simp]
theorem
TauCeti.skeletonPairMap_fst
{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 : ℕ)
:
@[simp]
theorem
TauCeti.skeletonPairMap_snd
{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 : ℕ)
:
def
TauCeti.skeletonBasePairMap
{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 : ℕ)
:
A cellular map restricts to each skeleton relative to the base.
Equations
- TauCeti.skeletonBasePairMap C C' hf n = TopPair.ofHom (TauCeti.skeletonMap C C' hf (n + 1)) (TauCeti.skeletonMap C C' hf 0) ⋯
Instances For
@[simp]
theorem
TauCeti.skeletonBasePairMap_fst
{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 : ℕ)
:
@[simp]
theorem
TauCeti.skeletonBasePairMap_snd
{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 : ℕ)
:
def
TauCeti.complexBasePairMap
{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)
:
A cellular map induces a map of the whole complexes relative to their bases.
Equations
- TauCeti.complexBasePairMap C C' hf = TopPair.ofHom f (TauCeti.skeletonMap C C' hf 0) ⋯
Instances For
@[simp]
theorem
TauCeti.complexBasePairMap_fst
{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)
:
@[simp]
theorem
TauCeti.complexBasePairMap_snd
{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)
:
theorem
TauCeti.skeletonBasePairMap_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 (skeletonBasePairMap C C' hf n) (skeletonBasePairInclusion C' h) = CategoryTheory.CategoryStruct.comp (skeletonBasePairInclusion C h) (skeletonBasePairMap C C' hf m)
Restriction relative to the base commutes with inclusions between skeleta.
theorem
TauCeti.skeletonBasePairMap_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 : TopPair}
(h✝ : skeletonBasePair C' m ⟶ Z)
:
Restriction relative to the base commutes with inclusions between skeleta.
theorem
TauCeti.skeletonBasePairMap_comp_toSkeletonPair
{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 (skeletonBasePairMap C C' hf n) (skeletonBasePairToSkeletonPair C' n) = CategoryTheory.CategoryStruct.comp (skeletonBasePairToSkeletonPair C n) (skeletonPairMap C C' hf n)
Restriction relative to the base commutes with the map to a consecutive skeletal pair.
theorem
TauCeti.skeletonBasePairMap_comp_toSkeletonPair_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 : TopPair}
(h : skeletonPair C' n ⟶ Z)
:
Restriction relative to the base commutes with the map to a consecutive skeletal pair.
theorem
TauCeti.skeletonBasePairMap_comp_toComplex
{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 (skeletonBasePairMap C C' hf n) (skeletonBasePairToComplex C' n) = CategoryTheory.CategoryStruct.comp (skeletonBasePairToComplex C n) (complexBasePairMap C C' hf)
Restriction relative to the base commutes with inclusion into the whole complex.
theorem
TauCeti.skeletonBasePairMap_comp_toComplex_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 : TopPair}
(h : complexBasePair C' ⟶ Z)
:
Restriction relative to the base commutes with inclusion into the whole complex.
@[simp]
theorem
TauCeti.skeletonPairMap_id
{X : Type w}
[TopologicalSpace X]
[T2Space X]
{D : Set X}
(C : Set X)
[Topology.RelCWComplex C D]
(n : ℕ)
:
Restriction of the identity map to a skeletal pair is the identity pair map.
@[simp]
theorem
TauCeti.skeletonBasePairMap_id
{X : Type w}
[TopologicalSpace X]
[T2Space X]
{D : Set X}
(C : Set X)
[Topology.RelCWComplex C D]
(n : ℕ)
:
The identity cellular map restricts to the identity on each base pair.
@[simp]
theorem
TauCeti.complexBasePairMap_id
{X : Type w}
[TopologicalSpace X]
[T2Space X]
{D : Set X}
(C : Set X)
[Topology.RelCWComplex C D]
:
The identity cellular map induces the identity on the whole base pair.
theorem
TauCeti.skeletonPairMap_comp
{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)
{Z : Type w}
[TopologicalSpace Z]
[T2Space Z]
{F : Set Z}
(C'' : Set Z)
[Topology.RelCWComplex C'' F]
{g : ↧↑C' ⟶ ↧↑C''}
(hg : IsCellular C' C'' g)
(n : ℕ)
:
skeletonPairMap C C'' ⋯ n = CategoryTheory.CategoryStruct.comp (skeletonPairMap C C' hf n) (skeletonPairMap C' C'' hg n)
Maps of skeletal pairs respect composition of cellular maps.
theorem
TauCeti.skeletonPairMap_comp_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)
{Z : Type w}
[TopologicalSpace Z]
[T2Space Z]
{F : Set Z}
(C'' : Set Z)
[Topology.RelCWComplex C'' F]
{g : ↧↑C' ⟶ ↧↑C''}
(hg : IsCellular C' C'' g)
(n : ℕ)
{Z✝ : TopPair}
(h : skeletonPair C'' n ⟶ Z✝)
:
CategoryTheory.CategoryStruct.comp (skeletonPairMap C C'' ⋯ n) h = CategoryTheory.CategoryStruct.comp (skeletonPairMap C C' hf n)
(CategoryTheory.CategoryStruct.comp (skeletonPairMap C' C'' hg n) h)
Maps of skeletal pairs respect composition of cellular maps.
theorem
TauCeti.skeletonBasePairMap_comp
{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)
{Z : Type w}
[TopologicalSpace Z]
[T2Space Z]
{F : Set Z}
(C'' : Set Z)
[Topology.RelCWComplex C'' F]
{g : ↧↑C' ⟶ ↧↑C''}
(hg : IsCellular C' C'' g)
(n : ℕ)
:
skeletonBasePairMap C C'' ⋯ n = CategoryTheory.CategoryStruct.comp (skeletonBasePairMap C C' hf n) (skeletonBasePairMap C' C'' hg n)
Restrictions to base pairs respect composition of cellular maps.
theorem
TauCeti.skeletonBasePairMap_comp_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)
{Z : Type w}
[TopologicalSpace Z]
[T2Space Z]
{F : Set Z}
(C'' : Set Z)
[Topology.RelCWComplex C'' F]
{g : ↧↑C' ⟶ ↧↑C''}
(hg : IsCellular C' C'' g)
(n : ℕ)
{Z✝ : TopPair}
(h : skeletonBasePair C'' n ⟶ Z✝)
:
CategoryTheory.CategoryStruct.comp (skeletonBasePairMap C C'' ⋯ n) h = CategoryTheory.CategoryStruct.comp (skeletonBasePairMap C C' hf n)
(CategoryTheory.CategoryStruct.comp (skeletonBasePairMap C' C'' hg n) h)
Restrictions to base pairs respect composition of cellular maps.
theorem
TauCeti.complexBasePairMap_comp
{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)
{Z : Type w}
[TopologicalSpace Z]
[T2Space Z]
{F : Set Z}
(C'' : Set Z)
[Topology.RelCWComplex C'' F]
{g : ↧↑C' ⟶ ↧↑C''}
(hg : IsCellular C' C'' g)
:
complexBasePairMap C C'' ⋯ = CategoryTheory.CategoryStruct.comp (complexBasePairMap C C' hf) (complexBasePairMap C' C'' hg)
Maps of whole base pairs respect composition of cellular maps.
theorem
TauCeti.complexBasePairMap_comp_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)
{Z : Type w}
[TopologicalSpace Z]
[T2Space Z]
{F : Set Z}
(C'' : Set Z)
[Topology.RelCWComplex C'' F]
{g : ↧↑C' ⟶ ↧↑C''}
(hg : IsCellular C' C'' g)
{Z✝ : TopPair}
(h : complexBasePair C'' ⟶ Z✝)
:
CategoryTheory.CategoryStruct.comp (complexBasePairMap C C'' ⋯) h = CategoryTheory.CategoryStruct.comp (complexBasePairMap C C' hf)
(CategoryTheory.CategoryStruct.comp (complexBasePairMap C' C'' hg) h)
Maps of whole base pairs respect composition of cellular maps.
noncomputable def
TauCeti.cellularChainGroupMap
{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)
{A : Type u}
[CategoryTheory.Category.{v, u} A]
[CategoryTheory.Limits.HasCoproducts A]
[CategoryTheory.Abelian A]
(R : A)
(n : ℕ)
:
A cellular map induces a morphism on each cellular chain group.
Equations
- TauCeti.cellularChainGroupMap C C' hf R n = TopPair.singularHomologyMap (TauCeti.skeletonPairMap C C' hf n) R n
Instances For
theorem
TauCeti.cellularChainGroupMap_def
{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)
{A : Type u}
[CategoryTheory.Category.{v, u} A]
[CategoryTheory.Limits.HasCoproducts A]
[CategoryTheory.Abelian A]
(R : A)
(n : ℕ)
:
The map on a cellular chain group is relative singular homology of the skeletal pair map. This formula allows importing modules to rewrite without exposing the definition's body.
@[simp]
theorem
TauCeti.cellularChainGroupMap_id
{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 : ℕ)
:
The identity cellular map acts as the identity on each cellular chain group.
theorem
TauCeti.cellularChainGroupMap_comp
{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)
{Z : Type w}
[TopologicalSpace Z]
[T2Space Z]
{F : Set Z}
(C'' : Set Z)
[Topology.RelCWComplex C'' F]
{g : ↧↑C' ⟶ ↧↑C''}
(hg : IsCellular C' C'' g)
{A : Type u}
[CategoryTheory.Category.{v, u} A]
[CategoryTheory.Limits.HasCoproducts A]
[CategoryTheory.Abelian A]
(R : A)
(n : ℕ)
:
cellularChainGroupMap C C'' ⋯ R n = CategoryTheory.CategoryStruct.comp (cellularChainGroupMap C C' hf R n) (cellularChainGroupMap C' C'' hg R n)
The maps on cellular chain groups respect composition of cellular maps.
theorem
TauCeti.cellularChainGroupMap_comp_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)
{Z : Type w}
[TopologicalSpace Z]
[T2Space Z]
{F : Set Z}
(C'' : Set Z)
[Topology.RelCWComplex C'' F]
{g : ↧↑C' ⟶ ↧↑C''}
(hg : IsCellular C' C'' g)
{A : Type u}
[CategoryTheory.Category.{v, u} A]
[CategoryTheory.Limits.HasCoproducts A]
[CategoryTheory.Abelian A]
(R : A)
(n : ℕ)
{Z✝ : A}
(h : cellularChainGroup C'' R n ⟶ Z✝)
:
CategoryTheory.CategoryStruct.comp (cellularChainGroupMap C C'' ⋯ R n) h = CategoryTheory.CategoryStruct.comp (cellularChainGroupMap C C' hf R n)
(CategoryTheory.CategoryStruct.comp (cellularChainGroupMap C' C'' hg R n) h)
The maps on cellular chain groups respect composition of cellular maps.
theorem
TauCeti.cellularChainGroupMap_comp_cellularDifferential
{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)
{A : Type u}
[CategoryTheory.Category.{v, u} A]
[CategoryTheory.Limits.HasCoproducts A]
[CategoryTheory.Abelian A]
(R : A)
(n : ℕ)
:
CategoryTheory.CategoryStruct.comp (cellularChainGroupMap C C' hf R (n + 1)) (cellularDifferential C' R n) = CategoryTheory.CategoryStruct.comp (cellularDifferential C R n) (cellularChainGroupMap C C' hf R n)
The cellular chain-group maps commute with the cellular differential.
theorem
TauCeti.cellularChainGroupMap_comp_cellularDifferential_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)
{A : Type u}
[CategoryTheory.Category.{v, u} A]
[CategoryTheory.Limits.HasCoproducts A]
[CategoryTheory.Abelian A]
(R : A)
(n : ℕ)
{Z : A}
(h : cellularChainGroup C' R n ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (cellularChainGroupMap C C' hf R (n + 1))
(CategoryTheory.CategoryStruct.comp (cellularDifferential C' R n) h) = CategoryTheory.CategoryStruct.comp (cellularDifferential C R n)
(CategoryTheory.CategoryStruct.comp (cellularChainGroupMap C C' hf R n) h)
The cellular chain-group maps commute with the cellular differential.
noncomputable def
TauCeti.cellularChainComplexMap
{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)
{A : Type u}
[CategoryTheory.Category.{v, u} A]
[CategoryTheory.Limits.HasCoproducts A]
[CategoryTheory.Abelian A]
(R : A)
:
A cellular map induces a chain map between the cellular chain complexes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TauCeti.cellularChainComplexMap_f
{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)
{A : Type u}
[CategoryTheory.Category.{v, u} A]
[CategoryTheory.Limits.HasCoproducts A]
[CategoryTheory.Abelian A]
(R : A)
(n : ℕ)
:
(cellularChainComplexMap C C' hf R).f n = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
(CategoryTheory.CategoryStruct.comp (cellularChainGroupMap C C' hf R n) (CategoryTheory.eqToHom ⋯))
@[simp]
theorem
TauCeti.cellularChainComplexMap_id
{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)
:
The identity cellular map induces the identity chain map.
theorem
TauCeti.cellularChainComplexMap_comp
{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)
{Z : Type w}
[TopologicalSpace Z]
[T2Space Z]
{F : Set Z}
(C'' : Set Z)
[Topology.RelCWComplex C'' F]
{g : ↧↑C' ⟶ ↧↑C''}
(hg : IsCellular C' C'' g)
{A : Type u}
[CategoryTheory.Category.{v, u} A]
[CategoryTheory.Limits.HasCoproducts A]
[CategoryTheory.Abelian A]
(R : A)
:
cellularChainComplexMap C C'' ⋯ R = CategoryTheory.CategoryStruct.comp (cellularChainComplexMap C C' hf R) (cellularChainComplexMap C' C'' hg R)
Composition of cellular maps induces composition of cellular chain maps.
theorem
TauCeti.cellularChainComplexMap_comp_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)
{Z : Type w}
[TopologicalSpace Z]
[T2Space Z]
{F : Set Z}
(C'' : Set Z)
[Topology.RelCWComplex C'' F]
{g : ↧↑C' ⟶ ↧↑C''}
(hg : IsCellular C' C'' g)
{A : Type u}
[CategoryTheory.Category.{v, u} A]
[CategoryTheory.Limits.HasCoproducts A]
[CategoryTheory.Abelian A]
(R : A)
{Z✝ : ChainComplex A ℕ}
(h : cellularChainComplex C'' R ⟶ Z✝)
:
CategoryTheory.CategoryStruct.comp (cellularChainComplexMap C C'' ⋯ R) h = CategoryTheory.CategoryStruct.comp (cellularChainComplexMap C C' hf R)
(CategoryTheory.CategoryStruct.comp (cellularChainComplexMap C' C'' hg R) h)
Composition of cellular maps induces composition of cellular chain maps.