Isomorphisms between free groups come from equivalences of their generators

This file proves that an isomorphism e : G ≃* H between free groups G and H is induced by an equivalence of generators.

TODO

We currently construct the equivalence of generators, but don't show that it induces the isomorphism of groups.

noncomputable def FreeAbelianGroup.basis (α : Type u_5) : Basis α ℤ (FreeAbelianGroup α)

A is a basis of the ℤ-module FreeAbelianGroup A.

Equations

• FreeAbelianGroup.basis α = { repr := (FreeAbelianGroup.equivFinsupp α).toIntLinearEquiv }

def Equiv.ofFreeAbelianGroupLinearEquiv {α : Type u_1} {β : Type u_2} (e : FreeAbelianGroup α ≃ₗ[ℤ] FreeAbelianGroup β) : α ≃ β

Isomorphic free abelian groups (as modules) have equivalent bases.

Equations

• Equiv.ofFreeAbelianGroupLinearEquiv e = ((FreeAbelianGroup.basis α).map e).indexEquiv (FreeAbelianGroup.basis β)

def Equiv.ofFreeAbelianGroupEquiv {α : Type u_1} {β : Type u_2} (e : FreeAbelianGroup α ≃+ FreeAbelianGroup β) : α ≃ β

Isomorphic free abelian groups (as additive groups) have equivalent bases.

Equations

• Equiv.ofFreeAbelianGroupEquiv e = Equiv.ofFreeAbelianGroupLinearEquiv e.toIntLinearEquiv

def Equiv.ofFreeGroupEquiv {α : Type u_1} {β : Type u_2} (e : FreeGroup α ≃* FreeGroup β) : α ≃ β

Isomorphic free groups have equivalent bases.

Equations

• Equiv.ofFreeGroupEquiv e = Equiv.ofFreeAbelianGroupEquiv (MulEquiv.toAdditive e.abelianizationCongr)

def Equiv.ofIsFreeGroupEquiv {G : Type u_3} {H : Type u_4} [Group G] [Group H] [IsFreeGroup G] [IsFreeGroup H] (e : G ≃* H) : IsFreeGroup.Generators G ≃ IsFreeGroup.Generators H

Isomorphic free groups have equivalent bases (IsFreeGroup variant).

Equations

• Equiv.ofIsFreeGroupEquiv e = Equiv.ofFreeGroupEquiv ((IsFreeGroup.toFreeGroup G).symm.trans (e.trans (IsFreeGroup.toFreeGroup H)))