The product of two finite CW complexes

For finite CW complexes C in X and D in Y, the product C ×ˢ D in X × Y is a finite CW complex whose n-cells are the pairs of a p-cell of C and a q-cell of D with p + q = n (TauCeti.cwComplexProd, TauCeti.cellProdEquiv). Mathlib's classical CW complexes parametrise an n-cell by the unit ball of Fin n → ℝ in the sup norm, and appending coordinates Fin.appendIsometryOfEq : (Fin p → ℝ) × (Fin q → ℝ) ≃ᵢ (Fin n → ℝ) is an isometry, so it identifies the product of the unit balls of the factors with the unit ball, and similarly for closed balls. The characteristic map of a product cell is the product of the characteristic maps of its factors after this isometry. The unit sphere of a product is (sphere × closedBall) ∪ (closedBall × sphere), so the boundary of a product cell lies in products of cells of smaller total dimension. With finitely many cells the weak topology condition is automatic (Topology.CWComplex.mkFinite).

Main declarations

• TauCeti.cwComplexProd: the product CW structure on C ×ˢ D, an instance, which is finite (TauCeti.finite_cwComplexProd).
• TauCeti.cellProdEquiv: the n-cells of C ×ˢ D are the pairs of a p-cell of C and a q-cell of D with p + q = n. The characteristic map, open cell, closed cell and boundary of a product cell are described by TauCeti.map_cellProdEquiv_symm_apply, TauCeti.openCell_cellProdEquiv_symm, TauCeti.closedCell_cellProdEquiv_symm and TauCeti.cellFrontier_cellProdEquiv_symm.
• TauCeti.nat_card_cell_prod: C ×ˢ D has ∑_{p + q = n} #(p-cells of C) · #(q-cells of D) cells of dimension n.
• TauCeti.FiniteCWType.prod: a product of two spaces of finite CW type has finite CW type.
• TauCeti.FiniteCWType.pi: a finite product of spaces of finite CW type has finite CW type.

For infinite complexes the product topology can be strictly coarser than the weak topology of the product cells (Hatcher, Theorem A.6, gives conditions under which they agree); this file treats finite complexes, where the two agree automatically.

References

• A. Hatcher, Algebraic Topology, Chapter 0, products of CW complexes, and Appendix, Theorem A.6.

@[instance_reducible]

instance TauCeti.cwComplexProd {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {C : Set X} {D : Set Y} [Topology.CWComplex C] [Topology.CWComplex D] [Topology.RelCWComplex.Finite C] [Topology.RelCWComplex.Finite D] : Topology.CWComplex (C ×ˢ D)

The product of two finite CW complexes. The n-cells of C ×ˢ D are the pairs of a p-cell of C and a q-cell of D with p + q = n (TauCeti.cellProdEquiv), and the characteristic map of such a pair is the product of the characteristic maps after the isometry Fin.appendIsometryOfEq : (Fin p → ℝ) × (Fin q → ℝ) ≃ᵢ (Fin n → ℝ).

instance TauCeti.finite_cwComplexProd {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {C : Set X} {D : Set Y} [Topology.CWComplex C] [Topology.CWComplex D] [Topology.RelCWComplex.Finite C] [Topology.RelCWComplex.Finite D] : Topology.RelCWComplex.Finite (C ×ˢ D)

The product of two finite CW complexes is finite.

noncomputable def TauCeti.cellProdEquiv {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {C : Set X} {D : Set Y} [Topology.CWComplex C] [Topology.CWComplex D] [Topology.RelCWComplex.Finite C] [Topology.RelCWComplex.Finite D] (n : ℕ) : Topology.RelCWComplex.cell (C ×ˢ D) n ≃ (pq : ↥(Finset.antidiagonal n)) × Topology.RelCWComplex.cell C (↑pq).1 × Topology.RelCWComplex.cell D (↑pq).2

The n-cells of C ×ˢ D are the pairs of a p-cell of C and a q-cell of D with p + q = n.

@[simp]

theorem TauCeti.map_cellProdEquiv_symm_apply {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {C : Set X} {D : Set Y} [Topology.CWComplex C] [Topology.CWComplex D] [Topology.RelCWComplex.Finite C] [Topology.RelCWComplex.Finite D] {n : ℕ} (c : (pq : ↥(Finset.antidiagonal n)) × Topology.RelCWComplex.cell C (↑pq).1 × Topology.RelCWComplex.cell D (↑pq).2) (x : Fin n → ℝ) : ↑(Topology.RelCWComplex.map n ((cellProdEquiv n).symm c)) x = (↑(Topology.RelCWComplex.map (↑c.fst).1 c.snd.1) ((Fin.appendIsometryOfEq ⋯).symm x).1, ↑(Topology.RelCWComplex.map (↑c.fst).2 c.snd.2) ((Fin.appendIsometryOfEq ⋯).symm x).2)

The characteristic map of a product cell is the product of the characteristic maps of its factors, after splitting the coordinates of Fin n → ℝ into (Fin p → ℝ) × (Fin q → ℝ).

@[simp]

theorem TauCeti.openCell_cellProdEquiv_symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {C : Set X} {D : Set Y} [Topology.CWComplex C] [Topology.CWComplex D] [Topology.RelCWComplex.Finite C] [Topology.RelCWComplex.Finite D] {n : ℕ} (c : (pq : ↥(Finset.antidiagonal n)) × Topology.RelCWComplex.cell C (↑pq).1 × Topology.RelCWComplex.cell D (↑pq).2) : Topology.RelCWComplex.openCell n ((cellProdEquiv n).symm c) = Topology.RelCWComplex.openCell (↑c.fst).1 c.snd.1 ×ˢ Topology.RelCWComplex.openCell (↑c.fst).2 c.snd.2

The open product cell is the product of the open cells of its factors.

@[simp]

theorem TauCeti.closedCell_cellProdEquiv_symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {C : Set X} {D : Set Y} [Topology.CWComplex C] [Topology.CWComplex D] [Topology.RelCWComplex.Finite C] [Topology.RelCWComplex.Finite D] {n : ℕ} (c : (pq : ↥(Finset.antidiagonal n)) × Topology.RelCWComplex.cell C (↑pq).1 × Topology.RelCWComplex.cell D (↑pq).2) : Topology.RelCWComplex.closedCell n ((cellProdEquiv n).symm c) = Topology.RelCWComplex.closedCell (↑c.fst).1 c.snd.1 ×ˢ Topology.RelCWComplex.closedCell (↑c.fst).2 c.snd.2

The closed product cell is the product of the closed cells of its factors.

@[simp]

theorem TauCeti.cellFrontier_cellProdEquiv_symm {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {C : Set X} {D : Set Y} [Topology.CWComplex C] [Topology.CWComplex D] [Topology.RelCWComplex.Finite C] [Topology.RelCWComplex.Finite D] {n : ℕ} (c : (pq : ↥(Finset.antidiagonal n)) × Topology.RelCWComplex.cell C (↑pq).1 × Topology.RelCWComplex.cell D (↑pq).2) : Topology.RelCWComplex.cellFrontier n ((cellProdEquiv n).symm c) = Topology.RelCWComplex.cellFrontier (↑c.fst).1 c.snd.1 ×ˢ Topology.RelCWComplex.closedCell (↑c.fst).2 c.snd.2 ∪ Topology.RelCWComplex.closedCell (↑c.fst).1 c.snd.1 ×ˢ Topology.RelCWComplex.cellFrontier (↑c.fst).2 c.snd.2

The cell frontier of a product cell is the union of each factor's cell frontier times the other factor's closed cell.

theorem TauCeti.nat_card_cell_prod {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {C : Set X} {D : Set Y} [Topology.CWComplex C] [Topology.CWComplex D] [Topology.RelCWComplex.Finite C] [Topology.RelCWComplex.Finite D] (n : ℕ) : Nat.card (Topology.RelCWComplex.cell (C ×ˢ D) n) = ∑ pq ∈ Finset.antidiagonal n, Nat.card (Topology.RelCWComplex.cell C pq.1) * Nat.card (Topology.RelCWComplex.cell D pq.2)

The number of n-cells of C ×ˢ D is ∑_{p + q = n} #(p-cells of C) · #(q-cells of D).

instance TauCeti.FiniteCWType.prod {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [hX : FiniteCWType X] [hY : FiniteCWType Y] : FiniteCWType (X × Y)

A product of two spaces of finite CW type has finite CW type: it is homotopy equivalent to the product of finite CW complexes modelling the factors.

instance TauCeti.FiniteCWType.pi {ι : Type v} [Finite ι] (X : ι → Type u) [(i : ι) → TopologicalSpace (X i)] [∀ (i : ι), FiniteCWType (X i)] : FiniteCWType ((i : ι) → X i)

A finite product of spaces of finite CW type has finite CW type.