Documentation

Mathlib.Algebra.MonoidAlgebra.ToDirectSum

Conversion between AddMonoidAlgebra and homogenous DirectSum #

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

Note that since direct_sum.has_mul 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 #

def AddMonoidAlgebra.toDirectSum {ι : Type u_1} {M : Type u_3} [Semiring M] (f : AddMonoidAlgebra M ι) :
⨁ (x : ι), M

Interpret an AddMonoidAlgebra as a homogenous DirectSum.

Instances For
    @[simp]
    theorem AddMonoidAlgebra.toDirectSum_single {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] (i : ι) (m : M) :
    (AddMonoidAlgebra.toDirectSum fun₀ | i => m) = ↑(DirectSum.of (fun i => M) i) m
    def DirectSum.toAddMonoidAlgebra {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m 0)] (f : ⨁ (x : ι), M) :

    Interpret a homogenous DirectSum as an AddMonoidAlgebra.

    Instances For
      @[simp]
      theorem DirectSum.toAddMonoidAlgebra_of {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m 0)] (i : ι) (m : M) :
      DirectSum.toAddMonoidAlgebra (↑(DirectSum.of (fun x => M) i) m) = fun₀ | i => m
      @[simp]
      theorem DirectSum.toAddMonoidAlgebra_toDirectSum {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m 0)] (f : ⨁ (x : ι), M) :

      Lemmas about arithmetic operations #

      @[simp]
      theorem DirectSum.toAddMonoidAlgebra_zero {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m 0)] :
      @[simp]
      theorem DirectSum.toAddMonoidAlgebra_add {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m 0)] (f : ⨁ (x : ι), M) (g : ⨁ (x : ι), M) :
      @[simp]
      theorem DirectSum.toAddMonoidAlgebra_mul {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] [(m : M) → Decidable (m 0)] (f : ⨁ (x : ι), M) (g : ⨁ (x : ι), M) :

      Bundled Equivs #

      @[simp]
      theorem addMonoidAlgebraEquivDirectSum_symm_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m 0)] :
      addMonoidAlgebraEquivDirectSum.symm = DirectSum.toAddMonoidAlgebra
      @[simp]
      theorem addMonoidAlgebraEquivDirectSum_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m 0)] :
      addMonoidAlgebraEquivDirectSum = AddMonoidAlgebra.toDirectSum
      def addMonoidAlgebraEquivDirectSum {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m 0)] :
      AddMonoidAlgebra M ι ⨁ (x : ι), M

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

      Instances For
        @[simp]
        theorem addMonoidAlgebraAddEquivDirectSum_symm_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m 0)] :
        ↑(AddEquiv.symm addMonoidAlgebraAddEquivDirectSum) = DirectSum.toAddMonoidAlgebra
        @[simp]
        theorem addMonoidAlgebraAddEquivDirectSum_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m 0)] :
        addMonoidAlgebraAddEquivDirectSum = AddMonoidAlgebra.toDirectSum
        def addMonoidAlgebraAddEquivDirectSum {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m 0)] :
        AddMonoidAlgebra M ι ≃+ ⨁ (x : ι), M

        The additive version of AddMonoidAlgebra.addMonoidAlgebraEquivDirectSum.

        Instances For
          @[simp]
          theorem addMonoidAlgebraRingEquivDirectSum_symm_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] [(m : M) → Decidable (m 0)] :
          ↑(RingEquiv.symm addMonoidAlgebraRingEquivDirectSum) = DirectSum.toAddMonoidAlgebra
          @[simp]
          theorem addMonoidAlgebraRingEquivDirectSum_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] [(m : M) → Decidable (m 0)] :
          addMonoidAlgebraRingEquivDirectSum = AddMonoidAlgebra.toDirectSum
          def addMonoidAlgebraRingEquivDirectSum {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] [(m : M) → Decidable (m 0)] :
          AddMonoidAlgebra M ι ≃+* ⨁ (x : ι), M

          The ring version of AddMonoidAlgebra.addMonoidAlgebraEquivDirectSum.

          Instances For
            @[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)] :
            ↑(AlgEquiv.symm addMonoidAlgebraAlgEquivDirectSum) = DirectSum.toAddMonoidAlgebra
            @[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
            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] ⨁ (x : ι), A

            The algebra version of AddMonoidAlgebra.addMonoidAlgebraEquivDirectSum.

            Instances For