Fibres of regular connected covers as deck torsors

For a preconnected covering map with regular deck action, evaluation at any point of a fibre identifies the deck group with that fibre. This file packages the same fact in the standard Mathlib language of torsors: the fibre is a principal homogeneous space for the deck group.

Pointed covers and unpointed covers differ by changing a chosen lift of the basepoint, and regular covers are characterized by transitivity of the deck action on fibres; the torsor structure keeps track of both.

Main declarations

• TauCeti.Deck.fiberTorsor: the regular-cover specialization.
• TauCeti.Deck.fiber_sdiv_eq_deckEquivFiber_symm: fibre division is the unique deck transformation carrying the second point to the first.

References

It specializes the local torsor API in TauCeti.AlgebraicTopology.UniversalCover.Deck.Connected.Torsor using the regular deck-action API in TauCeti.AlgebraicTopology.UniversalCover.Deck.Regular.Basic.

@[reducible]

noncomputable def TauCeti.Deck.fiberTorsor {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} [PreconnectedSpace E] (hp : IsCoveringMap p) (hreg : IsRegular p) (b : B) : Torsor ↥(deck p) ↑(p ⁻¹' {b})

The fibre of a regular preconnected covering is a torsor for its deck group.

Equations

• TauCeti.Deck.fiberTorsor hp hreg b = TauCeti.Deck.fiberTorsorOfPretransitive hp b

theorem TauCeti.Deck.fiber_sdiv_eq_deckEquivFiber_symm {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} {b : B} [PreconnectedSpace E] (hp : IsCoveringMap p) (hreg : IsRegular p) (e₁ e₂ : ↑(p ⁻¹' {b})) : e₁ /ₛ e₂ = (deckEquivFiber hp hreg e₂).symm e₁

In the regular-cover fibre torsor, e₁ /ₛ e₂ is the inverse equivalence from e₂ applied to e₁.

@[simp]

theorem TauCeti.Deck.deckEquivFiber_symm_eq_sdiv {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} {b : B} [PreconnectedSpace E] (hp : IsCoveringMap p) (hreg : IsRegular p) (e e' : ↑(p ⁻¹' {b})) : (deckEquivFiber hp hreg e).symm e' = e' /ₛ e

In the regular-cover fibre torsor, the inverse of deckEquivFiber computes the quotient of a point by the chosen base point.