Deck orbits on fibres

This file packages the quotient of a single fibre by the restricted deck action. Mathlib already provides the generic orbit quotient MulAction.orbitRel.Quotient; the declarations here are the deck-specific spelling and transport API used when pointed covers are compared with unpointed covers.

For a map p : E → B and a base point b : B, Deck.FiberOrbitQuotient p b is the set of orbits of the action of deck p on the fibre p ⁻¹' {b}. An over-base homeomorphism identifies the corresponding quotients by transporting fibre points and conjugating deck transformations. Regularity of the deck action is equivalently surjectivity of p together with each of these fibre-orbit quotients being a subsingleton.

Main declarations

• TauCeti.Deck.FiberOrbitQuotient: the deck-orbit quotient of one fibre.
• TauCeti.Deck.fiberOrbitClass: the quotient map from a fibre to its deck orbit.
• TauCeti.Deck.fiberOrbitClass_eq_iff: equality of fibre-orbit classes is membership in the same deck orbit.
• TauCeti.Deck.fiberOrbitQuotientEquiv: fibre-orbit quotients are invariant under an over-base homeomorphism.
• TauCeti.Deck.isRegular_iff_surjective_subsingleton_fiberOrbitQuotient: regularity is surjectivity plus subsingleton fibre-orbit quotients.

References

The pointed/unpointed connected-cover correspondence records how chosen lifts vary up to the deck action, and regular covers are exactly those whose deck action is transitive on fibres.

@[reducible, inline]

abbrev TauCeti.Deck.FiberOrbitQuotient {E : Type u_1} {B : Type u_4} [TopologicalSpace E] (p : E → B) (b : B) : Type u_1

The quotient of the fibre over b by the restricted action of the deck group.

Equations

• TauCeti.Deck.FiberOrbitQuotient p b = MulAction.orbitRel.Quotient ↥(deck p) ↑(p ⁻¹' {b})

def TauCeti.Deck.fiberOrbitClass {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} (e : ↑(p ⁻¹' {b})) : FiberOrbitQuotient p b

The deck orbit class of a point in one fibre.

Equations

• TauCeti.Deck.fiberOrbitClass e = Quotient.mk'' e

theorem TauCeti.Deck.fiberOrbitClass_eq_mk {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} (e : ↑(p ⁻¹' {b})) : fiberOrbitClass e = Quotient.mk'' e

The deck-orbit quotient map sends a fibre point to its own class.

theorem TauCeti.Deck.fiberOrbitClass_eq_iff {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} (e e' : ↑(p ⁻¹' {b})) : fiberOrbitClass e = fiberOrbitClass e' ↔ e ∈ MulAction.orbit (↥(deck p)) e'

Two fibre points have the same deck-orbit class exactly when they lie in the same deck orbit. This uses the orientation of MulAction.orbitRel_apply: the left point is a member of the orbit of the right point.

def TauCeti.Deck.fiberOrbitQuotientEquiv {E : Type u_1} {F : Type u_2} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (b : B) : FiberOrbitQuotient p b ≃ FiberOrbitQuotient q b

An over-base homeomorphism identifies deck-orbit quotients of corresponding fibres.

Equations

• TauCeti.Deck.fiberOrbitQuotientEquiv h hpq b = Quotient.congr (TauCeti.Deck.fiberMap h hpq b).toEquiv ⋯

@[simp]

theorem TauCeti.Deck.fiberOrbitQuotientEquiv_apply {E : Type u_1} {F : Type u_2} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} {b : B} (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (e : ↑(p ⁻¹' {b})) : (fiberOrbitQuotientEquiv h hpq b) (fiberOrbitClass e) = fiberOrbitClass ((fiberMap h hpq b) e)

The induced equivalence on fibre-orbit quotients sends the class of a point to the class of its transported point.

@[simp]

theorem TauCeti.Deck.fiberOrbitQuotientEquiv_symm_apply {E : Type u_1} {F : Type u_2} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} {b : B} (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (f : ↑(q ⁻¹' {b})) : (fiberOrbitQuotientEquiv h hpq b).symm (fiberOrbitClass f) = fiberOrbitClass ((fiberMap h hpq b).symm f)

The inverse induced equivalence on fibre-orbit quotients sends the class of a target fibre point to the class of its inverse transport.

@[simp]

theorem TauCeti.Deck.fiberOrbitQuotientEquiv_refl {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} : fiberOrbitQuotientEquiv (Homeomorph.refl E) ⋯ b = Equiv.refl (FiberOrbitQuotient p b)

The identity over-base homeomorphism induces the identity on fibre-orbit quotients.

@[simp]

theorem TauCeti.Deck.fiberOrbitQuotientEquiv_trans {E : Type u_1} {F : Type u_2} {G : Type u_3} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] {p : E → B} {q : F → B} {r : G → B} {b : B} (h : E ≃ₜ F) (k : F ≃ₜ G) (hpq : ∀ (e : E), q (h e) = p e) (hqr : ∀ (f : F), r (k f) = q f) : fiberOrbitQuotientEquiv (h.trans k) ⋯ b = (fiberOrbitQuotientEquiv h hpq b).trans (fiberOrbitQuotientEquiv k hqr b)

Fibre-orbit quotient equivalences compose as the underlying over-base homeomorphisms compose.

theorem TauCeti.Deck.isRegular_iff_surjective_subsingleton_fiberOrbitQuotient {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} : IsRegular p ↔ Function.Surjective p ∧ ∀ (b : B), Subsingleton (FiberOrbitQuotient p b)

Regularity can be read from the orbit quotients of the fibre actions: the map is surjective, and each fibre has at most one deck orbit.

theorem TauCeti.Deck.IsRegular.subsingleton_fiberOrbitQuotient {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} (hreg : IsRegular p) (b : B) : Subsingleton (FiberOrbitQuotient p b)

A regular deck action has a subsingleton quotient of each fibre by deck orbits.

theorem TauCeti.Deck.IsRegular.fiberOrbitClass_eq {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} (hreg : IsRegular p) (e e' : ↑(p ⁻¹' {b})) : fiberOrbitClass e = fiberOrbitClass e'

For a regular deck action, all points in the same fibre have the same deck-orbit class.