Documentation

Mathlib.Algebra.FreeAbelianGroup.Finsupp

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 #

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

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

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

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

      Equations
        Instances For
          source
          @[simp]
          theorem FreeAbelianGroup.toFinsupp_of {X : Type u_1} (x : X) :
          toFinsupp (of x) = Finsupp.single x 1
          source
          @[simp]
          theorem Finsupp.toFreeAbelianGroup_single {X : Type u_1} (x : X) (n : ℤ) :
          toFreeAbelianGroup (single x n) = n • FreeAbelianGroup.of x
          source
          @[simp]
          theorem Finsupp.toFreeAbelianGroup_comp_singleAddHom {X : Type u_1} (x : X) :
          toFreeAbelianGroup.comp (singleAddHom x) = (smulAddHom ℤ (FreeAbelianGroup X)).flip (FreeAbelianGroup.of x)
          source
          @[simp]
          theorem FreeAbelianGroup.toFinsupp_comp_toFreeAbelianGroup {X : Type u_1} :
          toFinsupp.comp Finsupp.toFreeAbelianGroup = AddMonoidHom.id (X →₀ ℤ)
          source
          @[simp]
          theorem Finsupp.toFreeAbelianGroup_comp_toFinsupp {X : Type u_1} :
          toFreeAbelianGroup.comp FreeAbelianGroup.toFinsupp = AddMonoidHom.id (FreeAbelianGroup X)
          source
          @[simp]
          theorem Finsupp.toFreeAbelianGroup_toFinsupp {X : Type u_2} (x : FreeAbelianGroup X) :
          toFreeAbelianGroup (FreeAbelianGroup.toFinsupp x) = x
          source
          @[simp]
          theorem FreeAbelianGroup.toFinsupp_toFreeAbelianGroup {X : Type u_1} (f : X →₀ ℤ) :
          toFinsupp (Finsupp.toFreeAbelianGroup f) = f
          source
          def FreeAbelianGroup.equivFinsupp (X : Type u_1) :
          FreeAbelianGroup X ≃+ (X →₀ ℤ)

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

          Equations
            Instances For
              source
              @[simp]
              theorem FreeAbelianGroup.equivFinsupp_symm_apply (X : Type u_1) (a : X →₀ ℤ) :
              (equivFinsupp X).symm a = Finsupp.toFreeAbelianGroup a
              source
              @[simp]
              theorem FreeAbelianGroup.equivFinsupp_apply (X : Type u_1) (a : FreeAbelianGroup X) :
              (equivFinsupp X) a = toFinsupp a
              source
              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
                Instances For
                  source
                  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
                    Instances For
                      source
                      theorem FreeAbelianGroup.mem_support_iff {X : Type u_1} (x : X) (a : FreeAbelianGroup X) :
                      x ∈ a.support ↔ (coeff x) a ≠ 0
                      source
                      theorem FreeAbelianGroup.notMem_support_iff {X : Type u_1} (x : X) (a : FreeAbelianGroup X) :
                      x ∉ a.support ↔ (coeff x) a = 0
                      source
                      @[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.

                      source
                      @[simp]
                      theorem FreeAbelianGroup.support_zero {X : Type u_1} :
                      support 0 = ∅
                      source
                      @[simp]
                      theorem FreeAbelianGroup.support_of {X : Type u_1} (x : X) :
                      (of x).support = {x}
                      source
                      @[simp]
                      theorem FreeAbelianGroup.support_neg {X : Type u_1} (a : FreeAbelianGroup X) :
                      (-a).support = a.support
                      source
                      @[simp]
                      theorem FreeAbelianGroup.support_zsmul {X : Type u_1} (k : ℤ) (h : k ≠ 0) (a : FreeAbelianGroup X) :
                      (k • a).support = a.support
                      source
                      @[simp]
                      theorem FreeAbelianGroup.support_nsmul {X : Type u_1} (k : ℕ) (h : k ≠ 0) (a : FreeAbelianGroup X) :
                      (k • a).support = a.support
                      source
                      theorem FreeAbelianGroup.support_add {X : Type u_1} (a b : FreeAbelianGroup X) :
                      (a + b).support ⊆ a.support ∪ b.support