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 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

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; this file handles the change of basepoint and the isomorphisms of covers.

@[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)) : H.normalizerQuotient ≃* (Subgroup.map (↑(conjMulEquiv h hpq)) H).normalizerQuotient

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 = H.normalizerQuotientEquivMap (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) (H.normalizerQuotientMk φ) = (Subgroup.map (↑(conjMulEquiv h hpq)) H).normalizerQuotientMk ((H.normalizerEquivMap (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) (H.normalizerQuotientMk φ)) = H.normalizerQuotientMk φ

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.map (↑(conjMulEquiv h hpq)) H).normalizerQuotientMk ψ) = H.normalizerQuotientMk ((H.normalizerEquivMap (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) (H.normalizerQuotientMk φ)) = (Subgroup.map (↑(conjMulEquiv k hqr)) (Subgroup.map (↑(conjMulEquiv h hpq)) H)).normalizerQuotientMk (((Subgroup.map (↑(conjMulEquiv h hpq)) H).normalizerEquivMap (conjMulEquiv k hqr)) ((H.normalizerEquivMap (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) (H.normalizerQuotientMk φ))) = (normalizerQuotientConjEquiv (h.trans k) ⋯ H) (H.normalizerQuotientMk φ)

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.map (↑(conjMulEquiv h hpq)) H).normalizerQuotientMk ψ) = (Subgroup.map (↑(conjMulEquiv h.symm ⋯)) (Subgroup.map (↑(conjMulEquiv h hpq)) H)).normalizerQuotientMk (((Subgroup.map (↑(conjMulEquiv h hpq)) H).normalizerEquivMap (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) (H.normalizerQuotientMk φ) = (Subgroup.map (↑(conjMulEquiv h hpq)) H).normalizerQuotientMk ⟨(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.map (↑(conjMulEquiv h hpq)) H).normalizerQuotientMk ψ) = H.normalizerQuotientMk ⟨(conjMulEquiv h hpq).symm ↑ψ, ⋯⟩

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