Documentation

Mathlib.Data.Finsupp.ToDFinsupp

Conversion between Finsupp and homogeneous 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 #

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

Interpret a Finsupp as a homogeneous DFinsupp.

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

      Interpret a homogeneous 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
          source
          @[simp]
          theorem DFinsupp.toFinsupp_coe {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m ≠ 0)] (f : Π₀ (x : ι), M) :
          ⇑f.toFinsupp = ⇑f
          source
          @[simp]
          theorem DFinsupp.toFinsupp_support {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m ≠ 0)] (f : Π₀ (x : ι), M) :
          f.toFinsupp.support = f.support
          source
          @[simp]
          theorem DFinsupp.toFinsupp_single {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m ≠ 0)] (i : ι) (m : M) :
          (single i m).toFinsupp = Finsupp.single i m
          source
          @[simp]
          theorem Finsupp.toDFinsupp_toFinsupp {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m ≠ 0)] (f : ι →₀ M) :
          f.toDFinsupp.toFinsupp = f
          source
          @[simp]
          theorem DFinsupp.toFinsupp_toDFinsupp {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m ≠ 0)] (f : Π₀ (x : ι), M) :
          f.toFinsupp.toDFinsupp = f

          Lemmas about arithmetic operations #

          source
          @[simp]
          theorem Finsupp.toDFinsupp_zero {ι : Type u_1} {M : Type u_3} [Zero M] :
          toDFinsupp 0 = 0
          source
          @[simp]
          theorem Finsupp.toDFinsupp_add {ι : Type u_1} {M : Type u_3} [AddZeroClass M] (f g : ι →₀ M) :
          (f + g).toDFinsupp = f.toDFinsupp + g.toDFinsupp
          source
          @[simp]
          theorem Finsupp.toDFinsupp_neg {ι : Type u_1} {M : Type u_3} [AddGroup M] (f : ι →₀ M) :
          (-f).toDFinsupp = -f.toDFinsupp
          source
          @[simp]
          theorem Finsupp.toDFinsupp_sub {ι : Type u_1} {M : Type u_3} [AddGroup M] (f g : ι →₀ M) :
          (f - g).toDFinsupp = f.toDFinsupp - g.toDFinsupp
          source
          @[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) :
          (r • f).toDFinsupp = r • f.toDFinsupp
          source
          @[simp]
          theorem DFinsupp.toFinsupp_zero {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m ≠ 0)] :
          toFinsupp 0 = 0
          source
          @[simp]
          theorem DFinsupp.toFinsupp_add {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddZeroClass M] [(m : M) → Decidable (m ≠ 0)] (f g : Π₀ (x : ι), M) :
          (f + g).toFinsupp = f.toFinsupp + g.toFinsupp
          source
          @[simp]
          theorem DFinsupp.toFinsupp_neg {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddGroup M] [(m : M) → Decidable (m ≠ 0)] (f : Π₀ (x : ι), M) :
          (-f).toFinsupp = -f.toFinsupp
          source
          @[simp]
          theorem DFinsupp.toFinsupp_sub {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddGroup M] [(m : M) → Decidable (m ≠ 0)] (f g : Π₀ (x : ι), M) :
          (f - g).toFinsupp = f.toFinsupp - g.toFinsupp
          source
          @[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) :
          (r • f).toFinsupp = r • f.toFinsupp

          Bundled Equivs #

          source
          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
            Instances For
              source
              @[simp]
              theorem finsuppEquivDFinsupp_symm_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m ≠ 0)] :
              ⇑finsuppEquivDFinsupp.symm = DFinsupp.toFinsupp
              source
              @[simp]
              theorem finsuppEquivDFinsupp_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero M] [(m : M) → Decidable (m ≠ 0)] :
              ⇑finsuppEquivDFinsupp = Finsupp.toDFinsupp
              source
              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
                Instances For
                  source
                  @[simp]
                  theorem finsuppAddEquivDFinsupp_symm_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddZeroClass M] [(m : M) → Decidable (m ≠ 0)] :
                  ⇑finsuppAddEquivDFinsupp.symm = DFinsupp.toFinsupp
                  source
                  @[simp]
                  theorem finsuppAddEquivDFinsupp_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddZeroClass M] [(m : M) → Decidable (m ≠ 0)] :
                  ⇑finsuppAddEquivDFinsupp = Finsupp.toDFinsupp
                  source
                  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
                    Instances For
                      source
                      @[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
                      source
                      @[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] :
                      ⇑(finsuppLequivDFinsupp R).symm = DFinsupp.toFinsupp

                      Stronger versions of Finsupp.split #

                      source
                      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
                        Instances For
                          source
                          @[simp]
                          theorem sigmaFinsuppEquivDFinsupp_apply {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [Zero N] (f : (i : ι) × η i →₀ N) :
                          ⇑(sigmaFinsuppEquivDFinsupp f) = f.split
                          source
                          @[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
                          source
                          @[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) :
                          (sigmaFinsuppEquivDFinsupp f).support = f.splitSupport
                          source
                          @[simp]
                          theorem sigmaFinsuppEquivDFinsupp_single {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [DecidableEq ι] [Zero N] (a : (i : ι) × η i) (n : N) :
                          sigmaFinsuppEquivDFinsupp (Finsupp.single a n) = DFinsupp.single a.fst (Finsupp.single a.snd n)
                          source
                          @[simp]
                          theorem sigmaFinsuppEquivDFinsupp_add {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [AddZeroClass N] (f g : (i : ι) × η i →₀ N) :
                          sigmaFinsuppEquivDFinsupp (f + g) = sigmaFinsuppEquivDFinsupp f + sigmaFinsuppEquivDFinsupp g
                          source
                          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
                            Instances For
                              source
                              @[simp]
                              theorem sigmaFinsuppAddEquivDFinsupp_apply {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [AddZeroClass N] (a : (i : ι) × η i →₀ N) :
                              sigmaFinsuppAddEquivDFinsupp a = sigmaFinsuppEquivDFinsupp a
                              source
                              @[simp]
                              theorem sigmaFinsuppAddEquivDFinsupp_symm_apply {ι : Type u_1} {η : ι → Type u_4} {N : Type u_5} [AddZeroClass N] (a : Π₀ (i : ι), η i →₀ N) :
                              sigmaFinsuppAddEquivDFinsupp.symm a = sigmaFinsuppEquivDFinsupp.symm a
                              source
                              @[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) = r • sigmaFinsuppEquivDFinsupp f
                              source
                              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
                                Instances For
                                  source
                                  @[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) :
                                  (sigmaFinsuppLequivDFinsupp R).symm a✝ = sigmaFinsuppAddEquivDFinsupp.invFun a✝
                                  source
                                  @[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✝ = sigmaFinsuppAddEquivDFinsupp.toFun a✝