Documentation

TauCeti.AlgebraicTopology.UniversalCover.Deck.Connected.Torsor

Fibres of connected covers as deck torsors #

For a preconnected covering map, a nonempty fibre on which the deck group acts pretransitively is a principal homogeneous space for the deck group. This packages the local form of the simply transitive fibre action; regular covers specialize it by supplying pretransitivity on every fibre.

Pointed covers and unpointed covers differ by changing a chosen lift of the basepoint, which the torsor structure keeps track of.

Main declarations #

References #

It builds on the connected deck-action API in TauCeti.AlgebraicTopology.UniversalCover.Deck.Connected.Basic and Mathlib's generic torsor API (Mathlib.Algebra.Torsor.Basic).

source
@[reducible]
noncomputable def TauCeti.Deck.fiberTorsorOfPretransitive {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} [PreconnectedSpace E] (hp : IsCoveringMap p) (b : B) [Nonempty ↑(p ⁻¹' {b})] [MulAction.IsPretransitive ↥(deck p) ↑(p ⁻¹' {b})] :
Torsor ↥(deck p) ↑(p ⁻¹' {b})

A nonempty pretransitive fibre of a preconnected covering is a torsor for its deck group.

The division e₁ /ₛ e₂ is the unique deck transformation carrying e₂ to e₁, expressed using deckEquivFiberOfSurjective at the base point e₂.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem TauCeti.Deck.fiber_sdiv_eq_deckEquivFiberOfSurjective_symm {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} {b : B} [PreconnectedSpace E] (hp : IsCoveringMap p) [Nonempty ↑(p ⁻¹' {b})] [MulAction.IsPretransitive ↥(deck p) ↑(p ⁻¹' {b})] (e₁ e₂ : ↑(p ⁻¹' {b})) :
    e₁ /ₛ e₂ = (deckEquivFiberOfSurjective hp e₂ ⋯).symm e₁

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

    source
    @[simp]
    theorem TauCeti.Deck.deckEquivFiberOfSurjective_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) [Nonempty ↑(p ⁻¹' {b})] [MulAction.IsPretransitive ↥(deck p) ↑(p ⁻¹' {b})] (e e' : ↑(p ⁻¹' {b})) :
    (deckEquivFiberOfSurjective hp e ⋯).symm e' = e' /ₛ e

    In the local fibre torsor, the inverse of deckEquivFiberOfSurjective computes the quotient of a point by the chosen base point.