Documentation

Mathlib.Algebra.MonoidAlgebra.Basic

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.

Instances For
    instance MonoidAlgebra.inhabited (k : Type u₁) (G : Type u₂) [Semiring k] :
    instance MonoidAlgebra.coeFun (k : Type u₁) (G : Type u₂) [Semiring k] :
    CoeFun (MonoidAlgebra k G) fun x => Gk
    @[inline, reducible]
    abbrev MonoidAlgebra.single {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) (b : k) :
    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} :
      @[inline, reducible]
      abbrev MonoidAlgebra.mapDomain {k : Type u₁} {G : Type u₂} [Semiring k] {G' : Type u_3} (f : GG') (v : MonoidAlgebra k G) :
      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} :
        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.

        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) :
          ↑(MonoidAlgebra.liftNC f g) (MonoidAlgebra.single a b) = f b * g a
          instance MonoidAlgebra.mul {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.)

          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₁ b₁ => Finsupp.sum g fun a₂ b₂ => MonoidAlgebra.single (a₁ * a₂) (b₁ * b₂)
          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} [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
          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.

          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} [OneHomClass g_hom G R] (f : k →+* R) (g : g_hom) :
          ↑(MonoidAlgebra.liftNC f g) 1 = 1
          theorem MonoidAlgebra.nat_cast_def {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] (n : ) :

          Semiring structure #

          instance MonoidAlgebra.semiring {k : Type u₁} {G : Type u₂} [Semiring k] [Monoid G] :
          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

          Instances For

            Derived instances #

            instance MonoidAlgebra.unique {k : Type u₁} {G : Type u₂} [Semiring k] [Subsingleton k] :
            instance MonoidAlgebra.addCommGroup {k : Type u₁} {G : Type u₂} [Ring k] :
            theorem MonoidAlgebra.int_cast_def {k : Type u₁} {G : Type u₂} [Ring k] [MulOneClass G] (z : ) :
            instance MonoidAlgebra.ring {k : Type u₁} {G : Type u₂} [Ring k] [Monoid G] :
            instance MonoidAlgebra.commRing {k : Type u₁} {G : Type u₂} [CommRing k] [CommMonoid G] :
            instance MonoidAlgebra.smulZeroClass {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [SMulZeroClass R k] :
            instance MonoidAlgebra.distribSMul {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [DistribSMul R k] :
            instance MonoidAlgebra.distribMulAction {k : Type u₁} {G : Type u₂} {R : Type u_2} [Monoid R] [Semiring k] [DistribMulAction R k] :
            instance MonoidAlgebra.module {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring R] [Semiring k] [Module R k] :
            instance MonoidAlgebra.faithfulSMul {k : Type u₁} {G : Type u₂} {R : Type u_2} [Monoid R] [Semiring k] [DistribMulAction R k] [FaithfulSMul R k] [Nonempty G] :
            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] :
            instance MonoidAlgebra.smulCommClass {k : Type u₁} {G : Type u₂} {R : Type u_2} {S : Type u_3} [Monoid R] [Monoid S] [Semiring k] [DistribMulAction R k] [DistribMulAction S k] [SMulCommClass R S k] :

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

            Instances For
              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₁ b₁ => Finsupp.sum g fun a₂ b₂ => 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.fst * p.snd = x) :
              ↑(f * g) x = Finset.sum s fun p => f p.fst * g p.snd
              @[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₂)
              @[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} [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} [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.

              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.

                Instances For
                  theorem MonoidAlgebra.smul_of {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] (g : G) (r : k) :
                  @[simp]
                  theorem MonoidAlgebra.singleHom_apply {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] (a : k × G) :
                  MonoidAlgebra.singleHom a = MonoidAlgebra.single a.snd a.fst
                  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.

                  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' = 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 * 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] :
                    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.

                    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] :
                    theorem MonoidAlgebra.nonUnitalAlgHom_ext (k : Type u₁) {G : Type u₂} [Semiring k] [Mul G] {A : Type u₃} [NonUnitalNonAssocSemiring A] [DistribMulAction k A] {φ₁ : MonoidAlgebra k G →ₙₐ[k] A} {φ₂ : MonoidAlgebra k G →ₙₐ[k] A} (h : ∀ (x : G), φ₁ (MonoidAlgebra.single x 1) = φ₂ (MonoidAlgebra.single x 1)) :
                    φ₁ = φ₂

                    A non_unital k-algebra homomorphism from MonoidAlgebra k G is uniquely defined by its values on the functions single a 1.

                    See note [partially-applied ext lemmas].

                    @[simp]
                    theorem MonoidAlgebra.liftMagma_apply_apply (k : Type u₁) {G : Type u₂} [Semiring k] [Mul G] {A : Type u₃} [NonUnitalNonAssocSemiring A] [Module k A] [IsScalarTower k A A] [SMulCommClass k A A] (f : G →ₙ* A) (a : MonoidAlgebra k G) :
                    ↑(↑(MonoidAlgebra.liftMagma k) f) a = Finsupp.sum a fun m t => t f m
                    def MonoidAlgebra.liftMagma (k : Type u₁) {G : Type u₂} [Semiring k] [Mul G] {A : Type u₃} [NonUnitalNonAssocSemiring A] [Module k A] [IsScalarTower k A A] [SMulCommClass k A A] :

                    The functor G ↦ MonoidAlgebra k G, from the category of magmas to the category of non-unital, non-associative algebras over k is adjoint to the forgetful functor in the other direction.

                    Instances For

                      Algebra structure #

                      @[simp]
                      theorem MonoidAlgebra.singleOneRingHom_apply {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] :
                      ∀ (a : k), MonoidAlgebra.singleOneRingHom a = ZeroHom.toFun (↑(Finsupp.singleAddHom 1)) a

                      Finsupp.single 1 as a RingHom

                      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] [MonoidHomClass F G H] (f : F) :
                        def MonoidAlgebra.mapDomainRingHom {G : Type u₂} (k : Type u_3) {H : Type u_4} {F : Type u_5} [Semiring k] [Monoid G] [Monoid 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.

                        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' {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₁ : RingHom.comp f MonoidAlgebra.singleOneRingHom = RingHom.comp g MonoidAlgebra.singleOneRingHom) (h_of : MonoidHom.comp (f) (MonoidAlgebra.of k G) = MonoidHom.comp (g) (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].

                          instance MonoidAlgebra.algebra {k : Type u₁} {G : Type u₂} {A : Type u_3} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] :

                          The instance Algebra k (MonoidAlgebra A G) whenever we have Algebra k A.

                          In particular this provides the instance Algebra k (MonoidAlgebra k G).

                          @[simp]
                          theorem MonoidAlgebra.singleOneAlgHom_apply {k : Type u₁} {G : Type u₂} {A : Type u_3} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] :
                          ∀ (a : A), MonoidAlgebra.singleOneAlgHom a = fun₀ | 1 => a
                          def MonoidAlgebra.singleOneAlgHom {k : Type u₁} {G : Type u₂} {A : Type u_3} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] :

                          Finsupp.single 1 as an AlgHom

                          Instances For
                            @[simp]
                            theorem MonoidAlgebra.coe_algebraMap {k : Type u₁} {G : Type u₂} {A : Type u_3} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] :
                            theorem MonoidAlgebra.single_eq_algebraMap_mul_of {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] (a : G) (b : k) :
                            theorem MonoidAlgebra.single_algebraMap_eq_algebraMap_mul_of {k : Type u₁} {G : Type u₂} {A : Type u_3} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] (a : G) (b : k) :
                            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
                            def MonoidAlgebra.liftNCAlgHom {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] {B : Type u_3} [Semiring B] [Algebra k B] (f : A →ₐ[k] B) (g : G →* B) (h_comm : ∀ (x : A) (y : G), Commute (f x) (g y)) :

                            liftNCRingHom as an AlgHom, for when f is an AlgHom

                            Instances For
                              theorem MonoidAlgebra.algHom_ext {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] ⦃φ₁ : MonoidAlgebra k G →ₐ[k] A ⦃φ₂ : MonoidAlgebra k G →ₐ[k] A (h : ∀ (x : G), φ₁ (MonoidAlgebra.single x 1) = φ₂ (MonoidAlgebra.single x 1)) :
                              φ₁ = φ₂

                              A k-algebra homomorphism from MonoidAlgebra k G is uniquely defined by its values on the functions single a 1.

                              theorem MonoidAlgebra.algHom_ext' {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] ⦃φ₁ : MonoidAlgebra k G →ₐ[k] A ⦃φ₂ : MonoidAlgebra k G →ₐ[k] A (h : MonoidHom.comp (φ₁) (MonoidAlgebra.of k G) = MonoidHom.comp (φ₂) (MonoidAlgebra.of k G)) :
                              φ₁ = φ₂

                              See note [partially-applied ext lemmas].

                              def MonoidAlgebra.lift (k : Type u₁) (G : Type u₂) [CommSemiring k] [Monoid G] (A : Type u₃) [Semiring A] [Algebra k A] :

                              Any monoid homomorphism G →* A can be lifted to an algebra homomorphism MonoidAlgebra k G →ₐ[k] A.

                              Instances For
                                theorem MonoidAlgebra.lift_apply' {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : G →* A) (f : MonoidAlgebra k G) :
                                ↑(↑(MonoidAlgebra.lift k G A) F) f = Finsupp.sum f fun a b => ↑(algebraMap k A) b * F a
                                theorem MonoidAlgebra.lift_apply {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : G →* A) (f : MonoidAlgebra k G) :
                                ↑(↑(MonoidAlgebra.lift k G A) F) f = Finsupp.sum f fun a b => b F a
                                theorem MonoidAlgebra.lift_def {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : G →* A) :
                                ↑(↑(MonoidAlgebra.lift k G A) F) = ↑(MonoidAlgebra.liftNC ↑(algebraMap k A) F)
                                @[simp]
                                theorem MonoidAlgebra.lift_symm_apply {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : MonoidAlgebra k G →ₐ[k] A) (x : G) :
                                ↑((MonoidAlgebra.lift k G A).symm F) x = F (MonoidAlgebra.single x 1)
                                theorem MonoidAlgebra.lift_of {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : G →* A) (x : G) :
                                ↑(↑(MonoidAlgebra.lift k G A) F) (↑(MonoidAlgebra.of k G) x) = F x
                                @[simp]
                                theorem MonoidAlgebra.lift_single {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : G →* A) (a : G) (b : k) :
                                ↑(↑(MonoidAlgebra.lift k G A) F) (MonoidAlgebra.single a b) = b F a
                                theorem MonoidAlgebra.lift_unique' {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : MonoidAlgebra k G →ₐ[k] A) :
                                theorem MonoidAlgebra.lift_unique {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : MonoidAlgebra k G →ₐ[k] A) (f : MonoidAlgebra k G) :
                                F f = Finsupp.sum f fun a b => b F (MonoidAlgebra.single a 1)

                                Decomposition of a k-algebra homomorphism from MonoidAlgebra k G by its values on F (single a 1).

                                @[simp]
                                theorem MonoidAlgebra.mapDomainNonUnitalAlgHom_apply (k : Type u_4) (A : Type u_5) [CommSemiring k] [Semiring A] [Algebra k A] {G : Type u_6} {H : Type u_7} {F : Type u_8} [Mul G] [Mul H] [MulHomClass F G H] (f : F) :
                                def MonoidAlgebra.mapDomainNonUnitalAlgHom (k : Type u_4) (A : Type u_5) [CommSemiring k] [Semiring A] [Algebra k A] {G : Type u_6} {H : Type u_7} {F : Type u_8} [Mul G] [Mul H] [MulHomClass F G H] (f : F) :

                                If f : G → H is a homomorphism between two magmas, then Finsupp.mapDomain f is a non-unital algebra homomorphism between their magma algebras.

                                Instances For
                                  theorem MonoidAlgebra.mapDomain_algebraMap {k : Type u₁} {G : Type u₂} {H : Type u_1} [CommSemiring k] [Monoid G] [Monoid H] (A : Type u₃) [Semiring A] [Algebra k A] {F : Type u_4} [MonoidHomClass F G H] (f : F) (r : k) :
                                  @[simp]
                                  theorem MonoidAlgebra.mapDomainAlgHom_apply {G : Type u₂} [Monoid G] (k : Type u_4) (A : Type u_5) [CommSemiring k] [Semiring A] [Algebra k A] {H : Type u_6} {F : Type u_7} [Monoid H] [MonoidHomClass F G H] (f : F) :
                                  ∀ (a : G →₀ A), ↑(MonoidAlgebra.mapDomainAlgHom k A f) a = Finsupp.mapDomain (f) a
                                  def MonoidAlgebra.mapDomainAlgHom {G : Type u₂} [Monoid G] (k : Type u_4) (A : Type u_5) [CommSemiring k] [Semiring A] [Algebra k A] {H : Type u_6} {F : Type u_7} [Monoid H] [MonoidHomClass F G H] (f : F) :

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

                                  Instances For
                                    def MonoidAlgebra.domCongr (k : Type u₁) {G : Type u₂} {H : Type u_1} [CommSemiring k] [Monoid G] [Monoid H] (A : Type u₃) [Semiring A] [Algebra k A] (e : G ≃* H) :

                                    If e : G ≃* H is a multiplicative equivalence between two monoids, then MonoidAlgebra.domCongr e is an algebra equivalence between their monoid algebras.

                                    Instances For
                                      theorem MonoidAlgebra.domCongr_toAlgHom (k : Type u₁) {G : Type u₂} {H : Type u_1} [CommSemiring k] [Monoid G] [Monoid H] (A : Type u₃) [Semiring A] [Algebra k A] (e : G ≃* H) :
                                      @[simp]
                                      theorem MonoidAlgebra.domCongr_apply (k : Type u₁) {G : Type u₂} {H : Type u_1} [CommSemiring k] [Monoid G] [Monoid H] (A : Type u₃) [Semiring A] [Algebra k A] (e : G ≃* H) (f : MonoidAlgebra A G) (h : H) :
                                      ↑(↑(MonoidAlgebra.domCongr k A e) f) h = f (↑(MulEquiv.symm e) h)
                                      @[simp]
                                      theorem MonoidAlgebra.domCongr_support (k : Type u₁) {G : Type u₂} {H : Type u_1} [CommSemiring k] [Monoid G] [Monoid H] (A : Type u₃) [Semiring A] [Algebra k A] (e : G ≃* H) (f : MonoidAlgebra A G) :
                                      (↑(MonoidAlgebra.domCongr k A e) f).support = Finset.map (Equiv.toEmbedding e) f.support
                                      @[simp]
                                      theorem MonoidAlgebra.domCongr_single (k : Type u₁) {G : Type u₂} {H : Type u_1} [CommSemiring k] [Monoid G] [Monoid H] (A : Type u₃) [Semiring A] [Algebra k A] (e : G ≃* H) (g : G) (a : A) :
                                      @[simp]
                                      theorem MonoidAlgebra.domCongr_refl (k : Type u₁) {G : Type u₂} [CommSemiring k] [Monoid G] (A : Type u₃) [Semiring A] [Algebra k A] :
                                      MonoidAlgebra.domCongr k A (MulEquiv.refl G) = AlgEquiv.refl
                                      @[simp]
                                      theorem MonoidAlgebra.domCongr_symm (k : Type u₁) {G : Type u₂} {H : Type u_1} [CommSemiring k] [Monoid G] [Monoid H] (A : Type u₃) [Semiring A] [Algebra k A] (e : G ≃* H) :
                                      def MonoidAlgebra.GroupSmul.linearMap (k : Type u₁) {G : Type u₂} [Monoid G] [CommSemiring k] (V : Type u₃) [AddCommMonoid V] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] (g : G) :

                                      When V is a k[G]-module, multiplication by a group element g is a k-linear map.

                                      Instances For
                                        @[simp]
                                        theorem MonoidAlgebra.GroupSmul.linearMap_apply (k : Type u₁) {G : Type u₂} [Monoid G] [CommSemiring k] (V : Type u₃) [AddCommMonoid V] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] (g : G) (v : V) :
                                        def MonoidAlgebra.equivariantOfLinearOfComm {k : Type u₁} {G : Type u₂} [Monoid G] [CommSemiring k] {V : Type u₃} {W : Type u₄} [AddCommMonoid V] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] [AddCommMonoid W] [Module k W] [Module (MonoidAlgebra k G) W] [IsScalarTower k (MonoidAlgebra k G) W] (f : V →ₗ[k] W) (h : ∀ (g : G) (v : V), f (MonoidAlgebra.single g 1 v) = MonoidAlgebra.single g 1 f v) :

                                        Build a k[G]-linear map from a k-linear map and evidence that it is G-equivariant.

                                        Instances For
                                          @[simp]
                                          theorem MonoidAlgebra.equivariantOfLinearOfComm_apply {k : Type u₁} {G : Type u₂} [Monoid G] [CommSemiring k] {V : Type u₃} {W : Type u₄} [AddCommMonoid V] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] [AddCommMonoid W] [Module k W] [Module (MonoidAlgebra k G) W] [IsScalarTower k (MonoidAlgebra k G) W] (f : V →ₗ[k] W) (h : ∀ (g : G) (v : V), f (MonoidAlgebra.single g 1 v) = MonoidAlgebra.single g 1 f v) (v : V) :
                                          theorem MonoidAlgebra.prod_single {k : Type u₁} {G : Type u₂} {ι : Type ui} [CommSemiring k] [CommMonoid G] {s : Finset ι} {a : ιG} {b : ιk} :
                                          (Finset.prod s fun i => MonoidAlgebra.single (a i) (b i)) = MonoidAlgebra.single (Finset.prod s fun i => a i) (Finset.prod s fun i => 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 b => 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 b => f (x * a⁻¹) * b
                                          @[simp]
                                          theorem MonoidAlgebra.opRingEquiv_symm_apply {k : Type u₁} {G : Type u₂} [Semiring k] [Monoid G] :
                                          ∀ (a : Gᵐᵒᵖ →₀ kᵐᵒᵖ), ↑(RingEquiv.symm MonoidAlgebra.opRingEquiv) a = MulOpposite.op (Finsupp.mapRange MulOpposite.unop (_ : MulOpposite.unop 0 = 0) (Finsupp.equivMapDomain MulOpposite.opEquiv.symm a))
                                          @[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.opAddEquiv 0 = 0) (MulOpposite.unop 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.

                                          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) (v : V), v W↑(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

                                            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.

                                              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.

                                                Instances For
                                                  instance AddMonoidAlgebra.coeFun (k : Type u₁) (G : Type u₂) [Semiring k] :
                                                  CoeFun (AddMonoidAlgebra k G) fun x => Gk
                                                  @[inline, reducible]
                                                  abbrev AddMonoidAlgebra.single {k : Type u₁} {G : Type u₂} [Semiring k] (a : G) (b : k) :
                                                  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} :
                                                    @[inline, reducible]
                                                    abbrev AddMonoidAlgebra.mapDomain {k : Type u₁} {G : Type u₂} [Semiring k] {G' : Type u_3} (f : GG') (v : AddMonoidAlgebra k G) :
                                                    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.

                                                      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.)

                                                        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₁ b₁ => Finsupp.sum g fun a₂ b₂ => AddMonoidAlgebra.single (a₁ + a₂) (b₁ * b₂)
                                                        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} [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 1 1, i.e. the function that is 1 at 0 and zero elsewhere.

                                                        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} [OneHomClass g_hom (Multiplicative G) R] (f : k →+* R) (g : g_hom) :
                                                        ↑(AddMonoidAlgebra.liftNC f g) 1 = 1
                                                        theorem AddMonoidAlgebra.nat_cast_def {k : Type u₁} {G : Type u₂} [Semiring k] [AddZeroClass G] (n : ) :

                                                        Semiring structure #

                                                        instance AddMonoidAlgebra.smulZeroClass {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [SMulZeroClass R k] :
                                                        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

                                                        Instances For

                                                          Derived instances #

                                                          theorem AddMonoidAlgebra.int_cast_def {k : Type u₁} {G : Type u₂} [Ring k] [AddZeroClass G] (z : ) :
                                                          instance AddMonoidAlgebra.ring {k : Type u₁} {G : Type u₂} [Ring k] [AddMonoid G] :
                                                          instance AddMonoidAlgebra.distribSMul {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [DistribSMul R k] :
                                                          instance AddMonoidAlgebra.faithfulSMul {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [SMulZeroClass R k] [FaithfulSMul R k] [Nonempty G] :
                                                          instance AddMonoidAlgebra.module {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring R] [Semiring k] [Module R k] :
                                                          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] :
                                                          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] :

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

                                                          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₁ b₁ => Finsupp.sum g fun a₂ b₂ => 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.fst + p.snd = x) :
                                                          ↑(f * g) x = Finset.sum s fun p => f p.fst * g p.snd
                                                          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_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} [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} [AddHomClass F α α₂] (f : F) (x : AddMonoidAlgebra β α) (y : AddMonoidAlgebra β α) :

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

                                                          @[simp]

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

                                                          Instances For

                                                            Embedding of a magma with zero into its magma algebra.

                                                            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.

                                                              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) :
                                                                @[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.snd) a.fst

                                                                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.

                                                                Instances For
                                                                  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' = d + g) :
                                                                  ↑(x * AddMonoidAlgebra.single g r) g' = 0
                                                                  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 + d) :
                                                                  ↑(AddMonoidAlgebra.single g r * x) g' = 0
                                                                  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] [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] [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.

                                                                  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

                                                                    Instances For

                                                                      The equivalence between MonoidAlgebra and AddMonoidAlgebra in terms of Additive

                                                                      Instances For

                                                                        Non-unital, non-associative algebra structure #

                                                                        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.

                                                                        theorem AddMonoidAlgebra.nonUnitalAlgHom_ext (k : Type u₁) {G : Type u₂} [Semiring k] [Add G] {A : Type u₃} [NonUnitalNonAssocSemiring A] [DistribMulAction k A] {φ₁ : AddMonoidAlgebra k G →ₙₐ[k] A} {φ₂ : AddMonoidAlgebra k G →ₙₐ[k] A} (h : ∀ (x : G), φ₁ (AddMonoidAlgebra.single x 1) = φ₂ (AddMonoidAlgebra.single x 1)) :
                                                                        φ₁ = φ₂

                                                                        A non_unital k-algebra homomorphism from k[G] is uniquely defined by its values on the functions single a 1.

                                                                        See note [partially-applied ext lemmas].

                                                                        @[simp]
                                                                        theorem AddMonoidAlgebra.liftMagma_apply_apply (k : Type u₁) {G : Type u₂} [Semiring k] [Add G] {A : Type u₃} [NonUnitalNonAssocSemiring A] [Module k A] [IsScalarTower k A A] [SMulCommClass k A A] (f : Multiplicative G →ₙ* A) (a : AddMonoidAlgebra k G) :
                                                                        ↑(↑(AddMonoidAlgebra.liftMagma k) f) a = Finsupp.sum a fun m t => t f (Multiplicative.ofAdd m)

                                                                        The functor G ↦ k[G], from the category of magmas to the category of non-unital, non-associative algebras over k is adjoint to the forgetful functor in the other direction.

                                                                        Instances For

                                                                          Algebra structure #

                                                                          @[simp]
                                                                          theorem AddMonoidAlgebra.singleZeroRingHom_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddMonoid G] :
                                                                          ∀ (a : k), AddMonoidAlgebra.singleZeroRingHom a = ZeroHom.toFun (↑(Finsupp.singleAddHom 0)) a
                                                                          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' {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₁ : RingHom.comp f AddMonoidAlgebra.singleZeroRingHom = RingHom.comp g AddMonoidAlgebra.singleZeroRingHom) (h_of : MonoidHom.comp (f) (AddMonoidAlgebra.of k G) = MonoidHom.comp (g) (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_symm_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddCommMonoid G] :
                                                                          ∀ (a : G →₀ kᵐᵒᵖ), ↑(RingEquiv.symm AddMonoidAlgebra.opRingEquiv) a = MulOpposite.op (Finsupp.mapRange MulOpposite.unop (_ : MulOpposite.unop 0 = 0) a)
                                                                          @[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.opAddEquiv 0 = 0) (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.

                                                                          Instances For
                                                                            theorem AddMonoidAlgebra.opRingEquiv_single {k : Type u₁} {G : Type u₂} [Semiring k] [AddCommMonoid G] (r : k) (x : G) :
                                                                            AddMonoidAlgebra.opRingEquiv (MulOpposite.op (AddMonoidAlgebra.single x r)) = AddMonoidAlgebra.single x (MulOpposite.op r)
                                                                            instance AddMonoidAlgebra.algebra {k : Type u₁} {G : Type u₂} {R : Type u_2} [CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] :

                                                                            The instance Algebra R k[G] whenever we have Algebra R k.

                                                                            In particular this provides the instance Algebra k k[G].

                                                                            @[simp]
                                                                            theorem AddMonoidAlgebra.singleZeroAlgHom_apply {k : Type u₁} {G : Type u₂} {R : Type u_2} [CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] :
                                                                            ∀ (a : k), AddMonoidAlgebra.singleZeroAlgHom a = fun₀ | 0 => a
                                                                            def AddMonoidAlgebra.singleZeroAlgHom {k : Type u₁} {G : Type u₂} {R : Type u_2} [CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] :

                                                                            Finsupp.single 0 as an AlgHom

                                                                            Instances For
                                                                              @[simp]
                                                                              theorem AddMonoidAlgebra.coe_algebraMap {k : Type u₁} {G : Type u₂} {R : Type u_2} [CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] :
                                                                              def AddMonoidAlgebra.liftNCAlgHom {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] {B : Type u_3} [Semiring B] [Algebra k B] (f : A →ₐ[k] B) (g : Multiplicative G →* B) (h_comm : ∀ (x : A) (y : Multiplicative G), Commute (f x) (g y)) :

                                                                              liftNCRingHom as an AlgHom, for when f is an AlgHom

                                                                              Instances For
                                                                                theorem AddMonoidAlgebra.algHom_ext {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] ⦃φ₁ : AddMonoidAlgebra k G →ₐ[k] A ⦃φ₂ : AddMonoidAlgebra k G →ₐ[k] A (h : ∀ (x : G), φ₁ (AddMonoidAlgebra.single x 1) = φ₂ (AddMonoidAlgebra.single x 1)) :
                                                                                φ₁ = φ₂

                                                                                A k-algebra homomorphism from MonoidAlgebra k G is uniquely defined by its values on the functions single a 1.

                                                                                theorem AddMonoidAlgebra.algHom_ext' {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] ⦃φ₁ : AddMonoidAlgebra k G →ₐ[k] A ⦃φ₂ : AddMonoidAlgebra k G →ₐ[k] A (h : MonoidHom.comp (φ₁) (AddMonoidAlgebra.of k G) = MonoidHom.comp (φ₂) (AddMonoidAlgebra.of k G)) :
                                                                                φ₁ = φ₂

                                                                                See note [partially-applied ext lemmas].

                                                                                def AddMonoidAlgebra.lift (k : Type u₁) (G : Type u₂) [CommSemiring k] [AddMonoid G] (A : Type u₃) [Semiring A] [Algebra k A] :

                                                                                Any monoid homomorphism G →* A can be lifted to an algebra homomorphism MonoidAlgebra k G →ₐ[k] A.

                                                                                Instances For
                                                                                  theorem AddMonoidAlgebra.lift_apply' {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : Multiplicative G →* A) (f : MonoidAlgebra k G) :
                                                                                  ↑(↑(AddMonoidAlgebra.lift k G A) F) f = Finsupp.sum f fun a b => ↑(algebraMap k A) b * F (Multiplicative.ofAdd a)
                                                                                  theorem AddMonoidAlgebra.lift_apply {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : Multiplicative G →* A) (f : MonoidAlgebra k G) :
                                                                                  ↑(↑(AddMonoidAlgebra.lift k G A) F) f = Finsupp.sum f fun a b => b F (Multiplicative.ofAdd a)
                                                                                  theorem AddMonoidAlgebra.lift_def {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : Multiplicative G →* A) :
                                                                                  ↑(↑(AddMonoidAlgebra.lift k G A) F) = ↑(AddMonoidAlgebra.liftNC ↑(algebraMap k A) F)
                                                                                  @[simp]
                                                                                  theorem AddMonoidAlgebra.lift_symm_apply {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : AddMonoidAlgebra k G →ₐ[k] A) (x : Multiplicative G) :
                                                                                  ↑((AddMonoidAlgebra.lift k G A).symm F) x = F (AddMonoidAlgebra.single (Multiplicative.toAdd x) 1)
                                                                                  theorem AddMonoidAlgebra.lift_of {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : Multiplicative G →* A) (x : Multiplicative G) :
                                                                                  ↑(↑(AddMonoidAlgebra.lift k G A) F) (↑(AddMonoidAlgebra.of k G) x) = F x
                                                                                  @[simp]
                                                                                  theorem AddMonoidAlgebra.lift_single {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : Multiplicative G →* A) (a : G) (b : k) :
                                                                                  ↑(↑(AddMonoidAlgebra.lift k G A) F) (AddMonoidAlgebra.single a b) = b F (Multiplicative.ofAdd a)
                                                                                  theorem AddMonoidAlgebra.lift_unique' {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : AddMonoidAlgebra k G →ₐ[k] A) :
                                                                                  theorem AddMonoidAlgebra.lift_unique {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : AddMonoidAlgebra k G →ₐ[k] A) (f : MonoidAlgebra k G) :
                                                                                  F f = Finsupp.sum f fun a b => b F (AddMonoidAlgebra.single a 1)

                                                                                  Decomposition of a k-algebra homomorphism from MonoidAlgebra k G by its values on F (single a 1).

                                                                                  theorem AddMonoidAlgebra.algHom_ext_iff {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] {φ₁ : AddMonoidAlgebra k G →ₐ[k] A} {φ₂ : AddMonoidAlgebra k G →ₐ[k] A} :
                                                                                  (∀ (x : G), (φ₁ fun₀ | x => 1) = φ₂ fun₀ | x => 1) φ₁ = φ₂
                                                                                  theorem AddMonoidAlgebra.prod_single {k : Type u₁} {G : Type u₂} {ι : Type ui} [CommSemiring k] [AddCommMonoid G] {s : Finset ι} {a : ιG} {b : ιk} :
                                                                                  (Finset.prod s fun i => AddMonoidAlgebra.single (a i) (b i)) = AddMonoidAlgebra.single (Finset.sum s fun i => a i) (Finset.prod s fun i => b i)
                                                                                  theorem AddMonoidAlgebra.mapDomain_algebraMap {k : Type u₁} {G : Type u₂} (A : Type u_3) {H : Type u_4} {F : Type u_5} [CommSemiring k] [Semiring A] [Algebra k A] [AddMonoid G] [AddMonoid H] [AddMonoidHomClass F G H] (f : F) (r : k) :
                                                                                  @[simp]
                                                                                  theorem AddMonoidAlgebra.mapDomainNonUnitalAlgHom_apply (k : Type u_3) (A : Type u_4) [CommSemiring k] [Semiring A] [Algebra k A] {G : Type u_5} {H : Type u_6} {F : Type u_7} [Add G] [Add H] [AddHomClass F G H] (f : F) :
                                                                                  def AddMonoidAlgebra.mapDomainNonUnitalAlgHom (k : Type u_3) (A : Type u_4) [CommSemiring k] [Semiring A] [Algebra k A] {G : Type u_5} {H : Type u_6} {F : Type u_7} [Add G] [Add H] [AddHomClass F G H] (f : F) :

                                                                                  If f : G → H is a homomorphism between two additive magmas, then Finsupp.mapDomain f is a non-unital algebra homomorphism between their additive magma algebras.

                                                                                  Instances For
                                                                                    @[simp]
                                                                                    theorem AddMonoidAlgebra.mapDomainAlgHom_apply {G : Type u₂} (k : Type u_3) (A : Type u_4) [CommSemiring k] [Semiring A] [Algebra k A] [AddMonoid G] {H : Type u_5} {F : Type u_6} [AddMonoid H] [AddMonoidHomClass F G H] (f : F) :
                                                                                    ∀ (a : G →₀ A), ↑(AddMonoidAlgebra.mapDomainAlgHom k A f) a = Finsupp.mapDomain (f) a
                                                                                    def AddMonoidAlgebra.mapDomainAlgHom {G : Type u₂} (k : Type u_3) (A : Type u_4) [CommSemiring k] [Semiring A] [Algebra k A] [AddMonoid G] {H : Type u_5} {F : Type u_6} [AddMonoid H] [AddMonoidHomClass F G H] (f : F) :

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

                                                                                    Instances For
                                                                                      def AddMonoidAlgebra.domCongr (k : Type u₁) {G : Type u₂} {H : Type u_1} (A : Type u_3) [CommSemiring k] [AddMonoid G] [AddMonoid H] [Semiring A] [Algebra k A] (e : G ≃+ H) :

                                                                                      If e : G ≃* H is a multiplicative equivalence between two monoids, then MonoidAlgebra.domCongr e is an algebra equivalence between their monoid algebras.

                                                                                      Instances For
                                                                                        theorem AddMonoidAlgebra.domCongr_toAlgHom (k : Type u₁) {G : Type u₂} {H : Type u_1} (A : Type u_3) [CommSemiring k] [AddMonoid G] [AddMonoid H] [Semiring A] [Algebra k A] (e : G ≃+ H) :
                                                                                        @[simp]
                                                                                        theorem AddMonoidAlgebra.domCongr_apply (k : Type u₁) {G : Type u₂} {H : Type u_1} (A : Type u_3) [CommSemiring k] [AddMonoid G] [AddMonoid H] [Semiring A] [Algebra k A] (e : G ≃+ H) (f : MonoidAlgebra A G) (h : H) :
                                                                                        ↑(↑(AddMonoidAlgebra.domCongr k A e) f) h = f (↑(AddEquiv.symm e) h)
                                                                                        @[simp]
                                                                                        theorem AddMonoidAlgebra.domCongr_support (k : Type u₁) {G : Type u₂} {H : Type u_1} (A : Type u_3) [CommSemiring k] [AddMonoid G] [AddMonoid H] [Semiring A] [Algebra k A] (e : G ≃+ H) (f : MonoidAlgebra A G) :
                                                                                        (↑(AddMonoidAlgebra.domCongr k A e) f).support = Finset.map (Equiv.toEmbedding e) f.support
                                                                                        @[simp]
                                                                                        theorem AddMonoidAlgebra.domCongr_single (k : Type u₁) {G : Type u₂} {H : Type u_1} (A : Type u_3) [CommSemiring k] [AddMonoid G] [AddMonoid H] [Semiring A] [Algebra k A] (e : G ≃+ H) (g : G) (a : A) :
                                                                                        @[simp]
                                                                                        theorem AddMonoidAlgebra.domCongr_refl (k : Type u₁) {G : Type u₂} (A : Type u_3) [CommSemiring k] [AddMonoid G] [Semiring A] [Algebra k A] :
                                                                                        @[simp]

                                                                                        The algebra equivalence between AddMonoidAlgebra and MonoidAlgebra in terms of Multiplicative.

                                                                                        Instances For

                                                                                          The algebra equivalence between MonoidAlgebra and AddMonoidAlgebra in terms of Additive.

                                                                                          Instances For