Documentation

Mathlib.GroupTheory.FreeAbelianGroupFinsupp

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 #

The group homomorphism FreeAbelianGroup X →+ (X →₀ ℤ).

Equations
  • FreeAbelianGroup.toFinsupp = FreeAbelianGroup.lift fun (x : X) => Finsupp.single x 1

The group homomorphism (X →₀ ℤ) →+ FreeAbelianGroup X.

Equations
@[simp]
theorem Finsupp.toFreeAbelianGroup_comp_singleAddHom {X : Type u_1} (x : X) :
Finsupp.toFreeAbelianGroup.comp (Finsupp.singleAddHom x) = (smulAddHom (FreeAbelianGroup X)).flip (FreeAbelianGroup.of x)
@[simp]
theorem FreeAbelianGroup.toFinsupp_comp_toFreeAbelianGroup {X : Type u_1} :
FreeAbelianGroup.toFinsupp.comp Finsupp.toFreeAbelianGroup = AddMonoidHom.id (X →₀ )
@[simp]
theorem Finsupp.toFreeAbelianGroup_comp_toFinsupp {X : Type u_1} :
Finsupp.toFreeAbelianGroup.comp FreeAbelianGroup.toFinsupp = AddMonoidHom.id (FreeAbelianGroup X)
@[simp]
theorem Finsupp.toFreeAbelianGroup_toFinsupp {X : Type u_2} (x : FreeAbelianGroup X) :
Finsupp.toFreeAbelianGroup (FreeAbelianGroup.toFinsupp x) = x
@[simp]
theorem FreeAbelianGroup.toFinsupp_of {X : Type u_1} (x : X) :
FreeAbelianGroup.toFinsupp (FreeAbelianGroup.of x) = Finsupp.single x 1
@[simp]
theorem FreeAbelianGroup.toFinsupp_toFreeAbelianGroup {X : Type u_1} (f : X →₀ ) :
FreeAbelianGroup.toFinsupp (Finsupp.toFreeAbelianGroup f) = f
@[simp]
theorem FreeAbelianGroup.equivFinsupp_symm_apply (X : Type u_1) (a : X →₀ ) :
(FreeAbelianGroup.equivFinsupp X).symm a = Finsupp.toFreeAbelianGroup a
@[simp]
theorem FreeAbelianGroup.equivFinsupp_apply (X : Type u_1) (a : FreeAbelianGroup X) :
(FreeAbelianGroup.equivFinsupp X) a = FreeAbelianGroup.toFinsupp a

The additive equivalence between FreeAbelianGroup X and (X →₀ ℤ).

Equations
  • FreeAbelianGroup.equivFinsupp X = { toFun := FreeAbelianGroup.toFinsupp, invFun := Finsupp.toFreeAbelianGroup, left_inv := , right_inv := , map_add' := }
noncomputable def FreeAbelianGroup.basis (α : Type u_2) :

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

Equations

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

Equations

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

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

Isomorphic free groups have equivalent bases.

Equations

coeff x is the additive group homomorphism FreeAbelianGroup X →+ ℤ that sends a to the multiplicity of x : X in a.

Equations

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
theorem FreeAbelianGroup.mem_support_iff {X : Type u_1} (x : X) (a : FreeAbelianGroup X) :
x a.support (FreeAbelianGroup.coeff x) a 0
theorem FreeAbelianGroup.not_mem_support_iff {X : Type u_1} (x : X) (a : FreeAbelianGroup X) :
xa.support (FreeAbelianGroup.coeff x) a = 0
@[simp]
theorem FreeAbelianGroup.support_of {X : Type u_1} (x : X) :
(FreeAbelianGroup.of x).support = {x}
@[simp]
theorem FreeAbelianGroup.support_neg {X : Type u_1} (a : FreeAbelianGroup X) :
(-a).support = a.support
@[simp]
theorem FreeAbelianGroup.support_zsmul {X : Type u_1} (k : ) (h : k 0) (a : FreeAbelianGroup X) :
(k a).support = a.support
@[simp]
theorem FreeAbelianGroup.support_nsmul {X : Type u_1} (k : ) (h : k 0) (a : FreeAbelianGroup X) :
(k a).support = a.support
theorem FreeAbelianGroup.support_add {X : Type u_1} (a : FreeAbelianGroup X) (b : FreeAbelianGroup X) :
(a + b).support a.support b.support