The orbit quotient of a regular deck action

For any map p : E → B, deck transformations preserve the value of p, so p factors through the quotient of E by the orbit relation for the deck action. If the deck action is regular, the induced map from the orbit quotient to the base is an equivalence.

Quotient-cover and regular-cover statements compare the base with the orbit space of the deck action, and the basic equivalence only uses Deck.IsRegular p: surjectivity of p and transitivity of the deck action on each fibre.

Main declarations

• TauCeti.Deck.orbitQuotientToBase: the map E / deck p → B induced by p.
• TauCeti.Deck.IsRegular.orbitQuotientEquivBase: for a regular deck action, E / deck p is equivalent to the base.

theorem TauCeti.Deck.eq_proj_of_orbitRel {E : Type u_1} {B : Type u_3} [TopologicalSpace E] {p : E → B} {e e' : E} (h : (MulAction.orbitRel (↥(deck p)) E) e e') : p e = p e'

Points in the same deck orbit have the same projection under p.

def TauCeti.Deck.orbitQuotientToBase {E : Type u_1} {B : Type u_3} [TopologicalSpace E] (p : E → B) : MulAction.orbitRel.Quotient (↥(deck p)) E → B

The projection map factors through the quotient of E by deck orbits.

Equations

• TauCeti.Deck.orbitQuotientToBase p = Quotient.lift p ⋯

@[simp]

theorem TauCeti.Deck.orbitQuotientToBase_mk {E : Type u_1} {B : Type u_3} [TopologicalSpace E] {p : E → B} (e : E) : orbitQuotientToBase p (Quotient.mk'' e) = p e

The map from the deck-orbit quotient to the base evaluates on representatives by p.

theorem TauCeti.Deck.apply_eq_iff_mem_orbit_of_exists_apply_eq {E : Type u_1} {B : Type u_3} [TopologicalSpace E] {p : E → B} (hpoint : ∀ {e e' : E}, p e = p e' → ∃ (φ : ↥(deck p)), ↑φ e = e') {e₁ e₂ : E} : p e₁ = p e₂ ↔ e₁ ∈ MulAction.orbit (↥(deck p)) e₂

If every pair of points with the same projection is connected by a deck transformation, then two points of the total space have the same projection exactly when they lie in a common orbit of the deck transformation group. The reverse direction holds because deck transformations preserve the projection.

theorem TauCeti.Deck.orbitRel_homeomorph_iff {E : Type u_1} {F : Type u_2} {B : Type u_3} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (e e' : E) : (MulAction.orbitRel (↥(deck p)) E) e e' ↔ (MulAction.orbitRel (↥(deck q)) F) (h e) (h e')

An over-base homeomorphism preserves the corresponding deck-orbit relations.

def TauCeti.Deck.orbitQuotientEquiv {E : Type u_1} {F : Type u_2} {B : Type u_3} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) : MulAction.orbitRel.Quotient (↥(deck p)) E ≃ MulAction.orbitRel.Quotient (↥(deck q)) F

An over-base homeomorphism identifies the corresponding deck-orbit quotients.

Equations

• TauCeti.Deck.orbitQuotientEquiv h hpq = Quotient.congr h.toEquiv ⋯

@[simp]

theorem TauCeti.Deck.orbitQuotientEquiv_mk {E : Type u_1} {F : Type u_2} {B : Type u_3} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (e : E) : (orbitQuotientEquiv h hpq) (Quotient.mk'' e) = Quotient.mk'' (h e)

The over-base equivalence on orbit quotients evaluates on representatives by the homeomorphism.

@[simp]

theorem TauCeti.Deck.orbitQuotientEquiv_symm_mk {E : Type u_1} {F : Type u_2} {B : Type u_3} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (f : F) : (orbitQuotientEquiv h hpq).symm (Quotient.mk'' f) = Quotient.mk'' (h.symm f)

The inverse over-base equivalence on orbit quotients evaluates on representatives by the inverse homeomorphism.

theorem TauCeti.Deck.orbitQuotientToBase_injective_of_exists_apply_eq {E : Type u_1} {B : Type u_3} [TopologicalSpace E] {p : E → B} (hpoint : ∀ {e e' : E}, p e = p e' → ∃ (φ : ↥(deck p)), ↑φ e = e') : Function.Injective (orbitQuotientToBase p)

If deck transformations act transitively on each fibre of p, the map from the deck-orbit quotient to the base is injective.

theorem TauCeti.Deck.orbitQuotient_mk_eq_mk_iff_of_exists_apply_eq {E : Type u_1} {B : Type u_3} [TopologicalSpace E] {p : E → B} (hpoint : ∀ {e e' : E}, p e = p e' → ∃ (φ : ↥(deck p)), ↑φ e = e') (e e' : E) : Quotient.mk'' e = Quotient.mk'' e' ↔ p e = p e'

If deck transformations act transitively on each fibre of p, two points have the same deck-orbit quotient class exactly when they have the same projection.

theorem TauCeti.Deck.IsRegular.orbitQuotientToBase_injective {E : Type u_1} {B : Type u_3} [TopologicalSpace E] {p : E → B} (hreg : IsRegular p) : Function.Injective (orbitQuotientToBase p)

For a regular deck action, the map from deck-orbit quotient to the base is injective.

theorem TauCeti.Deck.IsRegular.apply_eq_iff_mem_orbit {E : Type u_1} {B : Type u_3} [TopologicalSpace E] {p : E → B} (hreg : IsRegular p) {e₁ e₂ : E} : p e₁ = p e₂ ↔ e₁ ∈ MulAction.orbit (↥(deck p)) e₂

For a regular deck action, two points have the same projection exactly when they lie in a common deck orbit.

noncomputable def TauCeti.Deck.IsRegular.orbitQuotientEquivBase {E : Type u_1} {B : Type u_3} [TopologicalSpace E] {p : E → B} (hreg : IsRegular p) : MulAction.orbitRel.Quotient (↥(deck p)) E ≃ B

A regular deck action identifies the quotient of the total space by deck orbits with the base.

Equations

• hreg.orbitQuotientEquivBase = Equiv.ofBijective (TauCeti.Deck.orbitQuotientToBase p) ⋯

@[simp]

theorem TauCeti.Deck.IsRegular.orbitQuotientEquivBase_mk {E : Type u_1} {B : Type u_3} [TopologicalSpace E] {p : E → B} (hreg : IsRegular p) (e : E) : hreg.orbitQuotientEquivBase (Quotient.mk'' e) = p e

The equivalence from the deck-orbit quotient to the base evaluates on representatives by the projection map.

@[simp]

theorem TauCeti.Deck.IsRegular.orbitQuotientEquivBase_symm_apply_proj {E : Type u_1} {B : Type u_3} [TopologicalSpace E] {p : E → B} (hreg : IsRegular p) (e : E) : hreg.orbitQuotientEquivBase.symm (p e) = Quotient.mk'' e

The inverse quotient-base equivalence sends a projected point to the class of any lift.

@[simp]

theorem TauCeti.Deck.IsRegular.orbitQuotient_mk_eq_mk_iff {E : Type u_1} {B : Type u_3} [TopologicalSpace E] {p : E → B} (hreg : IsRegular p) (e e' : E) : Quotient.mk'' e = Quotient.mk'' e' ↔ p e = p e'

For a regular deck action, two points have the same deck-orbit quotient class exactly when they have the same projection.

theorem TauCeti.Deck.IsRegular.orbitQuotientEquivBase_conj {E : Type u_1} {F : Type u_2} {B : Type u_3} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} (hreg : IsRegular p) (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (x : MulAction.orbitRel.Quotient (↥(deck p)) E) : ⋯.orbitQuotientEquivBase ((orbitQuotientEquiv h hpq) x) = hreg.orbitQuotientEquivBase x

Transporting a regular deck action along an over-base homeomorphism is compatible with the corresponding orbit-quotient equivalences.

theorem TauCeti.Deck.IsRegular.orbitQuotientEquivBase_conj_mk {E : Type u_1} {F : Type u_2} {B : Type u_3} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} (hreg : IsRegular p) (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (f : F) : ⋯.orbitQuotientEquivBase (Quotient.mk'' f) = hreg.orbitQuotientEquivBase (Quotient.mk'' (h.symm f))

Representative form of compatibility between over-base homeomorphisms and the regular orbit-quotient equivalences.