The universal covering group of a topological group

Let G be a topological group. A point of the universal cover UniversalCover (1 : G) based at the identity is a point x : G together with a homotopy class of paths from 1 to x. Two such classes can be multiplied pointwise: if p runs from 1 to x and q from 1 to y, then t ↦ p t * q t runs from 1 to x * y, and a pair of homotopies multiplies to a homotopy. With the pointwise inverse t ↦ (p t)⁻¹ and the constant path as identity, this makes UniversalCover (1 : G) a group, and the group laws hold already for the paths, pointwise.

When G is locally path-connected and semilocally simply connected, so that UniversalCover 1 is a simply connected covering space of the identity path component, these operations are continuous and UniversalCover (1 : G) is a topological group. Continuity is not visible from the formula, since the topology is a quotient topology. It comes from the lifting criterion instead: the map (a, b) ↦ proj a * proj b on the simply connected, locally path-connected space UniversalCover 1 × UniversalCover 1 lifts to a continuous map into the cover, and unique path lifting identifies that lift with the pointwise product. The same argument handles the inverse.

The endpoint projection is then a continuous homomorphism UniversalCover.projHom which is a covering map, and its kernel, a discrete normal subgroup of a connected group, is central. This is the topological half of the simply connected covering group of a connected Lie group.

The kernel is the fundamental group π₁(G, 1), for every topological group G. Its points are the homotopy classes of loops at 1, and on them the group law of the universal cover is pointwise multiplication of loops, which in a topological group agrees with concatenation by the Eckmann–Hilton argument (FundamentalGroup.cast_map_prod_mul).

Main definitions

• TauCeti.UniversalCover.instGroup: the group structure on UniversalCover (1 : G) given by pointwise multiplication of paths.
• TauCeti.UniversalCover.projHom: the endpoint projection as a continuous homomorphism UniversalCover (1 : G) →ₜ* G.
• TauCeti.UniversalCover.kerProjHomEquivFundamentalGroup: the kernel of projHom is isomorphic to the fundamental group π₁(G, 1).

Main statements

• TauCeti.UniversalCover.mk_mul_mk, TauCeti.UniversalCover.inv_mk, TauCeti.UniversalCover.one_def: the group operations on representatives.
• TauCeti.UniversalCover.instIsTopologicalGroup: for a locally path-connected, semilocally simply connected G, the universal cover is a topological group.
• TauCeti.UniversalCover.isCoveringMap_projHom: the projection is a covering homomorphism.
• TauCeti.UniversalCover.ker_projHom_le_center: its kernel is central.
• TauCeti.UniversalCover.discreteTopology_ker_projHom: its kernel is discrete.

References

• J. M. Lee, Introduction to Smooth Manifolds, 2nd ed., Springer GTM 218 (2013), Chapter 7, "Covering groups".
• B. C. Hall, Lie Groups, Lie Algebras, and Representations, 2nd ed., Springer GTM 222 (2015), Chapter 5.

The group structure

@[instance_reducible]

instance TauCeti.UniversalCover.instOne {G : Type u_1} [Group G] [TopologicalSpace G] : One (UniversalCover 1)

The identity of the universal cover based at 1 is the class of the constant path.

Equations

• TauCeti.UniversalCover.instOne = { one := { proj := 1, path := Path.Homotopic.Quotient.refl 1 } }

theorem TauCeti.UniversalCover.one_def {G : Type u_1} [Group G] [TopologicalSpace G] : 1 = { proj := 1, path := Path.Homotopic.Quotient.refl 1 }

The identity is the class of the constant path.

@[simp]

theorem TauCeti.UniversalCover.proj_one {G : Type u_1} [Group G] [TopologicalSpace G] : proj 1 = 1

theorem TauCeti.UniversalCover.one_eq_ofBasedPath_refl {G : Type u_1} [Group G] [TopologicalSpace G] : 1 = ofBasedPath 1 (BasedPath.refl 1)

The identity is the class of the constant based path.

@[instance_reducible]

instance TauCeti.UniversalCover.instMul {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Mul (UniversalCover 1)

Multiplication on the universal cover based at 1: the endpoints multiply, and the homotopy classes of paths multiply pointwise (TauCeti.UniversalCover.mk_mul_mk).

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance TauCeti.UniversalCover.instInv {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Inv (UniversalCover 1)

Inversion on the universal cover based at 1: the endpoint is inverted, and the homotopy class of paths is inverted pointwise (TauCeti.UniversalCover.inv_mk).

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.UniversalCover.mk_mul_mk {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {x y : G} (p : Path 1 x) (q : Path 1 y) : { proj := x, path := Path.Homotopic.Quotient.mk p } * { proj := y, path := Path.Homotopic.Quotient.mk q } = { proj := x * y, path := Path.Homotopic.Quotient.mk ((p.mul q).cast ⋯ ⋯) }

The product of the classes of two paths is the class of their pointwise product.

theorem TauCeti.UniversalCover.inv_mk {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {x : G} (p : Path 1 x) : { proj := x, path := Path.Homotopic.Quotient.mk p }⁻¹ = { proj := x⁻¹, path := Path.Homotopic.Quotient.mk (p.inv.cast ⋯ ⋯) }

The inverse of the class of a path is the class of its pointwise inverse.

@[simp]

theorem TauCeti.UniversalCover.proj_mul {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (a b : UniversalCover 1) : (a * b).proj = a.proj * b.proj

@[simp]

theorem TauCeti.UniversalCover.proj_inv {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (a : UniversalCover 1) : a⁻¹.proj = a.proj⁻¹

theorem TauCeti.UniversalCover.ofBasedPath_mul_ofBasedPath {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (α β : BasedPath 1) : ofBasedPath 1 α * ofBasedPath 1 β = ofBasedPath 1 (BasedPath.ofPath ((α.toPath.mul β.toPath).cast ⋯ ⋯))

The product of the classes of two based paths is the class of their pointwise product.

theorem TauCeti.UniversalCover.inv_ofBasedPath {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (α : BasedPath 1) : (ofBasedPath 1 α)⁻¹ = ofBasedPath 1 (BasedPath.ofPath (α.toPath.inv.cast ⋯ ⋯))

The inverse of the class of a based path is the class of its pointwise inverse.

@[instance_reducible]

instance TauCeti.UniversalCover.instGroup {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Group (UniversalCover 1)

The universal cover based at the identity of a topological group is a group under pointwise multiplication of paths.

Equations

• One or more equations did not get rendered due to their size.

def TauCeti.UniversalCover.projHom {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : UniversalCover 1 →ₜ* G

The endpoint projection of the universal cover based at the identity, as a continuous homomorphism.

Equations

• TauCeti.UniversalCover.projHom = { toFun := TauCeti.UniversalCover.proj, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ }

@[simp]

theorem TauCeti.UniversalCover.coe_projHom {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : ⇑projHom = proj

The kernel of the covering homomorphism

theorem TauCeti.UniversalCover.mem_ker_projHom {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {a : UniversalCover 1} : a ∈ (↑projHom).ker ↔ a.proj = 1

A point of the universal cover lies in the kernel of the covering homomorphism exactly when it lies over the identity.

noncomputable def TauCeti.UniversalCover.kerProjHomEquivFundamentalGroup {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : ↥(↑projHom).ker ≃* FundamentalGroup G 1

The kernel of the covering homomorphism is the fundamental group. A point of the universal cover based at 1 lying over 1 is a homotopy class of loops at 1, and the group law of the universal cover, pointwise multiplication of paths, multiplies loop classes as the fundamental group does (FundamentalGroup.cast_map_prod_mul).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.UniversalCover.coe_kerProjHomEquivFundamentalGroup_symm_apply {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (a : FundamentalGroup G 1) : ↑(kerProjHomEquivFundamentalGroup.symm a) = { proj := 1, path := a.toPath }

A loop class at the identity corresponds to the point of the universal cover over 1 that it defines.

theorem TauCeti.UniversalCover.kerProjHomEquivFundamentalGroup_apply {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (z : ↥(↑projHom).ker) : (kerProjHomEquivFundamentalGroup z).toPath = (↑z).path.cast ⋯ ⋯

A point of the universal cover over 1 corresponds to its homotopy class of loops.

The topological group structure

instance TauCeti.UniversalCover.instIsTopologicalGroup {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyPathConnectedSpace G] [SemilocallySimplyConnectedSpace G] : IsTopologicalGroup (UniversalCover 1)

The universal cover based at the identity of a locally path-connected, semilocally simply connected topological group is a topological group.

theorem TauCeti.UniversalCover.isCoveringMap_projHom {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyPathConnectedSpace G] [SemilocallySimplyConnectedSpace G] : IsCoveringMap ⇑projHom

The endpoint projection is a covering homomorphism.

theorem TauCeti.UniversalCover.mem_center_of_proj_eq_one {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyPathConnectedSpace G] [SemilocallySimplyConnectedSpace G] {z : UniversalCover 1} (hz : z.proj = 1) : z ∈ Subgroup.center (UniversalCover 1)

A point of the universal cover lying over the identity is central: conjugating it by a variable element gives a continuous map into the discrete fibre over 1 from a connected space.

theorem TauCeti.UniversalCover.ker_projHom_le_center {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyPathConnectedSpace G] [SemilocallySimplyConnectedSpace G] : (↑projHom).ker ≤ Subgroup.center (UniversalCover 1)

The kernel of the covering homomorphism is central.

instance TauCeti.UniversalCover.discreteTopology_ker_projHom {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyPathConnectedSpace G] [SemilocallySimplyConnectedSpace G] : DiscreteTopology ↥(↑projHom).ker

The kernel of the covering homomorphism is discrete: it is the fibre of the covering map over the identity.