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.

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
            • MonoidAlgebra.nonUnitalSemiring = let __src := MonoidAlgebra.nonUnitalNonAssocSemiring; NonUnitalSemiring.mk
            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
            • MonoidAlgebra.nonAssocSemiring = let __src := MonoidAlgebra.nonUnitalNonAssocSemiring; NonAssocSemiring.mk
            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 = let __src := MonoidAlgebra.nonUnitalSemiring; let __src_1 := MonoidAlgebra.nonAssocSemiring; Semiring.mk npowRec
            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
              • MonoidAlgebra.commSemiring = let __src := MonoidAlgebra.nonUnitalCommSemiring; let __src_1 := MonoidAlgebra.semiring; CommSemiring.mk
              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
              • MonoidAlgebra.nonUnitalNonAssocRing = let __src := MonoidAlgebra.addCommGroup; let __src_1 := MonoidAlgebra.nonUnitalNonAssocSemiring; NonUnitalNonAssocRing.mk
              instance MonoidAlgebra.nonUnitalRing {k : Type u₁} {G : Type u₂} [Ring k] [Semigroup G] :
              Equations
              • MonoidAlgebra.nonUnitalRing = let __src := MonoidAlgebra.addCommGroup; let __src_1 := MonoidAlgebra.nonUnitalSemiring; NonUnitalRing.mk
              instance MonoidAlgebra.nonAssocRing {k : Type u₁} {G : Type u₂} [Ring k] [MulOneClass G] :
              Equations
              • MonoidAlgebra.nonAssocRing = let __src := MonoidAlgebra.addCommGroup; let __src_1 := MonoidAlgebra.nonAssocSemiring; NonAssocRing.mk
              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 = let __src := MonoidAlgebra.nonAssocRing; let __src_1 := MonoidAlgebra.semiring; Ring.mk SubNegMonoid.zsmul
              Equations
              • MonoidAlgebra.nonUnitalCommRing = let __src := MonoidAlgebra.nonUnitalCommSemiring; let __src_1 := MonoidAlgebra.nonUnitalRing; NonUnitalCommRing.mk
              instance MonoidAlgebra.commRing {k : Type u₁} {G : Type u₂} [CommRing k] [CommMonoid G] :
              Equations
              • MonoidAlgebra.commRing = let __src := MonoidAlgebra.nonUnitalCommRing; let __src_1 := MonoidAlgebra.ring; CommRing.mk
              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
                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
                    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
                      • =
                      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.

                      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 : φ₁.toMulHom.comp (MonoidAlgebra.ofMagma k G) = φ₂.toMulHom.comp (MonoidAlgebra.ofMagma k G)) :
                      φ₁ = φ₂

                      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 : G) (t : k) => t f m
                      @[simp]
                      theorem MonoidAlgebra.liftMagma_symm_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 : MonoidAlgebra k G →ₙₐ[k] A) :
                      (MonoidAlgebra.liftMagma k).symm F = F.toMulHom.comp (MonoidAlgebra.ofMagma k G)
                      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.

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

                        Algebra structure #

                        @[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 = let __src := Finsupp.singleAddHom 1; { toFun := (__src).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' {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].

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

                            Equations
                            • MonoidAlgebra.algebra = let __src := MonoidAlgebra.singleOneRingHom.comp (algebraMap k A); Algebra.mk __src
                            @[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 = Finsupp.single 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

                            Equations
                            • MonoidAlgebra.singleOneAlgHom = let __src := MonoidAlgebra.singleOneRingHom; { toRingHom := __src, commutes' := }
                            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_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

                              Equations
                              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 : (φ₁).comp (MonoidAlgebra.of k G) = (φ₂).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.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                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 : G) (b : k) => (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 : G) (b : k) => 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)
                                  @[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) :
                                  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
                                  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.lift k G A) ((F).comp (MonoidAlgebra.of k G))
                                  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 : G) (b : k) => 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] [FunLike F G 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] [FunLike F G 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.

                                  Equations
                                  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} [FunLike F G H] [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] [FunLike F G 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] [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 an algebra homomorphism between their monoid algebras.

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem MonoidAlgebra.mapDomainAlgHom_comp (k : Type u_4) (A : Type u_5) {G₁ : Type u_6} {G₂ : Type u_7} {G₃ : Type u_8} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G₁] [Monoid G₂] [Monoid G₃] (f : G₁ →* G₂) (g : G₂ →* G₃) :
                                      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.

                                      Equations
                                      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 (e.symm 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 (e).toEmbedding 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.

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

                                          Equations
                                          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} :
                                            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_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))
                                            @[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))

                                            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
                                                          • AddMonoidAlgebra.nonUnitalSemiring = let __src := AddMonoidAlgebra.nonUnitalNonAssocSemiring; NonUnitalSemiring.mk
                                                          Equations
                                                          • AddMonoidAlgebra.nonAssocSemiring = let __src := AddMonoidAlgebra.nonUnitalNonAssocSemiring; NonAssocSemiring.mk
                                                          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 = let __src := AddMonoidAlgebra.nonUnitalSemiring; let __src_1 := AddMonoidAlgebra.nonAssocSemiring; Semiring.mk npowRec
                                                          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
                                                            • AddMonoidAlgebra.commSemiring = let __src := AddMonoidAlgebra.nonUnitalCommSemiring; let __src_1 := AddMonoidAlgebra.semiring; CommSemiring.mk
                                                            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
                                                            • AddMonoidAlgebra.nonUnitalNonAssocRing = let __src := AddMonoidAlgebra.addCommGroup; let __src_1 := AddMonoidAlgebra.nonUnitalNonAssocSemiring; NonUnitalNonAssocRing.mk
                                                            Equations
                                                            • AddMonoidAlgebra.nonUnitalRing = let __src := AddMonoidAlgebra.addCommGroup; let __src_1 := AddMonoidAlgebra.nonUnitalSemiring; NonUnitalRing.mk
                                                            Equations
                                                            • AddMonoidAlgebra.nonAssocRing = let __src := AddMonoidAlgebra.addCommGroup; let __src_1 := AddMonoidAlgebra.nonAssocSemiring; NonAssocRing.mk
                                                            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 = let __src := AddMonoidAlgebra.nonAssocRing; let __src_1 := AddMonoidAlgebra.semiring; Ring.mk SubNegMonoid.zsmul
                                                            Equations
                                                            • AddMonoidAlgebra.nonUnitalCommRing = let __src := AddMonoidAlgebra.nonUnitalCommSemiring; let __src_1 := AddMonoidAlgebra.nonUnitalRing; NonUnitalCommRing.mk
                                                            instance AddMonoidAlgebra.commRing {k : Type u₁} {G : Type u₂} [CommRing k] [AddCommMonoid G] :
                                                            Equations
                                                            • AddMonoidAlgebra.commRing = let __src := AddMonoidAlgebra.nonUnitalCommRing; let __src_1 := AddMonoidAlgebra.ring; CommRing.mk
                                                            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.

                                                            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
                                                                    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
                                                                          • =
                                                                          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.

                                                                          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 : φ₁.toMulHom.comp (AddMonoidAlgebra.ofMagma k G) = φ₂.toMulHom.comp (AddMonoidAlgebra.ofMagma k G)) :
                                                                          φ₁ = φ₂

                                                                          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 : G) (t : k) => t f (Multiplicative.ofAdd m)
                                                                          @[simp]
                                                                          theorem AddMonoidAlgebra.liftMagma_symm_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 : AddMonoidAlgebra k G →ₙₐ[k] A) :
                                                                          (AddMonoidAlgebra.liftMagma k).symm F = F.toMulHom.comp (AddMonoidAlgebra.ofMagma k G)

                                                                          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.

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

                                                                            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 = let __src := Finsupp.singleAddHom 0; { toFun := (__src).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' {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_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)
                                                                              @[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)

                                                                              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 = let __src := MulOpposite.opAddEquiv.symm.trans (Finsupp.mapRange.addEquiv MulOpposite.opAddEquiv); { toEquiv := __src.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) :
                                                                                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].

                                                                                Equations
                                                                                • AddMonoidAlgebra.algebra = let __src := AddMonoidAlgebra.singleZeroRingHom.comp (algebraMap R k); Algebra.mk __src
                                                                                @[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 = Finsupp.single 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

                                                                                Equations
                                                                                • AddMonoidAlgebra.singleZeroAlgHom = let __src := AddMonoidAlgebra.singleZeroRingHom; { toRingHom := __src, commutes' := }
                                                                                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

                                                                                  Equations
                                                                                  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 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 : (φ₁).comp (AddMonoidAlgebra.of k G) = (φ₂).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 k[G] →ₐ[k] A.

                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    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 : G) (b : k) => (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 : G) (b : k) => 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_of' {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : Multiplicative G →* A) (x : G) :
                                                                                      ((AddMonoidAlgebra.lift k G A) F) (AddMonoidAlgebra.of' k G x) = F (Multiplicative.ofAdd x)
                                                                                      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 = (AddMonoidAlgebra.lift k G A) ((F).comp (AddMonoidAlgebra.of k G))
                                                                                      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 : G) (b : k) => 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), φ₁ (Finsupp.single x 1) = φ₂ (Finsupp.single x 1)) φ₁ = φ₂
                                                                                      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)
                                                                                      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] [FunLike F G 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] [FunLike F G 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] [FunLike F G 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.

                                                                                      Equations
                                                                                      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] [FunLike F G H] [AddMonoidHomClass F G H] (f : F) :
                                                                                        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] [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 an algebra homomorphism between their add monoid algebras.

                                                                                        Equations
                                                                                        Instances For
                                                                                          @[simp]
                                                                                          theorem AddMonoidAlgebra.mapDomainAlgHom_comp (k : Type u_3) (A : Type u_4) {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [CommSemiring k] [Semiring A] [Algebra k A] [AddMonoid G₁] [AddMonoid G₂] [AddMonoid G₃] (f : G₁ →+ G₂) (g : G₂ →+ G₃) :
                                                                                          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 AddMonoidAlgebra.domCongr e is an algebra equivalence between their monoid algebras.

                                                                                          Equations
                                                                                          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 (e.symm 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 (e).toEmbedding 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]
                                                                                            theorem AddMonoidAlgebra.domCongr_symm (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) :

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

                                                                                            Equations
                                                                                            Instances For

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

                                                                                              Equations
                                                                                              Instances For