Joining a subgroup with a subgroup that normalizes it

Let H and K be subgroups of a group G with K ≤ Subgroup.normalizer H. Multiplication then carries the external semidirect product H ⋊ K into G, and its image is the join H ⊔ K.

Mathlib builds the homomorphism as SemidirectProduct.monoidHomSubgroup and computes the carrier of the join as Subgroup.coe_mul_of_right_le_normalizer_left, but records neither the range of that homomorphism nor the elementwise normal form g = x * t that the carrier computation gives.

Main results

• TauCeti.SemidirectProduct.range_monoidHomSubgroup: the range of the semidirect-product multiplication homomorphism is H ⊔ K.
• TauCeti.Subgroup.mem_sup_of_right_le_normalizer_left: an element of H ⊔ K is a product of an element of H followed by an element of K.

@[simp]

theorem TauCeti.Subgroup.mem_sup_of_right_le_normalizer_left {G : Type u_1} [Group G] {H K : Subgroup G} (hLE : K ≤ Subgroup.normalizer ↑H) {g : G} : g ∈ H ⊔ K ↔ ∃ x ∈ H, ∃ t ∈ K, g = x * t

An element of H ⊔ K is a product of an element of H followed by an element of K, as soon as K normalizes H.

@[simp]

theorem TauCeti.SemidirectProduct.range_monoidHomSubgroup {G : Type u_1} [Group G] {H K : Subgroup G} (hLE : K ≤ Subgroup.normalizer ↑H) : (SemidirectProduct.monoidHomSubgroup hLE).range = H ⊔ K

Multiplication from the semidirect product of a subgroup with a subgroup normalizing it is onto the join of the two subgroups.