Isomorphisms between free groups imply equivalences of their generators

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

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

Equations

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

noncomputable 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 β)

noncomputable 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

noncomputable 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)

noncomputable 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)))