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 #

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 homogenous DirectSum.

Equations
Instances For
    source
    @[simp]
    theorem AddMonoidAlgebra.toDirectSum_single {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] (i : ι) (m : M) :
    AddMonoidAlgebra.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 homogenous 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) :
      DirectSum.toAddMonoidAlgebra ((DirectSum.of (fun (x : ι) => M) i) m) = 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 ι) :
      DirectSum.toAddMonoidAlgebra (AddMonoidAlgebra.toDirectSum f) = 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) :
      AddMonoidAlgebra.toDirectSum (DirectSum.toAddMonoidAlgebra f) = f

      Lemmas about arithmetic operations #

      source
      @[simp]
      theorem AddMonoidAlgebra.toDirectSum_zero {ι : Type u_1} {M : Type u_3} [Semiring M] :
      AddMonoidAlgebra.toDirectSum 0 = 0
      source
      @[simp]
      theorem AddMonoidAlgebra.toDirectSum_add {ι : Type u_1} {M : Type u_3} [Semiring M] (f : AddMonoidAlgebra M ι) (g : AddMonoidAlgebra M ι) :
      AddMonoidAlgebra.toDirectSum (f + g) = AddMonoidAlgebra.toDirectSum f + AddMonoidAlgebra.toDirectSum g
      source
      @[simp]
      theorem AddMonoidAlgebra.toDirectSum_mul {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] (f : AddMonoidAlgebra M ι) (g : AddMonoidAlgebra M ι) :
      AddMonoidAlgebra.toDirectSum (f * g) = AddMonoidAlgebra.toDirectSum f * AddMonoidAlgebra.toDirectSum g
      source
      @[simp]
      theorem DirectSum.toAddMonoidAlgebra_zero {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] :
      DirectSum.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 : DirectSum ι fun (x : ι) => M) (g : DirectSum ι fun (x : ι) => M) :
      DirectSum.toAddMonoidAlgebra (f + g) = DirectSum.toAddMonoidAlgebra f + DirectSum.toAddMonoidAlgebra g
      source
      @[simp]
      theorem DirectSum.toAddMonoidAlgebra_mul {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddMonoid ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] (f : DirectSum ι fun (x : ι) => M) (g : DirectSum ι fun (x : ι) => M) :
      DirectSum.toAddMonoidAlgebra (f * g) = DirectSum.toAddMonoidAlgebra f * DirectSum.toAddMonoidAlgebra g

      Bundled Equivs #

      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 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
      • addMonoidAlgebraEquivDirectSum = let __src := finsuppEquivDFinsupp; { toFun := AddMonoidAlgebra.toDirectSum, invFun := DirectSum.toAddMonoidAlgebra, left_inv := ⋯, right_inv := ⋯ }
      Instances For
        source
        @[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
        source
        @[simp]
        theorem addMonoidAlgebraAddEquivDirectSum_apply {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [Semiring M] [(m : M) → Decidable (m ≠ 0)] :
        ⇑addMonoidAlgebraAddEquivDirectSum = 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
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[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
          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 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
          • One or more equations did not get rendered due to their size.
          Instances For
            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)] :
            ⇑(AlgEquiv.symm addMonoidAlgebraAlgEquivDirectSum) = DirectSum.toAddMonoidAlgebra
            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
            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
            • One or more equations did not get rendered due to their size.
            Instances For