Revision #2953 → #3448 · back to history
modifiedGeometric group theory797ca6d202a9
| Field | From #2953 | To #3448 |
|---|
| note | The field itself is not formalized, but its central object—finitely generated groups—is captured by the `Group.FG` typeclass. | The field itself is not formalized, but its central object—finitely generated groups—is captured by the `Group.FG` typeclass (verified). |
modifiedCayley graph and word metric9cbd480ce7f3
| Field | From #2953 | To #3448 |
|---|
| note | `SimpleGraph.mulCayley s` defines the Cayley graph from a generating set, though the word metric is not separately packaged. | `SimpleGraph.mulCayley s` (verified) defines the Cayley graph from a generating set; the word metric is not separately packaged. |
modifiedGroup presentation2846f9441d80
| Field | From #2953 | To #3448 |
|---|
| note | `PresentedGroup rels` constructs the group with the given generators and relations as a quotient of the free group. | `PresentedGroup rels` (verified) constructs the group with the given generators and relations as a quotient of the free group. |
modifiedHyperbolic groupa9cb61ae7102
| Field | From #2953 | To #3448 |
|---|
| note | Mathlib's only 'hyperbolic' references are to hyperbolic functions/geometry and `Matrix.IsHyperbolic`, not Gromov-hyperbolic groups. | Mathlib's only 'hyperbolic' references are to hyperbolic functions/geometry and `Matrix.GeneralLinearGroup.IsHyperbolic`, not Gromov-hyperbolic groups. |
modifiedBass–Serre theory5519795f7242
| Field | From #2953 | To #3448 |
|---|
| note | The Bass–Serre building blocks—amalgamated free products (`Monoid.PushoutI`) and HNN extensions (`HNNExtension`)—are formalized, but the full graph-of-groups/tree-action framework is not. | The Bass–Serre building blocks—amalgamated free products (`Monoid.PushoutI`, verified) and HNN extensions (`HNNExtension`, verified)—are formalized, but the full graph-of-groups/tree-action framework is not. |
modifiedAmenable groups53e3668e776c
| Field | From #2953 | To #3448 |
|---|
| note | Mathlib has the Følner-filter amenability theorem (`IsFoelner.amenable`) but no standalone `Amenable` group typeclass. | Mathlib has the Følner-filter amenability theorem (`IsFoelner.amenable`, verified) but no standalone `Amenable` group typeclass. |
modifiedInfinite cyclic group Zc2ccd70ca542
| Field | From #2953 | To #3448 |
|---|
| note | The infinite cyclic group is exactly ℤ, whose additive group structure is `Int.instAddCommGroup`. | The infinite cyclic group is exactly ℤ, whose additive group structure `Int.instAddCommGroup` is verified in Mathlib. |
modifiedFree groups960d5ebcf528
| Field | From #2953 | To #3448 |
|---|
| note | `FreeGroup α` is the free group on a generating type α. | `FreeGroup α` (verified) is the free group on a generating type α. |
modifiedFree productsec8063f3611f
| Field | From #2953 | To #3448 |
|---|
| note | `Monoid.CoprodI` is the free product (coproduct) of a family of groups. | `Monoid.CoprodI` (verified) is the free product (coproduct) of a family of groups. |
modifiedSymmetric groups344da8d8a6ea
| Field | From #2953 | To #3448 |
|---|
| note | `Equiv.Perm α` is the symmetric group of permutations of α. | `Equiv.Perm α` (verified) is the symmetric group of permutations of α. |
modifiedCoxeter groupseb46761186f6
| Field | From #2953 | To #3448 |
|---|
| note | `CoxeterSystem` and the `IsCoxeterGroup` class formalize Coxeter groups. | `CoxeterSystem` (verified) together with `IsCoxeterGroup` (verified) formalize Coxeter groups. |
modifiedBaumslag–Solitar groupsf3939a5a2244
| Field | From #2953 | To #3448 |
|---|
| note | Baumslag–Solitar groups are HNN extensions of ℤ; Mathlib has the general `HNNExtension` construction but not these specific groups. | Baumslag–Solitar groups are HNN extensions of ℤ; Mathlib has the general `HNNExtension` construction (verified) but not these specific groups. |
modifiedFundamental groups of graphs of groups2483e92e4704
| Field | From #2953 | To #3448 |
|---|
| note | The Bass–Serre building blocks—amalgamated products (`Monoid.PushoutI`) and HNN extensions—exist, but graph-of-groups fundamental groups are not formalized. | The Bass–Serre building blocks—amalgamated products (`Monoid.PushoutI`, verified) and HNN extensions—exist, but graph-of-groups fundamental groups are not formalized. |
modifiedBurnside problem226d7c07edc2
| Field | From #2953 | To #3448 |
|---|
| note | The Burnside problem on periodic finitely generated groups is not formalized in Mathlib. | The Burnside problem on periodic finitely generated groups is not formalized in Mathlib (only the group exponent machinery `Monoid.exponent` exists). |
addedFinitely presented group2de41d05f256
addedCannon's conjecture9a8234f83da0
addedPoisson boundarycf8315c1e46d
addedGroup actions on R-trees (Rips machine)255bc2f3583d
addedSubgroup growth69b5f84ed818