Profinite rigidity

AbbreviationProfinite completion#✓fully proved

The profinite completion of a group \(G\) is the inverse limit of the finite quotient groups \(G/N\), where \(N\) ranges over the normal subgroups of finite index in \(G\) and the maps are the quotient maps \(G/N \to G/M\) for \(N \le M\). It is a profinite group.

abbrev profiniteCompletion (G : Type u) [Group G] : Type u :=
  ProfiniteGrp.ProfiniteCompletion.completion (.mk G)

Used by 1

Used byProfinitely rigid group

DefinitionProfinitely rigid group#✓fully proved

A group \(\Gamma\) is profinitely rigid if it is finitely generated and residually finite, and \(\Gamma\) is isomorphic to every finitely generated residually finite group \(\Lambda\) whose profinite completion is isomorphic, as a group, to the profinite completion of \(\Gamma\).

Note that any such isomorphism of profinite completions is automatically a homeomorphism. This is a consequence of the Nikolov-Segal theorem which states that for a finitely generated group \(\Gamma\), every finite index subgroup of the profinite completion of \(\Gamma\) is automatically open. Conversely, every open subgroup has finite index by compactness, so in this case the open subgroups (which generate the topology) are exactly the subgroups of finite index. Thus, the topology on the profinite completion of \(\Gamma\) can be characterized algebraically as the topology generated by the finite index subgroups. In particular, any isomorphism between profinite completions of finitely generated groups automatically preserves the topology and is thus a homeomorphism.

def ProfinitelyRigid (Γ : Type u) [Group Γ] : Prop :=
  FG Γ ∧ ResiduallyFinite Γ ∧ ∀ (Λ : Type u) [Group Λ] [FG Λ] [ResiduallyFinite Λ],
    Nonempty (profiniteCompletion Γ ≃* profiniteCompletion Λ) → Nonempty (Γ ≃* Λ)

Uses 1 · Used by 1

Statement usesProfinite completion

Used byProfinite rigidity of the Bianchi group over the Eisenstein integers

AbbreviationRing of integers of a field obtained by adjoining a square root to \(\mathbb{Q}\)#✓fully proved

For a natural number \(d\), the ring of integers of the number field \(\mathbb{Q}(\sqrt{-d})\), realized as the splitting field of \(X^2 + d\) over \(\mathbb{Q}\).

abbrev RingOfIntegers (d : ℕ) := NumberField.RingOfIntegers (SplittingField (X ^ 2 + C (d : ℚ)))

Used by 2

Used byBianchi group · Profinite rigidity of the Bianchi group over the Eisenstein integers

AbbreviationBianchi group#✓fully proved

For a natural number \(d\), let \(\mathcal{O}_d\) be the ring of integers of \(\mathbb{Q}(\sqrt{-d})\). The Bianchi group is \(\mathrm{PSL}(2, \mathcal{O}_d)\), the projective special linear group of \(2 \times 2\) matrices over \(\mathcal{O}_d\).

abbrev BianchiGroup (d : ℕ) := Matrix.ProjectiveSpecialLinearGroup (Fin 2) (RingOfIntegers d)

Uses 1 · Used by 1

Statement usesRing of integers of a field obtained by adjoining a square root to \(\mathbb{Q}\)

Used byProfinite rigidity of the Bianchi group over the Eisenstein integers

TheoremProfinite rigidity of the Bianchi group over the Eisenstein integers#●ready to prove

Let \(\omega\) be a primitive cube root of unity, so that the ring \(\mathbb{Z}[\omega]\) of Eisenstein integers is the ring of integers of \(\mathbb{Q}(\sqrt{-3})\). The Bianchi group \(\mathrm{PSL}(2, \mathbb{Z}[\omega])\) is profinitely rigid: it is finitely generated and residually finite, and it is isomorphic to every finitely generated residually finite group whose profinite completion is isomorphic, as a group, to its own.

This is Theorem 7.1 of the source.

public theorem_wanted theorem_7_1 : ProfinitelyRigid (BianchiGroup 3)

Sources

• M. R. Bridson, D. B. McReynolds, A. W. Reid, and R. Spitler, Absolute profinite rigidity and hyperbolic geometry, Annals of Math, 192 (3) 2020. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_absolute_profinite_rigidity of the lean-eval benchmark.

Uses 3

Statement usesBianchi group · Profinitely rigid group · Ring of integers of a field obtained by adjoining a square root to \(\mathbb{Q}\)

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.