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
Instances For

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

    Equations
    Instances For
      @[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' := }
      Instances For
        noncomputable def FreeAbelianGroup.basis (α : Type u_2) :

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

        Equations
        Instances For

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

          Equations
          Instances For

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

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

              Isomorphic free groups have equivalent bases.

              Equations
              Instances For

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

                Equations
                Instances For

                  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
                  Instances For
                    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