Deck transformations of connected covers

For a covering projection with preconnected total space, two deck transformations are equal as soon as they agree at one point. Equivalently, the deck action on the total space is cancellative, and so is the induced action on every fibre.

The pointed and unpointed cover correspondences track deck transformations through their action on a chosen fibre, and regular-cover statements use the fact that a deck transformation of a connected cover cannot fix a point unless it is the identity.

Main declarations

• TauCeti.Deck.orbitMap_injective: evaluation at a fibre point is injective on deck transformations of a preconnected covering.
• TauCeti.Deck.deckEquivFiberOfSurjective: if that evaluation map is also surjective, it identifies the deck group with the chosen fibre.

theorem TauCeti.Deck.eq_of_apply_eq {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} [PreconnectedSpace E] (hp : IsCoveringMap p) (φ ψ : ↥(deck p)) {e : E} (h : ↑φ e = ↑ψ e) : φ = ψ

Two deck transformations of a covering map with preconnected total space are equal if they agree at one point of the total space.

theorem TauCeti.Deck.eq_of_smul_eq_smul {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} [PreconnectedSpace E] (hp : IsCoveringMap p) (φ ψ : ↥(deck p)) {e : E} (h : φ • e = ψ • e) : φ = ψ

On a covering map with preconnected total space, equality of the ambient deck action at one point determines the deck transformation.

theorem TauCeti.Deck.isCancelSMul {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} [PreconnectedSpace E] (hp : IsCoveringMap p) : IsCancelSMul (↥(deck p)) E

The deck action on the total space of a preconnected covering is cancellative.

@[simp]

theorem TauCeti.Deck.stabilizer_eq_bot {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} [PreconnectedSpace E] (hp : IsCoveringMap p) (e : E) : MulAction.stabilizer (↥(deck p)) e = ⊥

The stabilizer of any point under the deck action of a preconnected covering is trivial.

theorem TauCeti.Deck.eq_of_fiber_smul_eq_fiber_smul {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} {b : B} [PreconnectedSpace E] (hp : IsCoveringMap p) (φ ψ : ↥(deck p)) {e : ↑(p ⁻¹' {b})} (h : φ • e = ψ • e) : φ = ψ

A deck transformation of a preconnected covering is determined by its action on one point of a chosen fibre.

theorem TauCeti.Deck.eq_of_fiberHomeomorph_apply_eq {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} {b : B} [PreconnectedSpace E] (hp : IsCoveringMap p) (φ ψ : ↥(deck p)) {e : ↑(p ⁻¹' {b})} (h : (deck.fiberHomeomorph φ b) e = (deck.fiberHomeomorph ψ b) e) : φ = ψ

A deck transformation of a preconnected covering is determined by the value of its restricted fibre homeomorphism at one point.

theorem TauCeti.Deck.fiber_isCancelSMul {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} {b : B} [PreconnectedSpace E] (hp : IsCoveringMap p) : IsCancelSMul ↥(deck p) ↑(p ⁻¹' {b})

The induced deck action on a fibre of a preconnected covering is cancellative.

@[simp]

theorem TauCeti.Deck.fiber_stabilizer_eq_bot {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} {b : B} [PreconnectedSpace E] (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {b})) : MulAction.stabilizer (↥(deck p)) e = ⊥

The stabilizer of any fibre point under the restricted deck action of a preconnected covering is trivial.

theorem TauCeti.Deck.fiberHomeomorphHom_injective {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})] : Function.Injective ⇑(fiberHomeomorphHom p b)

For a nonempty fibre of a preconnected covering, restricting deck transformations to that fibre is injective.

@[simp]

theorem TauCeti.Deck.fiberHomeomorphHom_ker_eq_bot {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})] : (fiberHomeomorphHom p b).ker = ⊥

For a nonempty fibre of a preconnected covering, the homomorphism restricting deck transformations to that fibre has trivial kernel.

theorem TauCeti.Deck.orbitMap_injective {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} {b : B} [PreconnectedSpace E] (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {b})) : Function.Injective fun (φ : ↥(deck p)) => φ • e

Evaluation at a point in a fibre is injective for a preconnected covering.

noncomputable def TauCeti.Deck.deckEquivFiberOfSurjective {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} {b : B} [PreconnectedSpace E] (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {b})) (hsurj : Function.Surjective fun (φ : ↥(deck p)) => φ • e) : ↥(deck p) ≃ ↑(p ⁻¹' {b})

For a preconnected covering whose orbit map at the chosen fibre point is surjective, evaluation at that point identifies the deck group with that fibre.

This is the simply-transitive fibre action package used later when regular covers are compared with normal subgroups and normalizer quotients.

Equations

• TauCeti.Deck.deckEquivFiberOfSurjective hp e hsurj = Equiv.ofBijective (fun (φ : ↥(deck p)) => φ • e) ⋯

@[simp]

theorem TauCeti.Deck.deckEquivFiberOfSurjective_apply {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} {b : B} [PreconnectedSpace E] (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {b})) (hsurj : Function.Surjective fun (φ : ↥(deck p)) => φ • e) (φ : ↥(deck p)) : (deckEquivFiberOfSurjective hp e hsurj) φ = φ • e

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

theorem TauCeti.Deck.deckEquivFiberOfSurjective_apply_coe {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} {b : B} [PreconnectedSpace E] (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {b})) (hsurj : Function.Surjective fun (φ : ↥(deck p)) => φ • e) (φ : ↥(deck p)) : ↑((deckEquivFiberOfSurjective hp e hsurj) φ) = ↑φ ↑e

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

@[simp]

theorem TauCeti.Deck.deckEquivFiberOfSurjective_symm_smul {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} {b : B} [PreconnectedSpace E] (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {b})) (hsurj : Function.Surjective fun (φ : ↥(deck p)) => φ • e) (e' : ↑(p ⁻¹' {b})) : (deckEquivFiberOfSurjective hp e hsurj).symm e' • e = e'

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

@[simp]

theorem TauCeti.Deck.deckEquivFiberOfSurjective_symm_apply_coe {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} {b : B} [PreconnectedSpace E] (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {b})) (hsurj : Function.Surjective fun (φ : ↥(deck p)) => φ • e) (e' : ↑(p ⁻¹' {b})) : ↑((deckEquivFiberOfSurjective hp e hsurj).symm e') ↑e = ↑e'

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

theorem TauCeti.Deck.deckEquivFiberOfSurjective_one {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} {b : B} [PreconnectedSpace E] (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {b})) (hsurj : Function.Surjective fun (φ : ↥(deck p)) => φ • e) : (deckEquivFiberOfSurjective hp e hsurj) 1 = e

The local deck-to-fibre equivalence sends the identity to the chosen base point.

theorem TauCeti.Deck.deckEquivFiberOfSurjective_mul {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} {b : B} [PreconnectedSpace E] (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {b})) (hsurj : Function.Surjective fun (φ : ↥(deck p)) => φ • e) (φ ψ : ↥(deck p)) : (deckEquivFiberOfSurjective hp e hsurj) (φ * ψ) = φ • (deckEquivFiberOfSurjective hp e hsurj) ψ

The local deck-to-fibre equivalence is equivariant for left multiplication on the deck group and the deck action on the fibre.

@[simp]

theorem TauCeti.Deck.deckEquivFiberOfSurjective_symm_apply_smul {E : Type u_1} {B : Type u_2} [TopologicalSpace E] [TopologicalSpace B] {p : E → B} {b : B} [PreconnectedSpace E] (hp : IsCoveringMap p) (e : ↑(p ⁻¹' {b})) (hsurj : Function.Surjective fun (φ : ↥(deck p)) => φ • e) (e' : ↑(p ⁻¹' {b})) (φ : ↥(deck p)) : (deckEquivFiberOfSurjective hp e hsurj).symm (φ • e') = φ * (deckEquivFiberOfSurjective hp e hsurj).symm e'

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