The Krasner–Kaloujnine embedding

For a group G and a normal subgroup N, the Krasner–Kaloujnine homomorphism krasnerKaloujnineHom : G →* N ≀ᵣ (G ⧸ N) into Mathlib's regular wreath product is injective (krasnerKaloujnine_injective). Combined with the bridge of MonoidWreathBridge.lean, group_sgdiv_via_normal shows that G divides WreathProduct N (G ⧸ N) (G ⧸ N); this is the step that splits a finite group along a normal series.

Implementation notes

The embedding needs a section s : G ⧸ N → G of the quotient map, obtained noncomputably via Function.surjInv. The component n_g(q) := s(q)⁻¹ * g * s(π(g)⁻¹ * q) lies in N because its image under π is q⁻¹ * π(g) * π(g)⁻¹ * q = 1.

Krasner-Kaloujnine universal embedding

noncomputable def LeanPool.KrohnRhodes.section_ {G : Type u} [Group G] (N : Subgroup G) [N.Normal] : G ⧸ N → G

A noncomputable section G ⧸ N → G of the quotient map.

Equations

• LeanPool.KrohnRhodes.section_ N = Function.surjInv ⋯

theorem LeanPool.KrohnRhodes.section_apply {G : Type u} [Group G] (N : Subgroup G) [N.Normal] (q : G ⧸ N) : (QuotientGroup.mk' N) (section_ N q) = q

The section is a right inverse of the quotient map.

noncomputable def LeanPool.KrohnRhodes.krasnerLeftRaw {G : Type u} [Group G] (N : Subgroup G) [N.Normal] (g : G) (q : G ⧸ N) : G

The "left component" of the Krasner-Kaloujnine homomorphism, before showing it lands in N.

Equations

• LeanPool.KrohnRhodes.krasnerLeftRaw N g q = (LeanPool.KrohnRhodes.section_ N q)⁻¹ * g * LeanPool.KrohnRhodes.section_ N (((QuotientGroup.mk' N) g)⁻¹ * q)

theorem LeanPool.KrohnRhodes.krasnerLeftRaw_mem {G : Type u} [Group G] (N : Subgroup G) [N.Normal] (g : G) (q : G ⧸ N) : krasnerLeftRaw N g q ∈ N

krasnerLeftRaw g q lies in N (kernel of the quotient map).

noncomputable def LeanPool.KrohnRhodes.krasnerLeft {G : Type u} [Group G] (N : Subgroup G) [N.Normal] (g : G) (q : G ⧸ N) : ↥N

The "left component" of the Krasner-Kaloujnine homomorphism, valued in N.

Equations

• LeanPool.KrohnRhodes.krasnerLeft N g q = ⟨LeanPool.KrohnRhodes.krasnerLeftRaw N g q, ⋯⟩

noncomputable def LeanPool.KrohnRhodes.krasnerKaloujnineFun {G : Type u} [Group G] (N : Subgroup G) [N.Normal] (g : G) : ↥N ≀ᵣ (G ⧸ N)

The Krasner-Kaloujnine map G → N ≀ᵣ (G ⧸ N) (as bare data).

Equations

• LeanPool.KrohnRhodes.krasnerKaloujnineFun N g = { left := LeanPool.KrohnRhodes.krasnerLeft N g, right := (QuotientGroup.mk' N) g }

theorem LeanPool.KrohnRhodes.krasnerKaloujnine_map_mul {G : Type u} [Group G] (N : Subgroup G) [N.Normal] (g₁ g₂ : G) : krasnerKaloujnineFun N (g₁ * g₂) = krasnerKaloujnineFun N g₁ * krasnerKaloujnineFun N g₂

Multiplicativity of the Krasner-Kaloujnine map.

theorem LeanPool.KrohnRhodes.krasnerKaloujnine_map_one {G : Type u} [Group G] (N : Subgroup G) [N.Normal] : krasnerKaloujnineFun N 1 = 1

Triviality at 1 of the Krasner-Kaloujnine map.

noncomputable def LeanPool.KrohnRhodes.krasnerKaloujnineHom {G : Type u} [Group G] (N : Subgroup G) [N.Normal] : G →* ↥N ≀ᵣ (G ⧸ N)

The Krasner-Kaloujnine universal embedding G →* N ≀ᵣ (G ⧸ N).

Equations

• LeanPool.KrohnRhodes.krasnerKaloujnineHom N = { toFun := LeanPool.KrohnRhodes.krasnerKaloujnineFun N, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem LeanPool.KrohnRhodes.krasnerKaloujnineHom_left {G : Type u} [Group G] (N : Subgroup G) [N.Normal] (g : G) (q : G ⧸ N) : ↑(((krasnerKaloujnineHom N) g).left q) = (section_ N q)⁻¹ * g * section_ N (((QuotientGroup.mk' N) g)⁻¹ * q)

theorem LeanPool.KrohnRhodes.krasnerKaloujnine_injective {G : Type u} [Group G] (N : Subgroup G) [N.Normal] : Function.Injective ⇑(krasnerKaloujnineHom N)

Injectivity of the Krasner-Kaloujnine embedding.

From the embedding to SgDiv

theorem LeanPool.KrohnRhodes.group_sgdiv_via_normal {G : Type u} [Group G] (N : Subgroup G) [N.Normal] : SgDiv G (WreathProduct (↥N) (G ⧸ N) (G ⧸ N))

For a group G with a normal subgroup N, G divides WreathProduct N (G/N) (G/N) as a semigroup.