The quotient homomorphism between two quotients of a group

For normal subgroups V ≤ U of a group G, the class of g modulo V determines its class modulo U, so there is a homomorphism G ⧸ V →* G ⧸ U: the homomorphism underlying Mathlib's Subgroup.quotientMapOfLE. It is Mathlib's QuotientGroup.map at the identity of G, the map ProfiniteGrp.toFiniteQuotientFunctor sends V ≤ U to, and it is the canonical transition map of the system of quotient groups of G indexed by its normal subgroups ordered by inclusion, and of the systems built from those quotients.

QuotientGroup.map asks for V ≤ Subgroup.comap (MonoidHom.id G) U rather than V ≤ U, and the two are equal only up to unfolding; naming the specialization keeps the systems built on it rewritable.

Main definitions

• TauCeti.QuotientGroup.mapOfLE hVU: the quotient homomorphism G ⧸ V →* G ⧸ U for V ≤ U.

Main statements

• TauCeti.QuotientGroup.mapOfLE_mk: the map sends the class of g to the class of g, which is what characterizes it.
• TauCeti.QuotientGroup.mapOfLE_refl and TauCeti.QuotientGroup.mapOfLE_comp: the two functor laws.
• TauCeti.QuotientGroup.mapOfLE_comp_mk': composing it with the quotient map of G modulo V gives the quotient map of G modulo U.
• TauCeti.QuotientGroup.map_comp_mapOfLE and TauCeti.QuotientGroup.mapOfLE_comp_map: it commutes with the homomorphisms QuotientGroup.map induced by a homomorphism G →* H on the quotients.
• TauCeti.QuotientGroup.mapOfLE_surjective: the map is surjective.
• TauCeti.QuotientGroup.ker_mapOfLE: its kernel is the image of U in G ⧸ V.
• TauCeti.QuotientGroup.map_injective_of_eq_comap: the homomorphism G ⧸ f⁻¹(M) →* H ⧸ M induced by f : G →* H is injective.

Usage

Work with mapOfLE through the lemmas above: mapOfLE_mk evaluates it on classes, mapOfLE_refl, mapOfLE_comp, mapOfLE_comp_mk', map_comp_mapOfLE and mapOfLE_comp_map simplify identities and composites, mapOfLE_surjective feeds constructions that need a surjection, such as Sylow.mapSurjective, and ker_mapOfLE identifies its kernel. To identify mapOfLE hVU with another homomorphism out of G ⧸ V, compare the two on classes with QuotientGroup.induction_on and mapOfLE_mk.

def TauCeti.QuotientGroup.mapOfLE {G : Type u_1} [Group G] {U V : Subgroup G} [U.Normal] [V.Normal] (hVU : V ≤ U) : G ⧸ V →* G ⧸ U

The quotient homomorphism G ⧸ V →* G ⧸ U for normal subgroups V ≤ U. This is Mathlib's QuotientGroup.map at the identity of G, the map ProfiniteGrp.toFiniteQuotientFunctor sends V ≤ U to.

Equations

• TauCeti.QuotientGroup.mapOfLE hVU = QuotientGroup.map V U (MonoidHom.id G) ⋯

@[simp]

theorem TauCeti.QuotientGroup.mapOfLE_mk {G : Type u_1} [Group G] {U V : Subgroup G} [U.Normal] [V.Normal] (hVU : V ≤ U) (g : G) : (mapOfLE hVU) ↑g = ↑g

The quotient homomorphism sends the class of g modulo V to the class of g modulo U.

@[simp]

theorem TauCeti.QuotientGroup.mapOfLE_refl {G : Type u_1} [Group G] {U : Subgroup G} [U.Normal] : mapOfLE ⋯ = MonoidHom.id (G ⧸ U)

The quotient homomorphism for U ≤ U is the identity of G ⧸ U.

@[simp]

theorem TauCeti.QuotientGroup.mapOfLE_comp {G : Type u_1} [Group G] {U V W : Subgroup G} [U.Normal] [V.Normal] [W.Normal] (hWV : W ≤ V) (hVU : V ≤ U) : (mapOfLE hVU).comp (mapOfLE hWV) = mapOfLE ⋯

The quotient homomorphisms compose: G ⧸ W → G ⧸ V → G ⧸ U is the quotient homomorphism for W ≤ U.

@[simp]

theorem TauCeti.QuotientGroup.mapOfLE_comp_mk' {G : Type u_1} [Group G] {U V : Subgroup G} [U.Normal] [V.Normal] (hVU : V ≤ U) : (mapOfLE hVU).comp (QuotientGroup.mk' V) = QuotientGroup.mk' U

The quotient homomorphism G ⧸ V →* G ⧸ U is the quotient map of G modulo U, read through the quotient map of G modulo V.

@[simp]

theorem TauCeti.QuotientGroup.map_comp_mapOfLE {G : Type u_1} [Group G] {U V : Subgroup G} {H : Type u_2} [Group H] {N : Subgroup H} [N.Normal] [U.Normal] [V.Normal] (hVU : V ≤ U) (f : G →* H) (h : U ≤ Subgroup.comap f N) : (QuotientGroup.map U N f h).comp (mapOfLE hVU) = QuotientGroup.map V N f ⋯

The homomorphism G ⧸ U →* H ⧸ N induced by f composed with the quotient homomorphism G ⧸ V →* G ⧸ U is the homomorphism G ⧸ V →* H ⧸ N induced by f.

@[simp]

theorem TauCeti.QuotientGroup.mapOfLE_comp_map {G : Type u_1} [Group G] {U : Subgroup G} {H : Type u_2} [Group H] {M N : Subgroup H} [M.Normal] [N.Normal] [U.Normal] (hMN : M ≤ N) (f : G →* H) (h : U ≤ Subgroup.comap f M) : (mapOfLE hMN).comp (QuotientGroup.map U M f h) = QuotientGroup.map U N f ⋯

The quotient homomorphism H ⧸ M →* H ⧸ N composed with the homomorphism G ⧸ U →* H ⧸ M induced by f is the homomorphism G ⧸ U →* H ⧸ N induced by f.

theorem TauCeti.QuotientGroup.mapOfLE_surjective {G : Type u_1} [Group G] {U V : Subgroup G} [U.Normal] [V.Normal] (hVU : V ≤ U) : Function.Surjective ⇑(mapOfLE hVU)

The quotient homomorphism G ⧸ V →* G ⧸ U is surjective.

@[simp]

theorem TauCeti.QuotientGroup.ker_mapOfLE {G : Type u_1} [Group G] {U V : Subgroup G} [U.Normal] [V.Normal] (hVU : V ≤ U) : (mapOfLE hVU).ker = Subgroup.map (QuotientGroup.mk' V) U

The kernel of the quotient homomorphism G ⧸ V →* G ⧸ U is the image of U in G ⧸ V.

theorem TauCeti.QuotientGroup.map_injective_of_eq_comap {G : Type u_1} [Group G] {U : Subgroup G} {H : Type u_2} [Group H] (f : G →* H) [U.Normal] (M : Subgroup H) [M.Normal] (h : U = Subgroup.comap f M) : Function.Injective ⇑(QuotientGroup.map U M f ⋯)

The homomorphism G ⧸ N →* H ⧸ M induced by f : G →* H on the quotients is injective when N is the preimage f⁻¹(M): its kernel is the image of f⁻¹(M), which is trivial in G ⧸ N.