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
    @[inline, reducible]
    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} :
      @[inline, reducible]
      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) :
          instance MonoidAlgebra.mul {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] :

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

          Equations
          • One or more equations did not get rendered due to their size.
          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.nat_cast_def {k : Type u₁} {G : Type u₂} [Semiring k] [MulOneClass G] (n : ) :

          Semiring structure #

          instance MonoidAlgebra.semiring {k : Type u₁} {G : Type u₂} [Semiring k] [Monoid G] :
          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
          • One or more equations did not get rendered due to their size.
          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.int_cast_def {k : Type u₁} {G : Type u₂} [Ring k] [MulOneClass G] (z : ) :
            instance MonoidAlgebra.ring {k : Type u₁} {G : Type u₂} [Ring k] [Monoid G] :
            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} [Monoid R] [Semiring k] [DistribMulAction 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} [Monoid R] [Monoid S] [Semiring k] [DistribMulAction R k] [DistribMulAction 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 = Finset.sum s fun (p : G × G) => 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 = { toOneHom := { 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.

                    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
                    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; { toMonoidHom := { toOneHom := { 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) :
                        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
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          theorem MonoidAlgebra.ringHom_ext {k : Type u₁} {G : Type u₂} {R : Type u_3} [Semiring k] [MulOneClass G] [Semiring R] {f : MonoidAlgebra k G →+* R} {g : MonoidAlgebra k G →+* R} (h₁ : ∀ (b : k), f (MonoidAlgebra.single 1 b) = g (MonoidAlgebra.single 1 b)) (h_of : ∀ (a : G), f (MonoidAlgebra.single a 1) = g (MonoidAlgebra.single a 1)) :
                          f = g

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

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

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

                          See note [partially-applied ext lemmas].

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

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

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

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

                              See note [partially-applied ext lemmas].

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

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

                              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) :
                                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
                                • One or more equations did not get rendered due to their size.
                                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
                                    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 ((MulEquiv.symm e) h)
                                      @[simp]
                                      theorem MonoidAlgebra.domCongr_support (k : Type u₁) {G : Type u₂} {H : Type u_1} [CommSemiring k] [Monoid G] [Monoid H] (A : Type u₃) [Semiring A] [Algebra k A] (e : G ≃* H) (f : MonoidAlgebra A G) :
                                      ((MonoidAlgebra.domCongr k A e) f).support = Finset.map (Equiv.toEmbedding e) f.support
                                      @[simp]
                                      theorem MonoidAlgebra.domCongr_single (k : Type u₁) {G : Type u₂} {H : Type u_1} [CommSemiring k] [Monoid G] [Monoid H] (A : Type u₃) [Semiring A] [Algebra k A] (e : G ≃* H) (g : G) (a : A) :
                                      @[simp]
                                      theorem MonoidAlgebra.domCongr_refl (k : Type u₁) {G : Type u₂} [CommSemiring k] [Monoid G] (A : Type u₃) [Semiring A] [Algebra k A] :
                                      MonoidAlgebra.domCongr k A (MulEquiv.refl G) = AlgEquiv.refl
                                      @[simp]
                                      theorem MonoidAlgebra.domCongr_symm (k : Type u₁) {G : Type u₂} {H : Type u_1} [CommSemiring k] [Monoid G] [Monoid H] (A : Type u₃) [Semiring A] [Algebra k A] (e : G ≃* H) :
                                      def MonoidAlgebra.GroupSMul.linearMap (k : Type u₁) {G : Type u₂} [Monoid G] [CommSemiring k] (V : Type u₃) [AddCommMonoid V] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] (g : G) :

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

                                      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} :
                                          (Finset.prod s fun (i : ι) => MonoidAlgebra.single (a i) (b i)) = MonoidAlgebra.single (Finset.prod s fun (i : ι) => a i) (Finset.prod s fun (i : ι) => b i)
                                          @[simp]
                                          theorem MonoidAlgebra.mul_single_apply {k : Type u₁} {G : Type u₂} [Semiring k] [Group G] (f : MonoidAlgebra k G) (r : k) (x : G) (y : G) :
                                          (f * MonoidAlgebra.single x r) y = f (y * x⁻¹) * r
                                          @[simp]
                                          theorem MonoidAlgebra.single_mul_apply {k : Type u₁} {G : Type u₂} [Semiring k] [Group G] (r : k) (x : G) (f : MonoidAlgebra k G) (y : G) :
                                          (MonoidAlgebra.single x r * f) y = r * f (x⁻¹ * y)
                                          theorem MonoidAlgebra.mul_apply_left {k : Type u₁} {G : Type u₂} [Semiring k] [Group G] (f : MonoidAlgebra k G) (g : MonoidAlgebra k G) (x : G) :
                                          (f * g) x = Finsupp.sum f fun (a : 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ᵐᵒᵖ), (RingEquiv.symm MonoidAlgebra.opRingEquiv) 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
                                                  @[inline, reducible]
                                                  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} :
                                                    @[inline, reducible]
                                                    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
                                                        • One or more equations did not get rendered due to their size.
                                                        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 1 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.nat_cast_def {k : Type u₁} {G : Type u₂} [Semiring k] [AddZeroClass G] (n : ) :

                                                        Semiring structure #

                                                        instance AddMonoidAlgebra.smulZeroClass {k : Type u₁} {G : Type u₂} {R : Type u_2} [Semiring k] [SMulZeroClass R k] :
                                                        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
                                                        • One or more equations did not get rendered due to their size.
                                                        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.int_cast_def {k : Type u₁} {G : Type u₂} [Ring k] [AddZeroClass G] (z : ) :
                                                          instance AddMonoidAlgebra.ring {k : Type u₁} {G : Type u₂} [Ring k] [AddMonoid G] :
                                                          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 = Finset.sum s fun (p : G × G) => 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
                                                                • One or more equations did not get rendered due to their size.
                                                                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
                                                                  • One or more equations did not get rendered due to their size.
                                                                  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.

                                                                        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)

                                                                        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
                                                                          • One or more equations did not get rendered due to their size.
                                                                          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₁ : RingHom.comp f AddMonoidAlgebra.singleZeroRingHom = RingHom.comp g AddMonoidAlgebra.singleZeroRingHom) (h_of : MonoidHom.comp (f) (AddMonoidAlgebra.of k G) = MonoidHom.comp (g) (AddMonoidAlgebra.of k G)) :
                                                                            f = g

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

                                                                            See note [partially-applied ext lemmas].

                                                                            @[simp]
                                                                            theorem AddMonoidAlgebra.opRingEquiv_symm_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddCommMonoid G] :
                                                                            ∀ (a : G →₀ kᵐᵒᵖ), (RingEquiv.symm AddMonoidAlgebra.opRingEquiv) a = MulOpposite.op (Finsupp.mapRange MulOpposite.unop 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
                                                                            • One or more equations did not get rendered due to their size.
                                                                            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
                                                                              @[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 : MonoidHom.comp (φ₁) (AddMonoidAlgebra.of k G) = MonoidHom.comp (φ₂) (AddMonoidAlgebra.of k G)) :
                                                                                  φ₁ = φ₂

                                                                                  See note [partially-applied ext lemmas].

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

                                                                                  Any monoid homomorphism G →* A can be lifted to an algebra homomorphism 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) :
                                                                                    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} :
                                                                                    (Finset.prod s fun (i : ι) => AddMonoidAlgebra.single (a i) (b i)) = AddMonoidAlgebra.single (Finset.sum s fun (i : ι) => a i) (Finset.prod s fun (i : ι) => b i)
                                                                                    theorem AddMonoidAlgebra.mapDomain_algebraMap {k : Type u₁} {G : Type u₂} (A : Type u_3) {H : Type u_4} {F : Type u_5} [CommSemiring k] [Semiring A] [Algebra k A] [AddMonoid G] [AddMonoid H] [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
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    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
                                                                                        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 ((AddEquiv.symm e) h)
                                                                                          @[simp]
                                                                                          theorem AddMonoidAlgebra.domCongr_support (k : Type u₁) {G : Type u₂} {H : Type u_1} (A : Type u_3) [CommSemiring k] [AddMonoid G] [AddMonoid H] [Semiring A] [Algebra k A] (e : G ≃+ H) (f : MonoidAlgebra A G) :
                                                                                          ((AddMonoidAlgebra.domCongr k A e) f).support = Finset.map (Equiv.toEmbedding e) f.support
                                                                                          @[simp]
                                                                                          theorem AddMonoidAlgebra.domCongr_single (k : Type u₁) {G : Type u₂} {H : Type u_1} (A : Type u_3) [CommSemiring k] [AddMonoid G] [AddMonoid H] [Semiring A] [Algebra k A] (e : G ≃+ H) (g : G) (a : A) :
                                                                                          @[simp]
                                                                                          theorem AddMonoidAlgebra.domCongr_refl (k : Type u₁) {G : Type u₂} (A : Type u_3) [CommSemiring k] [AddMonoid G] [Semiring A] [Algebra k A] :
                                                                                          @[simp]

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

                                                                                          Equations
                                                                                          Instances For

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

                                                                                            Equations
                                                                                            Instances For