Conjugating deck normalizer quotients

An isomorphism of covers over a common base identifies deck groups by conjugation. This file records the induced identification on the normalizer quotients N(H) / H of deck subgroups. Those quotients are the algebraic groups appearing in the universal-covers roadmap as deck groups of covers attached to subgroups.

Main declarations

• TauCeti.Deck.normalizerQuotientConjEquiv: conjugation along an over-base homeomorphism identifies N(H) / H with N(conj(H)) / conj(H).
• Representative formulas for the forward and inverse maps, including composition compatibility on representatives.

References

This supplies a basepoint-change and cover-isomorphism bookkeeping prerequisite for TauCetiRoadmap/UniversalCovers/README.md, Stage 2, item 8: pointed connected covers correspond to subgroups, unpointed connected covers correspond to conjugacy classes of subgroups, and the deck group attached to H is N(H) / H.

@[reducible, inline]

noncomputable abbrev TauCeti.Deck.normalizerQuotientConjEquiv {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) (H : Subgroup ↥(Deck p)) : Subgroup.normalizerQuotient H ≃* Subgroup.normalizerQuotient (Subgroup.map (↑(conjMulEquiv h hpq)) H)

Conjugating an over-base homeomorphism identifies the normalizer quotient of a deck subgroup with the normalizer quotient of the conjugated subgroup.

Equations

• TauCeti.Deck.normalizerQuotientConjEquiv h hpq H = TauCeti.Subgroup.normalizerQuotientEquivMap H (TauCeti.Deck.conjMulEquiv h hpq)

theorem TauCeti.Deck.normalizerQuotientConjEquiv_mk {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) (H : Subgroup ↥(Deck p)) (φ : ↥(Subgroup.normalizer ↑H)) : (normalizerQuotientConjEquiv h hpq H) ((Subgroup.normalizerQuotientMk H) φ) = (Subgroup.normalizerQuotientMk (Subgroup.map (↑(conjMulEquiv h hpq)) H)) ((Subgroup.normalizerEquivMap H (conjMulEquiv h hpq)) φ)

On normalizer representatives, the deck normalizer-quotient conjugation equivalence is induced by conjugating deck transformations.

theorem TauCeti.Deck.normalizerQuotientConjEquiv_refl_mk_congr {E : Type u_1} {B : Type u_3} [TopologicalSpace E] {p : E → B} (H : Subgroup ↥(Deck p)) (φ : ↥(Subgroup.normalizer ↑H)) : (Subgroup.normalizerQuotientCongr ⋯) ((normalizerQuotientConjEquiv (Homeomorph.refl E) ⋯ H) ((Subgroup.normalizerQuotientMk H) φ)) = (Subgroup.normalizerQuotientMk H) φ

After the subgroup equality induced by identity conjugation, conjugating the normalizer quotient by the identity over-base homeomorphism is the canonical identity on representatives.

theorem TauCeti.Deck.normalizerQuotientConjEquiv_symm_mk {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) (H : Subgroup ↥(Deck p)) (ψ : ↥(Subgroup.normalizer ↑(Subgroup.map (↑(conjMulEquiv h hpq)) H))) : (normalizerQuotientConjEquiv h hpq H).symm ((Subgroup.normalizerQuotientMk (Subgroup.map (↑(conjMulEquiv h hpq)) H)) ψ) = (Subgroup.normalizerQuotientMk H) ((Subgroup.normalizerEquivMap H (conjMulEquiv h hpq)).symm ψ)

The inverse deck normalizer-quotient conjugation equivalence is induced by inverse conjugation of deck transformations.

theorem TauCeti.Deck.normalizerQuotientConjEquiv_trans_mk {E : Type u_1} {F : Type u_2} {B : Type u_3} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} {G : Type u_4} [TopologicalSpace G] {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.normalizer ↑H)) : (normalizerQuotientConjEquiv k hqr (Subgroup.map (↑(conjMulEquiv h hpq)) H)) ((normalizerQuotientConjEquiv h hpq H) ((Subgroup.normalizerQuotientMk H) φ)) = (Subgroup.normalizerQuotientMk (Subgroup.map (↑(conjMulEquiv k hqr)) (Subgroup.map (↑(conjMulEquiv h hpq)) H))) ((Subgroup.normalizerEquivMap (Subgroup.map (↑(conjMulEquiv h hpq)) H) (conjMulEquiv k hqr)) ((Subgroup.normalizerEquivMap H (conjMulEquiv h hpq)) φ))

Composing two deck normalizer-quotient conjugation equivalences sends representatives through the two successive conjugation transports.

theorem TauCeti.Deck.normalizerQuotientConjEquiv_trans_mk_congr {E : Type u_1} {F : Type u_2} {B : Type u_3} [TopologicalSpace E] [TopologicalSpace F] {p : E → B} {q : F → B} {G : Type u_4} [TopologicalSpace G] {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.normalizer ↑H)) : (Subgroup.normalizerQuotientCongr ⋯) ((normalizerQuotientConjEquiv k hqr (Subgroup.map (↑(conjMulEquiv h hpq)) H)) ((normalizerQuotientConjEquiv h hpq H) ((Subgroup.normalizerQuotientMk H) φ))) = (normalizerQuotientConjEquiv (h.trans k) ⋯ H) ((Subgroup.normalizerQuotientMk H) φ)

After identifying the twice-conjugated subgroup with the subgroup conjugated by the composite over-base homeomorphism, composing deck normalizer-quotient conjugation equivalences agrees with conjugation by the composite on representatives.

theorem TauCeti.Deck.normalizerQuotientConjEquiv_symm_mk' {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) (H : Subgroup ↥(Deck p)) (ψ : ↥(Subgroup.normalizer ↑(Subgroup.map (↑(conjMulEquiv h hpq)) H))) : (normalizerQuotientConjEquiv h.symm ⋯ (Subgroup.map (↑(conjMulEquiv h hpq)) H)) ((Subgroup.normalizerQuotientMk (Subgroup.map (↑(conjMulEquiv h hpq)) H)) ψ) = (Subgroup.normalizerQuotientMk (Subgroup.map (↑(conjMulEquiv h.symm ⋯)) (Subgroup.map (↑(conjMulEquiv h hpq)) H))) ((Subgroup.normalizerEquivMap (Subgroup.map (↑(conjMulEquiv h hpq)) H) (conjMulEquiv h.symm ⋯)) ψ)

Inverse-conjugating a representative of the h-conjugated subgroup quotient gives the stated representative in the twice-mapped subgroup.

theorem TauCeti.Deck.normalizerQuotientConjEquiv_mk_coe {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) (H : Subgroup ↥(Deck p)) (φ : ↥(Subgroup.normalizer ↑H)) : (normalizerQuotientConjEquiv h hpq H) ((Subgroup.normalizerQuotientMk H) φ) = (Subgroup.normalizerQuotientMk (Subgroup.map (↑(conjMulEquiv h hpq)) H)) ⟨(conjMulEquiv h hpq) ↑φ, ⋯⟩

On underlying deck transformations, the normalizer representative in the target quotient is obtained by conjugation.

theorem TauCeti.Deck.normalizerQuotientConjEquiv_symm_mk_coe {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) (H : Subgroup ↥(Deck p)) (ψ : ↥(Subgroup.normalizer ↑(Subgroup.map (↑(conjMulEquiv h hpq)) H))) : (normalizerQuotientConjEquiv h hpq H).symm ((Subgroup.normalizerQuotientMk (Subgroup.map (↑(conjMulEquiv h hpq)) H)) ψ) = (Subgroup.normalizerQuotientMk H) ⟨(conjMulEquiv h hpq).symm ↑ψ, ⋯⟩

On representatives, inverse transport of the deck normalizer quotient applies inverse conjugation.