Documentation

TauCeti.AlgebraicTopology.UniversalCover.Descent

Homomorphism descent from a universal covering group #

Continuous homomorphisms from a path-connected topological group are exactly the continuous homomorphisms from its universal covering group that kill the kernel of the covering projection.

Main result #

source
noncomputable def TauCeti.UniversalCover.homEquivKerProjHom {G : Type u_1} {K : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyPathConnectedSpace G] [PathConnectedSpace G] [SemilocallySimplyConnectedSpace G] [Monoid K] [TopologicalSpace K] :
(G →ₜ* K) ≃ { f : UniversalCover 1 →ₜ* K // (↑projHom).ker ≤ (↑f).ker }

Continuous homomorphisms out of a path-connected group are equivalent to continuous homomorphisms out of its universal cover that kill the projection kernel.

Instances For
    source
    @[simp]
    theorem TauCeti.UniversalCover.homEquivKerProjHom_apply_coe {G : Type u_1} {K : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyPathConnectedSpace G] [PathConnectedSpace G] [SemilocallySimplyConnectedSpace G] [Monoid K] [TopologicalSpace K] (f : G →ₜ* K) :
    ↑(homEquivKerProjHom f) = f.comp projHom

    The universal-cover correspondence sends a homomorphism to its composition with the covering projection.

    source
    @[simp]
    theorem TauCeti.UniversalCover.homEquivKerProjHom_symm_apply_comp {G : Type u_1} {K : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyPathConnectedSpace G] [PathConnectedSpace G] [SemilocallySimplyConnectedSpace G] [Monoid K] [TopologicalSpace K] (f : { g : UniversalCover 1 →ₜ* K // (↑projHom).ker ≤ (↑g).ker }) :
    (homEquivKerProjHom.symm f).comp projHom = ↑f

    Descending a homomorphism from the universal cover and composing again with the covering projection recovers the original homomorphism.