mathlib3 documentation

group_theory.free_abelian_group_finsupp

Isomorphism between free_abelian_group X and X →₀ ℤ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we construct the canonical isomorphism between free_abelian_group X and X →₀ ℤ. We use this to transport the notion of support from finsupp to free_abelian_group.

Main declarations #

source
noncomputable def free_abelian_group.to_finsupp {X : Type u_1} :
free_abelian_group X →+ X →₀ ℤ

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

Equations
source
noncomputable def finsupp.to_free_abelian_group {X : Type u_1} :
(X →₀ ℤ) →+ free_abelian_group X

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

Equations
source
@[simp]
theorem finsupp.to_free_abelian_group_comp_single_add_hom {X : Type u_1} (x : X) :
finsupp.to_free_abelian_group.comp (finsupp.single_add_hom x) = ⇑((smul_add_hom ℤ (free_abelian_group X)).flip) (free_abelian_group.of x)
source
@[simp]
theorem free_abelian_group.to_finsupp_comp_to_free_abelian_group {X : Type u_1} :
free_abelian_group.to_finsupp.comp finsupp.to_free_abelian_group = add_monoid_hom.id (X →₀ ℤ)
source
@[simp]
theorem finsupp.to_free_abelian_group_comp_to_finsupp {X : Type u_1} :
finsupp.to_free_abelian_group.comp free_abelian_group.to_finsupp = add_monoid_hom.id (free_abelian_group X)
source
@[simp]
theorem finsupp.to_free_abelian_group_to_finsupp {X : Type u_1} (x : free_abelian_group X) :
⇑finsupp.to_free_abelian_group (⇑free_abelian_group.to_finsupp x) = x
source
@[simp]
theorem free_abelian_group.to_finsupp_of {X : Type u_1} (x : X) :
⇑free_abelian_group.to_finsupp (free_abelian_group.of x) = finsupp.single x 1
source
@[simp]
theorem free_abelian_group.to_finsupp_to_free_abelian_group {X : Type u_1} (f : X →₀ ℤ) :
⇑free_abelian_group.to_finsupp (⇑finsupp.to_free_abelian_group f) = f
source
@[simp]
theorem free_abelian_group.equiv_finsupp_apply (X : Type u_1) (ᾰ : free_abelian_group X) :
⇑(free_abelian_group.equiv_finsupp X) ᾰ = ⇑free_abelian_group.to_finsupp ᾰ
source
noncomputable def free_abelian_group.equiv_finsupp (X : Type u_1) :
free_abelian_group X ≃+ (X →₀ ℤ)

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

Equations
source
@[simp]
theorem free_abelian_group.equiv_finsupp_symm_apply (X : Type u_1) (ᾰ : X →₀ ℤ) :
⇑((free_abelian_group.equiv_finsupp X).symm) ᾰ = ⇑finsupp.to_free_abelian_group ᾰ
source
noncomputable def free_abelian_group.basis (α : Type u_1) :
basis α ℤ (free_abelian_group α)

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

Equations
source
noncomputable def free_abelian_group.equiv.of_free_abelian_group_linear_equiv {α : Type u_1} {β : Type u_2} (e : free_abelian_group α ≃ₗ[ℤ] free_abelian_group β) :
α ≃ β

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

Equations
source
noncomputable def free_abelian_group.equiv.of_free_abelian_group_equiv {α : Type u_1} {β : Type u_2} (e : free_abelian_group α ≃+ free_abelian_group β) :
α ≃ β

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

Equations
source
noncomputable def free_abelian_group.equiv.of_free_group_equiv {α : Type u_1} {β : Type u_2} (e : free_group α ≃* free_group β) :
α ≃ β

Isomorphic free groups have equivalent bases.

Equations
source
noncomputable def free_abelian_group.equiv.of_is_free_group_equiv {G : Type u_1} {H : Type u_2} [group G] [group H] [is_free_group G] [is_free_group H] (e : G ≃* H) :
is_free_group.generators G ≃ is_free_group.generators H

Isomorphic free groups have equivalent bases (is_free_group variant`).

Equations
source
noncomputable def free_abelian_group.coeff {X : Type u_1} (x : X) :
free_abelian_group X →+ ℤ

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

Equations
source
noncomputable def free_abelian_group.support {X : Type u_1} (a : free_abelian_group X) :
finset X

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

Equations
source
theorem free_abelian_group.mem_support_iff {X : Type u_1} (x : X) (a : free_abelian_group X) :
x ∈ a.support ↔ ⇑(free_abelian_group.coeff x) a ≠ 0
source
theorem free_abelian_group.not_mem_support_iff {X : Type u_1} (x : X) (a : free_abelian_group X) :
x ∉ a.support ↔ ⇑(free_abelian_group.coeff x) a = 0
source
@[simp]
theorem free_abelian_group.support_zero {X : Type u_1} :
0.support = ∅
source
@[simp]
theorem free_abelian_group.support_of {X : Type u_1} (x : X) :
(free_abelian_group.of x).support = {x}
source
@[simp]
theorem free_abelian_group.support_neg {X : Type u_1} (a : free_abelian_group X) :
(-a).support = a.support
source
@[simp]
theorem free_abelian_group.support_zsmul {X : Type u_1} (k : ℤ) (h : k ≠ 0) (a : free_abelian_group X) :
(k • a).support = a.support
source
@[simp]
theorem free_abelian_group.support_nsmul {X : Type u_1} (k : ℕ) (h : k ≠ 0) (a : free_abelian_group X) :
(k • a).support = a.support
source
theorem free_abelian_group.support_add {X : Type u_1} (a b : free_abelian_group X) :
(a + b).support ⊆ a.support ∪ b.support