The Kurosh subgroup theorem in Bass--Serre form

The subgroup acts on the Bass--Serre tree of the free product. The quotient graph supplies one vertex group for each quotient vertex and a free group for the quotient graph. The universal graph-of-groups cover constructed in the supporting development identifies the resulting free product with the subgroup itself.

Adapted for Lean Pool from Arthur742Ramos/KuroshSubgroupTheorem, commit 911707126c8b9bb0c764bf853008fe1053c0aad9: imports, API compatibility, and proof organization were revised.

noncomputable def GraphCoveringTheory.Kurosh.kuroshBassSerreEquiv {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : TreeKuroshProduct G H ≃* ↥H

The Bass--Serre graph-of-groups form of Kurosh's theorem.

Equations

• GraphCoveringTheory.Kurosh.kuroshBassSerreEquiv G H = GraphCoveringTheory.Kurosh.treeKuroshProductMulEquivH G H

theorem GraphCoveringTheory.Kurosh.kurosh_bass_serre_decomposition {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : Nonempty (TreeKuroshProduct G H ≃* ↥H)

Every subgroup of a free product is the free product of its Bass--Serre vertex stabilizers and the free group of the quotient graph.

theorem GraphCoveringTheory.Kurosh.kurosh_decomposition {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : Nonempty (KuroshActiveProduct G H ≃* ↥H)

Every subgroup of a free product is a free product of the nontrivial vertex stabilizers in the quotient Bass--Serre graph and the quotient graph's free group.

theorem GraphCoveringTheory.Kurosh.kurosh_vertex_stabilizer_classification {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (a : RawBassSerreOrbitVertex G H) : (∃ (g : FreeProduct G), rawTreeRepresentative G H a = RawBassSerreVertex.central g ∧ treeVertexStabilizer G H a = ⊥) ∨ ∃ (i : ι) (g : FreeProduct G), rawTreeRepresentative G H a = RawBassSerreVertex.factor i (factorCosetMk G i g) ∧ treeVertexStabilizer G H a = intersectionFactorInH H i g

The vertex groups in the Bass--Serre decomposition are either trivial central-vertex stabilizers or intersections with conjugates of the original free factors.

theorem GraphCoveringTheory.Kurosh.kurosh_factor_is_conjugate_intersection {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (j : KuroshActiveVertexIndex G H) : ∃ (i : ι) (g : FreeProduct G), treeVertexStabilizer G H ↑j = intersectionFactorInH H i g

Each nontrivial factor in the factor-only form is an intersection with a conjugate of one of the original free factors.