Transporting deck actions on fibres

An isomorphism of maps over a common base identifies corresponding fibres. This file packages that fibre identification and records that it intertwines the restricted deck actions with conjugation of deck transformations.

Pointed cover isomorphisms carry chosen lifts of the basepoint between fibres, and the pointed/unpointed cover correspondences need the deck action on those fibres to be compatible with conjugating the deck group.

Main definitions

• TauCeti.Deck.fiberMap: the homeomorphism between fibres induced by an over-base homeomorphism.
• TauCeti.Deck.fiberMap_smul: fibre transport intertwines the restricted deck actions via conjugation of deck transformations.
• TauCeti.Deck.fiberMapStabilizerEquiv: fibre transport identifies stabilizers via conjugation of deck transformations.
• TauCeti.Deck.map_fiber_stabilizer_conjMulEquiv: conjugation maps the source fibre stabilizer onto the transported target fibre stabilizer.
• TauCeti.Deck.mem_orbit_fiberMap_iff: fibre transport preserves deck-orbit membership.

def TauCeti.Deck.fiberMap {E : Type u_1} {F : Type u_2} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (b : B) : ↑(p ⁻¹' {b}) ≃ₜ ↑(q ⁻¹' {b})

An over-base homeomorphism identifies the fibre over b for p with the fibre over b for q.

Equations

• TauCeti.Deck.fiberMap h hpq b = h.subtype ⋯

@[simp]

theorem TauCeti.Deck.fiberMap_apply_coe {E : Type u_1} {F : Type u_2} {B : Type u_4} [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})) : ↑((fiberMap h hpq b) e) = h ↑e

On underlying points, the fibre map induced by an over-base homeomorphism is just that homeomorphism.

@[simp]

theorem TauCeti.Deck.fiberMap_symm_apply_coe {E : Type u_1} {F : Type u_2} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} {b : B} (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (f : ↑(q ⁻¹' {b})) : ↑((fiberMap h hpq b).symm f) = h.symm ↑f

On underlying points, the inverse fibre map is the inverse of the over-base homeomorphism.

@[simp]

theorem TauCeti.Deck.fiberMap_refl {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} {b : B} : fiberMap (Homeomorph.refl E) ⋯ b = Homeomorph.refl ↑(p ⁻¹' {b})

The fibre map induced by the identity over-base homeomorphism is the identity.

@[simp]

theorem TauCeti.Deck.fiberMap_symm {E : Type u_1} {F : Type u_2} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} {b : B} (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) : (fiberMap h hpq b).symm = fiberMap h.symm ⋯ b

The inverse of the fibre map induced by an over-base homeomorphism is the fibre map induced by the inverse over-base homeomorphism.

@[simp]

theorem TauCeti.Deck.fiberMap_trans {E : Type u_1} {F : Type u_2} {G : Type u_3} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] {p : E → B} {q : F → B} {r : G → B} {b : B} (h : E ≃ₜ F) (k : F ≃ₜ G) (hpq : ∀ (e : E), q (h e) = p e) (hqr : ∀ (f : F), r (k f) = q f) : (fiberMap h hpq b).trans (fiberMap k hqr b) = fiberMap (h.trans k) ⋯ b

Fibre maps compose as the underlying over-base homeomorphisms compose.

@[simp]

theorem TauCeti.Deck.fiberMap_smul {E : Type u_1} {F : Type u_2} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} {b : B} (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (φ : ↥(deck p)) (e : ↑(p ⁻¹' {b})) : (fiberMap h hpq b) (φ • e) = (conjMulEquiv h hpq) φ • (fiberMap h hpq b) e

Fibre transport intertwines the restricted deck action with conjugation of deck transformations.

theorem TauCeti.Deck.fiberMap_symm_smul {E : Type u_1} {F : Type u_2} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} {b : B} (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (ψ : ↥(deck q)) (f : ↑(q ⁻¹' {b})) : (fiberMap h hpq b).symm (ψ • f) = (conjMulEquiv h hpq).symm ψ • (fiberMap h hpq b).symm f

The inverse fibre transport intertwines the restricted deck action with inverse conjugation of deck transformations.

@[simp]

theorem TauCeti.Deck.fiberMap_trans_fiberHomeomorph {E : Type u_1} {F : Type u_2} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} {b : B} (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (φ : ↥(deck p)) : (fiberMap h hpq b).trans (deck.fiberHomeomorph ((conjMulEquiv h hpq) φ) b) = (deck.fiberHomeomorph φ b).trans (fiberMap h hpq b)

Transporting a deck transformation to the target cover and then restricting it to a fibre is the same as restricting first and conjugating the resulting fibre homeomorphism by the fibre transport map.

@[simp]

theorem TauCeti.Deck.fiberHomeomorphHom_conjMulEquiv {E : Type u_1} {F : Type u_2} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} {b : B} (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (φ : ↥(deck p)) : (fiberHomeomorphHom q b) ((conjMulEquiv h hpq) φ) = (fiberMap h hpq b).symm.trans (((fiberHomeomorphHom p b) φ).trans (fiberMap h hpq b))

Restricting conjugated deck transformations to a fibre is compatible with the fibre restriction homomorphism.

theorem TauCeti.Deck.mem_stabilizer_conjMulEquiv_fiberMap_iff {E : Type u_1} {F : Type u_2} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} {b : B} (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (φ : ↥(deck p)) (e : ↑(p ⁻¹' {b})) : (conjMulEquiv h hpq) φ ∈ MulAction.stabilizer (↥(deck q)) ((fiberMap h hpq b) e) ↔ φ ∈ MulAction.stabilizer (↥(deck p)) e

Conjugation transports stabilizer membership along the fibre map.

theorem TauCeti.Deck.map_fiber_stabilizer_conjMulEquiv {E : Type u_1} {F : Type u_2} {B : Type u_4} [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})) : Subgroup.map (↑(conjMulEquiv h hpq)) (MulAction.stabilizer (↥(deck p)) e) = MulAction.stabilizer (↥(deck q)) ((fiberMap h hpq b) e)

Conjugation maps the source fibre stabilizer onto the transported target fibre stabilizer.

def TauCeti.Deck.fiberMapStabilizerEquiv {E : Type u_1} {F : Type u_2} {B : Type u_4} [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})) : ↥(MulAction.stabilizer (↥(deck p)) e) ≃* ↥(MulAction.stabilizer (↥(deck q)) ((fiberMap h hpq b) e))

Fibre transport identifies stabilizers, using conjugation on deck transformations.

Equations

• TauCeti.Deck.fiberMapStabilizerEquiv h hpq e = ((TauCeti.Deck.conjMulEquiv h hpq).subgroupMap (MulAction.stabilizer (↥(deck p)) e)).trans (MulEquiv.subgroupCongr ⋯)

@[simp]

theorem TauCeti.Deck.fiberMapStabilizerEquiv_apply_coe {E : Type u_1} {F : Type u_2} {B : Type u_4} [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})) (φ : ↥(MulAction.stabilizer (↥(deck p)) e)) : ↑((fiberMapStabilizerEquiv h hpq e) φ) = (conjMulEquiv h hpq) ↑φ

On deck transformations, the fibre-map stabilizer equivalence is conjugation.

@[simp]

theorem TauCeti.Deck.fiberMapStabilizerEquiv_symm_apply_coe {E : Type u_1} {F : Type u_2} {B : Type u_4} [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})) (ψ : ↥(MulAction.stabilizer (↥(deck q)) ((fiberMap h hpq b) e))) : ↑((fiberMapStabilizerEquiv h hpq e).symm ψ) = (conjMulEquiv h hpq).symm ↑ψ

On deck transformations, the inverse fibre-map stabilizer equivalence is inverse conjugation.

theorem TauCeti.Deck.fiberMap_mem_orbit {E : Type u_1} {F : Type u_2} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} {b : B} (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (φ : ↥(deck p)) (e : ↑(p ⁻¹' {b})) : (fiberMap h hpq b) (φ • e) ∈ MulAction.orbit (↥(deck q)) ((fiberMap h hpq b) e)

Applying a deck transformation and then transporting to the target fibre gives a point in the target deck orbit.

@[simp]

theorem TauCeti.Deck.fiberMap_image_orbit {E : Type u_1} {F : Type u_2} {B : Type u_4} [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})) : ⇑(fiberMap h hpq b) '' MulAction.orbit (↥(deck p)) e = MulAction.orbit (↥(deck q)) ((fiberMap h hpq b) e)

The fibre map carries the deck orbit of a point onto the deck orbit of the transported point.

theorem TauCeti.Deck.fiberMap_symm_mem_orbit {E : Type u_1} {F : Type u_2} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} {b : B} (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (ψ : ↥(deck q)) (f : ↑(q ⁻¹' {b})) : (fiberMap h hpq b).symm (ψ • f) ∈ MulAction.orbit (↥(deck p)) ((fiberMap h hpq b).symm f)

Applying a deck transformation and then transporting back to the source fibre gives a point in the source deck orbit.

theorem TauCeti.Deck.fiberMap_symm_image_orbit {E : Type u_1} {F : Type u_2} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} {b : B} (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (f : ↑(q ⁻¹' {b})) : ⇑(fiberMap h hpq b).symm '' MulAction.orbit (↥(deck q)) f = MulAction.orbit (↥(deck p)) ((fiberMap h hpq b).symm f)

The inverse fibre map carries the deck orbit of a point onto the deck orbit of the transported point.

@[simp]

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

Transporting both fibre points preserves membership in deck orbits.

theorem TauCeti.Deck.mem_orbit_fiberMap_symm_iff {E : Type u_1} {F : Type u_2} {B : Type u_4} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} {b : B} (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (f f' : ↑(q ⁻¹' {b})) : (fiberMap h hpq b).symm f' ∈ MulAction.orbit (↥(deck p)) ((fiberMap h hpq b).symm f) ↔ f' ∈ MulAction.orbit (↥(deck q)) f

Transporting both target-fibre points back preserves membership in deck orbits.