Documentation

Mathlib.GroupTheory.FreeGroup.GeneratorEquiv

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

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

Equations

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

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

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

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

Isomorphic free groups have equivalent bases.

Equations