Documentation

TauCeti.AlgebraicTopology.UniversalCover.Deck.Quotient.Homeomorph

The orbit quotient of a regular open map is homeomorphic to the base #

For a regular deck action, Deck.IsRegular.orbitQuotientEquivBase already identifies the deck-orbit quotient E / deck p with the base B as a bare equivalence. This file upgrades that equivalence to a homeomorphism when p is continuous and open.

This is the abstract form of the universal-covers identity UniversalCover x₀ / π₁(X, x₀) ≃ X, stated for an arbitrary regular open map rather than the specific based-path cover. The covering-map application supplies the continuity and openness hypotheses from IsCoveringMap.continuous and IsCoveringMap.isOpenMap; the total space is not assumed preconnected.

Main declarations #

References #

UniversalCover x₀ / π₁(X, x₀) ≃ X follows from the deck-group identification via Mathlib's IsQuotientCoveringMap; the present statement is its base-independent regular-cover form.

source
theorem TauCeti.Deck.continuous_orbitQuotientToBase {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (hp : Continuous p) :
Continuous (orbitQuotientToBase p)

A continuous map induces a continuous map from the deck-orbit quotient to the base.

source
theorem TauCeti.Deck.isOpenMap_orbitQuotientToBase {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (hp : IsOpenMap p) :
IsOpenMap (orbitQuotientToBase p)

An open map induces an open map from the deck-orbit quotient to the base.

source
noncomputable def TauCeti.Deck.IsRegular.orbitQuotientHomeomorphBase {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (hreg : IsRegular p) (hcont : Continuous p) (hopen : IsOpenMap p) :
MulAction.orbitRel.Quotient (↥(deck p)) E ≃ₜ B

For a regular continuous open map, the deck-orbit quotient E / deck p is homeomorphic to the base.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.Deck.IsRegular.orbitQuotientHomeomorphBase_apply {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (hreg : IsRegular p) (hcont : Continuous p) (hopen : IsOpenMap p) (x : MulAction.orbitRel.Quotient (↥(deck p)) E) :
    (hreg.orbitQuotientHomeomorphBase hcont hopen) x = hreg.orbitQuotientEquivBase x

    On the underlying equivalence, the orbit-quotient homeomorphism is orbitQuotientEquivBase.

    source
    @[simp]
    theorem TauCeti.Deck.IsRegular.orbitQuotientHomeomorphBase_mk {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (hreg : IsRegular p) (hcont : Continuous p) (hopen : IsOpenMap p) (e : E) :
    (hreg.orbitQuotientHomeomorphBase hcont hopen) (Quotient.mk'' e) = p e

    The orbit-quotient homeomorphism evaluates on representatives by the projection map.

    source
    @[simp]
    theorem TauCeti.Deck.IsRegular.orbitQuotientHomeomorphBase_symm_apply_proj {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} (hreg : IsRegular p) (hcont : Continuous p) (hopen : IsOpenMap p) (e : E) :
    (hreg.orbitQuotientHomeomorphBase hcont hopen).symm (p e) = Quotient.mk'' e

    The inverse orbit-quotient homeomorphism sends a projected point to the class of any lift.