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).
Used by 1

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
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
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).
Used by 1

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
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
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.
Uses 1
4 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.