Maps carrying characteristic maps to characteristic maps act on cells

Let f be a map between relative CW complexes that carries the base into the base and the characteristic map of every cell onto the characteristic map of a cell of the same dimension: f ∘ φᵢ = φᵢ' on the closed unit ball. Such a map is cellular (TauCeti.isCellular_of_map_eq, in TauCeti.Topology.CWComplex.Classical.Map), and on cellular chains it relabels the cells: the summand of the cell i in the cellular chain group Hₙ(Xⁿ, Xⁿ⁻¹) is sent identically onto the summand of i' (TauCeti.ι_cellularChainGroupIso_inv_comp_cellularChainGroupMap). With coefficients in a ring this says that f sends each cellular basis vector to a cellular basis vector, with no sign (TauCeti.cellularChainGroupMap_cellularChainBasis).

The deck transformations of the lift of a CW structure along a covering map are maps of this kind, which is how the cellular chains of a free G-CW complex become modules over the group ring. A map that only carries open cells onto open cells acts on the basis up to the local degrees ±1 of the induced self-maps of the cells; the strict compatibility assumed here excludes signs.

References

• A. Hatcher, Algebraic Topology, Section 2.2, cellular maps and cellular homology.

theorem TauCeti.ι_cellularChainGroupIso_inv_comp_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 : ℕ} [CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C n)) A] [CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C' n)) A] {i : Topology.RelCWComplex.cell C n} {i' : Topology.RelCWComplex.cell C' n} (hi : ∀ x ∈ Metric.closedBall 0 1, ∀ (hx : ↑(Topology.RelCWComplex.map n i) x ∈ C), ↑((CategoryTheory.ConcreteCategory.hom f) ⟨↑(Topology.RelCWComplex.map n i) x, hx⟩) = ↑(Topology.RelCWComplex.map n i') x) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : Topology.RelCWComplex.cell C n) => R) i) (CategoryTheory.CategoryStruct.comp (cellularChainGroupIso C R n).inv (cellularChainGroupMap C C' hf R n)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : Topology.RelCWComplex.cell C' n) => R) i') (cellularChainGroupIso C' R n).inv

A map carrying the characteristic map of i onto that of i' sends the summand of i in the cellular chain group onto the summand of i'.

theorem TauCeti.ι_cellularChainGroupIso_inv_comp_cellularChainGroupMap_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 : ℕ} [CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C n)) A] [CategoryTheory.HasExactColimitsOfShape (CategoryTheory.Discrete (Topology.RelCWComplex.cell C' n)) A] {i : Topology.RelCWComplex.cell C n} {i' : Topology.RelCWComplex.cell C' n} (hi : ∀ x ∈ Metric.closedBall 0 1, ∀ (hx : ↑(Topology.RelCWComplex.map n i) x ∈ C), ↑((CategoryTheory.ConcreteCategory.hom f) ⟨↑(Topology.RelCWComplex.map n i) x, hx⟩) = ↑(Topology.RelCWComplex.map n i') x) {Z : A} (h : cellularChainGroup C' R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : Topology.RelCWComplex.cell C n) => R) i) (CategoryTheory.CategoryStruct.comp (cellularChainGroupIso C R n).inv (CategoryTheory.CategoryStruct.comp (cellularChainGroupMap C C' hf R n) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : Topology.RelCWComplex.cell C' n) => R) i') (CategoryTheory.CategoryStruct.comp (cellularChainGroupIso C' R n).inv h)

A map carrying the characteristic map of i onto that of i' sends the summand of i in the cellular chain group onto the summand of i'.

theorem TauCeti.cellularChainGroupMap_cellularChainBasis {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) (R : Type w) [Ring R] {n : ℕ} {i : Topology.RelCWComplex.cell C n} {i' : Topology.RelCWComplex.cell C' n} (hi : ∀ x ∈ Metric.closedBall 0 1, ∀ (hx : ↑(Topology.RelCWComplex.map n i) x ∈ C), ↑((CategoryTheory.ConcreteCategory.hom f) ⟨↑(Topology.RelCWComplex.map n i) x, hx⟩) = ↑(Topology.RelCWComplex.map n i') x) : (CategoryTheory.ConcreteCategory.hom (cellularChainGroupMap C C' hf (↧R) n)) ((cellularChainBasis C R n) i) = (cellularChainBasis C' R n) i'

A map carrying the characteristic map of i onto that of i' sends the cellular basis vector of i to the cellular basis vector of i', with coefficients in a ring.