Inclusion-preserving Kurosh decomposition

This statement bridge expresses the decomposition using subgroups of H and their actual inclusion homomorphisms. It adapts the upstream Palomar statement and proves it from the Bass–Serre development.

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

@[reducible, inline]

abbrev GraphCoveringTheory.KuroshStatement.FreeProduct {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] : Type (max v u)

The group free product expressed using Mathlib's indexed monoid coproduct.

Equations

• GraphCoveringTheory.KuroshStatement.FreeProduct G = Monoid.CoprodI G

def GraphCoveringTheory.KuroshStatement.factorInclusion {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (i : ι) : G i →* FreeProduct G

The canonical inclusion of an indexed factor into the free product.

Equations

• GraphCoveringTheory.KuroshStatement.factorInclusion G i = Monoid.CoprodI.of

def GraphCoveringTheory.KuroshStatement.conjugateSubgroup {P : Type u} [Group P] (K : Subgroup P) (g : P) : Subgroup P

The image of a subgroup under conjugation by g.

Equations

• GraphCoveringTheory.KuroshStatement.conjugateSubgroup K g = Subgroup.map (↑(MulAut.conj g)) K

def GraphCoveringTheory.KuroshStatement.intersectionFactor {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (i : ι) (g : FreeProduct G) : Subgroup (FreeProduct G)

Intersect H with the conjugate of an indexed free factor.

Equations

• One or more equations did not get rendered due to their size.

def GraphCoveringTheory.KuroshStatement.intersectionFactorInH {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) (i : ι) (g : FreeProduct G) : Subgroup ↥H

Regard the conjugate-factor intersection as a subgroup of H.

Equations

• GraphCoveringTheory.KuroshStatement.intersectionFactorInH G H i g = Subgroup.comap H.subtype (GraphCoveringTheory.KuroshStatement.intersectionFactor G H i g)

def GraphCoveringTheory.KuroshStatement.Component {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {J : Type (max u v)} (A : J → Subgroup ↥H) (X : Type (max u v)) : J ⊕ PUnit.{1} → Type (max (u + 1) (v + 1))

The subgroup factors and a free group, lifted to a common universe.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance GraphCoveringTheory.KuroshStatement.componentGroup {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {J : Type (max u v)} (A : J → Subgroup ↥H) (X : Type (max u v)) (q : J ⊕ PUnit.{1}) : Group (Component G H A X q)

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev GraphCoveringTheory.KuroshStatement.Product {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {J : Type (max u v)} (A : J → Subgroup ↥H) (X : Type (max u v)) : Type (max (max u v) (u + 1) (v + 1))

The free product of the specified subgroup factors and the free group.

Equations

• GraphCoveringTheory.KuroshStatement.Product G H A X = Monoid.CoprodI (GraphCoveringTheory.KuroshStatement.Component G H A X)

The canonical maps from the displayed factors into H.

def GraphCoveringTheory.KuroshStatement.ComponentHom {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {J : Type (max u v)} (A : J → Subgroup ↥H) (X : Type (max u v)) (freePartMap : ULift.{max (u + 1) (v + 1), max u v} (FreeGroup X) →* ↥H) (q : J ⊕ PUnit.{1}) : Component G H A X q →* ↥H

Use actual subgroup inclusions on factors and the specified homomorphism on the free part.

Equations

• One or more equations did not get rendered due to their size.
• GraphCoveringTheory.KuroshStatement.ComponentHom G H A X freePartMap (Sum.inr val) = freePartMap

The homomorphism induced by the actual factor inclusions.

def GraphCoveringTheory.KuroshStatement.inducedHom {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) {J : Type (max u v)} (A : J → Subgroup ↥H) (X : Type (max u v)) (freePartMap : ULift.{max (u + 1) (v + 1), max u v} (FreeGroup X) →* ↥H) : Product G H A X →* ↥H

The free-product homomorphism induced by the subgroup inclusions and free-part map.

Equations

• GraphCoveringTheory.KuroshStatement.inducedHom G H A X freePartMap = Monoid.CoprodI.lift (GraphCoveringTheory.KuroshStatement.ComponentHom G H A X freePartMap)

The checked proof of the Kurosh Palomar statement.

theorem GraphCoveringTheory.KuroshStatement.kurosh_decomposition_with_inclusions {ι : Type v} (G : ι → Type u) [(i : ι) → Group (G i)] (H : Subgroup (FreeProduct G)) : ∃ (J : Type (max u v)) (X : Type (max u v)) (A : J → Subgroup ↥H), (∀ (j : J), ∃ (i : ι) (g : FreeProduct G), A j = intersectionFactorInH G H i g) ∧ ∃ (freePartMap : ULift.{max (u + 1) (v + 1), max u v} (FreeGroup X) →* ↥H) (decomposition : Product G H A X ≃* ↥H), decomposition.toMonoidHom = inducedHom G H A X freePartMap