Transporting deck fibre torsors

An over-base homeomorphism between two covers identifies their deck groups by conjugation and their corresponding fibres by Deck.fiberMap. This file records that these two identifications are compatible with the torsor structures on fibres.

The main statement is first proved for the local situation of a preconnected covering whose chosen fibre has a free transitive deck action. The regular-cover wrappers then specialize it using Deck.IsRegular, the form used when pointed covers are compared up to changing representatives over the same base.

Main declarations

• TauCeti.Deck.fiberMap_sdiv_eq_conjMulEquiv_of_pretransitive: fibre transport carries torsor division to conjugation of the corresponding deck transformation.
• TauCeti.Deck.fiberMap_sdiv_eq_conjMulEquiv: the regular-cover specialization.
• TauCeti.Deck.deckEquivFiber_fiberMap: transport is compatible with the deck-to-fibre equivalence of a regular cover.

References

The pointed and unpointed cover correspondences require changing the chosen lift in a fibre while transporting deck actions along isomorphisms of covers.

theorem TauCeti.Deck.isPretransitive_fiberMap {E : Type u_1} {F : Type u_2} {B : Type u_3} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} {b : B} (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) [MulAction.IsPretransitive ↥(deck p) ↑(p ⁻¹' {b})] : MulAction.IsPretransitive ↥(deck q) ↑(q ⁻¹' {b})

Fibre transport carries a pretransitive deck action on the source fibre to a pretransitive deck action on the target fibre.

theorem TauCeti.Deck.surjective_smul_fiberMap {E : Type u_1} {F : Type u_2} {B : Type u_3} [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})) (hsurj : Function.Surjective fun (φ : ↥(deck p)) => φ • e) : Function.Surjective fun (ψ : ↥(deck q)) => ψ • (fiberMap h hpq b) e

Fibre transport carries surjectivity of evaluation at a source fibre point to surjectivity of evaluation at the transported target fibre point.

@[simp]

theorem TauCeti.Deck.deckEquivFiberOfSurjective_symm_fiberMap {E : Type u_1} {F : Type u_2} {B : Type u_3} [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace B] {p : E → B} {q : F → B} {b : B} [PreconnectedSpace E] (hp : IsCoveringMap p) (hq : IsCoveringMap q) (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (e e' : ↑(p ⁻¹' {b})) (hsurj : Function.Surjective fun (φ : ↥(deck p)) => φ • e) : (deckEquivFiberOfSurjective hq ((fiberMap h hpq b) e) ⋯).symm ((fiberMap h hpq b) e') = (conjMulEquiv h hpq) ((deckEquivFiberOfSurjective hp e hsurj).symm e')

The inverse of the local deck-to-fibre equivalence is compatible with fibre transport: transport the target fibre point first, or compute the source deck transformation first and then conjugate it.

@[simp]

theorem TauCeti.Deck.fiberMap_sdiv_eq_conjMulEquiv_of_pretransitive {E : Type u_1} {F : Type u_2} {B : Type u_3} [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace B] {p : E → B} {q : F → B} {b : B} [PreconnectedSpace E] (hp : IsCoveringMap p) (hq : IsCoveringMap q) [Nonempty ↑(p ⁻¹' {b})] [MulAction.IsPretransitive ↥(deck p) ↑(p ⁻¹' {b})] (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (e₁ e₂ : ↑(p ⁻¹' {b})) : (fiberMap h hpq b) e₁ /ₛ (fiberMap h hpq b) e₂ = (conjMulEquiv h hpq) (e₁ /ₛ e₂)

Fibre transport preserves torsor division, with the deck-group element transported by conjugation along the over-base homeomorphism.

This is the local pretransitive-fibre form. The regular-cover API below supplies the nonemptiness and pretransitivity hypotheses from Deck.IsRegular.

theorem TauCeti.Deck.deckEquivFiberOfSurjective_fiberMap {E : Type u_1} {F : Type u_2} {B : Type u_3} [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace B] {p : E → B} {q : F → B} {b : B} [PreconnectedSpace E] (hp : IsCoveringMap p) (hq : IsCoveringMap q) (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (e : ↑(p ⁻¹' {b})) (hsurj : Function.Surjective fun (φ : ↥(deck p)) => φ • e) (φ : ↥(deck p)) : (deckEquivFiberOfSurjective hq ((fiberMap h hpq b) e) ⋯) ((conjMulEquiv h hpq) φ) = (fiberMap h hpq b) ((deckEquivFiberOfSurjective hp e hsurj) φ)

The local deck-to-fibre equivalence commutes with transport of deck transformations and fibre points along an over-base homeomorphism.

theorem TauCeti.Deck.deckEquivFiberOfSurjective_fiberMap_coe {E : Type u_1} {F : Type u_2} {B : Type u_3} [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace B] {p : E → B} {q : F → B} {b : B} [PreconnectedSpace E] (hp : IsCoveringMap p) (hq : IsCoveringMap q) (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (e : ↑(p ⁻¹' {b})) (hsurj : Function.Surjective fun (φ : ↥(deck p)) => φ • e) (φ : ↥(deck p)) : ↑((deckEquivFiberOfSurjective hq ((fiberMap h hpq b) e) ⋯) ((conjMulEquiv h hpq) φ)) = h (↑φ ↑e)

On underlying points, local compatibility of deckEquivFiberOfSurjective with fibre transport says that conjugating a deck transformation and then evaluating on the transported fibre point is the same as transporting the original evaluation.

theorem TauCeti.Deck.deckEquivFiber_symm_fiberMap {E : Type u_1} {F : Type u_2} {B : Type u_3} [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace B] {p : E → B} {q : F → B} {b : B} [PreconnectedSpace E] (hp : IsCoveringMap p) (hq : IsCoveringMap q) (hreg : IsRegular p) (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (e e' : ↑(p ⁻¹' {b})) : (deckEquivFiber hq ⋯ ((fiberMap h hpq b) e)).symm ((fiberMap h hpq b) e') = (conjMulEquiv h hpq) ((deckEquivFiber hp hreg e).symm e')

The inverse of the regular deck-to-fibre equivalence is compatible with fibre transport: transport the target fibre point first, or compute the source deck transformation first and then conjugate it.

theorem TauCeti.Deck.deckEquivFiber_fiberMap {E : Type u_1} {F : Type u_2} {B : Type u_3} [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace B] {p : E → B} {q : F → B} {b : B} [PreconnectedSpace E] (hp : IsCoveringMap p) (hq : IsCoveringMap q) (hreg : IsRegular p) (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (e : ↑(p ⁻¹' {b})) (φ : ↥(deck p)) : (deckEquivFiber hq ⋯ ((fiberMap h hpq b) e)) ((conjMulEquiv h hpq) φ) = (fiberMap h hpq b) ((deckEquivFiber hp hreg e) φ)

The regular deck-to-fibre equivalence commutes with transport of deck transformations and fibre points along an over-base homeomorphism.

theorem TauCeti.Deck.deckEquivFiber_fiberMap_coe {E : Type u_1} {F : Type u_2} {B : Type u_3} [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace B] {p : E → B} {q : F → B} {b : B} [PreconnectedSpace E] (hp : IsCoveringMap p) (hq : IsCoveringMap q) (hreg : IsRegular p) (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (e : ↑(p ⁻¹' {b})) (φ : ↥(deck p)) : ↑((deckEquivFiber hq ⋯ ((fiberMap h hpq b) e)) ((conjMulEquiv h hpq) φ)) = h (↑φ ↑e)

On underlying points, the compatibility of deckEquivFiber with fibre transport says that conjugating a deck transformation and then evaluating on the transported fibre point is the same as transporting the original evaluation.

@[simp]

theorem TauCeti.Deck.fiberMap_sdiv_eq_conjMulEquiv {E : Type u_1} {F : Type u_2} {B : Type u_3} [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace B] {p : E → B} {q : F → B} {b : B} [PreconnectedSpace E] (hp : IsCoveringMap p) (hq : IsCoveringMap q) (hreg : IsRegular p) (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (e₁ e₂ : ↑(p ⁻¹' {b})) : (fiberMap h hpq b) e₁ /ₛ (fiberMap h hpq b) e₂ = (conjMulEquiv h hpq) (e₁ /ₛ e₂)

For regular preconnected covers, fibre transport preserves torsor division, with the deck transformation conjugated to the target deck group.