Isomorphism between FreeAbelianGroup X
and X →₀ ℤ
#
In this file we construct the canonical isomorphism between FreeAbelianGroup X
and X →₀ ℤ
.
We use this to transport the notion of support
from Finsupp
to FreeAbelianGroup
.
Main declarations #
FreeAbelianGroup.equivFinsupp
: group isomorphism betweenFreeAbelianGroup X
andX →₀ ℤ
FreeAbelianGroup.coeff
: the multiplicity ofx : X
ina : FreeAbelianGroup X
FreeAbelianGroup.support
: the finset ofx : X
that occur ina : FreeAbelianGroup X
The group homomorphism FreeAbelianGroup X →+ (X →₀ ℤ)
.
Equations
- FreeAbelianGroup.toFinsupp = FreeAbelianGroup.lift fun (x : X) => Finsupp.single x 1
Instances For
The group homomorphism (X →₀ ℤ) →+ FreeAbelianGroup X
.
Equations
- Finsupp.toFreeAbelianGroup = Finsupp.liftAddHom fun (x : X) => (smulAddHom ℤ (FreeAbelianGroup X)).flip (FreeAbelianGroup.of x)
Instances For
The additive equivalence between FreeAbelianGroup X
and (X →₀ ℤ)
.
Equations
- FreeAbelianGroup.equivFinsupp X = { toFun := ⇑FreeAbelianGroup.toFinsupp, invFun := ⇑Finsupp.toFreeAbelianGroup, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
Instances For
A
is a basis of the ℤ-module FreeAbelianGroup A
.
Equations
- FreeAbelianGroup.basis α = { repr := (FreeAbelianGroup.equivFinsupp α).toIntLinearEquiv }
Instances For
Isomorphic free abelian groups (as modules) have equivalent bases.
Equations
- FreeAbelianGroup.Equiv.ofFreeAbelianGroupLinearEquiv e = ((FreeAbelianGroup.basis α).map e).indexEquiv (FreeAbelianGroup.basis β)
Instances For
Isomorphic free abelian groups (as additive groups) have equivalent bases.
Equations
Instances For
Isomorphic free groups have equivalent bases.
Equations
- FreeAbelianGroup.Equiv.ofFreeGroupEquiv e = FreeAbelianGroup.Equiv.ofFreeAbelianGroupEquiv (MulEquiv.toAdditive e.abelianizationCongr)
Instances For
Isomorphic free groups have equivalent bases (IsFreeGroup
variant).
Equations
- FreeAbelianGroup.Equiv.ofIsFreeGroupEquiv e = FreeAbelianGroup.Equiv.ofFreeGroupEquiv ((IsFreeGroup.toFreeGroup G).symm.trans (e.trans (IsFreeGroup.toFreeGroup H)))
Instances For
coeff x
is the additive group homomorphism FreeAbelianGroup X →+ ℤ
that sends a
to the multiplicity of x : X
in a
.
Equations
- FreeAbelianGroup.coeff x = (Finsupp.applyAddHom x).comp FreeAbelianGroup.toFinsupp
Instances For
support a
for a : FreeAbelianGroup X
is the finite set of x : X
that occur in the formal sum a
.
Equations
- a.support = (FreeAbelianGroup.toFinsupp a).support