Documentation

Mathlib.Data.Finsupp.ToDFinsupp

Conversion between Finsupp and homogenous DFinsupp #

This module provides conversions between Finsupp and DFinsupp. It is in its own file since neither Finsupp or DFinsupp depend on each other.

Main definitions #

Theorems #

The defining features of these operations is that they preserve the function and support:

and therefore map Finsupp.single to DFinsupp.single and vice versa:

as well as preserving arithmetic operations.

For the bundled equivalences, we provide lemmas that they reduce to Finsupp.toDFinsupp:

Implementation notes #

We provide DFinsupp.toFinsupp and finsuppEquivDFinsupp computably by adding [DecidableEq ι] and [Π m : M, Decidable (m ≠ 0)] arguments. To aid with definitional unfolding, these arguments are also present on the noncomputable equivs.

Basic definitions and lemmas #

def Finsupp.toDFinsupp {ι : Type u_1} {M : Type u_3} [Zero M] (f : ι →₀ M) :
Π₀ (x : ι), M

Interpret a Finsupp as a homogenous DFinsupp.

Equations
Instances For
    @[simp]
    theorem Finsupp.toDFinsupp_coe {ι : Type u_1} {M : Type u_3} [Zero M] (f : ι →₀ M) :
    ↑(Finsupp.toDFinsupp f) = f
    @[simp]
    theorem Finsupp.toDFinsupp_single {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] (i : ι) (m : M) :
    (Finsupp.toDFinsupp fun₀ | i => m) = DFinsupp.single i m
    @[simp]
    theorem toDFinsupp_support {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m 0)] (f : ι →₀ M) :
    def DFinsupp.toFinsupp {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m 0)] (f : Π₀ (x : ι), M) :
    ι →₀ M

    Interpret a homogenous DFinsupp as a Finsupp.

    Note that the elaborator has a lot of trouble with this definition - it is often necessary to write (DFinsupp.toFinsupp f : ι →₀ M) instead of f.toFinsupp, as for some unknown reason using dot notation or omitting the type ascription prevents the type being resolved correctly.

    Equations
    Instances For
      @[simp]
      theorem DFinsupp.toFinsupp_coe {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m 0)] (f : Π₀ (x : ι), M) :
      ↑(DFinsupp.toFinsupp f) = f
      @[simp]
      theorem DFinsupp.toFinsupp_support {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m 0)] (f : Π₀ (x : ι), M) :
      @[simp]
      theorem DFinsupp.toFinsupp_single {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m 0)] (i : ι) (m : M) :
      DFinsupp.toFinsupp (DFinsupp.single i m) = fun₀ | i => m
      @[simp]
      theorem Finsupp.toDFinsupp_toFinsupp {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m 0)] (f : ι →₀ M) :
      @[simp]
      theorem DFinsupp.toFinsupp_toDFinsupp {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m 0)] (f : Π₀ (x : ι), M) :

      Lemmas about arithmetic operations #

      @[simp]
      theorem Finsupp.toDFinsupp_zero {ι : Type u_1} {M : Type u_3} [Zero M] :
      @[simp]
      theorem Finsupp.toDFinsupp_add {ι : Type u_1} {M : Type u_3} [AddZeroClass M] (f : ι →₀ M) (g : ι →₀ M) :
      @[simp]
      theorem Finsupp.toDFinsupp_neg {ι : Type u_1} {M : Type u_3} [AddGroup M] (f : ι →₀ M) :
      @[simp]
      theorem Finsupp.toDFinsupp_sub {ι : Type u_1} {M : Type u_3} [AddGroup M] (f : ι →₀ M) (g : ι →₀ M) :
      @[simp]
      theorem Finsupp.toDFinsupp_smul {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Monoid R] [AddMonoid M] [DistribMulAction R M] (r : R) (f : ι →₀ M) :
      @[simp]
      theorem DFinsupp.toFinsupp_zero {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m 0)] :
      @[simp]
      theorem DFinsupp.toFinsupp_add {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddZeroClass M] [(m : M) → Decidable (m 0)] (f : Π₀ (x : ι), M) (g : Π₀ (x : ι), M) :
      @[simp]
      theorem DFinsupp.toFinsupp_neg {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddGroup M] [(m : M) → Decidable (m 0)] (f : Π₀ (x : ι), M) :
      @[simp]
      theorem DFinsupp.toFinsupp_sub {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddGroup M] [(m : M) → Decidable (m 0)] (f : Π₀ (x : ι), M) (g : Π₀ (x : ι), M) :
      @[simp]
      theorem DFinsupp.toFinsupp_smul {ι : Type u_1} {R : Type u_2} {M : Type u_3} [DecidableEq ι] [Monoid R] [AddMonoid M] [DistribMulAction R M] [(m : M) → Decidable (m 0)] (r : R) (f : Π₀ (x : ι), M) :

      Bundled Equivs #

      @[simp]
      theorem finsuppEquivDFinsupp_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m 0)] :
      finsuppEquivDFinsupp = Finsupp.toDFinsupp
      @[simp]
      theorem finsuppEquivDFinsupp_symm_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m 0)] :
      finsuppEquivDFinsupp.symm = DFinsupp.toFinsupp
      def finsuppEquivDFinsupp {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m 0)] :
      (ι →₀ M) Π₀ (x : ι), M

      Finsupp.toDFinsupp and DFinsupp.toFinsupp together form an equiv.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem finsuppAddEquivDFinsupp_symm_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddZeroClass M] [(m : M) → Decidable (m 0)] :
        ↑(AddEquiv.symm finsuppAddEquivDFinsupp) = DFinsupp.toFinsupp
        @[simp]
        theorem finsuppAddEquivDFinsupp_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddZeroClass M] [(m : M) → Decidable (m 0)] :
        finsuppAddEquivDFinsupp = Finsupp.toDFinsupp
        def finsuppAddEquivDFinsupp {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddZeroClass M] [(m : M) → Decidable (m 0)] :
        (ι →₀ M) ≃+ Π₀ (x : ι), M

        The additive version of finsupp.toFinsupp. Note that this is noncomputable because Finsupp.add is noncomputable.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def finsuppLequivDFinsupp {ι : Type u_1} (R : Type u_2) {M : Type u_3} [DecidableEq ι] [Semiring R] [AddCommMonoid M] [(m : M) → Decidable (m 0)] [Module R M] :
          (ι →₀ M) ≃ₗ[R] Π₀ (x : ι), M

          The additive version of Finsupp.toFinsupp. Note that this is noncomputable because Finsupp.add is noncomputable.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem finsuppLequivDFinsupp_apply_apply {ι : Type u_1} (R : Type u_2) {M : Type u_3} [DecidableEq ι] [Semiring R] [AddCommMonoid M] [(m : M) → Decidable (m 0)] [Module R M] :
            ↑(finsuppLequivDFinsupp R) = Finsupp.toDFinsupp
            @[simp]
            theorem finsuppLequivDFinsupp_symm_apply {ι : Type u_1} (R : Type u_2) {M : Type u_3} [DecidableEq ι] [Semiring R] [AddCommMonoid M] [(m : M) → Decidable (m 0)] [Module R M] :
            ↑(LinearEquiv.symm (finsuppLequivDFinsupp R)) = DFinsupp.toFinsupp

            Stronger versions of Finsupp.split #

            def sigmaFinsuppEquivDFinsupp {ι : Type u_1} {η : ιType u_4} {N : Type u_5} [Zero N] :
            ((i : ι) × η i →₀ N) Π₀ (i : ι), η i →₀ N

            Finsupp.split is an equivalence between (Σ i, η i) →₀ N and Π₀ i, (η i →₀ N).

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem sigmaFinsuppEquivDFinsupp_apply {ι : Type u_1} {η : ιType u_4} {N : Type u_5} [Zero N] (f : (i : ι) × η i →₀ N) :
              ↑(sigmaFinsuppEquivDFinsupp f) = Finsupp.split f
              @[simp]
              theorem sigmaFinsuppEquivDFinsupp_symm_apply {ι : Type u_1} {η : ιType u_4} {N : Type u_5} [Zero N] (f : Π₀ (i : ι), η i →₀ N) (s : (i : ι) × η i) :
              ↑(sigmaFinsuppEquivDFinsupp.symm f) s = ↑(f s.fst) s.snd
              @[simp]
              theorem sigmaFinsuppEquivDFinsupp_support {ι : Type u_1} {η : ιType u_4} {N : Type u_5} [DecidableEq ι] [Zero N] [(i : ι) → (x : η i →₀ N) → Decidable (x 0)] (f : (i : ι) × η i →₀ N) :
              DFinsupp.support (sigmaFinsuppEquivDFinsupp f) = Finsupp.splitSupport f
              @[simp]
              theorem sigmaFinsuppEquivDFinsupp_single {ι : Type u_1} {η : ιType u_4} {N : Type u_5} [DecidableEq ι] [Zero N] (a : (i : ι) × η i) (n : N) :
              (sigmaFinsuppEquivDFinsupp fun₀ | a => n) = DFinsupp.single a.fst fun₀ | a.snd => n
              @[simp]
              theorem sigmaFinsuppEquivDFinsupp_add {ι : Type u_1} {η : ιType u_4} {N : Type u_5} [AddZeroClass N] (f : (i : ι) × η i →₀ N) (g : (i : ι) × η i →₀ N) :
              sigmaFinsuppEquivDFinsupp (f + g) = sigmaFinsuppEquivDFinsupp f + sigmaFinsuppEquivDFinsupp g
              @[simp]
              theorem sigmaFinsuppAddEquivDFinsupp_apply {ι : Type u_1} {η : ιType u_4} {N : Type u_5} [AddZeroClass N] (a : (i : ι) × η i →₀ N) :
              sigmaFinsuppAddEquivDFinsupp a = sigmaFinsuppEquivDFinsupp a
              @[simp]
              theorem sigmaFinsuppAddEquivDFinsupp_symm_apply {ι : Type u_1} {η : ιType u_4} {N : Type u_5} [AddZeroClass N] (a : Π₀ (i : ι), η i →₀ N) :
              ↑(AddEquiv.symm sigmaFinsuppAddEquivDFinsupp) a = sigmaFinsuppEquivDFinsupp.symm a
              def sigmaFinsuppAddEquivDFinsupp {ι : Type u_1} {η : ιType u_4} {N : Type u_5} [AddZeroClass N] :
              ((i : ι) × η i →₀ N) ≃+ Π₀ (i : ι), η i →₀ N

              Finsupp.split is an additive equivalence between (Σ i, η i) →₀ N and Π₀ i, (η i →₀ N).

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem sigmaFinsuppEquivDFinsupp_smul {ι : Type u_1} {η : ιType u_4} {N : Type u_5} {R : Type u_6} [Monoid R] [AddMonoid N] [DistribMulAction R N] (r : R) (f : (i : ι) × η i →₀ N) :
                sigmaFinsuppEquivDFinsupp (r f) = SMul.smul r (sigmaFinsuppEquivDFinsupp f)
                @[simp]
                theorem sigmaFinsuppLequivDFinsupp_symm_apply {ι : Type u_1} (R : Type u_2) {η : ιType u_4} {N : Type u_5} [Semiring R] [AddCommMonoid N] [Module R N] (a : Π₀ (i : ι), η i →₀ N) :
                ↑(LinearEquiv.symm (sigmaFinsuppLequivDFinsupp R)) a = sigmaFinsuppEquivDFinsupp.symm a
                @[simp]
                theorem sigmaFinsuppLequivDFinsupp_apply {ι : Type u_1} (R : Type u_2) {η : ιType u_4} {N : Type u_5} [Semiring R] [AddCommMonoid N] [Module R N] (a : (i : ι) × η i →₀ N) :
                ↑(sigmaFinsuppLequivDFinsupp R) a = sigmaFinsuppEquivDFinsupp a
                def sigmaFinsuppLequivDFinsupp {ι : Type u_1} (R : Type u_2) {η : ιType u_4} {N : Type u_5} [Semiring R] [AddCommMonoid N] [Module R N] :
                ((i : ι) × η i →₀ N) ≃ₗ[R] Π₀ (i : ι), η i →₀ N

                Finsupp.split is a linear equivalence between (Σ i, η i) →₀ N and Π₀ i, (η i →₀ N).

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For