Inert and compressed subgroups of free groups

DefinitionRank of a subgroup#✓fully proved

For a subgroup \(H\) of a group \(G\), the rank \(r(H) \in \mathbb{N} \cup \{\infty\}\) is the least size of a finite subset of \(G\) that generates \(H\), with \(r(H) = \infty\) when \(H\) is not finitely generated.

noncomputable def subgroupRank {G : Type} [Group G] (H : Subgroup G) : ℕ∞ :=
  ⨅ (s : Finset G) (_ : Subgroup.closure (s : Set G) = H), (s.card : ℕ∞)

Used by 2

Used byCompressed subgroup of a free group of finite rank · Inert subgroup of a free group of finite rank

DefinitionInert subgroup of a free group of finite rank#✓fully proved

Let \(F_n\) be the free group on \(n\) generators and \(r(K) \in \mathbb{N} \cup \{\infty\}\) the rank of a subgroup \(K\). A subgroup \(H\) of \(F_n\) is inert when \(r(H \cap K) \le r(K)\) for every subgroup \(K\) of \(F_n\).

def IsInert {n : ℕ} (H : Subgroup (FreeGroup (Fin n))) : Prop :=
  ∀ K : Subgroup (FreeGroup (Fin n)), subgroupRank (H ⊓ K) ≤ subgroupRank K

Uses 1 · Used by 1

Statement usesRank of a subgroup

Used byVentura's compressed-implies-inert problem in finite rank (Kourovka 19.102)

DefinitionCompressed subgroup of a free group of finite rank#✓fully proved

Let \(F_n\) be the free group on \(n\) generators and \(r(K) \in \mathbb{N} \cup \{\infty\}\) the rank of a subgroup \(K\). A subgroup \(H\) of \(F_n\) is compressed when \(r(H) \le r(K)\) for every subgroup \(K\) of \(F_n\) containing \(H\).

def IsCompressed {n : ℕ} (H : Subgroup (FreeGroup (Fin n))) : Prop :=
  ∀ K : Subgroup (FreeGroup (Fin n)), H ≤ K → subgroupRank H ≤ subgroupRank K

Uses 1 · Used by 1

Statement usesRank of a subgroup

Used byVentura's compressed-implies-inert problem in finite rank (Kourovka 19.102)

DefinitionVentura's compressed-implies-inert problem in finite rank (Kourovka 19.102)#✓fully proved

The proposition that for every \(n \in \mathbb{N}\), every compressed subgroup of the free group \(F_n\) on \(n\) generators is inert.

def compressedSubgroupsInert : Prop :=
  ∀ (n : ℕ) (H : Subgroup (FreeGroup (Fin n))), IsCompressed H → IsInert H

Uses 2 · Used by 1

Statement usesCompressed subgroup of a free group of finite rank · Inert subgroup of a free group of finite rank

Used byCompressed subgroups of free groups of finite rank are inert (Kourovka 19.102)

TheoremCompressed subgroups of free groups of finite rank are inert (Kourovka 19.102)#●ready to prove

For every \(n \in \mathbb{N}\), every compressed subgroup \(H\) of the free group \(F_n\) on \(n\) generators is inert.

The Kourovka Notebook (21st issue) answers 19.102 "Yes, it is true" (A. Jaikin-Zapirain, 2024), whose Corollary 1.2 proves that compressed and inert are equivalent for finitely generated subgroups of a free group.

public theorem_wanted compressedSubgroupsInert_holds : compressedSubgroupsInert

Sources

• E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 19.102 (E. Ventura); resolution: A. Jaikin-Zapirain, Free groups are L^2-subgroup rigid, preprint, arXiv:2403.09515 (2024), abstract and Corollary 1.2: for a finitely generated subgroup H of a free group F, H is compressed iff H is inert iff H is L²-independent, answering the question of Dicks and Ventura (Kourovka 19.102); the Kourovka Notebook (21st issue) marks 19.102 solved, https://arxiv.org/abs/2403.09515.

Uses 1

Statement usesVentura's compressed-implies-inert problem in finite rank (Kourovka 19.102)

DefinitionRank of a subgroup (Kourovka 19.103)#✓fully proved

For a subgroup \(H\) of a group \(G\), the rank \(r(H) \in \mathbb{N} \cup \{\infty\}\) is the least number of elements of a finite subset of \(G\) that generates \(H\), with \(r(H) = \infty\) when \(H\) is not finitely generated.

noncomputable def subgroupRank {G : Type} [Group G] (H : Subgroup G) : ℕ∞ :=
  ⨅ (s : Finset G) (_ : Subgroup.closure (s : Set G) = H), (s.card : ℕ∞)

Used by 1

Used byCompressed subgroup of a free group (Kourovka 19.103)

DefinitionCompressed subgroup of a free group (Kourovka 19.103)#✓fully proved

A subgroup \(H\) of the free group \(F_n\) on \(n\) generators is compressed when \(r(H) \le r(K)\) for every subgroup \(K\) of \(F_n\) that contains \(H\), where \(r\) denotes the rank of a subgroup.

def IsCompressed {n : ℕ} (H : Subgroup (FreeGroup (Fin n))) : Prop :=
  ∀ K : Subgroup (FreeGroup (Fin n)), H ≤ K → subgroupRank H ≤ subgroupRank K

Uses 1 · Used by 1

Statement usesRank of a subgroup (Kourovka 19.103)

Used byKourovka Problem 19.103 for two compressed subgroups

DefinitionKourovka Problem 19.103 for two compressed subgroups#✓fully proved

The statement that for every natural number \(n\) and all subgroups \(H\) and \(K\) of the free group \(F_n\) on \(n\) generators, if \(H\) and \(K\) are compressed, then \(H \cap K\) is compressed.

def intersectionOfCompressedCompressed : Prop :=
  ∀ (n : ℕ) (H K : Subgroup (FreeGroup (Fin n))), IsCompressed H → IsCompressed K →
    IsCompressed (H ⊓ K)

Uses 1 · Used by 1

Statement usesCompressed subgroup of a free group (Kourovka 19.103)

Used byThe intersection of two compressed subgroups of a finite-rank free group is compressed

TheoremThe intersection of two compressed subgroups of a finite-rank free group is compressed#●ready to prove

For every natural number \(n\) and all subgroups \(H\) and \(K\) of the free group \(F_n\) on \(n\) generators, if \(H\) and \(K\) are compressed, then \(H \cap K\) is compressed. That is, Kourovka Problem 19.103 has a positive answer for the intersection of two subgroups of a free group of finite rank.

public theorem_wanted intersectionOfCompressedCompressed_holds : intersectionOfCompressedCompressed

Sources

• E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 19.103 (E. Ventura); resolution: A. Jaikin-Zapirain, Free groups are L^2-subgroup rigid, preprint, arXiv:2403.09515 (2024), Corollary 1.3(1) (citing Kourovka 19.103): the intersection of two compressed subgroups of a free group is again compressed, from Corollary 1.2 (compressed iff inert for finitely generated subgroups); the Kourovka Notebook (21st issue) marks 19.103 solved, https://arxiv.org/abs/2403.09515.

Uses 1

Statement usesKourovka Problem 19.103 for two compressed subgroups

DefinitionRank of a subgroup#✓fully proved

For a subgroup \(H\) of a group \(G\), the rank \(r(H)\) is the least size of a finite subset of \(G\) that generates \(H\), or \(\infty\) if \(H\) is not finitely generated.

noncomputable def subgroupRank {G : Type} [Group G] (H : Subgroup G) : ℕ∞ :=
  ⨅ (s : Finset G) (_ : Subgroup.closure (s : Set G) = H), (s.card : ℕ∞)

Used by 1

Used byInert subgroups of a free group

DefinitionInert subgroups of a free group#✓fully proved

Let \(F_n\) be the free group on \(n\) generators and let \(r(K)\) denote the rank of a subgroup \(K\). A subgroup \(H \le F_n\) is inert if \(r(H \cap K) \le r(K)\) for every subgroup \(K \le F_n\).

def IsInert {n : ℕ} (H : Subgroup (FreeGroup (Fin n))) : Prop :=
  ∀ K : Subgroup (FreeGroup (Fin n)), subgroupRank (H ⊓ K) ≤ subgroupRank K

Uses 1 · Used by 1

Statement usesRank of a subgroup

Used byKourovka Problem 19.105 (Ventura) for free groups of finite rank

DefinitionKourovka Problem 19.105 (Ventura) for free groups of finite rank#✓fully proved

The statement that for every \(n \in \mathbb{N}\) and every endomorphism \(\varphi\) of the free group \(F_n\) on \(n\) generators, the fixed subgroup \(\{x \in F_n \mid \varphi(x) = x\}\) of \(\varphi\) is inert in \(F_n\).

def endomorphismFixedSubgroupInert : Prop :=
  ∀ (n : ℕ) (φ : FreeGroup (Fin n) →* FreeGroup (Fin n)),
    IsInert (MonoidHom.eqLocus φ (MonoidHom.id _))

Uses 1 · Used by 1

Statement usesInert subgroups of a free group

Used byFixed subgroups of endomorphisms of free groups are inert

TheoremFixed subgroups of endomorphisms of free groups are inert#●ready to prove

Let \(n \in \mathbb{N}\), let \(F_n\) be the free group on \(n\) generators, and for a subgroup \(H \le F_n\) let \(r(H)\) be its rank, the least size of a finite generating set of \(H\), or \(\infty\) if \(H\) is not finitely generated. For every endomorphism \(\varphi\) of \(F_n\), the fixed subgroup \(\{x \in F_n \mid \varphi(x) = x\}\) of \(\varphi\) is inert in \(F_n\): its intersection with every subgroup \(K \le F_n\) has rank at most \(r(K)\). This answers Kourovka Problem 19.105 (E. Ventura) in the affirmative.

The Kourovka Notebook (21st issue) answers 19.105 "Yes, it is true", citing A. Jaikin-Zapirain (2024), whose Corollary 1.2 proves that compressed and inert are equivalent for finitely generated subgroups of a free group.

public theorem_wanted endomorphismFixedSubgroupInert_holds : endomorphismFixedSubgroupInert

Sources

• E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 19.105 (E. Ventura); resolution: A. Jaikin-Zapirain, Free groups are L^2-subgroup rigid, preprint, arXiv:2403.09515 (2024), Corollary 1.2: for a finitely generated subgroup of a free group, compressed iff inert; the Kourovka Notebook (21st issue) answers 19.105 "Yes, it is true" citing this preprint, https://arxiv.org/abs/2403.09515.

Uses 1

Statement usesKourovka Problem 19.105 (Ventura) for free groups of finite rank

DefinitionRank of a subgroup, possibly infinite#✓fully proved

For a subgroup \(H\) of a group \(G\), the rank \(r(H) \in \mathbb{N} \cup \{\infty\}\) is the least size of a finite subset of \(G\) that generates \(H\), and \(r(H) = \infty\) if \(H\) is not finitely generated.

noncomputable def subgroupRank {G : Type} [Group G] (H : Subgroup G) : ℕ∞ :=
  ⨅ (s : Finset G) (_ : Subgroup.closure (s : Set G) = H), (s.card : ℕ∞)

Used by 1

Used byInert subgroup of a free group of finite rank

DefinitionInert subgroup of a free group of finite rank#✓fully proved

A subgroup \(H\) of the free group \(F_n\) on \(n\) generators is inert if \(r(H \cap K) \le r(K)\) for every subgroup \(K\) of \(F_n\), where the rank \(r(L)\) of a subgroup \(L\) is the least size of a finite generating set of \(L\), and \(\infty\) when \(L\) is not finitely generated.

def IsInert {n : ℕ} (H : Subgroup (FreeGroup (Fin n))) : Prop :=
  ∀ K : Subgroup (FreeGroup (Fin n)), subgroupRank (H ⊓ K) ≤ subgroupRank K

Uses 1 · Used by 1

Statement usesRank of a subgroup, possibly infinite

Used byKourovka Problem 19.104 (statement): deciding inertness

DefinitionSubgroup of a free group generated by a list of words#✓fully proved

Let \(F_n\) be the free group on generators \(x_0, \dots, x_{n-1}\). A word is a finite list of letters \((i, b)\) with \(i < n\) and \(b\) a boolean, where \((i, \mathrm{true})\) stands for \(x_i\) and \((i, \mathrm{false})\) for \(x_i^{-1}\). Given a finite list of words, this is the subgroup of \(F_n\) generated by the elements of \(F_n\) that the words represent, each word representing the product of its letters.

def generatedBy {n : ℕ} (ws : List (List (Fin n × Bool))) : Subgroup (FreeGroup (Fin n)) :=
  Subgroup.closure {x | ∃ w ∈ ws, x = FreeGroup.mk w}

Used by 1

Used byKourovka Problem 19.104 (statement): deciding inertness

DefinitionKourovka Problem 19.104 (statement): deciding inertness#✓fully proved

The statement that for every natural number \(n\) there is an algorithm deciding, for a finite list of words in the generators \(x_0, \dots, x_{n-1}\) of the free group \(F_n\) and their inverses, whether the subgroup of \(F_n\) they generate is inert; that is, the predicate on lists of words is computable.

def inertSubgroupDecidable : Prop :=
  ∀ n : ℕ, ComputablePred fun ws : List (List (Fin n × Bool)) => IsInert (generatedBy ws)

Uses 2 · Used by 1

Statement usesInert subgroup of a free group of finite rank · Subgroup of a free group generated by a list of words

Used byInertness is decidable in free groups of finite rank (Kourovka Problem 19.104)

TheoremInertness is decidable in free groups of finite rank (Kourovka Problem 19.104)#●ready to prove

For every natural number \(n\), let \(F_n\) be the free group on generators \(x_0, \dots, x_{n-1}\), and give a finitely generated subgroup of \(F_n\) by a finite list of generating words in the letters \(x_i^{\pm 1}\). Then there is an algorithm deciding, for such a list, whether the subgroup \(H\) it generates is inert, that is, whether \(r(H \cap K) \le r(K)\) for every subgroup \(K\) of \(F_n\). Here the rank \(r(L)\) of a subgroup \(L\) is the least size of a finite generating set of \(L\), and \(r(L) = \infty\) when \(L\) is not finitely generated; "an algorithm" means that the predicate on lists of words is computable.

Jaikin-Zapirain proved that a finitely generated subgroup of a free group is inert if and only if it is compressed, and compressedness is known to be decidable.

public theorem_wanted inertSubgroupDecidable_holds : inertSubgroupDecidable

Sources

• E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 19.104 (E. Ventura); resolution: A. Jaikin-Zapirain, Free groups are L^2-subgroup rigid, preprint, arXiv:2403.09515 (2024), Corollary 1.3(2) (citing Kourovka 19.104): it is algorithmically decidable, for a finitely generated subgroup of a free group, whether it is inert (compressedness is decidable and equivalent to inertness by Corollary 1.2); the Kourovka Notebook (21st issue) marks 19.104 solved, https://arxiv.org/abs/2403.09515.

Uses 1

Statement usesKourovka Problem 19.104 (statement): deciding inertness

14 fully proved4 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.