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 between FreeAbelianGroup X and X →₀ ℤ
• FreeAbelianGroup.coeff: the multiplicity of x : X in a : FreeAbelianGroup X
• FreeAbelianGroup.support: the finset of x : X that occur in a : FreeAbelianGroup X

def FreeAbelianGroup.toFinsupp {X : Type u_1} : FreeAbelianGroup X →+ X →₀ ℤ

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

def Finsupp.toFreeAbelianGroup {X : Type u_1} : (X →₀ ℤ) →+ FreeAbelianGroup X

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

@[simp]

theorem Finsupp.toFreeAbelianGroup_comp_singleAddHom {X : Type u_1} (x : X) : AddMonoidHom.comp Finsupp.toFreeAbelianGroup (Finsupp.singleAddHom x) = ↑(AddMonoidHom.flip (smulAddHom ℤ (FreeAbelianGroup X))) (FreeAbelianGroup.of x)

@[simp]

theorem FreeAbelianGroup.toFinsupp_comp_toFreeAbelianGroup {X : Type u_1} : AddMonoidHom.comp FreeAbelianGroup.toFinsupp Finsupp.toFreeAbelianGroup = AddMonoidHom.id (X →₀ ℤ)

@[simp]

theorem Finsupp.toFreeAbelianGroup_comp_toFinsupp {X : Type u_1} : AddMonoidHom.comp Finsupp.toFreeAbelianGroup 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) = fun₀ | x => 1

@[simp]

theorem FreeAbelianGroup.toFinsupp_toFreeAbelianGroup {X : Type u_1} (f : X →₀ ℤ) : ↑FreeAbelianGroup.toFinsupp (↑Finsupp.toFreeAbelianGroup f) = f

@[simp]

theorem FreeAbelianGroup.equivFinsupp_apply (X : Type u_1) (a : FreeAbelianGroup X) : ↑(FreeAbelianGroup.equivFinsupp X) a = ↑FreeAbelianGroup.toFinsupp a

@[simp]

theorem FreeAbelianGroup.equivFinsupp_symm_apply (X : Type u_1) (a : X →₀ ℤ) : ↑(AddEquiv.symm (FreeAbelianGroup.equivFinsupp X)) a = ↑Finsupp.toFreeAbelianGroup a

def FreeAbelianGroup.equivFinsupp (X : Type u_1) : FreeAbelianGroup X ≃+ (X →₀ ℤ)

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

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

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

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

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

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

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

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

Isomorphic free groups have equivalent bases.

def FreeAbelianGroup.Equiv.ofIsFreeGroupEquiv {G : Type u_2} {H : Type u_3} [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).

def FreeAbelianGroup.coeff {X : Type u_1} (x : X) : FreeAbelianGroup X →+ ℤ

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

def FreeAbelianGroup.support {X : Type u_1} (a : FreeAbelianGroup X) : Finset X

support a for a : FreeAbelianGroup X is the finite set of x : X that occur in the formal sum a.

theorem FreeAbelianGroup.mem_support_iff {X : Type u_1} (x : X) (a : FreeAbelianGroup X) : x ∈ FreeAbelianGroup.support a ↔ ↑(FreeAbelianGroup.coeff x) a ≠ 0

theorem FreeAbelianGroup.not_mem_support_iff {X : Type u_1} (x : X) (a : FreeAbelianGroup X) : ¬x ∈ FreeAbelianGroup.support a ↔ ↑(FreeAbelianGroup.coeff x) a = 0

@[simp]

theorem FreeAbelianGroup.support_zero {X : Type u_1} : FreeAbelianGroup.support 0 = ∅

@[simp]

theorem FreeAbelianGroup.support_of {X : Type u_1} (x : X) : FreeAbelianGroup.support (FreeAbelianGroup.of x) = {x}

@[simp]

theorem FreeAbelianGroup.support_neg {X : Type u_1} (a : FreeAbelianGroup X) : FreeAbelianGroup.support (-a) = FreeAbelianGroup.support a

@[simp]

theorem FreeAbelianGroup.support_zsmul {X : Type u_1} (k : ℤ) (h : k ≠ 0) (a : FreeAbelianGroup X) : FreeAbelianGroup.support (k • a) = FreeAbelianGroup.support a

@[simp]

theorem FreeAbelianGroup.support_nsmul {X : Type u_1} (k : ℕ) (h : k ≠ 0) (a : FreeAbelianGroup X) : FreeAbelianGroup.support (k • a) = FreeAbelianGroup.support a

theorem FreeAbelianGroup.support_add {X : Type u_1} (a : FreeAbelianGroup X) (b : FreeAbelianGroup X) : FreeAbelianGroup.support (a + b) ⊆ FreeAbelianGroup.support a ∪ FreeAbelianGroup.support b