Lifting a CW structure along a covering map

Let p : E → B be a covering map and let C be a CW complex in the Hausdorff space B. The closed unit ball is convex, so the characteristic map of each cell of C lifts through p, uniquely once the lift of one point is prescribed (IsCoveringMap.existsUnique_continuousMap_lifts_of_convex). Lifting every characteristic map through every point over the centre of its cell makes p ⁻¹' C a CW complex (TauCeti.cwComplexPreimage):

• its n-cells are the pairs of an n-cell i of C and a point of E over the centre map n i 0 (TauCeti.cellPreimageEquiv);
• the characteristic map of such a pair lifts the characteristic map of i (TauCeti.apply_map_cellPreimageEquiv_symm) and sends the centre to the chosen point (TauCeti.map_cellPreimageEquiv_symm_zero).

The open cells of distinct pairs are disjoint because two lifts of one characteristic map that meet are equal, and every point of E over a closed cell of C lies on a lift of that cell, which gives the covering of p ⁻¹' C by the closed lifted cells. Near a point of a lift, every point over the characteristic map lies on that same lift, because p is a local homeomorphism. Two consequences of this local rigidity finish the construction. Only finitely many lifts of a cell meet a compact set, which bounds the boundary of a lifted cell by finitely many lifted cells. And the lift has the weak topology: a set meeting every closed lifted cell in a closed set is, near each point, the preimage under a local inverse of p of a set meeting every closed cell of C in a closed set. The covering map is cellular for the lifted structure (TauCeti.isCellular_restrictPreimage).

When p is the quotient covering map of a free action of a group G on E (IsQuotientCoveringMap p G), the group permutes the lifted cells (TauCeti.cellPreimageMulAction), translating characteristic maps (TauCeti.map_smul_cellPreimage). The action is free (TauCeti.isCancelSMul_cellPreimage), and there is exactly one orbit over each cell of C (TauCeti.exists_cellPreimageEquiv_fst_eq and TauCeti.exists_smul_eq_iff_cellPreimageEquiv_fst_eq): for a choice s of lifts of the cells of C, the lifted cells are the translates g • s i, each exactly once (TauCeti.sigmaSMulLiftEquiv). Translation by g, restricted to p ⁻¹' C (TauCeti.preimageSMul), is cellular (TauCeti.isCellular_preimageSMul).

For a finite CW complex and a cover with finite fibres the lift is finite (TauCeti.finite_cwComplexPreimage). Counting cells, if C has finitely many cells in each dimension, p ⁻¹' C has, in each dimension, the sum over the cells of C of the number of points over their centres (TauCeti.nat_card_cell_preimage), so d times as many cells as C when every fibre over C has d points (TauCeti.nat_card_cell_preimage_of_card_fiber). This is the input for the multiplicativity of the Euler characteristic in finite covers. In particular the total space of such a cover of a finite CW complex is a finite CW complex. More generally, the total space of a cover with finite fibres of a space of finite CW type has finite CW type (IsCoveringMap.finiteCWType): pulled back along a homotopy equivalence with a finite CW complex, the cover becomes a finite CW complex homotopy equivalent to its total space (IsCoveringMap.pullbackHomotopyEquiv).

References

• A. Hatcher, Algebraic Topology, Section 1.3, Proposition 1.33 (the lifting criterion), and the exercises of Section 2.2 on the Euler characteristic of an n-sheeted covering space.
• T. tom Dieck, Transformation Groups, de Gruyter, 1987, Section II.1 (free G-CW complexes).

@[instance_reducible]

noncomputable def TauCeti.cwComplexPreimage {E B : Type u} [TopologicalSpace B] {p : E → B} (C : Set B) [TopologicalSpace E] [Topology.CWComplex C] [T2Space B] (hp : IsCoveringMap p) : Topology.CWComplex (p ⁻¹' C)

A CW structure lifts along a covering map. If C is a CW complex in the Hausdorff space B and p : E → B is a covering map, then p ⁻¹' C is a CW complex in E. Its n-cells are the pairs of an n-cell of C and a point of E over the centre of that cell (TauCeti.cellPreimageEquiv); the characteristic map of such a pair is the lift of the characteristic map of the cell through p sending the centre to the chosen point.

noncomputable def TauCeti.cellPreimageEquiv {E B : Type u} [TopologicalSpace B] {p : E → B} (C : Set B) [TopologicalSpace E] [Topology.CWComplex C] [T2Space B] (hp : IsCoveringMap p) (n : ℕ) : Topology.RelCWComplex.cell (p ⁻¹' C) n ≃ (i : Topology.RelCWComplex.cell C n) × ↑(p ⁻¹' {↑(Topology.RelCWComplex.map n i) 0})

The n-cells of the lift of C along p are the pairs of an n-cell i of C and a point of E over the centre map n i 0 of that cell.

theorem TauCeti.map_cellPreimageEquiv_symm_zero {E B : Type u} [TopologicalSpace B] {p : E → B} (C : Set B) [TopologicalSpace E] [Topology.CWComplex C] [T2Space B] (hp : IsCoveringMap p) {n : ℕ} (c : (i : Topology.RelCWComplex.cell C n) × ↑(p ⁻¹' {↑(Topology.RelCWComplex.map n i) 0})) : ↑(Topology.RelCWComplex.map n ((cellPreimageEquiv C hp n).symm c)) 0 = ↑c.snd

The characteristic map of a lifted cell sends the centre to the chosen point over the centre of the underlying cell.

theorem TauCeti.apply_map_cellPreimageEquiv_symm {E B : Type u} [TopologicalSpace B] {p : E → B} (C : Set B) [TopologicalSpace E] [Topology.CWComplex C] [T2Space B] (hp : IsCoveringMap p) {n : ℕ} (c : (i : Topology.RelCWComplex.cell C n) × ↑(p ⁻¹' {↑(Topology.RelCWComplex.map n i) 0})) {x : Fin n → ℝ} (hx : x ∈ Metric.closedBall 0 1) : p (↑(Topology.RelCWComplex.map n ((cellPreimageEquiv C hp n).symm c)) x) = ↑(Topology.RelCWComplex.map n c.fst) x

The characteristic map of a lifted cell lifts the characteristic map of the underlying cell on the closed unit ball.

theorem TauCeti.exists_cellPreimageEquiv_fst_eq {E B : Type u} [TopologicalSpace B] {p : E → B} (C : Set B) [TopologicalSpace E] [Topology.CWComplex C] [T2Space B] (hp : IsCoveringMap p) {n : ℕ} (hsurj : Function.Surjective p) (i : Topology.RelCWComplex.cell C n) : ∃ (c : Topology.RelCWComplex.cell (p ⁻¹' C) n), ((cellPreimageEquiv C hp n) c).fst = i

Over a surjective covering map, every cell of C has a lift.

theorem TauCeti.finite_cwComplexPreimage {E B : Type u} [TopologicalSpace B] {p : E → B} (C : Set B) [TopologicalSpace E] [Topology.CWComplex C] [T2Space B] (hp : IsCoveringMap p) [Topology.RelCWComplex.Finite C] (hfin : ∀ (b : B), Finite ↑(p ⁻¹' {b})) : Topology.RelCWComplex.Finite (p ⁻¹' C)

The lift of a finite CW complex along a covering map with finite fibres is finite.

theorem TauCeti.nat_card_cell_preimage {E B : Type u} [TopologicalSpace B] {p : E → B} (C : Set B) [TopologicalSpace E] [Topology.CWComplex C] [T2Space B] (hp : IsCoveringMap p) {n : ℕ} [Topology.RelCWComplex.FiniteType C] (hfin : ∀ (b : B), Finite ↑(p ⁻¹' {b})) : Nat.card (Topology.RelCWComplex.cell (p ⁻¹' C) n) = ∑ᶠ (i : Topology.RelCWComplex.cell C n), Nat.card ↑(p ⁻¹' {↑(Topology.RelCWComplex.map n i) 0})

The number of n-cells of the lift of C along p is the sum, over the n-cells of C, of the number of points over their centres.

theorem TauCeti.nat_card_cell_preimage_of_card_fiber {E B : Type u} [TopologicalSpace B] {p : E → B} (C : Set B) [TopologicalSpace E] [Topology.CWComplex C] [T2Space B] (hp : IsCoveringMap p) {n : ℕ} [Topology.RelCWComplex.FiniteType C] (hfin : ∀ (b : B), Finite ↑(p ⁻¹' {b})) {d : ℕ} (hd : ∀ b ∈ C, Nat.card ↑(p ⁻¹' {b}) = d) : Nat.card (Topology.RelCWComplex.cell (p ⁻¹' C) n) = d * Nat.card (Topology.RelCWComplex.cell C n)

Cells of a d-sheeted cover. If every fibre of p over C has d points, the lift of C along p has d times as many n-cells as C.

theorem IsCoveringMap.finiteCWType {E B : Type u} [TopologicalSpace B] {p : E → B} [TopologicalSpace E] [TauCeti.FiniteCWType B] (hp : IsCoveringMap p) (hfin : ∀ (b : B), Finite ↑(p ⁻¹' {b})) : TauCeti.FiniteCWType E

The total space of a covering, with finite fibres, of a space of finite CW type has finite CW type.

theorem TauCeti.isCellular_restrictPreimage {E B : Type u} [TopologicalSpace B] {p : E → B} (C : Set B) [TopologicalSpace E] [Topology.CWComplex C] [T2Space B] (hp : IsCoveringMap p) : IsCellular (p ⁻¹' C) C (TopCat.ofHom { toFun := C.restrictPreimage p, continuous_toFun := ⋯ })

The covering map is cellular for the lifted CW structure, as a map from p ⁻¹' C to C: the lifted open n-cells lie over the open n-cells of C.

The deck action on the lifted cells

When p is the quotient covering map of a free action of a group G on E (IsQuotientCoveringMap p G), the group permutes the lifted cells: g carries the lift through a point e over the centre of a cell to the lift through g • e. The action is free, and its orbits are exactly the sets of lifts of one cell of C.

def TauCeti.preimageSMul {E B : Type u} [TopologicalSpace B] {p : E → B} (C : Set B) [TopologicalSpace E] {G : Type u_1} [Group G] [MulAction G E] (hG : IsQuotientCoveringMap p G) (g : G) : ↧↑(p ⁻¹' C) ⟶ ↧↑(p ⁻¹' C)

Translation by g, restricted to the preimage p ⁻¹' C, which it preserves because p is invariant under the action.

@[simp]

theorem TauCeti.coe_preimageSMul_apply {E B : Type u} [TopologicalSpace B] {p : E → B} (C : Set B) [TopologicalSpace E] {G : Type u_1} [Group G] [MulAction G E] (hG : IsQuotientCoveringMap p G) (g : G) (x : ↑(p ⁻¹' C)) : ↑((CategoryTheory.ConcreteCategory.hom (preimageSMul C hG g)) x) = g • ↑x

@[simp]

theorem TauCeti.preimageSMul_one {E B : Type u} [TopologicalSpace B] {p : E → B} (C : Set B) [TopologicalSpace E] {G : Type u_1} [Group G] [MulAction G E] (hG : IsQuotientCoveringMap p G) : preimageSMul C hG 1 = CategoryTheory.CategoryStruct.id ↧↑(p ⁻¹' C)

Translation by the identity is the identity on the preimage subset.

theorem TauCeti.preimageSMul_mul {E B : Type u} [TopologicalSpace B] {p : E → B} (C : Set B) [TopologicalSpace E] {G : Type u_1} [Group G] [MulAction G E] (hG : IsQuotientCoveringMap p G) (g h : G) : preimageSMul C hG (g * h) = CategoryTheory.CategoryStruct.comp (preimageSMul C hG h) (preimageSMul C hG g)

Translation by a product is successive translation on the preimage subset.

@[implicit_reducible]

noncomputable def TauCeti.cellPreimageMulAction {E B : Type u} [TopologicalSpace B] {p : E → B} (C : Set B) [TopologicalSpace E] {G : Type u_1} [Group G] [MulAction G E] (hG : IsQuotientCoveringMap p G) [Topology.CWComplex C] [T2Space B] (n : ℕ) : MulAction G (Topology.RelCWComplex.cell (p ⁻¹' C) n)

The action of G on the n-cells of the lift of C along a quotient covering map, by its action on the points over the centres of the cells of C.

@[simp]

theorem TauCeti.cellPreimageEquiv_smul_fst {E B : Type u} [TopologicalSpace B] {p : E → B} (C : Set B) [TopologicalSpace E] {G : Type u_1} [Group G] [MulAction G E] (hG : IsQuotientCoveringMap p G) {n : ℕ} [Topology.CWComplex C] [T2Space B] (g : G) (c : Topology.RelCWComplex.cell (p ⁻¹' C) n) : ((cellPreimageEquiv C ⋯ n) (g • c)).fst = ((cellPreimageEquiv C ⋯ n) c).fst

The first component of cellPreimageEquiv of a translated cell: translation does not move the underlying cell of C.

@[simp]

theorem TauCeti.coe_cellPreimageEquiv_smul_snd {E B : Type u} [TopologicalSpace B] {p : E → B} (C : Set B) [TopologicalSpace E] {G : Type u_1} [Group G] [MulAction G E] (hG : IsQuotientCoveringMap p G) {n : ℕ} [Topology.CWComplex C] [T2Space B] (g : G) (c : Topology.RelCWComplex.cell (p ⁻¹' C) n) : ↑((cellPreimageEquiv C ⋯ n) (g • c)).snd = g • ↑((cellPreimageEquiv C ⋯ n) c).snd

The second component of cellPreimageEquiv of a translated cell: the chosen point over the centre is translated.

theorem TauCeti.map_smul_cellPreimage {E B : Type u} [TopologicalSpace B] {p : E → B} (C : Set B) [TopologicalSpace E] {G : Type u_1} [Group G] [MulAction G E] (hG : IsQuotientCoveringMap p G) {n : ℕ} [Topology.CWComplex C] [T2Space B] (g : G) (c : Topology.RelCWComplex.cell (p ⁻¹' C) n) (x : Fin n → ℝ) : ↑(Topology.RelCWComplex.map n (g • c)) x = g • ↑(Topology.RelCWComplex.map n c) x

The characteristic map of a translated cell is the translate of the characteristic map.

theorem TauCeti.isCancelSMul_cellPreimage {E B : Type u} [TopologicalSpace B] {p : E → B} (C : Set B) [TopologicalSpace E] {G : Type u_1} [Group G] [MulAction G E] (hG : IsQuotientCoveringMap p G) {n : ℕ} [Topology.CWComplex C] [T2Space B] : IsCancelSMul G (Topology.RelCWComplex.cell (p ⁻¹' C) n)

G acts freely on the lifted cells.

theorem TauCeti.exists_smul_eq_iff_cellPreimageEquiv_fst_eq {E B : Type u} [TopologicalSpace B] {p : E → B} (C : Set B) [TopologicalSpace E] {G : Type u_1} [Group G] [MulAction G E] (hG : IsQuotientCoveringMap p G) {n : ℕ} [Topology.CWComplex C] [T2Space B] (c c' : Topology.RelCWComplex.cell (p ⁻¹' C) n) : (∃ (g : G), g • c = c') ↔ ((cellPreimageEquiv C ⋯ n) c).fst = ((cellPreimageEquiv C ⋯ n) c').fst

Two lifted cells lie in the same G-orbit exactly when they lift the same cell of C.

theorem TauCeti.isCellular_preimageSMul {E B : Type u} [TopologicalSpace B] {p : E → B} (C : Set B) [TopologicalSpace E] {G : Type u_1} [Group G] [MulAction G E] (hG : IsQuotientCoveringMap p G) [Topology.CWComplex C] [T2Space B] (g : G) : IsCellular (p ⁻¹' C) (p ⁻¹' C) (preimageSMul C hG g)

Translation by a group element is cellular for the lifted CW structure.

noncomputable def TauCeti.sigmaSMulLiftEquiv {E B : Type u} [TopologicalSpace B] {p : E → B} (C : Set B) [TopologicalSpace E] {G : Type u_1} [Group G] [MulAction G E] (hG : IsQuotientCoveringMap p G) {n : ℕ} [Topology.CWComplex C] [T2Space B] (s : Topology.RelCWComplex.cell C n → Topology.RelCWComplex.cell (p ⁻¹' C) n) (hs : ∀ (i : Topology.RelCWComplex.cell C n), ((cellPreimageEquiv C ⋯ n) (s i)).fst = i) : (_ : Topology.RelCWComplex.cell C n) × G ≃ Topology.RelCWComplex.cell (p ⁻¹' C) n

Given a lift s i of each n-cell i of C, the lifted n-cells are the translates g • s i, each exactly once.

@[simp]

theorem TauCeti.sigmaSMulLiftEquiv_apply {E B : Type u} [TopologicalSpace B] {p : E → B} (C : Set B) [TopologicalSpace E] {G : Type u_1} [Group G] [MulAction G E] (hG : IsQuotientCoveringMap p G) {n : ℕ} [Topology.CWComplex C] [T2Space B] (s : Topology.RelCWComplex.cell C n → Topology.RelCWComplex.cell (p ⁻¹' C) n) (hs : ∀ (i : Topology.RelCWComplex.cell C n), ((cellPreimageEquiv C ⋯ n) (s i)).fst = i) (x : (_ : Topology.RelCWComplex.cell C n) × G) : (sigmaSMulLiftEquiv C hG s hs) x = x.snd • s x.fst

The lifted cell indexed by ⟨i, g⟩ is the translate g • s i.