The normalizer quotient of a subgroup

This file packages the algebraic quotient N(H) / H, where N(H) is the normalizer of a subgroup H ≤ G. This is the group that occurs in the universal-covers roadmap when the deck group of the connected cover associated to H ≤ π₁(X, x₀) is identified with N(H) / H.

The construction is deliberately only a thin local API around Mathlib's Subgroup.normalizer, Subgroup.subgroupOf, and quotient groups. Mathlib already proves that H is normal in its normalizer; this file gives the quotient a stable name and records its canonical quotient map, an equality criterion by multiplication by an element of H, and the comparison with G / H in the normal case.

Main declarations

• Subgroup.normalizerQuotient: the quotient N(H) / H.
• Subgroup.normalizerQuotientMk: the canonical map N(H) →* N(H) / H.
• Subgroup.normalizerQuotientLift: the universal property for maps out of N(H) / H.
• Subgroup.normalizerQuotientToQuotientOfNormal: when H is normal in G, the natural map N(H) / H →* G / H.
• Subgroup.normalizerQuotientEquivQuotientOfNormal: when H is normal in G, the normalizer quotient is canonically isomorphic to G / H.

References

This supplies the algebraic normalizer-quotient prerequisite named in TauCetiRoadmap/UniversalCovers/README.md, Stage 2: for the cover associated to H ≤ π₁(X, x₀), the deck group is N(H) / H, and in the regular case H ◁ π₁(X, x₀) this becomes π₁(X, x₀) / H.

@[reducible, inline]

abbrev Subgroup.normalizerQuotient {G : Type u_1} [Group G] (H : Subgroup G) : Type u_1

The normalizer quotient N(H) / H of a subgroup H ≤ G. Here H is viewed as a normal subgroup of its normalizer, using Mathlib's Subgroup.normal_in_normalizer instance.

Equations

• H.normalizerQuotient = (↥(Subgroup.normalizer ↑H) ⧸ H.subgroupOf (Subgroup.normalizer ↑H))

@[reducible, inline]

abbrev Subgroup.normalizerQuotientMk {G : Type u_1} [Group G] (H : Subgroup G) : ↥(normalizer ↑H) →* H.normalizerQuotient

The canonical quotient map from the normalizer of H to N(H) / H.

Equations

• H.normalizerQuotientMk = QuotientGroup.mk' (H.subgroupOf (Subgroup.normalizer ↑H))

@[simp]

theorem Subgroup.normalizerQuotientMk_apply {G : Type u_1} [Group G] (H : Subgroup G) (g : ↥(normalizer ↑H)) : H.normalizerQuotientMk g = ↑g

The canonical quotient map evaluates as the quotient-group constructor.

theorem Subgroup.normalizerQuotientMk_eq_one_iff {G : Type u_1} [Group G] (H : Subgroup G) (g : ↥(normalizer ↑H)) : H.normalizerQuotientMk g = 1 ↔ ↑g ∈ H

A normalizer element maps to the identity in N(H) / H exactly when its underlying element of G lies in H.

theorem Subgroup.normalizerQuotientMk_ker {G : Type u_1} [Group G] (H : Subgroup G) : H.normalizerQuotientMk.ker = H.subgroupOf (normalizer ↑H)

The kernel of the quotient map N(H) →* N(H) / H is the copy of H inside its normalizer.

theorem Subgroup.normalizerQuotientMk_surjective {G : Type u_1} [Group G] (H : Subgroup G) : Function.Surjective ⇑H.normalizerQuotientMk

Every element of N(H) / H is represented by an element of the normalizer.

theorem Subgroup.normalizerQuotientMk_range {G : Type u_1} [Group G] (H : Subgroup G) : H.normalizerQuotientMk.range = ⊤

The canonical map N(H) →* N(H) / H has full range.

@[reducible, inline]

abbrev Subgroup.normalizerQuotientLift {G : Type u_1} [Group G] {M : Type u_2} [Group M] (H : Subgroup G) (φ : ↥(normalizer ↑H) →* M) (hφ : ∀ (g : ↥(normalizer ↑H)), ↑g ∈ H → φ g = 1) : H.normalizerQuotient →* M

The universal property of N(H) / H: a homomorphism from the normalizer that sends every ambient element of H to 1 descends to a homomorphism from the normalizer quotient.

Equations

• H.normalizerQuotientLift φ hφ = QuotientGroup.lift (H.subgroupOf (Subgroup.normalizer ↑H)) φ ⋯

@[simp]

theorem Subgroup.normalizerQuotientLift_mk {G : Type u_1} [Group G] {M : Type u_2} [Group M] (H : Subgroup G) (φ : ↥(normalizer ↑H) →* M) (hφ : ∀ (g : ↥(normalizer ↑H)), ↑g ∈ H → φ g = 1) (g : ↥(normalizer ↑H)) : (H.normalizerQuotientLift φ hφ) (H.normalizerQuotientMk g) = φ g

The lift from N(H) / H evaluates on representatives as the original homomorphism.

@[simp]

theorem Subgroup.normalizerQuotientLift_comp_mk {G : Type u_1} [Group G] {M : Type u_2} [Group M] (H : Subgroup G) (φ : ↥(normalizer ↑H) →* M) (hφ : ∀ (g : ↥(normalizer ↑H)), ↑g ∈ H → φ g = 1) : (H.normalizerQuotientLift φ hφ).comp H.normalizerQuotientMk = φ

The lift from N(H) / H, composed with the quotient map, is the original homomorphism from the normalizer.

theorem Subgroup.normalizerQuotientLift_surjective_of_surjective {G : Type u_1} [Group G] {M : Type u_2} [Group M] (H : Subgroup G) (φ : ↥(normalizer ↑H) →* M) (hφ : ∀ (g : ↥(normalizer ↑H)), ↑g ∈ H → φ g = 1) (hφsurj : Function.Surjective ⇑φ) : Function.Surjective ⇑(H.normalizerQuotientLift φ hφ)

A lift from N(H) / H is surjective when the original homomorphism from the normalizer is surjective.

theorem Subgroup.normalizerQuotientLift_injective_iff {G : Type u_1} [Group G] {M : Type u_2} [Group M] (H : Subgroup G) (φ : ↥(normalizer ↑H) →* M) (hφ : ∀ (g : ↥(normalizer ↑H)), ↑g ∈ H → φ g = 1) : Function.Injective ⇑(H.normalizerQuotientLift φ hφ) ↔ ∀ (g : ↥(normalizer ↑H)), φ g = 1 ↔ ↑g ∈ H

A lift from N(H) / H is injective exactly when the only normalizer elements killed by the original homomorphism are the elements of H.

theorem Subgroup.normalizerQuotientMk_eq_iff_div_mem {G : Type u_1} [Group G] (H : Subgroup G) (g k : ↥(normalizer ↑H)) : H.normalizerQuotientMk g = H.normalizerQuotientMk k ↔ ↑g / ↑k ∈ H

The quotient equality criterion for representatives in the normalizer, stated in the ambient group G.

theorem Subgroup.normalizerQuotientMk_eq_iff_exists_mul {G : Type u_1} [Group G] (H : Subgroup G) (g k : ↥(normalizer ↑H)) : H.normalizerQuotientMk g = H.normalizerQuotientMk k ↔ ∃ h ∈ H, h * ↑k = ↑g

A version of the equality criterion using multiplication by an element of H.

@[reducible, inline]

noncomputable abbrev Subgroup.normalizerQuotientCongr {G : Type u_1} [Group G] {H K : Subgroup G} (h : H = K) : H.normalizerQuotient ≃* K.normalizerQuotient

Equal subgroups have canonically equivalent normalizer quotients, by transporting both the normalizer and the distinguished subgroup inside it across the equality.

Equations

• Subgroup.normalizerQuotientCongr h = QuotientGroup.congr (H.subgroupOf (Subgroup.normalizer ↑H)) (K.subgroupOf (Subgroup.normalizer ↑K)) (MulEquiv.subgroupCongr ⋯) ⋯

@[simp]

theorem Subgroup.normalizerQuotientCongr_mk {G : Type u_1} [Group G] {H K : Subgroup G} (h : H = K) (g : ↥(normalizer ↑H)) : (normalizerQuotientCongr h) (H.normalizerQuotientMk g) = K.normalizerQuotientMk ((MulEquiv.subgroupCongr ⋯) g)

The equal-subgroup congruence on normalizer quotients sends representatives to the corresponding representatives under the normalizer congruence.

theorem Subgroup.normalizerQuotientCongr_symm_mk {G : Type u_1} [Group G] {H K : Subgroup G} (h : H = K) (g : ↥(normalizer ↑K)) : (normalizerQuotientCongr h).symm (K.normalizerQuotientMk g) = H.normalizerQuotientMk ((MulEquiv.subgroupCongr ⋯) g)

The inverse equal-subgroup congruence on normalizer quotients sends representatives to the corresponding representatives under the inverse normalizer congruence.

@[reducible, inline]

abbrev Subgroup.normalizerQuotientToQuotientOfNormal {G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] : H.normalizerQuotient →* G ⧸ H

When H is normal in G, the normalizer quotient maps naturally to the ordinary quotient G / H by forgetting that representatives lie in the normalizer.

Equations

• H.normalizerQuotientToQuotientOfNormal = QuotientGroup.map (H.subgroupOf (Subgroup.normalizer ↑H)) H (Subgroup.normalizer ↑H).subtype ⋯

@[simp]

theorem Subgroup.normalizerQuotientToQuotientOfNormal_mk {G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] (g : ↥(normalizer ↑H)) : H.normalizerQuotientToQuotientOfNormal (H.normalizerQuotientMk g) = (QuotientGroup.mk' H) ↑g

The comparison map from N(H) / H to G / H sends a normalizer representative to its ordinary quotient class.

@[simp]

theorem Subgroup.normalizerQuotientToQuotientOfNormal_comp_mk {G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] : H.normalizerQuotientToQuotientOfNormal.comp H.normalizerQuotientMk = (QuotientGroup.mk' H).comp (normalizer ↑H).subtype

The ordinary quotient map G →* G / H, factored through the normalizer under normality, agrees with the comparison map from N(H) / H.

@[reducible, inline]

noncomputable abbrev Subgroup.normalizerQuotientEquivQuotientOfNormal {G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] : H.normalizerQuotient ≃* G ⧸ H

If H is normal in G, then N(H) / H is canonically isomorphic to G / H. This is the algebraic form of the regular-cover specialization from N(H) / H to π₁(X, x₀) / H.

Equations

• H.normalizerQuotientEquivQuotientOfNormal = QuotientGroup.congr (H.subgroupOf (Subgroup.normalizer ↑H)) H ((MulEquiv.subgroupCongr ⋯).trans Subgroup.topEquiv) ⋯

theorem Subgroup.normalizerQuotientEquivQuotientOfNormal_mk {G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] (g : ↥(normalizer ↑H)) : H.normalizerQuotientEquivQuotientOfNormal (H.normalizerQuotientMk g) = (QuotientGroup.mk' H) ↑g

The normal-case equivalence sends a normalizer representative to its ordinary quotient class in G / H.

theorem Subgroup.normalizerQuotientEquivQuotientOfNormal_symm_mk {G : Type u_1} [Group G] (H : Subgroup G) [H.Normal] (g : G) : H.normalizerQuotientEquivQuotientOfNormal.symm ((QuotientGroup.mk' H) g) = H.normalizerQuotientMk ⟨g, ⋯⟩

The inverse normal-case equivalence sends an ordinary quotient representative to the corresponding representative in the normalizer quotient.