Free groups, equations over groups, and limit groups

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremConjugacy criterion in free groups#

Two elements of a free group are conjugate exactly when the cyclic reductions of their reduced words are cyclic rotations of each other.

FreeGroup.isConj_iff_isRotated_reduceCyclically.{u_1} {α : Type u_1} [DecidableEq α]
  {x y : FreeGroup α} :
  IsConj x y ↔ FreeGroup.reduceCyclically x.toWord ~r FreeGroup.reduceCyclically y.toWord
Lean

Formalized in Tau Ceti as FreeGroup.isConj_iff_isRotated_reduceCyclically.

Sources
LeanFreeGroup.isConj_iff_isRotated_reduceCyclically

TheoremFree groups are CSA#

every maximal abelian subgroup of a free group is malnormal.

IsFreeGroup.isCSA.{u_1} {G : Type u_1} [Group G] [IsFreeGroup G] : Group.IsCSA G
Lean

Formalized in Tau Ceti as IsFreeGroup.isCSA.

Sources
LeanIsFreeGroup.isCSA
Uses 1 · Used by 1
Proof usesIsFreeGroup.maximal_isMulCommutative_iff
Used byNonabelian free groups are domains (Baumslag–Myasnikov–Remeslennikov, Corollary 1)

TheoremIsFreeGroup.maximal_isMulCommutative_iff#

The maximal abelian subgroups of a nontrivial free group are exactly the cyclic subgroups generated by elements that are not proper powers.

IsFreeGroup.maximal_isMulCommutative_iff.{u_1} {G : Type u_1} [Group G] [IsFreeGroup G]
  [Nontrivial G] {M : Subgroup G} :
  Maximal (fun K => IsMulCommutative ↥K) M ↔ ∃ u, ¬Group.IsProperPower u ∧ M = Subgroup.zpowers u
Lean

Formalized in Tau Ceti as IsFreeGroup.maximal_isMulCommutative_iff.

Sources
LeanIsFreeGroup.maximal_isMulCommutative_iff
Used by 1
Used byFree groups are CSA

TheoremNonabelian free groups are domains (Baumslag–Myasnikov–Remeslennikov, Corollary 1)# 

IsFreeGroup.isGDomain_id.{u_1} {F : Type u_1} [Group F] [IsFreeGroup F] (hF : ¬IsMulCommutative F) :
  TauCeti.GroupAlgGeom.IsGDomain (MonoidHom.id F)
Lean

Formalized in Tau Ceti as IsFreeGroup.isGDomain_id.

Sources
LeanIsFreeGroup.isGDomain_id
Uses 2
Proof usesCSA groups are domains (Baumslag–Myasnikov–Remeslennikov, Proposition 1) · Free groups are CSA

TheoremCSA groups are domains (Baumslag–Myasnikov–Remeslennikov, Proposition 1)#

A CSA group in which the images of two coefficients do not commute is a domain over these coefficients.

TauCeti.GroupAlgGeom.IsGDomain.of_isCSA.{u_1, u_3} {G : Type u_1} {H : Type u_3} [Group G] [Group H]
  {ι : G →* H} (hH : Group.IsCSA H) {a b : G} (hab : ¬Commute (ι a) (ι b)) :
  TauCeti.GroupAlgGeom.IsGDomain ι
Lean

Formalized in Tau Ceti as TauCeti.GroupAlgGeom.IsGDomain.of_isCSA.

Sources
LeanTauCeti.GroupAlgGeom.IsGDomain.of_isCSA
Used by 1
Used byNonabelian free groups are domains (Baumslag–Myasnikov–Remeslennikov, Corollary 1)

TheoremSanov's theorem#

The matrices [[1, 2], [0, 1]] and [[1, 0], [2, 1]] freely generate a free subgroup of rank two of SL(2, ℤ). This is the case R = ℤ, c = d = 2 of injective_freeGroup_lift_transvection_of_two_le_abs.

TauCeti.injective_freeGroup_lift_transvection_two :
  Function.Injective
    ⇑(FreeGroup.lift
        ![Matrix.SpecialLinearGroup.transvection ⋯ 2, Matrix.SpecialLinearGroup.transvection ⋯ 2])
Lean

Formalized in Tau Ceti as TauCeti.injective_freeGroup_lift_transvection_two.

Other forms

Sanov's theorem. Formalized in Tau Ceti as TauCeti.injective_freeGroup_lift_transvection_of_two_le_abs.

TauCeti.injective_freeGroup_lift_transvection_of_two_le_abs.{u_1} {R : Type u_1} [CommRing R]
  [LinearOrder R] [IsStrictOrderedRing R] {c d : R} (hc : 2 ≤ |c|) (hd : 2 ≤ |d|) :
  Function.Injective
    ⇑(FreeGroup.lift
        ![Matrix.SpecialLinearGroup.transvection ⋯ c, Matrix.SpecialLinearGroup.transvection ⋯ d])
Sources
LeanTauCeti.injective_freeGroup_lift_transvection_two · TauCeti.injective_freeGroup_lift_transvection_of_two_le_abs

TheoremFree groups of countable rank are linear over ℤ#

Every free group on a countable basis embeds in SL(2, ℤ).

TauCeti.exists_injective_freeGroup_SL.{u_2} (ι : Type u_2) [Countable ι] :
  ∃ f, Function.Injective ⇑f
Lean

Formalized in Tau Ceti as TauCeti.exists_injective_freeGroup_SL.

Sources
LeanTauCeti.exists_injective_freeGroup_SL

TheoremLinear groups are equationally Noetherian#

Over a commutative Noetherian ring R, the general linear group GL n R is equationally Noetherian over any coefficients: every system of equations in finitely many variables has a finite subsystem with the same solutions in GL n R.

TauCeti.GroupAlgGeom.isEquationallyNoetherian_generalLinearGroup.{u_1, u_4, u_5} {G : Type u_1}
  [Group G] {R : Type u_4} {n : Type u_5} [CommRing R] [IsNoetherianRing R] [Fintype n]
  [DecidableEq n] (ι : G →* GL n R) : TauCeti.GroupAlgGeom.IsEquationallyNoetherian ι
Lean

Formalized in Tau Ceti as TauCeti.GroupAlgGeom.isEquationallyNoetherian_generalLinearGroup.

Sources
LeanTauCeti.GroupAlgGeom.isEquationallyNoetherian_generalLinearGroup

AbbreviationTauCeti.GroupAlgGeom.CoordGroup#

The coordinate group G_{R(S)} = G[X] ⧸ Rad_H(S) of a system S over H.

TauCeti.GroupAlgGeom.CoordGroup.{u_1, u_2, u_3} {G : Type u_1} {H : Type u_2} {X : Type u_3}
  [Group G] [Group H] (ι : G →* H) (S : Set (TauCeti.GroupAlgGeom.GX G X)) : Type (max u_3 u_1)
Lean

Formalized in Tau Ceti as TauCeti.GroupAlgGeom.CoordGroup.

Sources
LeanTauCeti.GroupAlgGeom.CoordGroup

DefinitionTauCeti.GroupAlgGeom.zariskiTopology#

The Zariski topology generated by the complements of algebraic sets over G.

TauCeti.GroupAlgGeom.zariskiTopology.{u_1, u_2, u_3} {G : Type u_1} {H : Type u_2} [Group G]
  [Group H] (ι : G →* H) (X : Type u_3) : TopologicalSpace (X → H)
Lean

Formalized in Tau Ceti as TauCeti.GroupAlgGeom.zariskiTopology.

Sources
LeanTauCeti.GroupAlgGeom.zariskiTopology

DefinitionGroup.IsPrimitive#

An element of a group is primitive when it belongs to some free basis of the group.

Group.IsPrimitive.{u} {G : Type u} [Group G] (x : G) : Prop
Lean

Formalized in Tau Ceti as Group.IsPrimitive.

Sources
LeanGroup.IsPrimitive

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.