The CW structure on a wedge of circles

The wedge of circles WedgeSum fun _ : S => (1 : Circle) indexed by a type S is a one-dimensional CW complex with one 0-cell, the wedge point, and one 1-cell for each s : S (TauCeti.WedgeSum.circleCWComplex, an instance). There is no finiteness hypothesis on S. The characteristic map TauCeti.WedgeSum.circleCellMap s of the s-th 1-cell wraps the interval [-1, 1] once around the s-th circle, sending t to exp (i (π t + π)), so that both end points go to the wedge point 1.

The wedge of circles is the 1-skeleton of the presentation complex of a group presentation, and the standard model of a classifying space of a free group. With this structure, and since the wedge sum of Hausdorff spaces is Hausdorff, the theory of classical CW complexes (cellular approximation, spaces of CW type and Whitehead's theorem) applies to it.

The weak topology of the CW structure is the quotient topology of the wedge sum: a set is closed as soon as its trace on every circle is closed (TauCeti.WedgeSum.isClosed_iff). The inverse of a characteristic map is continuous on its open cell because the closed interval is compact (ContinuousOn.continuousOn_invFunOn_image_of_isCompact).

Main definitions

• TauCeti.WedgeSum.circleCellMap s: the characteristic map of the s-th circle.
• TauCeti.WedgeSum.circleCWComplex: the CW structure on the wedge of circles.
• TauCeti.WedgeSum.circleCellOneEquiv: its 1-cells are indexed by S.

Main results

• TauCeti.WedgeSum.map_one_circleCWComplex: the characteristic map of the 1-cell indexed by s (through circleCellOneEquiv) is circleCellMap s.
• TauCeti.WedgeSum.closedCell_one_circleCWComplex, TauCeti.WedgeSum.openCell_one_circleCWComplex: the closed 1-cell indexed by s is the s-th circle, and the open 1-cell is that circle without the wedge point.
• TauCeti.WedgeSum.cellFrontier_one_circleCWComplex: the frontier of every 1-cell is the wedge point.
• TauCeti.WedgeSum.map_zero_circleCWComplex: the 0-cell is the wedge point.
• TauCeti.WedgeSum.isEmpty_cell_circleCWComplex: there are no cells of dimension at least 2.
• TauCeti.WedgeSum.skeletonLT_one_circleCWComplex: the 0-skeleton is the wedge point.
• The structure is finite dimensional, and finite when S is finite (instances).

References

• A. Hatcher, Algebraic Topology, Chapter 0, the cell structure of graphs, and Section 1.2, Example 1.21 for wedges of circles.

noncomputable def TauCeti.WedgeSum.circleCellMap (S : Type u) (s : S) : PartialEquiv (Fin 1 → ℝ) (WedgeSum fun (x : S) => 1)

The characteristic map of the 1-cell of the wedge of circles indexed by s : S: it wraps the interval [-1, 1] once around the s-th circle, sending t to exp (i (π t + π)), and is a bijection from the open interval (-1, 1) onto the s-th circle without the wedge point.

@[simp]

theorem TauCeti.WedgeSum.circleCellMap_apply {S : Type u} (s : S) (x : Fin 1 → ℝ) : ↑(circleCellMap S s) x = (incl (fun (x : S) => 1) s) (Circle.exp (Real.pi * x 0 + Real.pi))

@[simp]

theorem TauCeti.WedgeSum.circleCellMap_source {S : Type u} (s : S) : (circleCellMap S s).source = Metric.ball 0 1

theorem TauCeti.WedgeSum.coe_circleCellMap_symm {S : Type u} (s : S) : ↑(circleCellMap S s).symm = Function.invFunOn (↑(circleCellMap S s)) (Metric.ball 0 1)

The inverse of circleCellMap S s is the inverse of the wrapping map on the open interval.

theorem TauCeti.WedgeSum.continuous_circleCellMap {S : Type u} (s : S) : Continuous ↑(circleCellMap S s)

theorem TauCeti.WedgeSum.image_circleCellMap_closedBall {S : Type u} (s : S) : ↑(circleCellMap S s) '' Metric.closedBall 0 1 = Set.range ⇑(incl (fun (x : S) => 1) s)

The closed 1-cell of s is the s-th circle.

theorem TauCeti.WedgeSum.image_circleCellMap_ball {S : Type u} (s : S) : ↑(circleCellMap S s) '' Metric.ball 0 1 = Set.range ⇑(incl (fun (x : S) => 1) s) \ {base fun (x : S) => 1}

The open 1-cell of s is the s-th circle without the wedge point.

@[simp]

theorem TauCeti.WedgeSum.circleCellMap_target {S : Type u} (s : S) : (circleCellMap S s).target = Set.range ⇑(incl (fun (x : S) => 1) s) \ {base fun (x : S) => 1}

The target of circleCellMap S s, the image of the open interval, is the s-th circle without the wedge point.

theorem TauCeti.WedgeSum.circleCellMap_of_mem_sphere {S : Type u} (s : S) {x : Fin 1 → ℝ} (hx : x ∈ Metric.sphere 0 1) : ↑(circleCellMap S s) x = base fun (x : S) => 1

The boundary of the 1-cell of s is the wedge point.

@[instance_reducible]

noncomputable instance TauCeti.WedgeSum.circleCWComplex {S : Type u} : Topology.CWComplex Set.univ

The CW structure on a wedge of circles. The wedge of circles indexed by S has one 0-cell, the wedge point, and one 1-cell for each s : S, with characteristic map TauCeti.WedgeSum.circleCellMap s (TauCeti.WedgeSum.map_one_circleCWComplex).

noncomputable def TauCeti.WedgeSum.circleCellOneEquiv {S : Type u} : Topology.RelCWComplex.cell Set.univ 1 ≃ S

The 1-cells of the wedge of circles indexed by S are indexed by S.

@[simp]

theorem TauCeti.WedgeSum.map_one_circleCWComplex {S : Type u} (i : Topology.RelCWComplex.cell Set.univ 1) : Topology.RelCWComplex.map 1 i = circleCellMap S (circleCellOneEquiv i)

The characteristic map of the 1-cell i is TauCeti.WedgeSum.circleCellMap of the corresponding index circleCellOneEquiv i.

@[simp]

theorem TauCeti.WedgeSum.closedCell_one_circleCWComplex {S : Type u} (i : Topology.RelCWComplex.cell Set.univ 1) : Topology.RelCWComplex.closedCell 1 i = Set.range ⇑(incl (fun (x : S) => 1) (circleCellOneEquiv i))

The closed 1-cell i is the circle indexed by circleCellOneEquiv i.

@[simp]

theorem TauCeti.WedgeSum.openCell_one_circleCWComplex {S : Type u} (i : Topology.RelCWComplex.cell Set.univ 1) : Topology.RelCWComplex.openCell 1 i = Set.range ⇑(incl (fun (x : S) => 1) (circleCellOneEquiv i)) \ {base fun (x : S) => 1}

The open 1-cell i is the circle indexed by circleCellOneEquiv i without the wedge point.

@[simp]

theorem TauCeti.WedgeSum.cellFrontier_one_circleCWComplex {S : Type u} (i : Topology.RelCWComplex.cell Set.univ 1) : Topology.RelCWComplex.cellFrontier 1 i = {base fun (x : S) => 1}

The frontier of every 1-cell is the wedge point: each 1-cell is a loop.

@[instance_reducible]

noncomputable instance TauCeti.WedgeSum.instUniqueCellCircleOfNatUnivNat {S : Type u} : Unique (Topology.RelCWComplex.cell Set.univ 0)

The wedge of circles has a single 0-cell.

@[simp]

theorem TauCeti.WedgeSum.map_zero_circleCWComplex {S : Type u} (i : Topology.RelCWComplex.cell Set.univ 0) (x : Fin 0 → ℝ) : ↑(Topology.RelCWComplex.map 0 i) x = base fun (x : S) => 1

The 0-cell of the wedge of circles is the wedge point.

theorem TauCeti.WedgeSum.isEmpty_cell_circleCWComplex {S : Type u} {n : ℕ} (hn : 2 ≤ n) : IsEmpty (Topology.RelCWComplex.cell Set.univ n)

The wedge of circles has no cells of dimension at least 2.

instance TauCeti.WedgeSum.instFiniteDimensionalCircleOfNatUniv {S : Type u} : Topology.RelCWComplex.FiniteDimensional Set.univ

The wedge of circles is a finite dimensional CW complex.

instance TauCeti.WedgeSum.instFiniteCircleOfNatUnivOfFinite {S : Type u} [Finite S] : Topology.RelCWComplex.Finite Set.univ

A wedge of finitely many circles is a finite CW complex.

theorem TauCeti.WedgeSum.skeletonLT_one_circleCWComplex {S : Type u} : ↑(Topology.RelCWComplex.skeletonLT Set.univ 1) = {base fun (x : S) => 1}

The 0-skeleton of the wedge of circles, skeletonLT _ 1, is the wedge point.