Documentation

Mathlib.Algebra.MonoidAlgebra.ToDirectSum

Conversion between AddMonoidAlgebra and homogeneous DirectSum #

This module provides conversions between AddMonoidAlgebra and DirectSum. The latter is essentially a dependent version of the former.

Note that since DirectSum.instMul combines indices additively, there is no equivalent to MonoidAlgebra.

Main definitions #

Theorems #

The defining feature of these operations is that they map Finsupp.single to DirectSum.of and vice versa:

as well as preserving arithmetic operations.

For the bundled equivalences, we provide lemmas that they reduce to AddMonoidAlgebra.toDirectSum:

Implementation notes #

This file largely just copies the API of Mathlib/Data/Finsupp/ToDFinsupp.lean, and reuses the proofs. Recall that AddMonoidAlgebra M ι is defeq to ι →₀ M and ⨁ i : ι, M is defeq to Π₀ i : ι, M.

Note that there is no AddMonoidAlgebra equivalent to Finsupp.single, so many statements still involve this definition.

Basic definitions and lemmas #

source
def AddMonoidAlgebra.toDirectSum {ι : Type u_1} {M : Type u_3} [Semiring M] (f : AddMonoidAlgebra M ι) :
DirectSum ι fun (x : ι) => M

Interpret an AddMonoidAlgebra as a homogeneous DirectSum.

Equations
    Instances For
      source
      @[simp]
      theorem AddMonoidAlgebra.toDirectSum_single {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] (i : ι) (m : M) :
      toDirectSum (Finsupp.single i m) = (DirectSum.of (fun (i : ι) => M) i) m
      source
      def DirectSum.toAddMonoidAlgebra {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] (f : DirectSum ι fun (x : ι) => M) :
      AddMonoidAlgebra M ι

      Interpret a homogeneous DirectSum as an AddMonoidAlgebra.

      Equations
        Instances For
          source
          @[simp]
          theorem DirectSum.toAddMonoidAlgebra_of {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] (i : ι) (m : M) :
          ((of (fun (x : ι) => M) i) m).toAddMonoidAlgebra = Finsupp.single i m
          source
          @[simp]
          theorem AddMonoidAlgebra.toDirectSum_toAddMonoidAlgebra {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] (f : AddMonoidAlgebra M ι) :
          f.toDirectSum.toAddMonoidAlgebra = f
          source
          @[simp]
          theorem DirectSum.toAddMonoidAlgebra_toDirectSum {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] (f : DirectSum ι fun (x : ι) => M) :
          f.toAddMonoidAlgebra.toDirectSum = f

          Lemmas about arithmetic operations #

          source
          @[simp]
          theorem AddMonoidAlgebra.toDirectSum_zero {ι : Type u_1} {M : Type u_3} [Semiring M] :
          toDirectSum 0 = 0
          source
          @[simp]
          theorem AddMonoidAlgebra.toDirectSum_add {ι : Type u_1} {M : Type u_3} [Semiring M] (f g : AddMonoidAlgebra M ι) :
          (f + g).toDirectSum = f.toDirectSum + g.toDirectSum
          source
          @[simp]
          theorem AddMonoidAlgebra.toDirectSum_natCast {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] (n : ℕ) :
          (↑n).toDirectSum = ↑n
          source
          @[simp]
          theorem AddMonoidAlgebra.toDirectSum_ofNat {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] (n : ℕ) [n.AtLeastTwo] :
          (OfNat.ofNat n).toDirectSum = OfNat.ofNat n
          source
          @[simp]
          theorem AddMonoidAlgebra.toDirectSum_sub {ι : Type u_1} {M : Type u_3} [Ring M] (f g : AddMonoidAlgebra M ι) :
          (f - g).toDirectSum = f.toDirectSum - g.toDirectSum
          source
          @[simp]
          theorem AddMonoidAlgebra.toDirectSum_neg {ι : Type u_1} {M : Type u_3} [Ring M] (f : AddMonoidAlgebra M ι) :
          (-f).toDirectSum = -f.toDirectSum
          source
          @[simp]
          theorem AddMonoidAlgebra.toDirectSum_intCast {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Ring M] (z : ℤ) :
          (↑z).toDirectSum = ↑z
          source
          @[simp]
          theorem AddMonoidAlgebra.toDirectSum_one {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero ι] [Semiring M] :
          toDirectSum 1 = 1
          source
          @[simp]
          theorem AddMonoidAlgebra.toDirectSum_mul {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] (f g : AddMonoidAlgebra M ι) :
          (f * g).toDirectSum = f.toDirectSum * g.toDirectSum
          source
          @[simp]
          theorem DirectSum.toAddMonoidAlgebra_zero {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] :
          toAddMonoidAlgebra 0 = 0
          source
          @[simp]
          theorem DirectSum.toAddMonoidAlgebra_add {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] (f g : DirectSum ι fun (x : ι) => M) :
          (f + g).toAddMonoidAlgebra = f.toAddMonoidAlgebra + g.toAddMonoidAlgebra
          source
          @[simp]
          theorem DirectSum.toAddMonoidAlgebra_natCast {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] (n : ℕ) :
          (↑n).toAddMonoidAlgebra = ↑n
          source
          @[simp]
          theorem DirectSum.toAddMonoidAlgebra_ofNat {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] (n : ℕ) [n.AtLeastTwo] :
          (OfNat.ofNat n).toAddMonoidAlgebra = OfNat.ofNat n
          source
          @[simp]
          theorem DirectSum.toAddMonoidAlgebra_sub {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Ring M] [(m : M) → Decidable (m ≠ 0)] (f g : DirectSum ι fun (x : ι) => M) :
          (f - g).toAddMonoidAlgebra = f.toAddMonoidAlgebra - g.toAddMonoidAlgebra
          source
          @[simp]
          theorem DirectSum.toAddMonoidAlgebra_neg {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Ring M] [(m : M) → Decidable (m ≠ 0)] (f : DirectSum ι fun (x : ι) => M) :
          (-f).toAddMonoidAlgebra = -f.toAddMonoidAlgebra
          source
          @[simp]
          theorem DirectSum.toAddMonoidAlgebra_intCast {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Ring M] [(m : M) → Decidable (m ≠ 0)] (z : ℤ) :
          (↑z).toAddMonoidAlgebra = ↑z
          source
          @[simp]
          theorem DirectSum.toAddMonoidAlgebra_one {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Zero ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] :
          toAddMonoidAlgebra 1 = 1
          source
          @[simp]
          theorem DirectSum.toAddMonoidAlgebra_mul {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] (f g : DirectSum ι fun (x : ι) => M) :
          (f * g).toAddMonoidAlgebra = f.toAddMonoidAlgebra * g.toAddMonoidAlgebra

          Bundled Equivs #

          source
          def addMonoidAlgebraEquivDirectSum {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] :
          AddMonoidAlgebra M ι ≃ DirectSum ι fun (x : ι) => M

          AddMonoidAlgebra.toDirectSum and DirectSum.toAddMonoidAlgebra together form an equiv.

          Equations
            Instances For
              source
              @[simp]
              theorem addMonoidAlgebraEquivDirectSum_symm_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] :
              ⇑addMonoidAlgebraEquivDirectSum.symm = DirectSum.toAddMonoidAlgebra
              source
              @[simp]
              theorem addMonoidAlgebraEquivDirectSum_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] :
              ⇑addMonoidAlgebraEquivDirectSum = AddMonoidAlgebra.toDirectSum
              source
              def addMonoidAlgebraAddEquivDirectSum {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] :
              AddMonoidAlgebra M ι ≃+ DirectSum ι fun (x : ι) => M

              The additive version of AddMonoidAlgebra.addMonoidAlgebraEquivDirectSum.

              Equations
                Instances For
                  source
                  @[simp]
                  theorem addMonoidAlgebraAddEquivDirectSum_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] :
                  ⇑addMonoidAlgebraAddEquivDirectSum = AddMonoidAlgebra.toDirectSum
                  source
                  @[simp]
                  theorem addMonoidAlgebraAddEquivDirectSum_symm_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] :
                  ⇑addMonoidAlgebraAddEquivDirectSum.symm = DirectSum.toAddMonoidAlgebra
                  source
                  def addMonoidAlgebraRingEquivDirectSum {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] :
                  AddMonoidAlgebra M ι ≃+* DirectSum ι fun (x : ι) => M

                  The ring version of AddMonoidAlgebra.addMonoidAlgebraEquivDirectSum.

                  Equations
                    Instances For
                      source
                      @[simp]
                      theorem addMonoidAlgebraRingEquivDirectSum_symm_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] :
                      ⇑addMonoidAlgebraRingEquivDirectSum.symm = DirectSum.toAddMonoidAlgebra
                      source
                      @[simp]
                      theorem addMonoidAlgebraRingEquivDirectSum_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] :
                      ⇑addMonoidAlgebraRingEquivDirectSum = AddMonoidAlgebra.toDirectSum
                      source
                      def addMonoidAlgebraAlgEquivDirectSum {ι : Type u_1} {R : Type u_2} {A : Type u_4} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] [Semiring A] [Algebra R A] [(m : A) → Decidable (m ≠ 0)] :
                      AddMonoidAlgebra A ι ≃ₐ[R] DirectSum ι fun (x : ι) => A

                      The algebra version of AddMonoidAlgebra.addMonoidAlgebraEquivDirectSum.

                      Equations
                        Instances For
                          source
                          @[simp]
                          theorem addMonoidAlgebraAlgEquivDirectSum_apply {ι : Type u_1} {R : Type u_2} {A : Type u_4} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] [Semiring A] [Algebra R A] [(m : A) → Decidable (m ≠ 0)] :
                          ⇑addMonoidAlgebraAlgEquivDirectSum = AddMonoidAlgebra.toDirectSum
                          source
                          @[simp]
                          theorem addMonoidAlgebraAlgEquivDirectSum_symm_apply {ι : Type u_1} {R : Type u_2} {A : Type u_4} [DecidableEq ι] [AddMonoid ι] [CommSemiring R] [Semiring A] [Algebra R A] [(m : A) → Decidable (m ≠ 0)] :
                          ⇑addMonoidAlgebraAlgEquivDirectSum.symm = DirectSum.toAddMonoidAlgebra
                          source
                          @[simp]
                          theorem AddMonoidAlgebra.toDirectSum_pow {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] (f : AddMonoidAlgebra M ι) (n : ℕ) :
                          (f ^ n).toDirectSum = f.toDirectSum ^ n
                          source
                          @[simp]
                          theorem DirectSum.toAddMonoidAlgebra_pow {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] (f : DirectSum ι fun (x : ι) => M) (n : ℕ) :
                          (f ^ n).toAddMonoidAlgebra = f.toAddMonoidAlgebra ^ n