Documentation

Mathlib.Algebra.MonoidAlgebra.Defs

Monoid algebras #

When the domain of a Finsupp has a multiplicative or additive structure, we can define a convolution product. To mathematicians this structure is known as the "monoid algebra", i.e. the finite formal linear combinations over a given semiring of elements of the monoid. The "group ring" ℤ[G] or the "group algebra" k[G] are typical uses.

In fact the construction of the "monoid algebra" makes sense when G is not even a monoid, but merely a magma, i.e., when G carries a multiplication which is not required to satisfy any conditions at all. In this case the construction yields a not-necessarily-unital, not-necessarily-associative algebra but it is still adjoint to the forgetful functor from such algebras to magmas, and we prove this as MonoidAlgebra.liftMagma.

In this file we define MonoidAlgebra k G := G →₀ k, and AddMonoidAlgebra k G in the same way, and then define the convolution product on these.

When the domain is additive, this is used to define polynomials:

Polynomial R := AddMonoidAlgebra R ℕ
MvPolynomial σ α := AddMonoidAlgebra R (σ →₀ ℕ)

When the domain is multiplicative, e.g. a group, this will be used to define the group ring.

Notation #

We introduce the notation R[A] for AddMonoidAlgebra R A.

Implementation note #

Unfortunately because additive and multiplicative structures both appear in both cases, it doesn't appear to be possible to make much use of to_additive, and we just settle for saying everything twice.

Similarly, I attempted to just define k[G] := MonoidAlgebra k (Multiplicative G), but the definitional equality Multiplicative G = G leaks through everywhere, and seems impossible to use.

Multiplicative monoids #

def MonoidAlgebra (k : Type u₁) (G : Type u₂) [Semiring k] :
Type (max u₁ u₂)

The monoid algebra over a semiring k generated by the monoid G. It is the type of finite formal k-linear combinations of terms of G, endowed with the convolution product.

Equations
Instances For
    Equations
    • =
    instance MonoidAlgebra.coeFun (k : Type u₁) (G : Type u₂) [Semiring k] :
    CoeFun (MonoidAlgebra k G) fun (x : MonoidAlgebra k G) => Gk
    Equations
    @[reducible, inline]
    abbrev MonoidAlgebra.single {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) (b : k) :
    Equations
    Instances For
      theorem MonoidAlgebra.single_zero {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) :
      theorem MonoidAlgebra.single_add {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) (b₁ : k) (b₂ : k) :
      @[simp]
      theorem MonoidAlgebra.sum_single_index {k : Type u₁} {G : Type u₂} [Semiring k] {N : Type u_3} [AddCommMonoid N] {a : G} {b : k} {h : GkN} (h_zero : h a 0 = 0) :
      @[simp]
      theorem MonoidAlgebra.sum_single {k : Type u₁} {G : Type u₂} [Semiring k] (f : MonoidAlgebra k G) :
      Finsupp.sum f MonoidAlgebra.single = f
      theorem MonoidAlgebra.single_apply {k : Type u₁} {G : Type u₂} [Semiring k] {a : G} {a' : G} {b : k} [Decidable (a = a')] :
      (MonoidAlgebra.single a b) a' = if a = a' then b else 0
      @[simp]
      theorem MonoidAlgebra.single_eq_zero {k : Type u₁} {G : Type u₂} [Semiring k] {a : G} {b : k} :
      @[reducible, inline]
      abbrev MonoidAlgebra.mapDomain {k : Type u₁} {G : Type u₂} [Semiring k] {G' : Type u_3} (f : GG') (v : MonoidAlgebra k G) :
      Equations
      Instances For
        theorem MonoidAlgebra.mapDomain_sum {k : Type u₁} {G : Type u₂} [Semiring k] {k' : Type u_3} {G' : Type u_4} [Semiring k'] {f : GG'} {s : MonoidAlgebra k' G} {v : Gk'MonoidAlgebra k G} :
        MonoidAlgebra.mapDomain f (Finsupp.sum s v) = Finsupp.sum s fun (a : G) (b : k') => MonoidAlgebra.mapDomain f (v a b)
        def MonoidAlgebra.liftNC {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [NonUnitalNonAssocSemiring R] (f : k →+ R) (g : GR) :

        A non-commutative version of MonoidAlgebra.lift: given an additive homomorphism f : k →+ R and a homomorphism g : G → R, returns the additive homomorphism from MonoidAlgebra k G such that liftNC f g (single a b) = f b * g a. If f is a ring homomorphism and the range of either f or g is in center of R, then the result is a ring homomorphism. If R is a k-algebra and f = algebraMap k R, then the result is an algebra homomorphism called MonoidAlgebra.lift.

        Equations
        Instances For
          @[simp]
          theorem MonoidAlgebra.liftNC_single {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [NonUnitalNonAssocSemiring R] (f : k →+ R) (g : GR) (a : G) (b : k) :
          @[irreducible]
          def MonoidAlgebra.mul' {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] (f : MonoidAlgebra k G) (g : MonoidAlgebra k G) :

          The multiplication in a monoid algebra. We make it irreducible so that Lean doesn't unfold it trying to unify two things that are different.

          Equations
          Instances For
            instance MonoidAlgebra.instMul {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] :

            The product of f g : MonoidAlgebra k G is the finitely supported function whose value at a is the sum of f x * g y over all pairs x, y such that x * y = a. (Think of the group ring of a group.)

            Equations
            • MonoidAlgebra.instMul = { mul := MonoidAlgebra.mul' }
            theorem MonoidAlgebra.mul_def {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] {f : MonoidAlgebra k G} {g : MonoidAlgebra k G} :
            f * g = Finsupp.sum f fun (a₁ : G) (b₁ : k) => Finsupp.sum g fun (a₂ : G) (b₂ : k) => MonoidAlgebra.single (a₁ * a₂) (b₁ * b₂)
            Equations
            theorem MonoidAlgebra.liftNC_mul {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [Mul G] [Semiring R] {g_hom : Type u_3} [FunLike g_hom G R] [MulHomClass g_hom G R] (f : k →+* R) (g : g_hom) (a : MonoidAlgebra k G) (b : MonoidAlgebra k G) (h_comm : ∀ {x y : G}, y a.supportCommute (f (b x)) (g y)) :
            (MonoidAlgebra.liftNC f g) (a * b) = (MonoidAlgebra.liftNC f g) a * (MonoidAlgebra.liftNC f g) b
            Equations
            instance MonoidAlgebra.one {k : Type u₁} {G : Type u₂} [Semiring k] [One G] :

            The unit of the multiplication is single 1 1, i.e. the function that is 1 at 1 and zero elsewhere.

            Equations
            theorem MonoidAlgebra.one_def {k : Type u₁} {G : Type u₂} [Semiring k] [One G] :
            @[simp]
            theorem MonoidAlgebra.liftNC_one {k : Type u₁} {G : Type u₂} {R : Type u_2} [NonAssocSemiring R] [Semiring k] [One G] {g_hom : Type u_3} [FunLike g_hom G R] [OneHomClass g_hom G R] (f : k →+* R) (g : g_hom) :
            (MonoidAlgebra.liftNC f g) 1 = 1
            Equations
            theorem MonoidAlgebra.natCast_def {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] (n : ) :
            @[deprecated MonoidAlgebra.natCast_def]
            theorem MonoidAlgebra.nat_cast_def {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] (n : ) :

            Alias of MonoidAlgebra.natCast_def.

            Semiring structure #

            instance MonoidAlgebra.semiring {k : Type u₁} {G : Type u₂} [Semiring k] [Monoid G] :
            Equations
            • MonoidAlgebra.semiring = Semiring.mk npowRecAuto
            def MonoidAlgebra.liftNCRingHom {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [Monoid G] [Semiring R] (f : k →+* R) (g : G →* R) (h_comm : ∀ (x : k) (y : G), Commute (f x) (g y)) :

            liftNC as a RingHom, for when f x and g y commute

            Equations
            Instances For
              Equations
              instance MonoidAlgebra.nontrivial {k : Type u₁} {G : Type u₂} [Semiring k] [Nontrivial k] [Nonempty G] :
              Equations
              • =

              Derived instances #

              Equations
              instance MonoidAlgebra.unique {k : Type u₁} {G : Type u₂} [Semiring k] [Subsingleton k] :
              Equations
              • MonoidAlgebra.unique = Finsupp.uniqueOfRight
              instance MonoidAlgebra.addCommGroup {k : Type u₁} {G : Type u₂} [Ring k] :
              Equations
              • MonoidAlgebra.addCommGroup = Finsupp.instAddCommGroup
              Equations
              instance MonoidAlgebra.nonUnitalRing {k : Type u₁} {G : Type u₂} [Ring k] [Semigroup G] :
              Equations
              instance MonoidAlgebra.nonAssocRing {k : Type u₁} {G : Type u₂} [Ring k] [MulOneClass G] :
              Equations
              theorem MonoidAlgebra.intCast_def {k : Type u₁} {G : Type u₂} [Ring k] [MulOneClass G] (z : ) :
              @[deprecated MonoidAlgebra.intCast_def]
              theorem MonoidAlgebra.int_cast_def {k : Type u₁} {G : Type u₂} [Ring k] [MulOneClass G] (z : ) :

              Alias of MonoidAlgebra.intCast_def.

              instance MonoidAlgebra.ring {k : Type u₁} {G : Type u₂} [Ring k] [Monoid G] :
              Equations
              • MonoidAlgebra.ring = Ring.mk SubNegMonoid.zsmul
              Equations
              instance MonoidAlgebra.commRing {k : Type u₁} {G : Type u₂} [CommRing k] [CommMonoid G] :
              Equations
              instance MonoidAlgebra.smulZeroClass {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [SMulZeroClass R k] :
              Equations
              • MonoidAlgebra.smulZeroClass = Finsupp.smulZeroClass
              instance MonoidAlgebra.distribSMul {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [DistribSMul R k] :
              Equations
              instance MonoidAlgebra.distribMulAction {k : Type u₁} {G : Type u₂} {R : Type u_2} [Monoid R] [Semiring k] [DistribMulAction R k] :
              Equations
              instance MonoidAlgebra.module {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring R] [Semiring k] [Module R k] :
              Equations
              instance MonoidAlgebra.faithfulSMul {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [SMulZeroClass R k] [FaithfulSMul R k] [Nonempty G] :
              Equations
              • =
              instance MonoidAlgebra.isScalarTower {k : Type u₁} {G : Type u₂} {R : Type u_2} {S : Type u_3} [Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMul R S] [IsScalarTower R S k] :
              Equations
              • =
              instance MonoidAlgebra.smulCommClass {k : Type u₁} {G : Type u₂} {R : Type u_2} {S : Type u_3} [Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMulCommClass R S k] :
              Equations
              • =
              Equations
              • =

              This is not an instance as it conflicts with MonoidAlgebra.distribMulAction when G = kˣ.

              Equations
              • MonoidAlgebra.comapDistribMulActionSelf = Finsupp.comapDistribMulAction
              Instances For

                Copies of ext lemmas and bundled singles from Finsupp #

                As MonoidAlgebra is a type synonym, ext will not unfold it to find ext lemmas. We need bundled version of Finsupp.single with the right types to state these lemmas. It is good practice to have those, regardless of the ext issue.

                theorem MonoidAlgebra.ext_iff {k : Type u₁} {G : Type u₂} [Semiring k] {f : MonoidAlgebra k G} {g : MonoidAlgebra k G} :
                f = g ∀ (x : G), f x = g x
                theorem MonoidAlgebra.ext {k : Type u₁} {G : Type u₂} [Semiring k] ⦃f : MonoidAlgebra k G ⦃g : MonoidAlgebra k G (H : ∀ (x : G), f x = g x) :
                f = g

                A copy of Finsupp.ext for MonoidAlgebra.

                @[reducible, inline]
                abbrev MonoidAlgebra.singleAddHom {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) :

                A copy of Finsupp.singleAddHom for MonoidAlgebra.

                Equations
                Instances For
                  @[simp]
                  theorem MonoidAlgebra.singleAddHom_apply {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) (b : k) :
                  theorem MonoidAlgebra.addHom_ext'_iff {k : Type u₁} {G : Type u₂} {N : Type u_3} [Semiring k] [AddZeroClass N] {f : MonoidAlgebra k G →+ N} {g : MonoidAlgebra k G →+ N} :
                  f = g ∀ (x : G), f.comp (MonoidAlgebra.singleAddHom x) = g.comp (MonoidAlgebra.singleAddHom x)
                  theorem MonoidAlgebra.addHom_ext' {k : Type u₁} {G : Type u₂} {N : Type u_3} [Semiring k] [AddZeroClass N] ⦃f : MonoidAlgebra k G →+ N ⦃g : MonoidAlgebra k G →+ N (H : ∀ (x : G), f.comp (MonoidAlgebra.singleAddHom x) = g.comp (MonoidAlgebra.singleAddHom x)) :
                  f = g

                  A copy of Finsupp.addHom_ext' for MonoidAlgebra.

                  theorem MonoidAlgebra.distribMulActionHom_ext'_iff {k : Type u₁} {G : Type u₂} {R : Type u_2} {N : Type u_3} [Monoid R] [Semiring k] [AddMonoid N] [DistribMulAction R N] [DistribMulAction R k] {f : MonoidAlgebra k G →+[R] N} {g : MonoidAlgebra k G →+[R] N} :
                  theorem MonoidAlgebra.distribMulActionHom_ext' {k : Type u₁} {G : Type u₂} {R : Type u_2} {N : Type u_3} [Monoid R] [Semiring k] [AddMonoid N] [DistribMulAction R N] [DistribMulAction R k] {f : MonoidAlgebra k G →+[R] N} {g : MonoidAlgebra k G →+[R] N} (h : ∀ (a : G), f.comp (Finsupp.DistribMulActionHom.single a) = g.comp (Finsupp.DistribMulActionHom.single a)) :
                  f = g

                  A copy of Finsupp.distribMulActionHom_ext' for MonoidAlgebra.

                  @[reducible, inline]
                  abbrev MonoidAlgebra.lsingle {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring R] [Semiring k] [Module R k] (a : G) :

                  A copy of Finsupp.lsingle for MonoidAlgebra.

                  Equations
                  Instances For
                    @[simp]
                    theorem MonoidAlgebra.lsingle_apply {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring R] [Semiring k] [Module R k] (a : G) (b : k) :
                    theorem MonoidAlgebra.lhom_ext'_iff {k : Type u₁} {G : Type u₂} {R : Type u_2} {N : Type u_3} [Semiring R] [Semiring k] [AddCommMonoid N] [Module R N] [Module R k] {f : MonoidAlgebra k G →ₗ[R] N} {g : MonoidAlgebra k G →ₗ[R] N} :
                    f = g ∀ (x : G), f ∘ₗ MonoidAlgebra.lsingle x = g ∘ₗ MonoidAlgebra.lsingle x
                    theorem MonoidAlgebra.lhom_ext' {k : Type u₁} {G : Type u₂} {R : Type u_2} {N : Type u_3} [Semiring R] [Semiring k] [AddCommMonoid N] [Module R N] [Module R k] ⦃f : MonoidAlgebra k G →ₗ[R] N ⦃g : MonoidAlgebra k G →ₗ[R] N (H : ∀ (x : G), f ∘ₗ MonoidAlgebra.lsingle x = g ∘ₗ MonoidAlgebra.lsingle x) :
                    f = g

                    A copy of Finsupp.lhom_ext' for MonoidAlgebra.

                    theorem MonoidAlgebra.mul_apply {k : Type u₁} {G : Type u₂} [Semiring k] [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) (g : MonoidAlgebra k G) (x : G) :
                    (f * g) x = Finsupp.sum f fun (a₁ : G) (b₁ : k) => Finsupp.sum g fun (a₂ : G) (b₂ : k) => if a₁ * a₂ = x then b₁ * b₂ else 0
                    theorem MonoidAlgebra.mul_apply_antidiagonal {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] (f : MonoidAlgebra k G) (g : MonoidAlgebra k G) (x : G) (s : Finset (G × G)) (hs : ∀ {p : G × G}, p s p.1 * p.2 = x) :
                    (f * g) x = ps, f p.1 * g p.2
                    @[simp]
                    theorem MonoidAlgebra.single_mul_single {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] {a₁ : G} {a₂ : G} {b₁ : k} {b₂ : k} :
                    MonoidAlgebra.single a₁ b₁ * MonoidAlgebra.single a₂ b₂ = MonoidAlgebra.single (a₁ * a₂) (b₁ * b₂)
                    theorem MonoidAlgebra.single_commute_single {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] {a₁ : G} {a₂ : G} {b₁ : k} {b₂ : k} (ha : Commute a₁ a₂) (hb : Commute b₁ b₂) :
                    theorem MonoidAlgebra.single_commute {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] {a : G} {b : k} (ha : ∀ (a' : G), Commute a a') (hb : ∀ (b' : k), Commute b b') (f : MonoidAlgebra k G) :
                    @[simp]
                    theorem MonoidAlgebra.single_pow {k : Type u₁} {G : Type u₂} [Semiring k] [Monoid G] {a : G} {b : k} (n : ) :
                    @[simp]
                    theorem MonoidAlgebra.mapDomain_one {α : Type u_3} {β : Type u_4} {α₂ : Type u_5} [Semiring β] [One α] [One α₂] {F : Type u_6} [FunLike F α α₂] [OneHomClass F α α₂] (f : F) :

                    Like Finsupp.mapDomain_zero, but for the 1 we define in this file

                    theorem MonoidAlgebra.mapDomain_mul {α : Type u_3} {β : Type u_4} {α₂ : Type u_5} [Semiring β] [Mul α] [Mul α₂] {F : Type u_6} [FunLike F α α₂] [MulHomClass F α α₂] (f : F) (x : MonoidAlgebra β α) (y : MonoidAlgebra β α) :

                    Like Finsupp.mapDomain_add, but for the convolutive multiplication we define in this file

                    @[simp]
                    theorem MonoidAlgebra.ofMagma_apply (k : Type u₁) (G : Type u₂) [Semiring k] [Mul G] (a : G) :
                    def MonoidAlgebra.ofMagma (k : Type u₁) (G : Type u₂) [Semiring k] [Mul G] :

                    The embedding of a magma into its magma algebra.

                    Equations
                    Instances For
                      @[simp]
                      theorem MonoidAlgebra.of_apply (k : Type u₁) (G : Type u₂) [Semiring k] [MulOneClass G] (a : G) :
                      def MonoidAlgebra.of (k : Type u₁) (G : Type u₂) [Semiring k] [MulOneClass G] :

                      The embedding of a unital magma into its magma algebra.

                      Equations
                      Instances For
                        @[simp]
                        theorem MonoidAlgebra.smul_single' {k : Type u₁} {G : Type u₂} [Semiring k] (c : k) (a : G) (b : k) :

                        Copy of Finsupp.smul_single' that avoids the MonoidAlgebra = Finsupp defeq abuse.

                        theorem MonoidAlgebra.smul_of {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] (g : G) (r : k) :
                        theorem MonoidAlgebra.of_commute {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] {a : G} (h : ∀ (a' : G), Commute a a') (f : MonoidAlgebra k G) :
                        @[simp]
                        theorem MonoidAlgebra.singleHom_apply {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] (a : k × G) :
                        MonoidAlgebra.singleHom a = MonoidAlgebra.single a.2 a.1
                        def MonoidAlgebra.singleHom {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] :

                        Finsupp.single as a MonoidHom from the product type into the monoid algebra.

                        Note the order of the elements of the product are reversed compared to the arguments of Finsupp.single.

                        Equations
                        • MonoidAlgebra.singleHom = { toFun := fun (a : k × G) => MonoidAlgebra.single a.2 a.1, map_one' := , map_mul' := }
                        Instances For
                          theorem MonoidAlgebra.mul_single_apply_aux {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] (f : MonoidAlgebra k G) {r : k} {x : G} {y : G} {z : G} (H : ∀ (a : G), a * x = z a = y) :
                          (f * MonoidAlgebra.single x r) z = f y * r
                          theorem MonoidAlgebra.mul_single_one_apply {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] (f : MonoidAlgebra k G) (r : k) (x : G) :
                          (f * MonoidAlgebra.single 1 r) x = f x * r
                          theorem MonoidAlgebra.mul_single_apply_of_not_exists_mul {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] (r : k) {g : G} {g' : G} (x : MonoidAlgebra k G) (h : ¬∃ (d : G), g' = d * g) :
                          (x * MonoidAlgebra.single g r) g' = 0
                          theorem MonoidAlgebra.single_mul_apply_aux {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] (f : MonoidAlgebra k G) {r : k} {x : G} {y : G} {z : G} (H : ∀ (a : G), x * a = y a = z) :
                          (MonoidAlgebra.single x r * f) y = r * f z
                          theorem MonoidAlgebra.single_one_mul_apply {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] (f : MonoidAlgebra k G) (r : k) (x : G) :
                          (MonoidAlgebra.single 1 r * f) x = r * f x
                          theorem MonoidAlgebra.single_mul_apply_of_not_exists_mul {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] (r : k) {g : G} {g' : G} (x : MonoidAlgebra k G) (h : ¬∃ (d : G), g' = g * d) :
                          (MonoidAlgebra.single g r * x) g' = 0
                          theorem MonoidAlgebra.liftNC_smul {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] {R : Type u_3} [Semiring R] (f : k →+* R) (g : G →* R) (c : k) (φ : MonoidAlgebra k G) :
                          (MonoidAlgebra.liftNC f g) (c φ) = f c * (MonoidAlgebra.liftNC f g) φ

                          Non-unital, non-associative algebra structure #

                          instance MonoidAlgebra.isScalarTower_self (k : Type u₁) {G : Type u₂} {R : Type u_2} [Semiring k] [DistribSMul R k] [Mul G] [IsScalarTower R k k] :
                          Equations
                          • =
                          instance MonoidAlgebra.smulCommClass_self (k : Type u₁) {G : Type u₂} {R : Type u_2} [Semiring k] [DistribSMul R k] [Mul G] [SMulCommClass R k k] :

                          Note that if k is a CommSemiring then we have SMulCommClass k k k and so we can take R = k in the below. In other words, if the coefficients are commutative amongst themselves, they also commute with the algebra multiplication.

                          Equations
                          • =
                          instance MonoidAlgebra.smulCommClass_symm_self (k : Type u₁) {G : Type u₂} {R : Type u_2} [Semiring k] [DistribSMul R k] [Mul G] [SMulCommClass k R k] :
                          Equations
                          • =
                          @[simp]
                          theorem MonoidAlgebra.singleOneRingHom_apply {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] :
                          ∀ (a : k), MonoidAlgebra.singleOneRingHom a = (↑(Finsupp.singleAddHom 1)).toFun a

                          Finsupp.single 1 as a RingHom

                          Equations
                          • MonoidAlgebra.singleOneRingHom = { toFun := (↑(Finsupp.singleAddHom 1)).toFun, map_one' := , map_mul' := , map_zero' := , map_add' := }
                          Instances For
                            @[simp]
                            theorem MonoidAlgebra.mapDomainRingHom_apply {G : Type u₂} (k : Type u_3) {H : Type u_4} {F : Type u_5} [Semiring k] [Monoid G] [Monoid H] [FunLike F G H] [MonoidHomClass F G H] (f : F) :
                            ∀ (a : G →₀ k), (MonoidAlgebra.mapDomainRingHom k f) a = (↑(Finsupp.mapDomain.addMonoidHom f)).toFun a
                            def MonoidAlgebra.mapDomainRingHom {G : Type u₂} (k : Type u_3) {H : Type u_4} {F : Type u_5} [Semiring k] [Monoid G] [Monoid H] [FunLike F G H] [MonoidHomClass F G H] (f : F) :

                            If f : G → H is a multiplicative homomorphism between two monoids, then Finsupp.mapDomain f is a ring homomorphism between their monoid algebras.

                            Equations
                            Instances For
                              theorem MonoidAlgebra.ringHom_ext {k : Type u₁} {G : Type u₂} {R : Type u_3} [Semiring k] [MulOneClass G] [Semiring R] {f : MonoidAlgebra k G →+* R} {g : MonoidAlgebra k G →+* R} (h₁ : ∀ (b : k), f (MonoidAlgebra.single 1 b) = g (MonoidAlgebra.single 1 b)) (h_of : ∀ (a : G), f (MonoidAlgebra.single a 1) = g (MonoidAlgebra.single a 1)) :
                              f = g

                              If two ring homomorphisms from MonoidAlgebra k G are equal on all single a 1 and single 1 b, then they are equal.

                              theorem MonoidAlgebra.ringHom_ext'_iff {k : Type u₁} {G : Type u₂} {R : Type u_3} [Semiring k] [MulOneClass G] [Semiring R] {f : MonoidAlgebra k G →+* R} {g : MonoidAlgebra k G →+* R} :
                              f = g f.comp MonoidAlgebra.singleOneRingHom = g.comp MonoidAlgebra.singleOneRingHom (↑f).comp (MonoidAlgebra.of k G) = (↑g).comp (MonoidAlgebra.of k G)
                              theorem MonoidAlgebra.ringHom_ext' {k : Type u₁} {G : Type u₂} {R : Type u_3} [Semiring k] [MulOneClass G] [Semiring R] {f : MonoidAlgebra k G →+* R} {g : MonoidAlgebra k G →+* R} (h₁ : f.comp MonoidAlgebra.singleOneRingHom = g.comp MonoidAlgebra.singleOneRingHom) (h_of : (↑f).comp (MonoidAlgebra.of k G) = (↑g).comp (MonoidAlgebra.of k G)) :
                              f = g

                              If two ring homomorphisms from MonoidAlgebra k G are equal on all single a 1 and single 1 b, then they are equal.

                              See note [partially-applied ext lemmas].

                              theorem MonoidAlgebra.induction_on {k : Type u₁} {G : Type u₂} [Semiring k] [Monoid G] {p : MonoidAlgebra k GProp} (f : MonoidAlgebra k G) (hM : ∀ (g : G), p ((MonoidAlgebra.of k G) g)) (hadd : ∀ (f g : MonoidAlgebra k G), p fp gp (f + g)) (hsmul : ∀ (r : k) (f : MonoidAlgebra k G), p fp (r f)) :
                              p f
                              theorem MonoidAlgebra.prod_single {k : Type u₁} {G : Type u₂} {ι : Type ui} [CommSemiring k] [CommMonoid G] {s : Finset ι} {a : ιG} {b : ιk} :
                              is, MonoidAlgebra.single (a i) (b i) = MonoidAlgebra.single (∏ is, a i) (∏ is, b i)
                              @[simp]
                              theorem MonoidAlgebra.mul_single_apply {k : Type u₁} {G : Type u₂} [Semiring k] [Group G] (f : MonoidAlgebra k G) (r : k) (x : G) (y : G) :
                              (f * MonoidAlgebra.single x r) y = f (y * x⁻¹) * r
                              @[simp]
                              theorem MonoidAlgebra.single_mul_apply {k : Type u₁} {G : Type u₂} [Semiring k] [Group G] (r : k) (x : G) (f : MonoidAlgebra k G) (y : G) :
                              (MonoidAlgebra.single x r * f) y = r * f (x⁻¹ * y)
                              theorem MonoidAlgebra.mul_apply_left {k : Type u₁} {G : Type u₂} [Semiring k] [Group G] (f : MonoidAlgebra k G) (g : MonoidAlgebra k G) (x : G) :
                              (f * g) x = Finsupp.sum f fun (a : G) (b : k) => b * g (a⁻¹ * x)
                              theorem MonoidAlgebra.mul_apply_right {k : Type u₁} {G : Type u₂} [Semiring k] [Group G] (f : MonoidAlgebra k G) (g : MonoidAlgebra k G) (x : G) :
                              (f * g) x = Finsupp.sum g fun (a : G) (b : k) => f (x * a⁻¹) * b
                              @[simp]
                              theorem MonoidAlgebra.opRingEquiv_apply {k : Type u₁} {G : Type u₂} [Semiring k] [Monoid G] :
                              ∀ (a : (G →₀ k)ᵐᵒᵖ), MonoidAlgebra.opRingEquiv a = Finsupp.equivMapDomain MulOpposite.opEquiv (Finsupp.mapRange MulOpposite.op (MulOpposite.unop a))
                              @[simp]
                              theorem MonoidAlgebra.opRingEquiv_symm_apply {k : Type u₁} {G : Type u₂} [Semiring k] [Monoid G] :
                              ∀ (a : Gᵐᵒᵖ →₀ kᵐᵒᵖ), MonoidAlgebra.opRingEquiv.symm a = MulOpposite.op (Finsupp.mapRange MulOpposite.unop (Finsupp.equivMapDomain MulOpposite.opEquiv.symm a))

                              The opposite of a MonoidAlgebra R I equivalent as a ring to the MonoidAlgebra Rᵐᵒᵖ Iᵐᵒᵖ over the opposite ring, taking elements to their opposite.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                theorem MonoidAlgebra.opRingEquiv_single {k : Type u₁} {G : Type u₂} [Semiring k] [Monoid G] (r : k) (x : G) :
                                def MonoidAlgebra.submoduleOfSMulMem {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {V : Type u_3} [AddCommMonoid V] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] (W : Submodule k V) (h : ∀ (g : G), vW, (MonoidAlgebra.of k G) g v W) :

                                A submodule over k which is stable under scalar multiplication by elements of G is a submodule over MonoidAlgebra k G

                                Equations
                                Instances For

                                  Additive monoids #

                                  def AddMonoidAlgebra (k : Type u₁) (G : Type u₂) [Semiring k] :
                                  Type (max u₂ u₁)

                                  The monoid algebra over a semiring k generated by the additive monoid G. It is the type of finite formal k-linear combinations of terms of G, endowed with the convolution product.

                                  Equations
                                  Instances For

                                    The monoid algebra over a semiring k generated by the additive monoid G. It is the type of finite formal k-linear combinations of terms of G, endowed with the convolution product.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      Equations
                                      • =
                                      instance AddMonoidAlgebra.coeFun (k : Type u₁) (G : Type u₂) [Semiring k] :
                                      CoeFun (AddMonoidAlgebra k G) fun (x : AddMonoidAlgebra k G) => Gk
                                      Equations
                                      @[reducible, inline]
                                      abbrev AddMonoidAlgebra.single {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) (b : k) :
                                      Equations
                                      Instances For
                                        theorem AddMonoidAlgebra.single_zero {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) :
                                        theorem AddMonoidAlgebra.single_add {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) (b₁ : k) (b₂ : k) :
                                        @[simp]
                                        theorem AddMonoidAlgebra.sum_single_index {k : Type u₁} {G : Type u₂} [Semiring k] {N : Type u_3} [AddCommMonoid N] {a : G} {b : k} {h : GkN} (h_zero : h a 0 = 0) :
                                        @[simp]
                                        theorem AddMonoidAlgebra.sum_single {k : Type u₁} {G : Type u₂} [Semiring k] (f : AddMonoidAlgebra k G) :
                                        Finsupp.sum f AddMonoidAlgebra.single = f
                                        theorem AddMonoidAlgebra.single_apply {k : Type u₁} {G : Type u₂} [Semiring k] {a : G} {a' : G} {b : k} [Decidable (a = a')] :
                                        (AddMonoidAlgebra.single a b) a' = if a = a' then b else 0
                                        @[simp]
                                        theorem AddMonoidAlgebra.single_eq_zero {k : Type u₁} {G : Type u₂} [Semiring k] {a : G} {b : k} :
                                        @[reducible, inline]
                                        abbrev AddMonoidAlgebra.mapDomain {k : Type u₁} {G : Type u₂} [Semiring k] {G' : Type u_3} (f : GG') (v : AddMonoidAlgebra k G) :
                                        Equations
                                        Instances For
                                          theorem AddMonoidAlgebra.mapDomain_sum {k : Type u₁} {G : Type u₂} [Semiring k] {k' : Type u_3} {G' : Type u_4} [Semiring k'] {f : GG'} {s : AddMonoidAlgebra k' G} {v : Gk'AddMonoidAlgebra k G} :
                                          theorem AddMonoidAlgebra.mapDomain_single {k : Type u₁} {G : Type u₂} [Semiring k] {G' : Type u_3} {f : GG'} {a : G} {b : k} :
                                          def AddMonoidAlgebra.liftNC {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [NonUnitalNonAssocSemiring R] (f : k →+ R) (g : Multiplicative GR) :

                                          A non-commutative version of AddMonoidAlgebra.lift: given an additive homomorphism f : k →+ R and a map g : Multiplicative G → R, returns the additive homomorphism from k[G] such that liftNC f g (single a b) = f b * g a. If f is a ring homomorphism and the range of either f or g is in center of R, then the result is a ring homomorphism. If R is a k-algebra and f = algebraMap k R, then the result is an algebra homomorphism called AddMonoidAlgebra.lift.

                                          Equations
                                          Instances For
                                            @[simp]
                                            theorem AddMonoidAlgebra.liftNC_single {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [NonUnitalNonAssocSemiring R] (f : k →+ R) (g : Multiplicative GR) (a : G) (b : k) :
                                            (AddMonoidAlgebra.liftNC f g) (AddMonoidAlgebra.single a b) = f b * g (Multiplicative.ofAdd a)
                                            instance AddMonoidAlgebra.hasMul {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] :

                                            The product of f g : k[G] is the finitely supported function whose value at a is the sum of f x * g y over all pairs x, y such that x + y = a. (Think of the product of multivariate polynomials where α is the additive monoid of monomial exponents.)

                                            Equations
                                            theorem AddMonoidAlgebra.mul_def {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] {f : AddMonoidAlgebra k G} {g : AddMonoidAlgebra k G} :
                                            f * g = Finsupp.sum f fun (a₁ : G) (b₁ : k) => Finsupp.sum g fun (a₂ : G) (b₂ : k) => AddMonoidAlgebra.single (a₁ + a₂) (b₁ * b₂)
                                            Equations
                                            theorem AddMonoidAlgebra.liftNC_mul {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [Add G] [Semiring R] {g_hom : Type u_3} [FunLike g_hom (Multiplicative G) R] [MulHomClass g_hom (Multiplicative G) R] (f : k →+* R) (g : g_hom) (a : AddMonoidAlgebra k G) (b : AddMonoidAlgebra k G) (h_comm : ∀ {x y : G}, y a.supportCommute (f (b x)) (g (Multiplicative.ofAdd y))) :
                                            (AddMonoidAlgebra.liftNC f g) (a * b) = (AddMonoidAlgebra.liftNC f g) a * (AddMonoidAlgebra.liftNC f g) b
                                            instance AddMonoidAlgebra.one {k : Type u₁} {G : Type u₂} [Semiring k] [Zero G] :

                                            The unit of the multiplication is single 0 1, i.e. the function that is 1 at 0 and zero elsewhere.

                                            Equations
                                            theorem AddMonoidAlgebra.one_def {k : Type u₁} {G : Type u₂} [Semiring k] [Zero G] :
                                            @[simp]
                                            theorem AddMonoidAlgebra.liftNC_one {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [Zero G] [NonAssocSemiring R] {g_hom : Type u_3} [FunLike g_hom (Multiplicative G) R] [OneHomClass g_hom (Multiplicative G) R] (f : k →+* R) (g : g_hom) :
                                            (AddMonoidAlgebra.liftNC f g) 1 = 1
                                            Equations
                                            Equations
                                            theorem AddMonoidAlgebra.natCast_def {k : Type u₁} {G : Type u₂} [Semiring k] [AddZeroClass G] (n : ) :
                                            @[deprecated AddMonoidAlgebra.natCast_def]
                                            theorem AddMonoidAlgebra.nat_cast_def {k : Type u₁} {G : Type u₂} [Semiring k] [AddZeroClass G] (n : ) :

                                            Alias of AddMonoidAlgebra.natCast_def.

                                            Semiring structure #

                                            instance AddMonoidAlgebra.smulZeroClass {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [SMulZeroClass R k] :
                                            Equations
                                            • AddMonoidAlgebra.smulZeroClass = Finsupp.smulZeroClass
                                            instance AddMonoidAlgebra.semiring {k : Type u₁} {G : Type u₂} [Semiring k] [AddMonoid G] :
                                            Equations
                                            • AddMonoidAlgebra.semiring = Semiring.mk npowRecAuto
                                            def AddMonoidAlgebra.liftNCRingHom {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [AddMonoid G] [Semiring R] (f : k →+* R) (g : Multiplicative G →* R) (h_comm : ∀ (x : k) (y : Multiplicative G), Commute (f x) (g y)) :

                                            liftNC as a RingHom, for when f and g commute

                                            Equations
                                            Instances For
                                              Equations
                                              Equations
                                              • =

                                              Derived instances #

                                              Equations
                                              instance AddMonoidAlgebra.unique {k : Type u₁} {G : Type u₂} [Semiring k] [Subsingleton k] :
                                              Equations
                                              • AddMonoidAlgebra.unique = Finsupp.uniqueOfRight
                                              instance AddMonoidAlgebra.addCommGroup {k : Type u₁} {G : Type u₂} [Ring k] :
                                              Equations
                                              • AddMonoidAlgebra.addCommGroup = Finsupp.instAddCommGroup
                                              Equations
                                              Equations
                                              Equations
                                              theorem AddMonoidAlgebra.intCast_def {k : Type u₁} {G : Type u₂} [Ring k] [AddZeroClass G] (z : ) :
                                              @[deprecated AddMonoidAlgebra.intCast_def]
                                              theorem AddMonoidAlgebra.int_cast_def {k : Type u₁} {G : Type u₂} [Ring k] [AddZeroClass G] (z : ) :

                                              Alias of AddMonoidAlgebra.intCast_def.

                                              instance AddMonoidAlgebra.ring {k : Type u₁} {G : Type u₂} [Ring k] [AddMonoid G] :
                                              Equations
                                              • AddMonoidAlgebra.ring = Ring.mk SubNegMonoid.zsmul
                                              Equations
                                              instance AddMonoidAlgebra.commRing {k : Type u₁} {G : Type u₂} [CommRing k] [AddCommMonoid G] :
                                              Equations
                                              instance AddMonoidAlgebra.distribSMul {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [DistribSMul R k] :
                                              Equations
                                              instance AddMonoidAlgebra.distribMulAction {k : Type u₁} {G : Type u₂} {R : Type u_2} [Monoid R] [Semiring k] [DistribMulAction R k] :
                                              Equations
                                              instance AddMonoidAlgebra.faithfulSMul {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [SMulZeroClass R k] [FaithfulSMul R k] [Nonempty G] :
                                              Equations
                                              • =
                                              instance AddMonoidAlgebra.module {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring R] [Semiring k] [Module R k] :
                                              Equations
                                              instance AddMonoidAlgebra.isScalarTower {k : Type u₁} {G : Type u₂} {R : Type u_2} {S : Type u_3} [Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMul R S] [IsScalarTower R S k] :
                                              Equations
                                              • =
                                              instance AddMonoidAlgebra.smulCommClass {k : Type u₁} {G : Type u₂} {R : Type u_2} {S : Type u_3} [Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMulCommClass R S k] :
                                              Equations
                                              • =
                                              Equations
                                              • =

                                              It is hard to state the equivalent of DistribMulAction G k[G] because we've never discussed actions of additive groups.

                                              Copies of ext lemmas and bundled singles from Finsupp #

                                              As AddMonoidAlgebra is a type synonym, ext will not unfold it to find ext lemmas. We need bundled version of Finsupp.single with the right types to state these lemmas. It is good practice to have those, regardless of the ext issue.

                                              theorem AddMonoidAlgebra.ext_iff {k : Type u₁} {G : Type u₂} [Semiring k] {f : AddMonoidAlgebra k G} {g : AddMonoidAlgebra k G} :
                                              f = g ∀ (x : G), f x = g x
                                              theorem AddMonoidAlgebra.ext {k : Type u₁} {G : Type u₂} [Semiring k] ⦃f : AddMonoidAlgebra k G ⦃g : AddMonoidAlgebra k G (H : ∀ (x : G), f x = g x) :
                                              f = g

                                              A copy of Finsupp.ext for AddMonoidAlgebra.

                                              @[reducible, inline]
                                              abbrev AddMonoidAlgebra.singleAddHom {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) :

                                              A copy of Finsupp.singleAddHom for AddMonoidAlgebra.

                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem AddMonoidAlgebra.addHom_ext'_iff {k : Type u₁} {G : Type u₂} {N : Type u_3} [Semiring k] [AddZeroClass N] {f : AddMonoidAlgebra k G →+ N} {g : AddMonoidAlgebra k G →+ N} :
                                                f = g ∀ (x : G), f.comp (AddMonoidAlgebra.singleAddHom x) = g.comp (AddMonoidAlgebra.singleAddHom x)
                                                theorem AddMonoidAlgebra.addHom_ext' {k : Type u₁} {G : Type u₂} {N : Type u_3} [Semiring k] [AddZeroClass N] ⦃f : AddMonoidAlgebra k G →+ N ⦃g : AddMonoidAlgebra k G →+ N (H : ∀ (x : G), f.comp (AddMonoidAlgebra.singleAddHom x) = g.comp (AddMonoidAlgebra.singleAddHom x)) :
                                                f = g

                                                A copy of Finsupp.addHom_ext' for AddMonoidAlgebra.

                                                @[reducible, inline]
                                                abbrev AddMonoidAlgebra.lsingle {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring R] [Semiring k] [Module R k] (a : G) :

                                                A copy of Finsupp.lsingle for AddMonoidAlgebra.

                                                Equations
                                                Instances For
                                                  @[simp]
                                                  theorem AddMonoidAlgebra.lsingle_apply {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring R] [Semiring k] [Module R k] (a : G) (b : k) :
                                                  theorem AddMonoidAlgebra.lhom_ext'_iff {k : Type u₁} {G : Type u₂} {R : Type u_2} {N : Type u_3} [Semiring R] [Semiring k] [AddCommMonoid N] [Module R N] [Module R k] {f : AddMonoidAlgebra k G →ₗ[R] N} {g : AddMonoidAlgebra k G →ₗ[R] N} :
                                                  f = g ∀ (x : G), f ∘ₗ AddMonoidAlgebra.lsingle x = g ∘ₗ AddMonoidAlgebra.lsingle x
                                                  theorem AddMonoidAlgebra.lhom_ext' {k : Type u₁} {G : Type u₂} {R : Type u_2} {N : Type u_3} [Semiring R] [Semiring k] [AddCommMonoid N] [Module R N] [Module R k] ⦃f : AddMonoidAlgebra k G →ₗ[R] N ⦃g : AddMonoidAlgebra k G →ₗ[R] N (H : ∀ (x : G), f ∘ₗ AddMonoidAlgebra.lsingle x = g ∘ₗ AddMonoidAlgebra.lsingle x) :
                                                  f = g

                                                  A copy of Finsupp.lhom_ext' for AddMonoidAlgebra.

                                                  theorem AddMonoidAlgebra.mul_apply {k : Type u₁} {G : Type u₂} [Semiring k] [DecidableEq G] [Add G] (f : AddMonoidAlgebra k G) (g : AddMonoidAlgebra k G) (x : G) :
                                                  (f * g) x = Finsupp.sum f fun (a₁ : G) (b₁ : k) => Finsupp.sum g fun (a₂ : G) (b₂ : k) => if a₁ + a₂ = x then b₁ * b₂ else 0
                                                  theorem AddMonoidAlgebra.mul_apply_antidiagonal {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] (f : AddMonoidAlgebra k G) (g : AddMonoidAlgebra k G) (x : G) (s : Finset (G × G)) (hs : ∀ {p : G × G}, p s p.1 + p.2 = x) :
                                                  (f * g) x = ps, f p.1 * g p.2
                                                  theorem AddMonoidAlgebra.single_mul_single {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] {a₁ : G} {a₂ : G} {b₁ : k} {b₂ : k} :
                                                  AddMonoidAlgebra.single a₁ b₁ * AddMonoidAlgebra.single a₂ b₂ = AddMonoidAlgebra.single (a₁ + a₂) (b₁ * b₂)
                                                  theorem AddMonoidAlgebra.single_commute_single {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] {a₁ : G} {a₂ : G} {b₁ : k} {b₂ : k} (ha : AddCommute a₁ a₂) (hb : Commute b₁ b₂) :
                                                  theorem AddMonoidAlgebra.single_pow {k : Type u₁} {G : Type u₂} [Semiring k] [AddMonoid G] {a : G} {b : k} (n : ) :
                                                  @[simp]
                                                  theorem AddMonoidAlgebra.mapDomain_one {α : Type u_3} {β : Type u_4} {α₂ : Type u_5} [Semiring β] [Zero α] [Zero α₂] {F : Type u_6} [FunLike F α α₂] [ZeroHomClass F α α₂] (f : F) :

                                                  Like Finsupp.mapDomain_zero, but for the 1 we define in this file

                                                  theorem AddMonoidAlgebra.mapDomain_mul {α : Type u_3} {β : Type u_4} {α₂ : Type u_5} [Semiring β] [Add α] [Add α₂] {F : Type u_6} [FunLike F α α₂] [AddHomClass F α α₂] (f : F) (x : AddMonoidAlgebra β α) (y : AddMonoidAlgebra β α) :

                                                  Like Finsupp.mapDomain_add, but for the convolutive multiplication we define in this file

                                                  The embedding of an additive magma into its additive magma algebra.

                                                  Equations
                                                  Instances For

                                                    Embedding of a magma with zero into its magma algebra.

                                                    Equations
                                                    Instances For
                                                      def AddMonoidAlgebra.of' (k : Type u₁) (G : Type u₂) [Semiring k] :

                                                      Embedding of a magma with zero G, into its magma algebra, having G as source.

                                                      Equations
                                                      Instances For
                                                        @[simp]
                                                        theorem AddMonoidAlgebra.of_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddZeroClass G] (a : Multiplicative G) :
                                                        (AddMonoidAlgebra.of k G) a = AddMonoidAlgebra.single (Multiplicative.toAdd a) 1
                                                        @[simp]
                                                        theorem AddMonoidAlgebra.of'_apply {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) :
                                                        theorem AddMonoidAlgebra.of'_eq_of {k : Type u₁} {G : Type u₂} [Semiring k] [AddZeroClass G] (a : G) :
                                                        AddMonoidAlgebra.of' k G a = (AddMonoidAlgebra.of k G) (Multiplicative.ofAdd a)
                                                        theorem AddMonoidAlgebra.of'_commute {k : Type u₁} {G : Type u₂} [Semiring k] [AddZeroClass G] {a : G} (h : ∀ (a' : G), AddCommute a a') (f : AddMonoidAlgebra k G) :
                                                        @[simp]
                                                        theorem AddMonoidAlgebra.singleHom_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddZeroClass G] (a : k × Multiplicative G) :
                                                        AddMonoidAlgebra.singleHom a = AddMonoidAlgebra.single (Multiplicative.toAdd a.2) a.1

                                                        Finsupp.single as a MonoidHom from the product type into the additive monoid algebra.

                                                        Note the order of the elements of the product are reversed compared to the arguments of Finsupp.single.

                                                        Equations
                                                        Instances For
                                                          @[simp]
                                                          theorem AddMonoidAlgebra.smul_single' {k : Type u₁} {G : Type u₂} [Semiring k] (c : k) (a : G) (b : k) :

                                                          Copy of Finsupp.smul_single' that avoids the AddMonoidAlgebra = Finsupp defeq abuse.

                                                          theorem AddMonoidAlgebra.mul_single_apply_aux {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] (f : AddMonoidAlgebra k G) (r : k) (x : G) (y : G) (z : G) (H : ∀ (a : G), a + x = z a = y) :
                                                          (f * AddMonoidAlgebra.single x r) z = f y * r
                                                          theorem AddMonoidAlgebra.mul_single_zero_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddZeroClass G] (f : AddMonoidAlgebra k G) (r : k) (x : G) :
                                                          (f * AddMonoidAlgebra.single 0 r) x = f x * r
                                                          theorem AddMonoidAlgebra.mul_single_apply_of_not_exists_add {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] (r : k) {g : G} {g' : G} (x : AddMonoidAlgebra k G) (h : ¬∃ (d : G), g' = d + g) :
                                                          theorem AddMonoidAlgebra.single_mul_apply_aux {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] (f : AddMonoidAlgebra k G) (r : k) (x : G) (y : G) (z : G) (H : ∀ (a : G), x + a = y a = z) :
                                                          (AddMonoidAlgebra.single x r * f) y = r * f z
                                                          theorem AddMonoidAlgebra.single_zero_mul_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddZeroClass G] (f : AddMonoidAlgebra k G) (r : k) (x : G) :
                                                          (AddMonoidAlgebra.single 0 r * f) x = r * f x
                                                          theorem AddMonoidAlgebra.single_mul_apply_of_not_exists_add {k : Type u₁} {G : Type u₂} [Semiring k] [Add G] (r : k) {g : G} {g' : G} (x : AddMonoidAlgebra k G) (h : ¬∃ (d : G), g' = g + d) :
                                                          theorem AddMonoidAlgebra.mul_single_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddGroup G] (f : AddMonoidAlgebra k G) (r : k) (x : G) (y : G) :
                                                          (f * AddMonoidAlgebra.single x r) y = f (y - x) * r
                                                          theorem AddMonoidAlgebra.single_mul_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddGroup G] (r : k) (x : G) (f : AddMonoidAlgebra k G) (y : G) :
                                                          (AddMonoidAlgebra.single x r * f) y = r * f (-x + y)
                                                          theorem AddMonoidAlgebra.liftNC_smul {k : Type u₁} {G : Type u₂} [Semiring k] {R : Type u_3} [AddZeroClass G] [Semiring R] (f : k →+* R) (g : Multiplicative G →* R) (c : k) (φ : MonoidAlgebra k G) :
                                                          (AddMonoidAlgebra.liftNC f g) (c φ) = f c * (AddMonoidAlgebra.liftNC f g) φ
                                                          theorem AddMonoidAlgebra.induction_on {k : Type u₁} {G : Type u₂} [Semiring k] [AddMonoid G] {p : AddMonoidAlgebra k GProp} (f : AddMonoidAlgebra k G) (hM : ∀ (g : G), p ((AddMonoidAlgebra.of k G) (Multiplicative.ofAdd g))) (hadd : ∀ (f g : AddMonoidAlgebra k G), p fp gp (f + g)) (hsmul : ∀ (r : k) (f : AddMonoidAlgebra k G), p fp (r f)) :
                                                          p f
                                                          @[simp]
                                                          theorem AddMonoidAlgebra.mapDomainRingHom_apply {G : Type u₂} (k : Type u_3) [Semiring k] {H : Type u_4} {F : Type u_5} [AddMonoid G] [AddMonoid H] [FunLike F G H] [AddMonoidHomClass F G H] (f : F) :
                                                          def AddMonoidAlgebra.mapDomainRingHom {G : Type u₂} (k : Type u_3) [Semiring k] {H : Type u_4} {F : Type u_5} [AddMonoid G] [AddMonoid H] [FunLike F G H] [AddMonoidHomClass F G H] (f : F) :

                                                          If f : G → H is an additive homomorphism between two additive monoids, then Finsupp.mapDomain f is a ring homomorphism between their add monoid algebras.

                                                          Equations
                                                          Instances For

                                                            Conversions between AddMonoidAlgebra and MonoidAlgebra #

                                                            We have not defined k[G] = MonoidAlgebra k (Multiplicative G) because historically this caused problems; since the changes that have made nsmul definitional, this would be possible, but for now we just construct the ring isomorphisms using RingEquiv.refl _.

                                                            The equivalence between AddMonoidAlgebra and MonoidAlgebra in terms of Multiplicative

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

                                                              The equivalence between MonoidAlgebra and AddMonoidAlgebra in terms of Additive

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

                                                                Non-unital, non-associative algebra structure #

                                                                instance AddMonoidAlgebra.isScalarTower_self (k : Type u₁) {G : Type u₂} {R : Type u_2} [Semiring k] [DistribSMul R k] [Add G] [IsScalarTower R k k] :
                                                                Equations
                                                                • =
                                                                instance AddMonoidAlgebra.smulCommClass_self (k : Type u₁) {G : Type u₂} {R : Type u_2} [Semiring k] [DistribSMul R k] [Add G] [SMulCommClass R k k] :

                                                                Note that if k is a CommSemiring then we have SMulCommClass k k k and so we can take R = k in the below. In other words, if the coefficients are commutative amongst themselves, they also commute with the algebra multiplication.

                                                                Equations
                                                                • =
                                                                instance AddMonoidAlgebra.smulCommClass_symm_self (k : Type u₁) {G : Type u₂} {R : Type u_2} [Semiring k] [DistribSMul R k] [Add G] [SMulCommClass k R k] :
                                                                Equations
                                                                • =

                                                                Algebra structure #

                                                                @[simp]
                                                                theorem AddMonoidAlgebra.singleZeroRingHom_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddMonoid G] :
                                                                ∀ (a : k), AddMonoidAlgebra.singleZeroRingHom a = (↑(Finsupp.singleAddHom 0)).toFun a

                                                                Finsupp.single 0 as a RingHom

                                                                Equations
                                                                • AddMonoidAlgebra.singleZeroRingHom = { toFun := (↑(Finsupp.singleAddHom 0)).toFun, map_one' := , map_mul' := , map_zero' := , map_add' := }
                                                                Instances For
                                                                  theorem AddMonoidAlgebra.ringHom_ext {k : Type u₁} {G : Type u₂} {R : Type u_3} [Semiring k] [AddMonoid G] [Semiring R] {f : AddMonoidAlgebra k G →+* R} {g : AddMonoidAlgebra k G →+* R} (h₀ : ∀ (b : k), f (AddMonoidAlgebra.single 0 b) = g (AddMonoidAlgebra.single 0 b)) (h_of : ∀ (a : G), f (AddMonoidAlgebra.single a 1) = g (AddMonoidAlgebra.single a 1)) :
                                                                  f = g

                                                                  If two ring homomorphisms from k[G] are equal on all single a 1 and single 0 b, then they are equal.

                                                                  theorem AddMonoidAlgebra.ringHom_ext'_iff {k : Type u₁} {G : Type u₂} {R : Type u_3} [Semiring k] [AddMonoid G] [Semiring R] {f : AddMonoidAlgebra k G →+* R} {g : AddMonoidAlgebra k G →+* R} :
                                                                  f = g f.comp AddMonoidAlgebra.singleZeroRingHom = g.comp AddMonoidAlgebra.singleZeroRingHom (↑f).comp (AddMonoidAlgebra.of k G) = (↑g).comp (AddMonoidAlgebra.of k G)
                                                                  theorem AddMonoidAlgebra.ringHom_ext' {k : Type u₁} {G : Type u₂} {R : Type u_3} [Semiring k] [AddMonoid G] [Semiring R] {f : AddMonoidAlgebra k G →+* R} {g : AddMonoidAlgebra k G →+* R} (h₁ : f.comp AddMonoidAlgebra.singleZeroRingHom = g.comp AddMonoidAlgebra.singleZeroRingHom) (h_of : (↑f).comp (AddMonoidAlgebra.of k G) = (↑g).comp (AddMonoidAlgebra.of k G)) :
                                                                  f = g

                                                                  If two ring homomorphisms from k[G] are equal on all single a 1 and single 0 b, then they are equal.

                                                                  See note [partially-applied ext lemmas].

                                                                  @[simp]
                                                                  theorem AddMonoidAlgebra.opRingEquiv_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddCommMonoid G] :
                                                                  ∀ (a : (G →₀ k)ᵐᵒᵖ), AddMonoidAlgebra.opRingEquiv a = Finsupp.mapRange MulOpposite.op (MulOpposite.unop a)
                                                                  @[simp]
                                                                  theorem AddMonoidAlgebra.opRingEquiv_symm_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddCommMonoid G] :
                                                                  ∀ (a : G →₀ kᵐᵒᵖ), AddMonoidAlgebra.opRingEquiv.symm a = MulOpposite.op (Finsupp.mapRange MulOpposite.unop a)

                                                                  The opposite of an R[I] is ring equivalent to the AddMonoidAlgebra Rᵐᵒᵖ I over the opposite ring, taking elements to their opposite.

                                                                  Equations
                                                                  • AddMonoidAlgebra.opRingEquiv = { toEquiv := (MulOpposite.opAddEquiv.symm.trans (Finsupp.mapRange.addEquiv MulOpposite.opAddEquiv)).toEquiv, map_mul' := , map_add' := }
                                                                  Instances For
                                                                    theorem AddMonoidAlgebra.opRingEquiv_single {k : Type u₁} {G : Type u₂} [Semiring k] [AddCommMonoid G] (r : k) (x : G) :
                                                                    theorem AddMonoidAlgebra.prod_single {k : Type u₁} {G : Type u₂} {ι : Type ui} [CommSemiring k] [AddCommMonoid G] {s : Finset ι} {a : ιG} {b : ιk} :
                                                                    is, AddMonoidAlgebra.single (a i) (b i) = AddMonoidAlgebra.single (∑ is, a i) (∏ is, b i)