Regular deck actions on fibres

For a map p : E → B, regularity of the deck action is the statement that p is surjective and the deck transformation group acts transitively on every fibre. This is the deck-action formulation of regular covers.

The definition in this file is deliberately phrased only in terms of the existing deck p group and Mathlib's MulAction.IsPretransitive. It does not assert that p is a covering map; the covering hypothesis is needed only for the connected-cover freeness result that turns fibre transitivity into a canonical equivalence between the deck group and a chosen fibre.

Main declarations

• TauCeti.Deck.IsRegular: p is surjective and deck p acts transitively on each fibre.
• TauCeti.Deck.isRegular_iff_exists_apply_eq: regularity is equivalent to surjectivity plus pointwise deck transitivity on fibres.
• TauCeti.Deck.IsRegular.exists_apply_eq: regularity moves any point of a fibre to any other point of the same fibre by a deck transformation.
• TauCeti.Deck.IsRegular.conj: regularity is invariant under isomorphism of maps over the same base.
• TauCeti.Deck.deckEquivFiber: for a preconnected covering with regular deck action, evaluation at one fibre point identifies the deck group with that fibre.

References

Regular covers are characterized by transitivity of the deck action on fibres, and the deck group of the cover associated to a subgroup is computed as a normalizer quotient.

def TauCeti.Deck.IsRegular {E : Type u_1} {B : Type u_3} [TopologicalSpace E] (p : E → B) : Prop

The deck action of a map is regular when the map is surjective and the deck group acts transitively on every fibre.

For covering maps between connected, locally path-connected spaces this is the usual deck-action formulation of a regular covering. The definition is kept independent of IsCoveringMap so it can also be transported along isomorphisms of maps without carrying unused topological hypotheses.

Equations

• TauCeti.Deck.IsRegular p = (Function.Surjective p ∧ ∀ (b : B), MulAction.IsPretransitive ↥(deck p) ↑(p ⁻¹' {b}))

theorem TauCeti.Deck.isRegular_iff {E : Type u_1} {B : Type u_3} [TopologicalSpace E] {p : E → B} : IsRegular p ↔ Function.Surjective p ∧ ∀ (b : B), MulAction.IsPretransitive ↥(deck p) ↑(p ⁻¹' {b})

Characteristic restatement of regularity of the deck action.

theorem TauCeti.Deck.isRegular_iff_exists_apply_eq {E : Type u_1} {B : Type u_3} [TopologicalSpace E] {p : E → B} : IsRegular p ↔ Function.Surjective p ∧ ∀ {e e' : E}, p e = p e' → ∃ (φ : ↥(deck p)), ↑φ e = e'

Characteristic pointwise restatement of regularity of the deck action.

theorem TauCeti.Deck.IsRegular.nonempty_fiber {E : Type u_1} {B : Type u_3} [TopologicalSpace E] {p : E → B} (hreg : IsRegular p) (b : B) : Nonempty ↑(p ⁻¹' {b})

A regular deck action has nonempty fibres.

theorem TauCeti.Deck.IsRegular.fiber_isPretransitive {E : Type u_1} {B : Type u_3} [TopologicalSpace E] {p : E → B} (hreg : IsRegular p) (b : B) : MulAction.IsPretransitive ↥(deck p) ↑(p ⁻¹' {b})

The deck action on each fibre of a regular map is transitive.

theorem TauCeti.Deck.IsRegular.exists_apply_eq {E : Type u_1} {B : Type u_3} [TopologicalSpace E] {p : E → B} (hreg : IsRegular p) {e e' : E} (heq : p e = p e') : ∃ (φ : ↥(deck p)), ↑φ e = e'

For a regular map, any two points with the same projection differ by a deck transformation.

theorem TauCeti.Deck.IsRegular.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) : IsRegular q

Regularity of the deck action is transported by an over-base homeomorphism.

theorem TauCeti.Deck.IsRegular.conj_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) : IsRegular q ↔ IsRegular p

Regularity is invariant under an over-base homeomorphism.

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

For a preconnected covering with regular deck action, evaluation at a chosen fibre point identifies the deck group with that fibre.

Equations

• TauCeti.Deck.deckEquivFiber hp hreg e = TauCeti.Deck.deckEquivFiberOfSurjective hp e ⋯

@[simp]

theorem TauCeti.Deck.deckEquivFiber_apply {E : Type u_1} {B : Type u_3} [TopologicalSpace E] {p : E → B} [TopologicalSpace B] {b : B} [PreconnectedSpace E] (hp : IsCoveringMap p) (hreg : IsRegular p) (e : ↑(p ⁻¹' {b})) (φ : ↥(deck p)) : (deckEquivFiber hp hreg e) φ = φ • e

The equivalence from deck transformations to a fibre evaluates a deck transformation at the chosen fibre point.

theorem TauCeti.Deck.deckEquivFiber_apply_coe {E : Type u_1} {B : Type u_3} [TopologicalSpace E] {p : E → B} [TopologicalSpace B] {b : B} [PreconnectedSpace E] (hp : IsCoveringMap p) (hreg : IsRegular p) (e : ↑(p ⁻¹' {b})) (φ : ↥(deck p)) : ↑((deckEquivFiber hp hreg e) φ) = ↑φ ↑e

On underlying points, the deck-to-fibre equivalence is evaluation of the underlying homeomorphism.

theorem TauCeti.Deck.deckEquivFiber_one {E : Type u_1} {B : Type u_3} [TopologicalSpace E] {p : E → B} [TopologicalSpace B] {b : B} [PreconnectedSpace E] (hp : IsCoveringMap p) (hreg : IsRegular p) (e : ↑(p ⁻¹' {b})) : (deckEquivFiber hp hreg e) 1 = e

The equivalence from deck transformations to a fibre sends the identity to the chosen base point.

theorem TauCeti.Deck.deckEquivFiber_mul {E : Type u_1} {B : Type u_3} [TopologicalSpace E] {p : E → B} [TopologicalSpace B] {b : B} [PreconnectedSpace E] (hp : IsCoveringMap p) (hreg : IsRegular p) (e : ↑(p ⁻¹' {b})) (φ ψ : ↥(deck p)) : (deckEquivFiber hp hreg e) (φ * ψ) = φ • (deckEquivFiber hp hreg e) ψ

The equivalence from deck transformations to a fibre is equivariant for left multiplication on the deck group and the deck action on the fibre.

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

The inverse of deckEquivFiber is characterized by the deck transformation it returns: it sends the chosen fibre point to the requested fibre point.

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

On underlying points, the inverse of deckEquivFiber sends the chosen point to the requested point.

theorem TauCeti.Deck.deckEquivFiber_symm_apply_smul {E : Type u_1} {B : Type u_3} [TopologicalSpace E] {p : E → B} [TopologicalSpace B] {b : B} [PreconnectedSpace E] (hp : IsCoveringMap p) (hreg : IsRegular p) (e e' : ↑(p ⁻¹' {b})) (φ : ↥(deck p)) : (deckEquivFiber hp hreg e).symm (φ • e') = φ * (deckEquivFiber hp hreg e).symm e'

Translating a fibre point before applying the inverse deckEquivFiber multiplies the corresponding deck transformation on the left.