Transporting normalizer quotients along group isomorphisms

The universal-covers roadmap uses the algebraic quotient N(H) / H as the deck group of the cover attached to a subgroup H. When subgroups are transported by a basepoint change or by an isomorphism of covers, the corresponding normalizer quotients have to be identified.

This file records the generic group-theoretic transport: a multiplicative equivalence e : G ≃* K carries N(H) to N(e(H)), and therefore induces a multiplicative equivalence N(H) / H ≃* N(e(H)) / e(H).

Main declarations

• Subgroup.normalizerEquivMap: the normalizer of H is identified with the normalizer of H.map e.
• Subgroup.normalizerQuotientEquivMap: the induced equivalence of normalizer quotients.
• Representative formulas, including compatibility with composition, inverse, and identity equivalences on representatives.

References

This is the algebraic conjugacy bookkeeping needed by TauCetiRoadmap/UniversalCovers/README.md, Stage 2, item 8: the unpointed cover correspondence identifies subgroups only up to conjugacy, and the deck group of the cover attached to H is N(H) / H.

@[reducible, inline]

noncomputable abbrev Subgroup.normalizerEquivMap {G : Type u_1} {K : Type u_2} [Group G] [Group K] (H : Subgroup G) (e : G ≃* K) : ↥(normalizer ↑H) ≃* ↥(normalizer ↑(map (↑e) H))

A group isomorphism identifies the normalizer of a subgroup with the normalizer of its image.

Equations

• H.normalizerEquivMap e = (e.subgroupMap (Subgroup.normalizer ↑H)).trans (MulEquiv.subgroupCongr ⋯)

theorem Subgroup.normalizerEquivMap_apply_coe {G : Type u_1} {K : Type u_2} [Group G] [Group K] (H : Subgroup G) (e : G ≃* K) (g : ↥(normalizer ↑H)) : ↑((H.normalizerEquivMap e) g) = e ↑g

On underlying group elements, normalizerEquivMap is the given group isomorphism.

theorem Subgroup.normalizerEquivMap_symm_apply_coe {G : Type u_1} {K : Type u_2} [Group G] [Group K] (H : Subgroup G) (e : G ≃* K) (k : ↥(normalizer ↑(map (↑e) H))) : ↑((H.normalizerEquivMap e).symm k) = e.symm ↑k

On underlying group elements, the inverse of normalizerEquivMap is the inverse group isomorphism.

theorem Subgroup.normalizerEquivMap_refl {G : Type u_1} [Group G] (H : Subgroup G) (g : ↥(normalizer ↑H)) : (H.normalizerEquivMap (MulEquiv.refl G)) g = ⟨↑g, ⋯⟩

Transporting normalizer representatives along the identity group isomorphism is the identity on underlying representatives.

theorem Subgroup.normalizerEquivMap_trans_apply_coe {G : Type u_1} {K : Type u_2} {L : Type u_3} [Group G] [Group K] [Group L] (H : Subgroup G) (e : G ≃* K) (f : K ≃* L) (g : ↥(normalizer ↑H)) : ↑(((map (↑e) H).normalizerEquivMap f) ((H.normalizerEquivMap e) g)) = f (e ↑g)

Transporting a normalizer representative through two group isomorphisms has underlying value f (e g).

theorem Subgroup.normalizerEquivMap_symm_apply_coe' {G : Type u_1} {K : Type u_2} [Group G] [Group K] (H : Subgroup G) (e : G ≃* K) (k : ↥(normalizer ↑(map (↑e) H))) : ↑(((map (↑e) H).normalizerEquivMap e.symm) k) = e.symm ↑k

Rephrasing the inverse of normalizerEquivMap as transport along the inverse group isomorphism sends a representative to its inverse image.

theorem Subgroup.subgroupOf_map_normalizerEquivMap {G : Type u_1} {K : Type u_2} [Group G] [Group K] (H : Subgroup G) (e : G ≃* K) : map (↑(H.normalizerEquivMap e)) (H.subgroupOf (normalizer ↑H)) = (map (↑e) H).subgroupOf (normalizer ↑(map (↑e) H))

The copy of H inside its normalizer maps to the copy of e(H) inside the target normalizer.

@[reducible, inline]

noncomputable abbrev Subgroup.normalizerQuotientEquivMap {G : Type u_1} {K : Type u_2} [Group G] [Group K] (H : Subgroup G) (e : G ≃* K) : H.normalizerQuotient ≃* (map (↑e) H).normalizerQuotient

A group isomorphism induces an isomorphism on normalizer quotients.

Equations

• One or more equations did not get rendered due to their size.

theorem Subgroup.normalizerQuotientEquivMap_mk {G : Type u_1} {K : Type u_2} [Group G] [Group K] (H : Subgroup G) (e : G ≃* K) (g : ↥(normalizer ↑H)) : (H.normalizerQuotientEquivMap e) (H.normalizerQuotientMk g) = (map (↑e) H).normalizerQuotientMk ((H.normalizerEquivMap e) g)

The induced equivalence on normalizer quotients sends a representative to the image representative.

theorem Subgroup.normalizerQuotientEquivMap_symm_mk {G : Type u_1} {K : Type u_2} [Group G] [Group K] (H : Subgroup G) (e : G ≃* K) (k : ↥(normalizer ↑(map (↑e) H))) : (H.normalizerQuotientEquivMap e).symm ((map (↑e) H).normalizerQuotientMk k) = H.normalizerQuotientMk ((H.normalizerEquivMap e).symm k)

The inverse induced equivalence sends a target representative to the inverse-image representative.

theorem Subgroup.normalizerQuotientEquivMap_refl_mk {G : Type u_1} [Group G] (H : Subgroup G) (g : ↥(normalizer ↑H)) : (H.normalizerQuotientEquivMap (MulEquiv.refl G)) (H.normalizerQuotientMk g) = (map (↑(MulEquiv.refl G)) H).normalizerQuotientMk ⟨↑g, ⋯⟩

After identifying H.map (MulEquiv.refl G) with H, identity transport on normalizer quotients fixes representatives.

theorem Subgroup.normalizerQuotientEquivMap_trans_mk {G : Type u_1} {K : Type u_2} {L : Type u_3} [Group G] [Group K] [Group L] (H : Subgroup G) (e : G ≃* K) (f : K ≃* L) (g : ↥(normalizer ↑H)) : ((map (↑e) H).normalizerQuotientEquivMap f) ((H.normalizerQuotientEquivMap e) (H.normalizerQuotientMk g)) = (map (↑f) (map (↑e) H)).normalizerQuotientMk (((map (↑e) H).normalizerEquivMap f) ((H.normalizerEquivMap e) g))

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

theorem Subgroup.normalizerQuotientEquivMap_refl_mk_congr {G : Type u_1} [Group G] (H : Subgroup G) (g : ↥(normalizer ↑H)) : (normalizerQuotientCongr ⋯) ((H.normalizerQuotientEquivMap (MulEquiv.refl G)) (H.normalizerQuotientMk g)) = H.normalizerQuotientMk g

After the subgroup equality H.map id = H, identity transport on normalizer quotients is the canonical identity on representatives.

theorem Subgroup.normalizerQuotientEquivMap_trans_mk_congr {G : Type u_1} {K : Type u_2} {L : Type u_3} [Group G] [Group K] [Group L] (H : Subgroup G) (e : G ≃* K) (f : K ≃* L) (g : ↥(normalizer ↑H)) : (normalizerQuotientCongr ⋯) (((map (↑e) H).normalizerQuotientEquivMap f) ((H.normalizerQuotientEquivMap e) (H.normalizerQuotientMk g))) = (H.normalizerQuotientEquivMap (e.trans f)) (H.normalizerQuotientMk g)

After identifying the twice-mapped subgroup with the subgroup mapped by e.trans f, composing normalizer-quotient transports agrees with transport by the composite isomorphism on representatives.

theorem Subgroup.normalizerQuotientEquivMap_symm_mk' {G : Type u_1} {K : Type u_2} [Group G] [Group K] (H : Subgroup G) (e : G ≃* K) (k : ↥(normalizer ↑(map (↑e) H))) : ((map (↑e) H).normalizerQuotientEquivMap e.symm) ((map (↑e) H).normalizerQuotientMk k) = (map (↑e.symm) (map (↑e) H)).normalizerQuotientMk (((map (↑e) H).normalizerEquivMap e.symm) k)

Transporting a representative of H.map e along e.symm gives the stated inverse-image representative in (H.map e).map e.symm.

theorem Subgroup.normalizerQuotientEquivMap_mk_coe {G : Type u_1} {K : Type u_2} [Group G] [Group K] (H : Subgroup G) (e : G ≃* K) (g : ↥(normalizer ↑H)) : (H.normalizerQuotientEquivMap e) (H.normalizerQuotientMk g) = (map (↑e) H).normalizerQuotientMk ⟨e ↑g, ⋯⟩

On representatives, normalizerQuotientEquivMap applies the original group isomorphism.