Conjugating deck transformations

An isomorphism of maps over the same base transports deck transformations by conjugation. This file packages that transport as a multiplicative equivalence of deck groups, so that covers identified up to isomorphism over the base have their deck groups identified by conjugating along the chosen total-space homeomorphism.

Main definitions

• TauCeti.Deck.conjMulEquiv: if h : E ≃ₜ F satisfies q (h e) = p e, then conjugation by h gives deck p ≃* deck q.
• TauCeti.Deck.conjMulEquiv_refl: the identity over-base homeomorphism induces the identity deck-group equivalence.
• TauCeti.Deck.conjMulEquiv_trans: conjugating along a composite over-base homeomorphism is the composite of the conjugation equivalences.

theorem TauCeti.Deck.map_symm_eq_of_map_eq {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) (f : F) : p (h.symm f) = q f

If h : E ≃ₜ F lies over the base, then its inverse also lies over the base in the opposite direction.

def TauCeti.Deck.conjMulEquiv {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) : ↥(deck p) ≃* ↥(deck q)

An isomorphism of maps over the same base identifies their deck transformation groups by conjugation on the total spaces.

Equations

• TauCeti.Deck.conjMulEquiv h hpq = ((TauCeti.Deck.conjHomeomorphMulEquiv✝ h).subgroupMap (deck p)).trans (MulEquiv.subgroupCongr ⋯)

@[simp]

theorem TauCeti.Deck.conjMulEquiv_apply_coe {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) (φ : ↥(deck p)) (f : F) : ↑((conjMulEquiv h hpq) φ) f = h (↑φ (h.symm f))

The deck transformation produced by conjMulEquiv evaluates by conjugation.

@[simp]

theorem TauCeti.Deck.conjMulEquiv_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} (h : E ≃ₜ F) (hpq : ∀ (e : E), q (h e) = p e) (ψ : ↥(deck q)) (e : E) : ↑((conjMulEquiv h hpq).symm ψ) e = h.symm (↑ψ (h e))

The inverse equivalence of conjMulEquiv is conjugation by the inverse homeomorphism.

@[simp]

theorem TauCeti.Deck.conjMulEquiv_refl {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} : conjMulEquiv (Homeomorph.refl E) ⋯ = MulEquiv.refl ↥(deck p)

Conjugating deck transformations along the identity over-base homeomorphism gives the identity deck-group equivalence.

theorem TauCeti.Deck.conjMulEquiv_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} (h : E ≃ₜ F) (k : F ≃ₜ G) (hpq : ∀ (e : E), q (h e) = p e) (hqr : ∀ (f : F), r (k f) = q f) : conjMulEquiv (h.trans k) ⋯ = (conjMulEquiv h hpq).trans (conjMulEquiv k hqr)

Conjugating along a composite over-base homeomorphism is the composite of the two conjugation equivalences.

theorem TauCeti.Deck.subgroup_map_conj_refl {E : Type u_1} {B : Type u_4} [TopologicalSpace E] {p : E → B} (H : Subgroup ↥(deck p)) : Subgroup.map (↑(conjMulEquiv (Homeomorph.refl E) ⋯)) H = H

Conjugation by the identity over-base homeomorphism maps a subgroup to itself.

theorem TauCeti.Deck.subgroup_map_conj_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} (h : E ≃ₜ F) (k : F ≃ₜ G) (hpq : ∀ (e : E), q (h e) = p e) (hqr : ∀ (f : F), r (k f) = q f) (H : Subgroup ↥(deck p)) : Subgroup.map (↑(conjMulEquiv k hqr)) (Subgroup.map (↑(conjMulEquiv h hpq)) H) = Subgroup.map (↑(conjMulEquiv (h.trans k) ⋯)) H

Mapping a subgroup through two successive conjugations agrees with mapping it through the conjugation attached to the composite over-base homeomorphism.