Varieties, quasivarieties and equations
Groups defined by laws and quasi-identities: varieties, relatively free groups, test ranks, quasivarieties and their lattices, Hall's verbal conjectures, plus equations over groups, equationally Noetherian groups, geometric equivalence and elementary theories of groups.
- Automorphisms of categories of relatively free groups
- Axiomatizable classes of groups
- Elementary theory of torsion-free hyperbolic groups
- Equationally Noetherian groups
- Equations over free groups
- Geometric equivalence of groups
- Hall's verbal conjectures
- Lattices of quasivarieties
- Presentations in the torsion-free quasivariety
- Quasivarieties of groups
- Independent bases of laws
- Test ranks of relatively free groups
- Torsion groups of unbounded exponent in proper varieties
DefinitionLocally finite variety#✓fully proved
MathlibExt.GroupTheory.GroupVarietyShared.IsLocallyFiniteVariety
Let \(F\) be the free group on countably many generators \(x_0, x_1, x_2, \dots\) and let \(N\) be a subgroup of \(F\), regarded as a set of laws. The variety defined by \(N\) is locally finite if every finitely generated group satisfying all laws in \(N\) is finite.
def IsLocallyFiniteVariety (N : Subgroup (FreeGroup ℕ)) : Prop :=
∀ (G : Type) [Group G], SatisfiesLaws (N : Set (FreeGroup ℕ)) G → Group.FG G → Finite Gdef SatisfiesLaws (W : Set (FreeGroup ℕ)) (G : Type) [Group G] : Prop :=
∀ w ∈ W, ∀ f : FreeGroup ℕ →* G, f w = 1WantedExt/GroupTheory/FormationVarietyPGroupsKourovka11Problem21Wanted.lean:58
Uses 1
Statement usesGroups satisfying a set of laws
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.