Main theorem of coverings
Let
Construction
Take the universal covering
and consider Λ π : Λ π β π where Ξ¦ ( π» ) β Ξ is an isomorphism. The covering is given by Ξ¦ : π 1 ( Λ π , π₯ 0 ) β Ξ with Λ π = Λ π / Ξ¦ ( π» ) π : ( Λ π , Λ π₯ 0 ) β ( π , π₯ 0 ) Λ π₯ Ξ¦ ( π» ) β¦ Λ π ( Λ π₯ 0 )
Proof
Uniqueness up to equivalence follows from equivalence of coverings criterion. Since
is semilocally simply connected, it has a universal covering ( π , π₯ 0 ) . Let Λ π : ( Λ π , Λ π₯ 0 ) β ( π , π₯ 0 ) According to Deck transformation group of a regular covering as quotient Ξ = A u t π’ π π π β‘ ( Λ π ) Ξ¦ : π 1 ( π , π₯ 0 ) β Ξ [ πΌ ] β¦ ( Λ π₯ 0 β¦ Λ πΌ ( 1 ) ) is an isomorphism, where
is the unique lift of Λ πΌ with πΌ , and Λ πΌ ( 0 ) = Λ π₯ 0 denotes a unique deck transformation with this property. ( Λ π₯ 0 β¦ Λ πΌ ( 1 ) ) Now take the orbit space
with the canonical projection Λ π = Λ π / Ξ¦ ( π» ) π : ( Λ π , Λ π₯ 0 ) β ( Λ π , Λ π₯ 0 ) Λ π₯ β¦ Ξ¦ ( π» ) Λ π₯ Since the deck transformation group acts properly discontinuously, so too does
, and the orbit space of a properly discontinuous effective group action forms a covering, which in this case is universal. Thus Ξ¦ ( π» ) β Ξ A u t π’ π π Λ π β‘ ( π ) β π 1 ( Λ π , Λ π₯ 0 ) β Ξ¦ ( π» ) β π» We now define
π : ( Λ π , Λ π₯ 0 ) β ( π , π₯ 0 ) π ( Λ π₯ ) β¦ Λ π ( Λ π₯ ) which is well-defined since
iff π ( Λ π₯ ) = π ( Λ π₯ β² ) for some Λ π₯ β² = πΎ ( Λ π₯ ) , and then πΎ β π» β Ξ ; and continuous by Universal property. Λ π β πΎ ( Λ π₯ ) = Λ π ( Λ π₯ )
Now let
and let π₯ β π be a neighbourhood of π evenly covered by π₯ with sheets Λ π . Let { Λ π π } π β πΌ such that for all π½ β πΌ there exists exactly one π β πΌ such that π β π½ , and let π ( Λ π π ) = π ( Λ π π ) . Then Λ π π = π ( Λ π π ) π β 1 ( π ) = β π β π½ Λ π π and
, therefore ( π βΎ Λ π π ) β 1 = ( π βΎ Λ π π ) β ( Λ π βΎ Λ π π ) β 1 is a covering. Then by construction π [ πΌ ] β π» βΊ ( Λ π₯ 0 β¦ Λ πΌ ( 1 ) ) β Ξ¦ ( π» ) βΊ Λ πΌ ( 1 ) = π β Λ πΌ ( 1 ) = Λ π₯ 0 βΊ [ πΌ ] = π 1 π [ Λ πΌ ] so
as required. π» = π 1 π ( π 1 ( Λ π , Λ π₯ 0 ) )