Finite-index subgroups of automorphism groups of free groups
DefinitionFirst Betti number of a group#✓fully proved
The first Betti number of a group \(G\) is the rank, as a cardinal, of its abelianization \(G^{\mathrm{ab}}\) viewed as a \(\mathbb{Z}\)-module.
noncomputable def firstBettiRank (G : Type*) [Group G] : Cardinal :=
Module.rank ℤ (Additive (Abelianization G))
Sources
- [AMR-109-0273] (Question 2.5, PDF p. 330).
DefinitionFarb's positive first Betti number question for \(\mathrm{Aut}(F_n)\)#✓fully proved
The proposition that for every natural number \(n > 3\), the automorphism group \(\mathrm{Aut}(F_n)\) of the free group \(F_n\) on \(n\) generators has a finite-index subgroup \(H\) whose first Betti number, the \(\mathbb{Z}\)-rank of the abelianization of \(H\), is positive.
def conjecture : Prop :=
∀ (n : ℕ), 3 < n →
∃ (H : Subgroup (MulAut (FreeGroup (Fin n)))),
H.FiniteIndex ∧ 0 < firstBettiRank ↥H
noncomputable def firstBettiRank (G : Type*) [Group G] : Cardinal :=
Module.rank ℤ (Additive (Abelianization G))
WantedExt/Topology/AutFnFiniteIndexPositiveBettiWanted.lean:54
Sources
- Farb Question 2.5 [AMR-109-0273] (PDF p. 330).
Uses 1 · Used by 1
TheoremSome \(\mathrm{Aut}(F_n)\) with \(n > 3\) has no finite-index subgroup of positive first Betti number#●ready to prove
Some \(\mathrm{Aut}(F_n)\) with \(n > 3\) has no finite-index subgroup of positive first Betti number. It is not the case that for every natural number \(n > 3\) the automorphism group \(\mathrm{Aut}(F_n)\) of the free group \(F_n\) on \(n\) generators has a finite-index subgroup \(H\) whose first Betti number, the \(\mathbb{Z}\)-rank of the abelianization of \(H\), is positive.
The case \(n = 5\) fails: Kaluba, Nowak and Ozawa proved that \(\mathrm{Aut}(F_5)\) has Kazhdan's property (T), which passes to finite-index subgroups and forces finite abelianization, so every finite-index subgroup of \(\mathrm{Aut}(F_5)\) has first Betti number \(0\).
public theorem_wanted conjecture_refuted : ¬ conjecture
def conjecture : Prop :=
∀ (n : ℕ), 3 < n →
∃ (H : Subgroup (MulAut (FreeGroup (Fin n)))),
H.FiniteIndex ∧ 0 < firstBettiRank ↥H
WantedExt/Topology/AutFnFiniteIndexPositiveBettiWanted.lean:60
Sources
- M. Kaluba, P. W. Nowak, N. Ozawa, Aut(F5) has property (T), Math. Ann. 375 (2019), no. 3-4, 1169-1191, https://arxiv.org/abs/1712.07167.
Uses 1
DefinitionSerre's Property FA#✓fully proved
A group \(G\) has Property FA when every action of \(G\) on a tree without edge inversion has a global fixed vertex: for every tree \(T\) with vertex set \(V\) and every homomorphism \(\alpha\) from \(G\) to the group of permutations of \(V\) such that each \(\alpha(g)\) satisfies \(\alpha(g)(u) \sim \alpha(g)(v) \iff u \sim v\) for all vertices \(u, v\) (where \(\sim\) is adjacency in \(T\)), and such that no \(\alpha(g)\) swaps the two ends of an edge, there is a vertex \(v\) with \(\alpha(g)(v) = v\) for all \(g \in G\).
def HasPropertyFA (G : Type u) [Group G] : Prop :=
∀ (V : Type u) (T : SimpleGraph V), T.IsTree →
∀ (α : G →* Equiv.Perm V),
(∀ g : G, ∀ u v : V, T.Adj (⇑(α g) u) (⇑(α g) v) ↔ T.Adj u v) →
(∀ g : G, ∀ u v : V, T.Adj u v → ⇑(α g) u = v → ⇑(α g) v ≠ u) →
∃ v : V, ∀ g : G, ⇑(α g) v = v
Sources
- [AMR-109-0276] (Question 2.8, PDF p. 331).
DefinitionFarb's question on Property FA for finite-index subgroups of \(\operatorname{Aut}(F_n)\)#✓fully proved
The proposition that for every natural number \(n \ge 4\), every subgroup of finite index in the automorphism group \(\operatorname{Aut}(F_n)\) of the free group \(F_n\) on \(n\) generators has Serre's Property FA.
def conjecture : Prop :=
∀ n : ℕ, 4 ≤ n →
∀ H : Subgroup (MulAut (FreeGroup (Fin n))),
H.FiniteIndex → HasPropertyFA ↥H
def HasPropertyFA (G : Type u) [Group G] : Prop :=
∀ (V : Type u) (T : SimpleGraph V), T.IsTree →
∀ (α : G →* Equiv.Perm V),
(∀ g : G, ∀ u v : V, T.Adj (⇑(α g) u) (⇑(α g) v) ↔ T.Adj u v) →
(∀ g : G, ∀ u v : V, T.Adj u v → ⇑(α g) u = v → ⇑(α g) v ≠ u) →
∃ v : V, ∀ g : G, ⇑(α g) v = v
WantedExt/Topology/AutFnFiniteIndexPropertyFAWanted.lean:54
Sources
- Farb Question 2.8 [AMR-109-0276] (PDF p. 331).
Uses 1 · Used by 1
TheoremFinite-index subgroups of \(\operatorname{Aut}(F_n)\) have Property FA for \(n \ge 4\)#●ready to prove
For every natural number \(n \ge 4\), every subgroup of finite index in the automorphism group \(\operatorname{Aut}(F_n)\) of the free group \(F_n\) on \(n\) generators has Serre's Property FA.
This answers Farb's Question 2.8 positively: \(\operatorname{Aut}(F_n)\) has Kazhdan's property (T) for \(n \ge 4\) (Kaluba–Kielak–Nowak for \(n \ge 6\), Kaluba–Nowak–Ozawa for \(n = 5\), Nitsche for \(n = 4\)), property (T) passes to finite-index subgroups, and it implies Serre's Property FA (Watatani).
public theorem_wanted conjecture_holds : conjecture
def conjecture : Prop :=
∀ n : ℕ, 4 ≤ n →
∀ H : Subgroup (MulAut (FreeGroup (Fin n))),
H.FiniteIndex → HasPropertyFA ↥H
WantedExt/Topology/AutFnFiniteIndexPropertyFAWanted.lean:63
Sources
- Marek Kaluba, Dawid Kielak and Piotr W. Nowak, On property (T) for Aut(F_n) and SL_n(Z), Ann. of Math. 193 (2021), arXiv:1812.03456, https://arxiv.org/abs/1812.03456; Martin Nitsche, Computer proofs for Property (T), and SDP duality, arXiv:2009.05134v3 (2022), https://arxiv.org/abs/2009.05134.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.