General free-product rank infrastructure

This file records the factorwise part of the Grushko--Neumann argument for arbitrary groups. The free product of finitely generated groups is finitely generated, and the union of finite generating sets gives the upper bound.

For the lower bound, a tuple whose entries are already separated between the two factors can be projected back to each factor. The remaining, genuinely Grushko-specific step is to reduce an arbitrary generating tuple to this separated form without increasing its length.

Finite generation and the easy inequality

instance MarshallHall.GeneralGrushko.coprod_fg {G : Type u_1} {H : Type u_2} [Group G] [Group H] [Group.FG G] [Group.FG H] : Group.FG (Monoid.Coprod G H)

theorem MarshallHall.GeneralGrushko.rank_coprod_le_add {G : Type u_1} {H : Type u_2} [Group G] [Group H] [Group.FG G] [Group.FG H] : Group.rank (Monoid.Coprod G H) ≤ Group.rank G + Group.rank H

The lower bound for separated generating tuples

def MarshallHall.GeneralGrushko.separatedMap {G : Type u_1} {H : Type u_2} [Group G] [Group H] : G ⊕ H → Monoid.Coprod G H

The natural embedding of a tagged factor element into the free product.

Equations

• MarshallHall.GeneralGrushko.separatedMap (Sum.inl g) = Monoid.Coprod.inl g
• MarshallHall.GeneralGrushko.separatedMap (Sum.inr h) = Monoid.Coprod.inr h

def MarshallHall.GeneralGrushko.leftIndex {G : Type u_1} {H : Type u_2} {n : ℕ} (s : Fin n → G ⊕ H) : Type

The indices whose separated generator lies in the left factor.

Equations

• MarshallHall.GeneralGrushko.leftIndex s = { i : Fin n // ∃ (g : G), s i = Sum.inl g }

def MarshallHall.GeneralGrushko.rightIndex {G : Type u_1} {H : Type u_2} {n : ℕ} (s : Fin n → G ⊕ H) : Type

The indices whose separated generator lies in the right factor.

Equations

• MarshallHall.GeneralGrushko.rightIndex s = { i : Fin n // ¬∃ (g : G), s i = Sum.inl g }

def MarshallHall.GeneralGrushko.leftValue {G : Type u_1} {H : Type u_2} [Group G] {n : ℕ} (s : Fin n → G ⊕ H) (i : leftIndex s) : G

Extracts the left-factor value at an index known to carry a left label.

Equations

• MarshallHall.GeneralGrushko.leftValue s i = match s ↑i with | Sum.inl g => g | Sum.inr val => 1

def MarshallHall.GeneralGrushko.rightValue {G : Type u_1} {H : Type u_2} [Group H] {n : ℕ} (s : Fin n → G ⊕ H) (i : rightIndex s) : H

Extracts the right-factor value at an index known to carry a right label.

Equations

• MarshallHall.GeneralGrushko.rightValue s i = match s ↑i with | Sum.inl val => 1 | Sum.inr h => h

instance MarshallHall.GeneralGrushko.leftIndexFinite {G : Type u_1} {H : Type u_2} {n : ℕ} (s : Fin n → G ⊕ H) : Finite (leftIndex s)

instance MarshallHall.GeneralGrushko.rightIndexFinite {G : Type u_1} {H : Type u_2} {n : ℕ} (s : Fin n → G ⊕ H) : Finite (rightIndex s)

@[instance_reducible]

noncomputable instance MarshallHall.GeneralGrushko.leftIndexFintype {G : Type u_1} {H : Type u_2} {n : ℕ} (s : Fin n → G ⊕ H) : Fintype (leftIndex s)

Equations

• MarshallHall.GeneralGrushko.leftIndexFintype s = Fintype.ofFinite (MarshallHall.GeneralGrushko.leftIndex s)

@[instance_reducible]

noncomputable instance MarshallHall.GeneralGrushko.rightIndexFintype {G : Type u_1} {H : Type u_2} {n : ℕ} (s : Fin n → G ⊕ H) : Fintype (rightIndex s)

Equations

• MarshallHall.GeneralGrushko.rightIndexFintype s = Fintype.ofFinite (MarshallHall.GeneralGrushko.rightIndex s)

noncomputable def MarshallHall.GeneralGrushko.leftGenerators {G : Type u_1} {H : Type u_2} [Group G] {n : ℕ} (s : Fin n → G ⊕ H) : Finset G

The finite set of left-factor generators occurring in a separated generating tuple.

Equations

• MarshallHall.GeneralGrushko.leftGenerators s = Finset.image (MarshallHall.GeneralGrushko.leftValue s) Finset.univ

noncomputable def MarshallHall.GeneralGrushko.rightGenerators {G : Type u_1} {H : Type u_2} [Group H] {n : ℕ} (s : Fin n → G ⊕ H) : Finset H

The finite set of right-factor generators occurring in a separated generating tuple.

Equations

• MarshallHall.GeneralGrushko.rightGenerators s = Finset.image (MarshallHall.GeneralGrushko.rightValue s) Finset.univ

theorem MarshallHall.GeneralGrushko.separated_left_closure {G : Type u_1} {H : Type u_2} [Group G] [Group H] {n : ℕ} (s : Fin n → G ⊕ H) (hs : Subgroup.closure (Set.range (separatedMap ∘ s)) = ⊤) : Subgroup.closure ↑(leftGenerators s) = ⊤

theorem MarshallHall.GeneralGrushko.separated_right_closure {G : Type u_1} {H : Type u_2} [Group G] [Group H] {n : ℕ} (s : Fin n → G ⊕ H) (hs : Subgroup.closure (Set.range (separatedMap ∘ s)) = ⊤) : Subgroup.closure ↑(rightGenerators s) = ⊤

theorem MarshallHall.GeneralGrushko.rank_add_le_of_separated_generators {G : Type u_1} {H : Type u_2} [Group G] [Group H] {n : ℕ} (s : Fin n → G ⊕ H) [Group.FG G] [Group.FG H] (hs : Subgroup.closure (Set.range (separatedMap ∘ s)) = ⊤) : Group.rank G + Group.rank H ≤ n

inductive MarshallHall.GeneralGrushko.NielsenStep {A : Type u_3} [Group A] {n : ℕ} (x y : Fin n → A) : Prop

One elementary Nielsen move on a finite generating tuple. Permutations, inversion of one entry, and multiplication of one entry by a different entry all preserve the subgroup generated by the tuple.

• perm {A : Type u_3} [Group A] {n : ℕ} {x y : Fin n → A} (e : Fin n ≃ Fin n) (h : y = x ∘ ⇑e) : NielsenStep x y
• invert {A : Type u_3} [Group A] {n : ℕ} {x y : Fin n → A} (i : Fin n) (h : y = Function.update x i (x i)⁻¹) : NielsenStep x y
• mulRight {A : Type u_3} [Group A] {n : ℕ} {x y : Fin n → A} (i j : Fin n) (hij : i ≠ j) (h : y = Function.update x i (x i * x j)) : NielsenStep x y

theorem MarshallHall.GeneralGrushko.nielsenStep_closure_eq {A : Type u_3} [Group A] {n : ℕ} {x y : Fin n → A} (h : NielsenStep x y) : Subgroup.closure (Set.range x) = Subgroup.closure (Set.range y)

The subgroup generated by a tuple is unchanged by one Nielsen move.

def MarshallHall.GeneralGrushko.NielsenEquivalent {A : Type u_3} [Group A] {n : ℕ} (x y : Fin n → A) : Prop

Finite sequences of elementary Nielsen moves.

Equations

• MarshallHall.GeneralGrushko.NielsenEquivalent x y = Relation.ReflTransGen (fun (u v : Fin n → A) => MarshallHall.GeneralGrushko.NielsenStep u v) x y

theorem MarshallHall.GeneralGrushko.nielsenEquivalent_closure_eq {A : Type u_3} [Group A] {n : ℕ} {x y : Fin n → A} (h : NielsenEquivalent x y) : Subgroup.closure (Set.range x) = Subgroup.closure (Set.range y)

def MarshallHall.GeneralGrushko.HasNielsenSeparatedReduction {G : Type u_1} {H : Type u_2} [Group G] [Group H] : Prop

The generator-reduction statement in its stronger, classical form: every finite generating tuple is Nielsen-equivalent to a tuple separated between the two factors.

Equations

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

def MarshallHall.GeneralGrushko.HasSeparatedReduction {G : Type u_1} {H : Type u_2} [Group G] [Group H] : Prop

The generator-reduction statement needed for the lower bound in the general Grushko--Neumann theorem. It says that every finite generating tuple can be replaced, with the same number of entries, by a tuple whose entries lie in the two original factors. The fold/Nielsen argument is the substantive theorem still to be supplied; this definition keeps its exact interface separate from the rank bookkeeping.

Equations

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

theorem MarshallHall.GeneralGrushko.hasSeparatedReduction_of_hasNielsenSeparatedReduction {G : Type u_1} {H : Type u_2} [Group G] [Group H] (hred : HasNielsenSeparatedReduction) : HasSeparatedReduction

theorem MarshallHall.GeneralGrushko.rank_coprod_eq_add_of_separated_reduction {G : Type u_1} {H : Type u_2} [Group G] [Group H] [Group.FG G] [Group.FG H] (hred : HasSeparatedReduction) : Group.rank (Monoid.Coprod G H) = Group.rank G + Group.rank H

Once the separated-generators theorem is available, the elementary factorwise bounds assemble into full rank additivity.

theorem MarshallHall.GeneralGrushko.rank_coprod_eq_add_of_nielsen_separated_reduction {G : Type u_1} {H : Type u_2} [Group G] [Group H] [Group.FG G] [Group.FG H] (hred : HasNielsenSeparatedReduction) : Group.rank (Monoid.Coprod G H) = Group.rank G + Group.rank H

Rank additivity follows from the stronger Nielsen-equivalence form of generator reduction.

Finite indexed free products of free groups

noncomputable def MarshallHall.GeneralGrushko.coprodIFreeGroupEquiv {ι : Type u_3} (α : ι → Type u_4) : (Monoid.CoprodI fun (i : ι) => FreeGroup (α i)) ≃* FreeGroup ((i : ι) × α i)

A finite indexed free product of free groups is identified with the free group on the disjoint union of the bases. This is the finite-family version of the binary free-group calculation in MarshallHall.Grushko.

Equations

• MarshallHall.GeneralGrushko.coprodIFreeGroupEquiv α = (Monoid.CoprodI.FreeGroupBasis.coprodI fun (i : ι) => FreeGroupBasis.ofFreeGroup (α i)).repr

instance MarshallHall.GeneralGrushko.coprodI_freeGroup_fg {ι : Type u_3} [Finite ι] (α : ι → Type u_4) [∀ (i : ι), Finite (α i)] : Group.FG (Monoid.CoprodI fun (i : ι) => FreeGroup (α i))

theorem MarshallHall.GeneralGrushko.rank_coprodI_freeGroup {ι : Type u_3} [Fintype ι] (α : ι → Type u_4) [(i : ι) → Fintype (α i)] : Group.rank (Monoid.CoprodI fun (i : ι) => FreeGroup (α i)) = ∑ i : ι, Fintype.card (α i)

Grushko rank additivity for a finite indexed free product of finite-rank free groups. The arbitrary-factor theorem still requires the separate generator-reduction theorem above; this result is the fully formalized free factor subcase.

A finite-word length for the binary free product

The next step in the arbitrary-factor theorem is a reduction of a finite generating tuple. This gives the reduction argument an honest complexity measure without committing to a particular normal-form implementation. A word is a list of tagged factor elements, and its length is the least length of a word representing the given free-product element. The elementary calculus below is enough for induction on reductions: words concatenate, factor elements have length at most one, and multiplication is subadditive.

def MarshallHall.GeneralGrushko.factorWordProd {G : Type u_1} {H : Type u_2} [Group G] [Group H] : List (G ⊕ H) → Monoid.Coprod G H

Evaluation of a finite alternating-free word in the binary free product. The list is not required to be reduced; factorWordLength takes the minimum over all such representatives.

Equations

• MarshallHall.GeneralGrushko.factorWordProd [] = 1
• MarshallHall.GeneralGrushko.factorWordProd (x_1 :: xs) = MarshallHall.GeneralGrushko.separatedMap x_1 * MarshallHall.GeneralGrushko.factorWordProd xs

theorem MarshallHall.GeneralGrushko.factorWordProd_append {G : Type u_1} {H : Type u_2} [Group G] [Group H] (u v : List (G ⊕ H)) : factorWordProd (u ++ v) = factorWordProd u * factorWordProd v

theorem MarshallHall.GeneralGrushko.factorWordProd_surjective {G : Type u_1} {H : Type u_2} [Group G] [Group H] : Function.Surjective factorWordProd

def MarshallHall.GeneralGrushko.factorWordRepresented {G : Type u_1} {H : Type u_2} [Group G] [Group H] (x : Monoid.Coprod G H) (n : ℕ) : Prop

An element has a factor-word representation of the specified length.

Equations

• MarshallHall.GeneralGrushko.factorWordRepresented x n = ∃ (u : List (G ⊕ H)), u.length = n ∧ MarshallHall.GeneralGrushko.factorWordProd u = x

theorem MarshallHall.GeneralGrushko.factorWordRepresented_exists {G : Type u_1} {H : Type u_2} [Group G] [Group H] (x : Monoid.Coprod G H) : ∃ (n : ℕ), factorWordRepresented x n

noncomputable def MarshallHall.GeneralGrushko.factorWordLength {G : Type u_1} {H : Type u_2} [Group G] [Group H] (x : Monoid.Coprod G H) : ℕ

The least number of factor letters needed to represent an element.

Equations

• MarshallHall.GeneralGrushko.factorWordLength x = Nat.find ⋯

theorem MarshallHall.GeneralGrushko.factorWordLength_spec {G : Type u_1} {H : Type u_2} [Group G] [Group H] (x : Monoid.Coprod G H) : factorWordRepresented x (factorWordLength x)

theorem MarshallHall.GeneralGrushko.factorWordLength_wordProd_le {G : Type u_1} {H : Type u_2} [Group G] [Group H] (u : List (G ⊕ H)) : factorWordLength (factorWordProd u) ≤ u.length

@[simp]

theorem MarshallHall.GeneralGrushko.factorWordLength_one {G : Type u_1} {H : Type u_2} [Group G] [Group H] : factorWordLength 1 = 0

@[simp]

theorem MarshallHall.GeneralGrushko.factorWordLength_eq_zero_iff {G : Type u_1} {H : Type u_2} [Group G] [Group H] {x : Monoid.Coprod G H} : factorWordLength x = 0 ↔ x = 1

theorem MarshallHall.GeneralGrushko.factorWordLength_mul_le {G : Type u_1} {H : Type u_2} [Group G] [Group H] (x y : Monoid.Coprod G H) : factorWordLength (x * y) ≤ factorWordLength x + factorWordLength y

theorem MarshallHall.GeneralGrushko.factorWordLength_inl_le_one {G : Type u_1} {H : Type u_2} [Group G] [Group H] (g : G) : factorWordLength (Monoid.Coprod.inl g) ≤ 1

theorem MarshallHall.GeneralGrushko.factorWordLength_inr_le_one {G : Type u_1} {H : Type u_2} [Group G] [Group H] (h : H) : factorWordLength (Monoid.Coprod.inr h) ≤ 1