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 →₀ ℤ).

Equations

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

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

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

Equations

• Finsupp.toFreeAbelianGroup = Finsupp.liftAddHom fun (x : X) => (smulAddHom ℤ (FreeAbelianGroup X)).flip (FreeAbelianGroup.of x)

@[simp]

theorem FreeAbelianGroup.toFinsupp_of {X : Type u_1} (x : X) : toFinsupp (of x) = Finsupp.single x 1

@[simp]

theorem Finsupp.toFreeAbelianGroup_single {X : Type u_1} (x : X) (n : ℤ) : toFreeAbelianGroup (single x n) = n • FreeAbelianGroup.of x

@[simp]

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

@[simp]

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

@[simp]

theorem Finsupp.toFreeAbelianGroup_comp_toFinsupp {X : Type u_1} : toFreeAbelianGroup.comp FreeAbelianGroup.toFinsupp = AddMonoidHom.id (FreeAbelianGroup X)

@[simp]

theorem Finsupp.toFreeAbelianGroup_toFinsupp {X : Type u_2} (x : FreeAbelianGroup X) : toFreeAbelianGroup (FreeAbelianGroup.toFinsupp x) = x

@[simp]

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

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

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

Equations

• FreeAbelianGroup.equivFinsupp X = { toFun := ⇑FreeAbelianGroup.toFinsupp, invFun := ⇑Finsupp.toFreeAbelianGroup, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

@[simp]

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

@[simp]

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

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.

Equations

• FreeAbelianGroup.coeff x = (Finsupp.applyAddHom x).comp FreeAbelianGroup.toFinsupp

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.

Equations

• a.support = (FreeAbelianGroup.toFinsupp a).support

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

theorem FreeAbelianGroup.notMem_support_iff {X : Type u_1} (x : X) (a : FreeAbelianGroup X) : x ∉ a.support ↔ (coeff x) a = 0

@[deprecated FreeAbelianGroup.notMem_support_iff (since := "2025-05-23")]

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

Alias of FreeAbelianGroup.notMem_support_iff.

@[simp]

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

@[simp]

theorem FreeAbelianGroup.support_of {X : Type u_1} (x : X) : (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 b : FreeAbelianGroup X) : (a + b).support ⊆ a.support ∪ b.support