Basic.lean

/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Yury G. Kudryashov, Scott Morrison
-/
import Mathlib.Algebra.Algebra.Equiv
import Mathlib.Algebra.Algebra.NonUnitalHom
import Mathlib.Algebra.BigOperators.Finsupp
import Mathlib.Algebra.Module.BigOperators
import Mathlib.Data.Finsupp.Basic
import Mathlib.LinearAlgebra.Finsupp

#align_import algebra.monoid_algebra.basic from "leanprover-community/mathlib"@"949dc57e616a621462062668c9f39e4e17b64b69"

/-!
# 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.
-/


noncomputable section

open BigOperators

open Finset

open Finsupp hiding single mapDomain

universe u₁ u₂ u₃ u₄

variable (k : Type u₁) (G : Type u₂) (H : Type*) {R : Type*}

/-! ### Multiplicative monoids -/


section

variable [Semiring k]

/-- 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.
-/
def MonoidAlgebra : Type max u₁ u₂ :=
  G →₀ k
#align monoid_algebra MonoidAlgebra

-- Porting note: The compiler couldn't derive this.
instance MonoidAlgebra.inhabited : Inhabited (MonoidAlgebra k G) :=
  inferInstanceAs (Inhabited (G →₀ k))
#align monoid_algebra.inhabited MonoidAlgebra.inhabited

-- Porting note: The compiler couldn't derive this.
instance MonoidAlgebra.addCommMonoid : AddCommMonoid (MonoidAlgebra k G) :=
  inferInstanceAs (AddCommMonoid (G →₀ k))
#align monoid_algebra.add_comm_monoid MonoidAlgebra.addCommMonoid

instance MonoidAlgebra.instIsCancelAdd [IsCancelAdd k] : IsCancelAdd (MonoidAlgebra k G) :=
  inferInstanceAs (IsCancelAdd (G →₀ k))

instance MonoidAlgebra.coeFun : CoeFun (MonoidAlgebra k G) fun _ => G → k :=
  Finsupp.instCoeFun
#align monoid_algebra.has_coe_to_fun MonoidAlgebra.coeFun

end

namespace MonoidAlgebra

variable {k G}

section

variable [Semiring k] [NonUnitalNonAssocSemiring R]

-- Porting note: `reducible` cannot be `local`, so we replace some definitions and theorems with
--               new ones which have new types.

abbrev single (a : G) (b : k) : MonoidAlgebra k G := Finsupp.single a b

theorem single_zero (a : G) : (single a 0 : MonoidAlgebra k G) = 0 := Finsupp.single_zero a

theorem single_add (a : G) (b₁ b₂ : k) : single a (b₁ + b₂) = single a b₁ + single a b₂ :=
  Finsupp.single_add a b₁ b₂

@[simp]
theorem sum_single_index {N} [AddCommMonoid N] {a : G} {b : k} {h : G → k → N}
    (h_zero : h a 0 = 0) :
    (single a b).sum h = h a b := Finsupp.sum_single_index h_zero

@[simp]
theorem sum_single (f : MonoidAlgebra k G) : f.sum single = f :=
  Finsupp.sum_single f

theorem single_apply {a a' : G} {b : k} [Decidable (a = a')] :
    single a b a' = if a = a' then b else 0 :=
  Finsupp.single_apply

@[simp]
theorem single_eq_zero {a : G} {b : k} : single a b = 0 ↔ b = 0 := Finsupp.single_eq_zero

abbrev mapDomain {G' : Type*} (f : G → G') (v : MonoidAlgebra k G) : MonoidAlgebra k G' :=
  Finsupp.mapDomain f v

theorem mapDomain_sum {k' G' : Type*} [Semiring k'] {f : G → G'} {s : MonoidAlgebra k' G}
    {v : G → k' → MonoidAlgebra k G} :
    mapDomain f (s.sum v) = s.sum fun a b => mapDomain f (v a b) :=
  Finsupp.mapDomain_sum

/-- 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`. -/
def liftNC (f : k →+ R) (g : G → R) : MonoidAlgebra k G →+ R :=
  liftAddHom fun x : G => (AddMonoidHom.mulRight (g x)).comp f
#align monoid_algebra.lift_nc MonoidAlgebra.liftNC

@[simp]
theorem liftNC_single (f : k →+ R) (g : G → R) (a : G) (b : k) :
    liftNC f g (single a b) = f b * g a :=
  liftAddHom_apply_single _ _ _
#align monoid_algebra.lift_nc_single MonoidAlgebra.liftNC_single

end

section Mul

variable [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.) -/
instance mul : Mul (MonoidAlgebra k G) :=
  ⟨fun f g => f.sum fun a₁ b₁ => g.sum fun a₂ b₂ => single (a₁ * a₂) (b₁ * b₂)⟩
#align monoid_algebra.has_mul MonoidAlgebra.mul

theorem mul_def {f g : MonoidAlgebra k G} :
    f * g = f.sum fun a₁ b₁ => g.sum fun a₂ b₂ => single (a₁ * a₂) (b₁ * b₂) :=
  rfl
#align monoid_algebra.mul_def MonoidAlgebra.mul_def

instance nonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring (MonoidAlgebra k G) :=
  { Finsupp.instAddCommMonoid with
    -- Porting note: `refine` & `exact` are required because `simp` behaves differently.
    left_distrib := fun f g h => by
      haveI := Classical.decEq G
      simp only [mul_def]
      refine Eq.trans (congr_arg (sum f) (funext₂ fun a₁ b₁ => sum_add_index ?_ ?_)) ?_ <;>
        simp only [mul_add, mul_zero, single_zero, single_add, forall_true_iff, sum_add]
    right_distrib := fun f g h => by
      haveI := Classical.decEq G
      simp only [mul_def]
      refine Eq.trans (sum_add_index ?_ ?_) ?_ <;>
        simp only [add_mul, zero_mul, single_zero, single_add, forall_true_iff, sum_zero, sum_add]
    zero_mul := fun f => by
      simp only [mul_def]
      exact sum_zero_index
    mul_zero := fun f => by
      simp only [mul_def]
      exact Eq.trans (congr_arg (sum f) (funext₂ fun a₁ b₁ => sum_zero_index)) sum_zero }
#align monoid_algebra.non_unital_non_assoc_semiring MonoidAlgebra.nonUnitalNonAssocSemiring

variable [Semiring R]

theorem liftNC_mul {g_hom : Type*} [FunLike g_hom G R] [MulHomClass g_hom G R]
    (f : k →+* R) (g : g_hom) (a b : MonoidAlgebra k G)
    (h_comm : ∀ {x y}, y ∈ a.support → Commute (f (b x)) (g y)) :
    liftNC (f : k →+ R) g (a * b) = liftNC (f : k →+ R) g a * liftNC (f : k →+ R) g b := by
  conv_rhs => rw [← sum_single a, ← sum_single b]
  -- Porting note: `(liftNC _ g).map_finsupp_sum` → `map_finsupp_sum`
  simp_rw [mul_def, map_finsupp_sum, liftNC_single, Finsupp.sum_mul, Finsupp.mul_sum]
  refine Finset.sum_congr rfl fun y hy => Finset.sum_congr rfl fun x _hx => ?_
  simp [mul_assoc, (h_comm hy).left_comm]
#align monoid_algebra.lift_nc_mul MonoidAlgebra.liftNC_mul

end Mul

section Semigroup

variable [Semiring k] [Semigroup G] [Semiring R]

instance nonUnitalSemiring : NonUnitalSemiring (MonoidAlgebra k G) :=
  { MonoidAlgebra.nonUnitalNonAssocSemiring with
    mul_assoc := fun f g h => by
      -- Porting note: `reducible` cannot be `local` so proof gets long.
      simp only [mul_def]
      rw [sum_sum_index]; congr; ext a₁ b₁
      rw [sum_sum_index, sum_sum_index]; congr; ext a₂ b₂
      rw [sum_sum_index, sum_single_index]; congr; ext a₃ b₃
      rw [sum_single_index, mul_assoc, mul_assoc]
      all_goals simp only [single_zero, single_add, forall_true_iff, add_mul,
        mul_add, zero_mul, mul_zero, sum_zero, sum_add] }
#align monoid_algebra.non_unital_semiring MonoidAlgebra.nonUnitalSemiring

end Semigroup

section One

variable [NonAssocSemiring R] [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. -/
instance one : One (MonoidAlgebra k G) :=
  ⟨single 1 1⟩
#align monoid_algebra.has_one MonoidAlgebra.one

theorem one_def : (1 : MonoidAlgebra k G) = single 1 1 :=
  rfl
#align monoid_algebra.one_def MonoidAlgebra.one_def

@[simp]
theorem liftNC_one {g_hom : Type*} [FunLike g_hom G R] [OneHomClass g_hom G R]
    (f : k →+* R) (g : g_hom) :
    liftNC (f : k →+ R) g 1 = 1 := by simp [one_def]
#align monoid_algebra.lift_nc_one MonoidAlgebra.liftNC_one

end One

section MulOneClass

variable [Semiring k] [MulOneClass G]

instance nonAssocSemiring : NonAssocSemiring (MonoidAlgebra k G) :=
  { MonoidAlgebra.nonUnitalNonAssocSemiring with
    natCast := fun n => single 1 n
    natCast_zero := by simp
    natCast_succ := fun _ => by simp; rfl
    one_mul := fun f => by
      simp only [mul_def, one_def, sum_single_index, zero_mul, single_zero, sum_zero, zero_add,
        one_mul, sum_single]
    mul_one := fun f => by
      simp only [mul_def, one_def, sum_single_index, mul_zero, single_zero, sum_zero, add_zero,
        mul_one, sum_single] }
#align monoid_algebra.non_assoc_semiring MonoidAlgebra.nonAssocSemiring

theorem natCast_def (n : ℕ) : (n : MonoidAlgebra k G) = single (1 : G) (n : k) :=
  rfl
#align monoid_algebra.nat_cast_def MonoidAlgebra.natCast_def

end MulOneClass

/-! #### Semiring structure -/


section Semiring

variable [Semiring k] [Monoid G]

instance semiring : Semiring (MonoidAlgebra k G) :=
  { MonoidAlgebra.nonUnitalSemiring,
    MonoidAlgebra.nonAssocSemiring with }
#align monoid_algebra.semiring MonoidAlgebra.semiring

variable [Semiring R]

/-- `liftNC` as a `RingHom`, for when `f x` and `g y` commute -/
def liftNCRingHom (f : k →+* R) (g : G →* R) (h_comm : ∀ x y, Commute (f x) (g y)) :
    MonoidAlgebra k G →+* R :=
  { liftNC (f : k →+ R) g with
    map_one' := liftNC_one _ _
    map_mul' := fun _a _b => liftNC_mul _ _ _ _ fun {_ _} _ => h_comm _ _ }
#align monoid_algebra.lift_nc_ring_hom MonoidAlgebra.liftNCRingHom

end Semiring

instance nonUnitalCommSemiring [CommSemiring k] [CommSemigroup G] :
    NonUnitalCommSemiring (MonoidAlgebra k G) :=
  { MonoidAlgebra.nonUnitalSemiring with
    mul_comm := fun f g => by
      simp only [mul_def, Finsupp.sum, mul_comm]
      rw [Finset.sum_comm]
      simp only [mul_comm] }
#align monoid_algebra.non_unital_comm_semiring MonoidAlgebra.nonUnitalCommSemiring

instance nontrivial [Semiring k] [Nontrivial k] [Nonempty G] : Nontrivial (MonoidAlgebra k G) :=
  Finsupp.instNontrivial
#align monoid_algebra.nontrivial MonoidAlgebra.nontrivial

/-! #### Derived instances -/


section DerivedInstances

instance commSemiring [CommSemiring k] [CommMonoid G] : CommSemiring (MonoidAlgebra k G) :=
  { MonoidAlgebra.nonUnitalCommSemiring, MonoidAlgebra.semiring with }
#align monoid_algebra.comm_semiring MonoidAlgebra.commSemiring

instance unique [Semiring k] [Subsingleton k] : Unique (MonoidAlgebra k G) :=
  Finsupp.uniqueOfRight
#align monoid_algebra.unique MonoidAlgebra.unique

instance addCommGroup [Ring k] : AddCommGroup (MonoidAlgebra k G) :=
  Finsupp.instAddCommGroup
#align monoid_algebra.add_comm_group MonoidAlgebra.addCommGroup

instance nonUnitalNonAssocRing [Ring k] [Mul G] : NonUnitalNonAssocRing (MonoidAlgebra k G) :=
  { MonoidAlgebra.addCommGroup, MonoidAlgebra.nonUnitalNonAssocSemiring with }
#align monoid_algebra.non_unital_non_assoc_ring MonoidAlgebra.nonUnitalNonAssocRing

instance nonUnitalRing [Ring k] [Semigroup G] : NonUnitalRing (MonoidAlgebra k G) :=
  { MonoidAlgebra.addCommGroup, MonoidAlgebra.nonUnitalSemiring with }
#align monoid_algebra.non_unital_ring MonoidAlgebra.nonUnitalRing

instance nonAssocRing [Ring k] [MulOneClass G] : NonAssocRing (MonoidAlgebra k G) :=
  { MonoidAlgebra.addCommGroup,
    MonoidAlgebra.nonAssocSemiring with
    intCast := fun z => single 1 (z : k)
    -- Porting note: Both were `simpa`.
    intCast_ofNat := fun n => by simp; rfl
    intCast_negSucc := fun n => by simp; rfl }
#align monoid_algebra.non_assoc_ring MonoidAlgebra.nonAssocRing

theorem intCast_def [Ring k] [MulOneClass G] (z : ℤ) :
    (z : MonoidAlgebra k G) = single (1 : G) (z : k) :=
  rfl
#align monoid_algebra.int_cast_def MonoidAlgebra.intCast_def

instance ring [Ring k] [Monoid G] : Ring (MonoidAlgebra k G) :=
  { MonoidAlgebra.nonAssocRing, MonoidAlgebra.semiring with }
#align monoid_algebra.ring MonoidAlgebra.ring

instance nonUnitalCommRing [CommRing k] [CommSemigroup G] :
    NonUnitalCommRing (MonoidAlgebra k G) :=
  { MonoidAlgebra.nonUnitalCommSemiring, MonoidAlgebra.nonUnitalRing with }
#align monoid_algebra.non_unital_comm_ring MonoidAlgebra.nonUnitalCommRing

instance commRing [CommRing k] [CommMonoid G] : CommRing (MonoidAlgebra k G) :=
  { MonoidAlgebra.nonUnitalCommRing, MonoidAlgebra.ring with }
#align monoid_algebra.comm_ring MonoidAlgebra.commRing

variable {S : Type*}

instance smulZeroClass [Semiring k] [SMulZeroClass R k] : SMulZeroClass R (MonoidAlgebra k G) :=
  Finsupp.smulZeroClass
#align monoid_algebra.smul_zero_class MonoidAlgebra.smulZeroClass

instance distribSMul [Semiring k] [DistribSMul R k] : DistribSMul R (MonoidAlgebra k G) :=
  Finsupp.distribSMul _ _
#align monoid_algebra.distrib_smul MonoidAlgebra.distribSMul

instance distribMulAction [Monoid R] [Semiring k] [DistribMulAction R k] :
    DistribMulAction R (MonoidAlgebra k G) :=
  Finsupp.distribMulAction G k
#align monoid_algebra.distrib_mul_action MonoidAlgebra.distribMulAction

instance module [Semiring R] [Semiring k] [Module R k] : Module R (MonoidAlgebra k G) :=
  Finsupp.module G k
#align monoid_algebra.module MonoidAlgebra.module

instance faithfulSMul [Monoid R] [Semiring k] [DistribMulAction R k] [FaithfulSMul R k]
    [Nonempty G] : FaithfulSMul R (MonoidAlgebra k G) :=
  Finsupp.faithfulSMul
#align monoid_algebra.has_faithful_smul MonoidAlgebra.faithfulSMul

instance isScalarTower [Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMul R S]
    [IsScalarTower R S k] : IsScalarTower R S (MonoidAlgebra k G) :=
  Finsupp.isScalarTower G k
#align monoid_algebra.is_scalar_tower MonoidAlgebra.isScalarTower

instance smulCommClass [Monoid R] [Monoid S] [Semiring k] [DistribMulAction R k]
    [DistribMulAction S k] [SMulCommClass R S k] : SMulCommClass R S (MonoidAlgebra k G) :=
  Finsupp.smulCommClass G k
#align monoid_algebra.smul_comm_tower MonoidAlgebra.smulCommClass

instance isCentralScalar [Monoid R] [Semiring k] [DistribMulAction R k] [DistribMulAction Rᵐᵒᵖ k]
    [IsCentralScalar R k] : IsCentralScalar R (MonoidAlgebra k G) :=
  Finsupp.isCentralScalar G k
#align monoid_algebra.is_central_scalar MonoidAlgebra.isCentralScalar

/-- This is not an instance as it conflicts with `MonoidAlgebra.distribMulAction` when `G = kˣ`.
-/
def comapDistribMulActionSelf [Group G] [Semiring k] : DistribMulAction G (MonoidAlgebra k G) :=
  Finsupp.comapDistribMulAction
#align monoid_algebra.comap_distrib_mul_action_self MonoidAlgebra.comapDistribMulActionSelf

end DerivedInstances

section MiscTheorems

variable [Semiring k]

-- attribute [local reducible] MonoidAlgebra -- Porting note: `reducible` cannot be `local`.

theorem mul_apply [DecidableEq G] [Mul G] (f g : MonoidAlgebra k G) (x : G) :
    (f * g) x = f.sum fun a₁ b₁ => g.sum fun a₂ b₂ => if a₁ * a₂ = x then b₁ * b₂ else 0 := by
  -- Porting note: `reducible` cannot be `local` so proof gets long.
  rw [mul_def, Finsupp.sum_apply]; congr; ext
  rw [Finsupp.sum_apply]; congr; ext
  apply single_apply
#align monoid_algebra.mul_apply MonoidAlgebra.mul_apply

theorem mul_apply_antidiagonal [Mul G] (f g : MonoidAlgebra k G) (x : G) (s : Finset (G × G))
    (hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x) : (f * g) x = ∑ p in s, f p.1 * g p.2 := by
  classical exact
      let F : G × G → k := fun p => if p.1 * p.2 = x then f p.1 * g p.2 else 0
      calc
        (f * g) x = ∑ a₁ in f.support, ∑ a₂ in g.support, F (a₁, a₂) := mul_apply f g x
        _ = ∑ p in f.support ×ˢ g.support, F p := Finset.sum_product.symm
        _ = ∑ p in (f.support ×ˢ g.support).filter fun p : G × G => p.1 * p.2 = x, f p.1 * g p.2 :=
          (Finset.sum_filter _ _).symm
        _ = ∑ p in s.filter fun p : G × G => p.1 ∈ f.support ∧ p.2 ∈ g.support, f p.1 * g p.2 :=
          (sum_congr
            (by
              ext
              simp only [mem_filter, mem_product, hs, and_comm])
            fun _ _ => rfl)
        _ = ∑ p in s, f p.1 * g p.2 :=
          sum_subset (filter_subset _ _) fun p hps hp => by
            simp only [mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢
            by_cases h1 : f p.1 = 0
            · rw [h1, zero_mul]
            · rw [hp hps h1, mul_zero]
#align monoid_algebra.mul_apply_antidiagonal MonoidAlgebra.mul_apply_antidiagonal

@[simp]
theorem single_mul_single [Mul G] {a₁ a₂ : G} {b₁ b₂ : k} :
    single a₁ b₁ * single a₂ b₂ = single (a₁ * a₂) (b₁ * b₂) :=
  (sum_single_index (by simp only [zero_mul, single_zero, sum_zero])).trans
    (sum_single_index (by rw [mul_zero, single_zero]))
#align monoid_algebra.single_mul_single MonoidAlgebra.single_mul_single

theorem single_commute_single [Mul G] {a₁ a₂ : G} {b₁ b₂ : k}
    (ha : Commute a₁ a₂) (hb : Commute b₁ b₂) :
    Commute (single a₁ b₁) (single a₂ b₂) :=
  single_mul_single.trans <| congr_arg₂ single ha hb |>.trans single_mul_single.symm

theorem single_commute [Mul G] {a : G} {b : k} (ha : ∀ a', Commute a a') (hb : ∀ b', Commute b b') :
    ∀ f : MonoidAlgebra k G, Commute (single a b) f :=
  suffices AddMonoidHom.mulLeft (single a b) = AddMonoidHom.mulRight (single a b) from
    DFunLike.congr_fun this
  addHom_ext' fun a' => AddMonoidHom.ext fun b' => single_commute_single (ha a') (hb b')

@[simp]
theorem single_pow [Monoid G] {a : G} {b : k} : ∀ n : ℕ, single a b ^ n = single (a ^ n) (b ^ n)
  | 0 => by
    simp only [pow_zero]
    rfl
  | n + 1 => by simp only [pow_succ, single_pow n, single_mul_single]
#align monoid_algebra.single_pow MonoidAlgebra.single_pow

section

/-- Like `Finsupp.mapDomain_zero`, but for the `1` we define in this file -/
@[simp]
theorem mapDomain_one {α : Type*} {β : Type*} {α₂ : Type*} [Semiring β] [One α] [One α₂]
    {F : Type*} [FunLike F α α₂] [OneHomClass F α α₂] (f : F) :
    (mapDomain f (1 : MonoidAlgebra β α) : MonoidAlgebra β α₂) = (1 : MonoidAlgebra β α₂) := by
  simp_rw [one_def, mapDomain_single, map_one]
#align monoid_algebra.map_domain_one MonoidAlgebra.mapDomain_one

/-- Like `Finsupp.mapDomain_add`, but for the convolutive multiplication we define in this file -/
theorem mapDomain_mul {α : Type*} {β : Type*} {α₂ : Type*} [Semiring β] [Mul α] [Mul α₂]
    {F : Type*} [FunLike F α α₂] [MulHomClass F α α₂] (f : F) (x y : MonoidAlgebra β α) :
    mapDomain f (x * y) = mapDomain f x * mapDomain f y := by
  simp_rw [mul_def, mapDomain_sum, mapDomain_single, map_mul]
  rw [Finsupp.sum_mapDomain_index]
  · congr
    ext a b
    rw [Finsupp.sum_mapDomain_index]
    · simp
    · simp [mul_add]
  · simp
  · simp [add_mul]
#align monoid_algebra.map_domain_mul MonoidAlgebra.mapDomain_mul

variable (k G)

/-- The embedding of a magma into its magma algebra. -/
@[simps]
def ofMagma [Mul G] : G →ₙ* MonoidAlgebra k G where
  toFun a := single a 1
  map_mul' a b := by simp only [mul_def, mul_one, sum_single_index, single_eq_zero, mul_zero]
#align monoid_algebra.of_magma MonoidAlgebra.ofMagma
#align monoid_algebra.of_magma_apply MonoidAlgebra.ofMagma_apply

/-- The embedding of a unital magma into its magma algebra. -/
@[simps]
def of [MulOneClass G] : G →* MonoidAlgebra k G :=
  { ofMagma k G with
    toFun := fun a => single a 1
    map_one' := rfl }
#align monoid_algebra.of MonoidAlgebra.of
#align monoid_algebra.of_apply MonoidAlgebra.of_apply

end

theorem smul_of [MulOneClass G] (g : G) (r : k) : r • of k G g = single g r := by
  -- porting note (#10745): was `simp`.
  rw [of_apply, smul_single', mul_one]
#align monoid_algebra.smul_of MonoidAlgebra.smul_of

theorem of_injective [MulOneClass G] [Nontrivial k] :
    Function.Injective (of k G) := fun a b h => by
  simpa using (single_eq_single_iff _ _ _ _).mp h
#align monoid_algebra.of_injective MonoidAlgebra.of_injective

theorem of_commute [MulOneClass G] {a : G} (h : ∀ a', Commute a a') (f : MonoidAlgebra k G) :
    Commute (of k G a) f :=
  single_commute h Commute.one_left f

/-- `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`.
-/
@[simps]
def singleHom [MulOneClass G] : k × G →* MonoidAlgebra k G where
  toFun a := single a.2 a.1
  map_one' := rfl
  map_mul' _a _b := single_mul_single.symm
#align monoid_algebra.single_hom MonoidAlgebra.singleHom
#align monoid_algebra.single_hom_apply MonoidAlgebra.singleHom_apply

theorem mul_single_apply_aux [Mul G] (f : MonoidAlgebra k G) {r : k} {x y z : G}
    (H : ∀ a, a * x = z ↔ a = y) : (f * single x r) z = f y * r := by
  classical exact
      have A :
        ∀ a₁ b₁,
          ((single x r).sum fun a₂ b₂ => ite (a₁ * a₂ = z) (b₁ * b₂) 0) =
            ite (a₁ * x = z) (b₁ * r) 0 :=
        fun a₁ b₁ => sum_single_index <| by simp
      calc
        (HMul.hMul (β := MonoidAlgebra k G) f (single x r)) z =
            sum f fun a b => if a = y then b * r else 0 := by simp only [mul_apply, A, H]
        _ = if y ∈ f.support then f y * r else 0 := f.support.sum_ite_eq' _ _
        _ = f y * r := by split_ifs with h <;> simp at h <;> simp [h]
#align monoid_algebra.mul_single_apply_aux MonoidAlgebra.mul_single_apply_aux

theorem mul_single_one_apply [MulOneClass G] (f : MonoidAlgebra k G) (r : k) (x : G) :
    (HMul.hMul (β := MonoidAlgebra k G) f (single 1 r)) x = f x * r :=
  f.mul_single_apply_aux fun a => by rw [mul_one]
#align monoid_algebra.mul_single_one_apply MonoidAlgebra.mul_single_one_apply

theorem mul_single_apply_of_not_exists_mul [Mul G] (r : k) {g g' : G} (x : MonoidAlgebra k G)
    (h : ¬∃ d, g' = d * g) : (x * single g r) g' = 0 := by
  classical
    rw [mul_apply, Finsupp.sum_comm, Finsupp.sum_single_index]
    swap
    · simp_rw [Finsupp.sum, mul_zero, ite_self, Finset.sum_const_zero]
    · apply Finset.sum_eq_zero
      simp_rw [ite_eq_right_iff]
      rintro g'' _hg'' rfl
      exfalso
      exact h ⟨_, rfl⟩
#align monoid_algebra.mul_single_apply_of_not_exists_mul MonoidAlgebra.mul_single_apply_of_not_exists_mul

theorem single_mul_apply_aux [Mul G] (f : MonoidAlgebra k G) {r : k} {x y z : G}
    (H : ∀ a, x * a = y ↔ a = z) : (single x r * f) y = r * f z := by
  classical exact
      have : (f.sum fun a b => ite (x * a = y) (0 * b) 0) = 0 := by simp
      calc
        (HMul.hMul (α := MonoidAlgebra k G) (single x r) f) y =
            sum f fun a b => ite (x * a = y) (r * b) 0 :=
          (mul_apply _ _ _).trans <| sum_single_index this
        _ = f.sum fun a b => ite (a = z) (r * b) 0 := by simp only [H]
        _ = if z ∈ f.support then r * f z else 0 := f.support.sum_ite_eq' _ _
        _ = _ := by split_ifs with h <;> simp at h <;> simp [h]
#align monoid_algebra.single_mul_apply_aux MonoidAlgebra.single_mul_apply_aux

theorem single_one_mul_apply [MulOneClass G] (f : MonoidAlgebra k G) (r : k) (x : G) :
    (single (1 : G) r * f) x = r * f x :=
  f.single_mul_apply_aux fun a => by rw [one_mul]
#align monoid_algebra.single_one_mul_apply MonoidAlgebra.single_one_mul_apply

theorem single_mul_apply_of_not_exists_mul [Mul G] (r : k) {g g' : G} (x : MonoidAlgebra k G)
    (h : ¬∃ d, g' = g * d) : (single g r * x) g' = 0 := by
  classical
    rw [mul_apply, Finsupp.sum_single_index]
    swap
    · simp_rw [Finsupp.sum, zero_mul, ite_self, Finset.sum_const_zero]
    · apply Finset.sum_eq_zero
      simp_rw [ite_eq_right_iff]
      rintro g'' _hg'' rfl
      exfalso
      exact h ⟨_, rfl⟩
#align monoid_algebra.single_mul_apply_of_not_exists_mul MonoidAlgebra.single_mul_apply_of_not_exists_mul

theorem liftNC_smul [MulOneClass G] {R : Type*} [Semiring R] (f : k →+* R) (g : G →* R) (c : k)
    (φ : MonoidAlgebra k G) : liftNC (f : k →+ R) g (c • φ) = f c * liftNC (f : k →+ R) g φ := by
  suffices (liftNC (↑f) g).comp (smulAddHom k (MonoidAlgebra k G) c) =
      (AddMonoidHom.mulLeft (f c)).comp (liftNC (↑f) g) from
    DFunLike.congr_fun this φ
  -- Porting note: `ext` couldn't a find appropriate theorem.
  refine addHom_ext' fun a => AddMonoidHom.ext fun b => ?_
  -- Porting note: `reducible` cannot be `local` so the proof gets more complex.
  unfold MonoidAlgebra
  simp only [AddMonoidHom.coe_comp, Function.comp_apply, singleAddHom_apply, smulAddHom_apply,
    smul_single, smul_eq_mul, AddMonoidHom.coe_mulLeft]
  -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
  erw [liftNC_single, liftNC_single]; rw [AddMonoidHom.coe_coe, map_mul, mul_assoc]
#align monoid_algebra.lift_nc_smul MonoidAlgebra.liftNC_smul

end MiscTheorems

/-! #### Non-unital, non-associative algebra structure -/


section NonUnitalNonAssocAlgebra

variable (k) [Semiring k] [DistribSMul R k] [Mul G]

instance isScalarTower_self [IsScalarTower R k k] :
    IsScalarTower R (MonoidAlgebra k G) (MonoidAlgebra k G) :=
  ⟨fun t a b => by
    -- Porting note: `ext` → `refine Finsupp.ext fun _ => ?_`
    refine Finsupp.ext fun m => ?_
    -- Porting note: `refine` & `rw` are required because `simp` behaves differently.
    classical
      simp only [smul_eq_mul, mul_apply]
      rw [coe_smul]
      refine Eq.trans (sum_smul_index' (g := a) (b := t) ?_) ?_ <;>
        simp only [mul_apply, Finsupp.smul_sum, smul_ite, smul_mul_assoc,
          zero_mul, ite_self, imp_true_iff, sum_zero, Pi.smul_apply, smul_zero]⟩
#align monoid_algebra.is_scalar_tower_self MonoidAlgebra.isScalarTower_self

/-- Note that if `k` is a `CommSemiring` then we have `SMulCommClass k k k` and so we can take
`R = k` in the below. In other words, if the coefficients are commutative amongst themselves, they
also commute with the algebra multiplication. -/
instance smulCommClass_self [SMulCommClass R k k] :
    SMulCommClass R (MonoidAlgebra k G) (MonoidAlgebra k G) :=
  ⟨fun t a b => by
    -- Porting note: `ext` → `refine Finsupp.ext fun _ => ?_`
    refine Finsupp.ext fun m => ?_
    -- Porting note: `refine` & `rw` are required because `simp` behaves differently.
    classical
      simp only [smul_eq_mul, mul_apply]
      rw [coe_smul]
      refine Eq.symm (Eq.trans (congr_arg (sum a)
        (funext₂ fun a₁ b₁ => sum_smul_index' (g := b) (b := t) ?_)) ?_) <;>
      simp only [mul_apply, Finsupp.sum, Finset.smul_sum, smul_ite, mul_smul_comm,
        imp_true_iff, ite_eq_right_iff, Pi.smul_apply, mul_zero, smul_zero]⟩
#align monoid_algebra.smul_comm_class_self MonoidAlgebra.smulCommClass_self

instance smulCommClass_symm_self [SMulCommClass k R k] :
    SMulCommClass (MonoidAlgebra k G) R (MonoidAlgebra k G) :=
  ⟨fun t a b => by
    haveI := SMulCommClass.symm k R k
    rw [← smul_comm]⟩
#align monoid_algebra.smul_comm_class_symm_self MonoidAlgebra.smulCommClass_symm_self

variable {A : Type u₃} [NonUnitalNonAssocSemiring A]

/-- A non_unital `k`-algebra homomorphism from `MonoidAlgebra k G` is uniquely defined by its
values on the functions `single a 1`. -/
theorem nonUnitalAlgHom_ext [DistribMulAction k A] {φ₁ φ₂ : MonoidAlgebra k G →ₙₐ[k] A}
    (h : ∀ x, φ₁ (single x 1) = φ₂ (single x 1)) : φ₁ = φ₂ :=
  NonUnitalAlgHom.to_distribMulActionHom_injective <|
    Finsupp.distribMulActionHom_ext' fun a => DistribMulActionHom.ext_ring (h a)
#align monoid_algebra.non_unital_alg_hom_ext MonoidAlgebra.nonUnitalAlgHom_ext

/-- See note [partially-applied ext lemmas]. -/
@[ext high]
theorem nonUnitalAlgHom_ext' [DistribMulAction k A] {φ₁ φ₂ : MonoidAlgebra k G →ₙₐ[k] A}
    (h : φ₁.toMulHom.comp (ofMagma k G) = φ₂.toMulHom.comp (ofMagma k G)) : φ₁ = φ₂ :=
  nonUnitalAlgHom_ext k <| DFunLike.congr_fun h
#align monoid_algebra.non_unital_alg_hom_ext' MonoidAlgebra.nonUnitalAlgHom_ext'

/-- 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. -/
@[simps apply_apply symm_apply]
def liftMagma [Module k A] [IsScalarTower k A A] [SMulCommClass k A A] :
    (G →ₙ* A) ≃ (MonoidAlgebra k G →ₙₐ[k] A) where
  toFun f :=
    { liftAddHom fun x => (smulAddHom k A).flip (f x) with
      toFun := fun a => a.sum fun m t => t • f m
      map_smul' := fun t' a => by
        -- Porting note(#12129): additional beta reduction needed
        beta_reduce
        rw [Finsupp.smul_sum, sum_smul_index']
        · simp_rw [smul_assoc, MonoidHom.id_apply]
        · intro m
          exact zero_smul k (f m)
      map_mul' := fun a₁ a₂ => by
        let g : G → k → A := fun m t => t • f m
        have h₁ : ∀ m, g m 0 = 0 := by
          intro m
          exact zero_smul k (f m)
        have h₂ : ∀ (m) (t₁ t₂ : k), g m (t₁ + t₂) = g m t₁ + g m t₂ := by
          intros
          rw [← add_smul]
        -- Porting note: `reducible` cannot be `local` so proof gets long.
        simp_rw [Finsupp.mul_sum, Finsupp.sum_mul, smul_mul_smul, ← f.map_mul, mul_def,
          sum_comm a₂ a₁]
        rw [sum_sum_index h₁ h₂]; congr; ext
        rw [sum_sum_index h₁ h₂]; congr; ext
        rw [sum_single_index (h₁ _)] }
  invFun F := F.toMulHom.comp (ofMagma k G)
  left_inv f := by
    ext m
    simp only [NonUnitalAlgHom.coe_mk, ofMagma_apply, NonUnitalAlgHom.toMulHom_eq_coe,
      sum_single_index, Function.comp_apply, one_smul, zero_smul, MulHom.coe_comp,
      NonUnitalAlgHom.coe_to_mulHom]
  right_inv F := by
    -- Porting note: `ext` → `refine nonUnitalAlgHom_ext' k (MulHom.ext fun m => ?_)`
    refine nonUnitalAlgHom_ext' k (MulHom.ext fun m => ?_)
    simp only [NonUnitalAlgHom.coe_mk, ofMagma_apply, NonUnitalAlgHom.toMulHom_eq_coe,
      sum_single_index, Function.comp_apply, one_smul, zero_smul, MulHom.coe_comp,
      NonUnitalAlgHom.coe_to_mulHom]
#align monoid_algebra.lift_magma MonoidAlgebra.liftMagma
#align monoid_algebra.lift_magma_apply_apply MonoidAlgebra.liftMagma_apply_apply
#align monoid_algebra.lift_magma_symm_apply MonoidAlgebra.liftMagma_symm_apply

end NonUnitalNonAssocAlgebra

/-! #### Algebra structure -/


section Algebra

-- attribute [local reducible] MonoidAlgebra -- Porting note: `reducible` cannot be `local`.

theorem single_one_comm [CommSemiring k] [MulOneClass G] (r : k) (f : MonoidAlgebra k G) :
    single (1 : G) r * f = f * single (1 : G) r :=
  single_commute Commute.one_left (Commute.all _) f
#align monoid_algebra.single_one_comm MonoidAlgebra.single_one_comm

/-- `Finsupp.single 1` as a `RingHom` -/
@[simps]
def singleOneRingHom [Semiring k] [MulOneClass G] : k →+* MonoidAlgebra k G :=
  { Finsupp.singleAddHom 1 with
    map_one' := rfl
    map_mul' := fun x y => by
      -- Porting note (#10691): Was `rw`.
      simp only [ZeroHom.toFun_eq_coe, AddMonoidHom.toZeroHom_coe, singleAddHom_apply,
        single_mul_single, mul_one] }
#align monoid_algebra.single_one_ring_hom MonoidAlgebra.singleOneRingHom
#align monoid_algebra.single_one_ring_hom_apply MonoidAlgebra.singleOneRingHom_apply

/-- If `f : G → H` is a multiplicative homomorphism between two monoids, then
`Finsupp.mapDomain f` is a ring homomorphism between their monoid algebras. -/
@[simps]
def mapDomainRingHom (k : Type*) {H F : Type*} [Semiring k] [Monoid G] [Monoid H]
    [FunLike F G H] [MonoidHomClass F G H] (f : F) : MonoidAlgebra k G →+* MonoidAlgebra k H :=
  { (Finsupp.mapDomain.addMonoidHom f : MonoidAlgebra k G →+ MonoidAlgebra k H) with
    map_one' := mapDomain_one f
    map_mul' := fun x y => mapDomain_mul f x y }
#align monoid_algebra.map_domain_ring_hom MonoidAlgebra.mapDomainRingHom
#align monoid_algebra.map_domain_ring_hom_apply MonoidAlgebra.mapDomainRingHom_apply

/-- If two ring homomorphisms from `MonoidAlgebra k G` are equal on all `single a 1`
and `single 1 b`, then they are equal. -/
theorem ringHom_ext {R} [Semiring k] [MulOneClass G] [Semiring R] {f g : MonoidAlgebra k G →+* R}
    (h₁ : ∀ b, f (single 1 b) = g (single 1 b)) (h_of : ∀ a, f (single a 1) = g (single a 1)) :
    f = g :=
  RingHom.coe_addMonoidHom_injective <|
    addHom_ext fun a b => by
      rw [← single, ← one_mul a, ← mul_one b, ← single_mul_single]
      -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
      erw [AddMonoidHom.coe_coe f, AddMonoidHom.coe_coe g]; rw [f.map_mul, g.map_mul, h₁, h_of]
#align monoid_algebra.ring_hom_ext MonoidAlgebra.ringHom_ext

/-- 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]. -/
@[ext high]
theorem ringHom_ext' {R} [Semiring k] [MulOneClass G] [Semiring R] {f g : MonoidAlgebra k G →+* R}
    (h₁ : f.comp singleOneRingHom = g.comp singleOneRingHom)
    (h_of :
      (f : MonoidAlgebra k G →* R).comp (of k G) = (g : MonoidAlgebra k G →* R).comp (of k G)) :
    f = g :=
  ringHom_ext (RingHom.congr_fun h₁) (DFunLike.congr_fun h_of)
#align monoid_algebra.ring_hom_ext' MonoidAlgebra.ringHom_ext'

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

In particular this provides the instance `Algebra k (MonoidAlgebra k G)`.
-/
instance algebra {A : Type*} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] :
    Algebra k (MonoidAlgebra A G) :=
  { singleOneRingHom.comp (algebraMap k A) with
    -- Porting note: `ext` → `refine Finsupp.ext fun _ => ?_`
    smul_def' := fun r a => by
      refine Finsupp.ext fun _ => ?_
      -- Porting note: Newly required.
      rw [Finsupp.coe_smul]
      simp [single_one_mul_apply, Algebra.smul_def, Pi.smul_apply]
    commutes' := fun r f => by
      refine Finsupp.ext fun _ => ?_
      simp [single_one_mul_apply, mul_single_one_apply, Algebra.commutes] }

/-- `Finsupp.single 1` as an `AlgHom` -/
@[simps! apply]
def singleOneAlgHom {A : Type*} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] :
    A →ₐ[k] MonoidAlgebra A G :=
  { singleOneRingHom with
    commutes' := fun r => by
      -- Porting note: `ext` → `refine Finsupp.ext fun _ => ?_`
      refine Finsupp.ext fun _ => ?_
      simp
      rfl }
#align monoid_algebra.single_one_alg_hom MonoidAlgebra.singleOneAlgHom
#align monoid_algebra.single_one_alg_hom_apply MonoidAlgebra.singleOneAlgHom_apply

@[simp]
theorem coe_algebraMap {A : Type*} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] :
    ⇑(algebraMap k (MonoidAlgebra A G)) = single 1 ∘ algebraMap k A :=
  rfl
#align monoid_algebra.coe_algebra_map MonoidAlgebra.coe_algebraMap

theorem single_eq_algebraMap_mul_of [CommSemiring k] [Monoid G] (a : G) (b : k) :
    single a b = algebraMap k (MonoidAlgebra k G) b * of k G a := by simp
#align monoid_algebra.single_eq_algebra_map_mul_of MonoidAlgebra.single_eq_algebraMap_mul_of

theorem single_algebraMap_eq_algebraMap_mul_of {A : Type*} [CommSemiring k] [Semiring A]
    [Algebra k A] [Monoid G] (a : G) (b : k) :
    single a (algebraMap k A b) = algebraMap k (MonoidAlgebra A G) b * of A G a := by simp
#align monoid_algebra.single_algebra_map_eq_algebra_map_mul_of MonoidAlgebra.single_algebraMap_eq_algebraMap_mul_of

theorem induction_on [Semiring k] [Monoid G] {p : MonoidAlgebra k G → Prop} (f : MonoidAlgebra k G)
    (hM : ∀ g, p (of k G g)) (hadd : ∀ f g : MonoidAlgebra k G, p f → p g → p (f + g))
    (hsmul : ∀ (r : k) (f), p f → p (r • f)) : p f := by
  refine' Finsupp.induction_linear f _ (fun f g hf hg => hadd f g hf hg) fun g r => _
  · simpa using hsmul 0 (of k G 1) (hM 1)
  · convert hsmul r (of k G g) (hM g)
    -- Porting note: Was `simp only`.
    rw [of_apply, smul_single', mul_one]
#align monoid_algebra.induction_on MonoidAlgebra.induction_on

end Algebra

section lift

variable [CommSemiring k] [Monoid G] [Monoid H]
variable {A : Type u₃} [Semiring A] [Algebra k A] {B : Type*} [Semiring B] [Algebra k B]

/-- `liftNCRingHom` as an `AlgHom`, for when `f` is an `AlgHom` -/
def liftNCAlgHom (f : A →ₐ[k] B) (g : G →* B) (h_comm : ∀ x y, Commute (f x) (g y)) :
    MonoidAlgebra A G →ₐ[k] B :=
  { liftNCRingHom (f : A →+* B) g h_comm with
    commutes' := by simp [liftNCRingHom] }
#align monoid_algebra.lift_nc_alg_hom MonoidAlgebra.liftNCAlgHom

/-- A `k`-algebra homomorphism from `MonoidAlgebra k G` is uniquely defined by its
values on the functions `single a 1`. -/
theorem algHom_ext ⦃φ₁ φ₂ : MonoidAlgebra k G →ₐ[k] A⦄
    (h : ∀ x, φ₁ (single x 1) = φ₂ (single x 1)) : φ₁ = φ₂ :=
  AlgHom.toLinearMap_injective <| Finsupp.lhom_ext' fun a => LinearMap.ext_ring (h a)
#align monoid_algebra.alg_hom_ext MonoidAlgebra.algHom_ext

-- Porting note: The priority must be `high`.
/-- See note [partially-applied ext lemmas]. -/
@[ext high]
theorem algHom_ext' ⦃φ₁ φ₂ : MonoidAlgebra k G →ₐ[k] A⦄
    (h :
      (φ₁ : MonoidAlgebra k G →* A).comp (of k G) = (φ₂ : MonoidAlgebra k G →* A).comp (of k G)) :
    φ₁ = φ₂ :=
  algHom_ext <| DFunLike.congr_fun h
#align monoid_algebra.alg_hom_ext' MonoidAlgebra.algHom_ext'

variable (k G A)

/-- Any monoid homomorphism `G →* A` can be lifted to an algebra homomorphism
`MonoidAlgebra k G →ₐ[k] A`. -/
def lift : (G →* A) ≃ (MonoidAlgebra k G →ₐ[k] A) where
  invFun f := (f : MonoidAlgebra k G →* A).comp (of k G)
  toFun F := liftNCAlgHom (Algebra.ofId k A) F fun _ _ => Algebra.commutes _ _
  left_inv f := by
    ext
    simp [liftNCAlgHom, liftNCRingHom]
  right_inv F := by
    ext
    simp [liftNCAlgHom, liftNCRingHom]
#align monoid_algebra.lift MonoidAlgebra.lift

variable {k G H A}

theorem lift_apply' (F : G →* A) (f : MonoidAlgebra k G) :
    lift k G A F f = f.sum fun a b => algebraMap k A b * F a :=
  rfl
#align monoid_algebra.lift_apply' MonoidAlgebra.lift_apply'

theorem lift_apply (F : G →* A) (f : MonoidAlgebra k G) :
    lift k G A F f = f.sum fun a b => b • F a := by simp only [lift_apply', Algebra.smul_def]
#align monoid_algebra.lift_apply MonoidAlgebra.lift_apply

theorem lift_def (F : G →* A) : ⇑(lift k G A F) = liftNC ((algebraMap k A : k →+* A) : k →+ A) F :=
  rfl
#align monoid_algebra.lift_def MonoidAlgebra.lift_def

@[simp]
theorem lift_symm_apply (F : MonoidAlgebra k G →ₐ[k] A) (x : G) :
    (lift k G A).symm F x = F (single x 1) :=
  rfl
#align monoid_algebra.lift_symm_apply MonoidAlgebra.lift_symm_apply

@[simp]
theorem lift_single (F : G →* A) (a b) : lift k G A F (single a b) = b • F a := by
  rw [lift_def, liftNC_single, Algebra.smul_def, AddMonoidHom.coe_coe]
#align monoid_algebra.lift_single MonoidAlgebra.lift_single

theorem lift_of (F : G →* A) (x) : lift k G A F (of k G x) = F x := by simp
#align monoid_algebra.lift_of MonoidAlgebra.lift_of

theorem lift_unique' (F : MonoidAlgebra k G →ₐ[k] A) :
    F = lift k G A ((F : MonoidAlgebra k G →* A).comp (of k G)) :=
  ((lift k G A).apply_symm_apply F).symm
#align monoid_algebra.lift_unique' MonoidAlgebra.lift_unique'

/-- Decomposition of a `k`-algebra homomorphism from `MonoidAlgebra k G` by
its values on `F (single a 1)`. -/
theorem lift_unique (F : MonoidAlgebra k G →ₐ[k] A) (f : MonoidAlgebra k G) :
    F f = f.sum fun a b => b • F (single a 1) := by
  conv_lhs =>
    rw [lift_unique' F]
    simp [lift_apply]
#align monoid_algebra.lift_unique MonoidAlgebra.lift_unique

/-- If `f : G → H` is a homomorphism between two magmas, then
`Finsupp.mapDomain f` is a non-unital algebra homomorphism between their magma algebras. -/
@[simps apply]
def mapDomainNonUnitalAlgHom (k A : Type*) [CommSemiring k] [Semiring A] [Algebra k A]
    {G H F : Type*} [Mul G] [Mul H] [FunLike F G H] [MulHomClass F G H] (f : F) :
    MonoidAlgebra A G →ₙₐ[k] MonoidAlgebra A H :=
  { (Finsupp.mapDomain.addMonoidHom f : MonoidAlgebra A G →+ MonoidAlgebra A H) with
    map_mul' := fun x y => mapDomain_mul f x y
    map_smul' := fun r x => mapDomain_smul r x }
#align monoid_algebra.map_domain_non_unital_alg_hom MonoidAlgebra.mapDomainNonUnitalAlgHom
#align monoid_algebra.map_domain_non_unital_alg_hom_apply MonoidAlgebra.mapDomainNonUnitalAlgHom_apply

variable (A) in
theorem mapDomain_algebraMap {F : Type*} [FunLike F G H] [MonoidHomClass F G H] (f : F) (r : k) :
    mapDomain f (algebraMap k (MonoidAlgebra A G) r) = algebraMap k (MonoidAlgebra A H) r := by
  simp only [coe_algebraMap, mapDomain_single, map_one, (· ∘ ·)]
#align monoid_algebra.map_domain_algebra_map MonoidAlgebra.mapDomain_algebraMap

/-- If `f : G → H` is a multiplicative homomorphism between two monoids, then
`Finsupp.mapDomain f` is an algebra homomorphism between their monoid algebras. -/
@[simps!]
def mapDomainAlgHom (k A : Type*) [CommSemiring k] [Semiring A] [Algebra k A] {H F : Type*}
    [Monoid H] [FunLike F G H] [MonoidHomClass F G H] (f : F) :
    MonoidAlgebra A G →ₐ[k] MonoidAlgebra A H :=
  { mapDomainRingHom A f with commutes' := mapDomain_algebraMap A f }
#align monoid_algebra.map_domain_alg_hom MonoidAlgebra.mapDomainAlgHom
#align monoid_algebra.map_domain_alg_hom_apply MonoidAlgebra.mapDomainAlgHom_apply

variable (k A)

/-- If `e : G ≃* H` is a multiplicative equivalence between two monoids, then
`MonoidAlgebra.domCongr e` is an algebra equivalence between their monoid algebras. -/
def domCongr (e : G ≃* H) : MonoidAlgebra A G ≃ₐ[k] MonoidAlgebra A H :=
  AlgEquiv.ofLinearEquiv
    (Finsupp.domLCongr e : (G →₀ A) ≃ₗ[k] (H →₀ A))
    ((equivMapDomain_eq_mapDomain _ _).trans <| mapDomain_one e)
    (fun f g => (equivMapDomain_eq_mapDomain _ _).trans <| (mapDomain_mul e f g).trans <|
        congr_arg₂ _ (equivMapDomain_eq_mapDomain _ _).symm (equivMapDomain_eq_mapDomain _ _).symm)

theorem domCongr_toAlgHom (e : G ≃* H) : (domCongr k A e).toAlgHom = mapDomainAlgHom k A e :=
  AlgHom.ext fun _ => equivMapDomain_eq_mapDomain _ _

@[simp] theorem domCongr_apply (e : G ≃* H) (f : MonoidAlgebra A G) (h : H) :
    domCongr k A e f h = f (e.symm h) :=
  rfl

@[simp] theorem domCongr_support (e : G ≃* H) (f : MonoidAlgebra A G) :
    (domCongr k A e f).support = f.support.map e :=
  rfl

@[simp] theorem domCongr_single (e : G ≃* H) (g : G) (a : A) :
    domCongr k A e (single g a) = single (e g) a :=
  Finsupp.equivMapDomain_single _ _ _

@[simp] theorem domCongr_refl : domCongr k A (MulEquiv.refl G) = AlgEquiv.refl :=
  AlgEquiv.ext fun _ => Finsupp.ext fun _ => rfl

@[simp] theorem domCongr_symm (e : G ≃* H) : (domCongr k A e).symm = domCongr k A e.symm := rfl

end lift

section

-- attribute [local reducible] MonoidAlgebra -- Porting note: `reducible` cannot be `local`.

variable (k)

/-- When `V` is a `k[G]`-module, multiplication by a group element `g` is a `k`-linear map. -/
def GroupSMul.linearMap [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 →ₗ[k] V
    where
  toFun v := single g (1 : k) • v
  map_add' x y := smul_add (single g (1 : k)) x y
  map_smul' _c _x := smul_algebra_smul_comm _ _ _
#align monoid_algebra.group_smul.linear_map MonoidAlgebra.GroupSMul.linearMap

@[simp]
theorem GroupSMul.linearMap_apply [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) : (GroupSMul.linearMap k V g) v = single g (1 : k) • v :=
  rfl
#align monoid_algebra.group_smul.linear_map_apply MonoidAlgebra.GroupSMul.linearMap_apply

section

variable {k}
variable [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 (single g (1 : k) • v) = single g (1 : k) • f v)

/-- Build a `k[G]`-linear map from a `k`-linear map and evidence that it is `G`-equivariant. -/
def equivariantOfLinearOfComm : V →ₗ[MonoidAlgebra k G] W where
  toFun := f
  map_add' v v' := by simp
  map_smul' c v := by
    -- Porting note(#12129): additional beta reduction needed
    beta_reduce
    -- Porting note: Was `apply`.
    refine Finsupp.induction c ?_ ?_
    · simp
    · intro g r c' _nm _nz w
      dsimp at *
      simp only [add_smul, f.map_add, w, add_left_inj, single_eq_algebraMap_mul_of, ← smul_smul]
      erw [algebraMap_smul (MonoidAlgebra k G) r, algebraMap_smul (MonoidAlgebra k G) r, f.map_smul,
        h g v, of_apply]
#align monoid_algebra.equivariant_of_linear_of_comm MonoidAlgebra.equivariantOfLinearOfComm

@[simp]
theorem equivariantOfLinearOfComm_apply (v : V) : (equivariantOfLinearOfComm f h) v = f v :=
  rfl
#align monoid_algebra.equivariant_of_linear_of_comm_apply MonoidAlgebra.equivariantOfLinearOfComm_apply

end

end

section

universe ui

variable {ι : Type ui}

-- attribute [local reducible] MonoidAlgebra -- Porting note: `reducible` cannot be `local`.

theorem prod_single [CommSemiring k] [CommMonoid G] {s : Finset ι} {a : ι → G} {b : ι → k} :
    (∏ i in s, single (a i) (b i)) = single (∏ i in s, a i) (∏ i in s, b i) :=
  Finset.cons_induction_on s rfl fun a s has ih => by
    rw [prod_cons has, ih, single_mul_single, prod_cons has, prod_cons has]
#align monoid_algebra.prod_single MonoidAlgebra.prod_single

end

section

-- We now prove some additional statements that hold for group algebras.
variable [Semiring k] [Group G]

-- attribute [local reducible] MonoidAlgebra -- Porting note: `reducible` cannot be `local`.

@[simp]
theorem mul_single_apply (f : MonoidAlgebra k G) (r : k) (x y : G) :
    (f * single x r) y = f (y * x⁻¹) * r :=
  f.mul_single_apply_aux fun _a => eq_mul_inv_iff_mul_eq.symm
#align monoid_algebra.mul_single_apply MonoidAlgebra.mul_single_apply

@[simp]
theorem single_mul_apply (r : k) (x : G) (f : MonoidAlgebra k G) (y : G) :
    (single x r * f) y = r * f (x⁻¹ * y) :=
  f.single_mul_apply_aux fun _z => eq_inv_mul_iff_mul_eq.symm
#align monoid_algebra.single_mul_apply MonoidAlgebra.single_mul_apply

theorem mul_apply_left (f g : MonoidAlgebra k G) (x : G) :
    (f * g) x = f.sum fun a b => b * g (a⁻¹ * x) :=
  calc
    (f * g) x = sum f fun a b => (single a b * g) x := by
      rw [← Finsupp.sum_apply, ← Finsupp.sum_mul g f, f.sum_single]
    _ = _ := by simp only [single_mul_apply, Finsupp.sum]
#align monoid_algebra.mul_apply_left MonoidAlgebra.mul_apply_left

-- If we'd assumed `CommSemiring`, we could deduce this from `mul_apply_left`.
theorem mul_apply_right (f g : MonoidAlgebra k G) (x : G) :
    (f * g) x = g.sum fun a b => f (x * a⁻¹) * b :=
  calc
    (f * g) x = sum g fun a b => (f * single a b) x := by
      rw [← Finsupp.sum_apply, ← Finsupp.mul_sum f g, g.sum_single]
    _ = _ := by simp only [mul_single_apply, Finsupp.sum]
#align monoid_algebra.mul_apply_right MonoidAlgebra.mul_apply_right

end

section Opposite

open Finsupp MulOpposite

variable [Semiring k]

/-- 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. -/
@[simps! (config := { simpRhs := true }) apply symm_apply]
protected noncomputable def opRingEquiv [Monoid G] :
    (MonoidAlgebra k G)ᵐᵒᵖ ≃+* MonoidAlgebra kᵐᵒᵖ Gᵐᵒᵖ :=
  { opAddEquiv.symm.trans <|
      (Finsupp.mapRange.addEquiv (opAddEquiv : k ≃+ kᵐᵒᵖ)).trans <| Finsupp.domCongr opEquiv with
    map_mul' := by
      -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
      rw [Equiv.toFun_as_coe, AddEquiv.toEquiv_eq_coe]; erw [AddEquiv.coe_toEquiv]
      rw [← AddEquiv.coe_toAddMonoidHom]
      refine Iff.mpr (AddMonoidHom.map_mul_iff (R := (MonoidAlgebra k G)ᵐᵒᵖ)
        (S := MonoidAlgebra kᵐᵒᵖ Gᵐᵒᵖ) _) ?_
      -- Porting note: Was `ext`.
      refine AddMonoidHom.mul_op_ext _ _ <| addHom_ext' fun i₁ => AddMonoidHom.ext fun r₁ =>
        AddMonoidHom.mul_op_ext _ _ <| addHom_ext' fun i₂ => AddMonoidHom.ext fun r₂ => ?_
      -- Porting note: `reducible` cannot be `local` so proof gets long.
      simp only [AddMonoidHom.coe_comp, AddEquiv.coe_toAddMonoidHom, opAddEquiv_apply,
        Function.comp_apply, singleAddHom_apply, AddMonoidHom.compr₂_apply, AddMonoidHom.coe_mul,
        AddMonoidHom.coe_mulLeft, AddMonoidHom.compl₂_apply]
      -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
      erw [AddEquiv.trans_apply, AddEquiv.trans_apply, AddEquiv.trans_apply, AddEquiv.trans_apply,
        AddEquiv.trans_apply, AddEquiv.trans_apply, MulOpposite.opAddEquiv_symm_apply]
      rw [MulOpposite.unop_mul (α := MonoidAlgebra k G)]
      -- This was not needed before leanprover/lean4#2644
      erw [unop_op, unop_op, single_mul_single]
      simp }
#align monoid_algebra.op_ring_equiv MonoidAlgebra.opRingEquiv
#align monoid_algebra.op_ring_equiv_apply MonoidAlgebra.opRingEquiv_apply
#align monoid_algebra.op_ring_equiv_symm_apply MonoidAlgebra.opRingEquiv_symm_apply

-- @[simp] -- Porting note (#10618): simp can prove this
theorem opRingEquiv_single [Monoid G] (r : k) (x : G) :
    MonoidAlgebra.opRingEquiv (op (single x r)) = single (op x) (op r) := by simp
#align monoid_algebra.op_ring_equiv_single MonoidAlgebra.opRingEquiv_single

-- @[simp] -- Porting note (#10618): simp can prove this
theorem opRingEquiv_symm_single [Monoid G] (r : kᵐᵒᵖ) (x : Gᵐᵒᵖ) :
    MonoidAlgebra.opRingEquiv.symm (single x r) = op (single x.unop r.unop) := by simp
#align monoid_algebra.op_ring_equiv_symm_single MonoidAlgebra.opRingEquiv_symm_single

end Opposite

section Submodule

variable [CommSemiring k] [Monoid G]
variable {V : Type*} [AddCommMonoid V]
variable [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V]

/-- A submodule over `k` which is stable under scalar multiplication by elements of `G` is a
submodule over `MonoidAlgebra k G`  -/
def submoduleOfSMulMem (W : Submodule k V) (h : ∀ (g : G) (v : V), v ∈ W → of k G g • v ∈ W) :
    Submodule (MonoidAlgebra k G) V where
  carrier := W
  zero_mem' := W.zero_mem'
  add_mem' := W.add_mem'
  smul_mem' := by
    intro f v hv
    rw [← Finsupp.sum_single f, Finsupp.sum, Finset.sum_smul]
    simp_rw [← smul_of, smul_assoc]
    exact Submodule.sum_smul_mem W _ fun g _ => h g v hv
#align monoid_algebra.submodule_of_smul_mem MonoidAlgebra.submoduleOfSMulMem

end Submodule

end MonoidAlgebra

/-! ### Additive monoids -/


section

variable [Semiring k]

/-- 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.
-/
def AddMonoidAlgebra :=
  G →₀ k
#align add_monoid_algebra AddMonoidAlgebra

@[inherit_doc]
scoped[AddMonoidAlgebra] notation:9000 R:max "[" A "]" => AddMonoidAlgebra R A

namespace AddMonoidAlgebra

-- Porting note: The compiler couldn't derive this.
instance inhabited : Inhabited k[G] :=
  inferInstanceAs (Inhabited (G →₀ k))
#align add_monoid_algebra.inhabited AddMonoidAlgebra.inhabited

-- Porting note: The compiler couldn't derive this.
instance addCommMonoid : AddCommMonoid k[G] :=
  inferInstanceAs (AddCommMonoid (G →₀ k))
#align add_monoid_algebra.add_comm_monoid AddMonoidAlgebra.addCommMonoid

instance instIsCancelAdd [IsCancelAdd k] : IsCancelAdd (AddMonoidAlgebra k G) :=
  inferInstanceAs (IsCancelAdd (G →₀ k))

instance coeFun : CoeFun k[G] fun _ => G → k :=
  Finsupp.instCoeFun
#align add_monoid_algebra.has_coe_to_fun AddMonoidAlgebra.coeFun

end AddMonoidAlgebra

end

namespace AddMonoidAlgebra

variable {k G}

section

variable [Semiring k] [NonUnitalNonAssocSemiring R]

-- Porting note: `reducible` cannot be `local`, so we replace some definitions and theorems with
--               new ones which have new types.

abbrev single (a : G) (b : k) : k[G] := Finsupp.single a b

theorem single_zero (a : G) : (single a 0 : k[G]) = 0 := Finsupp.single_zero a

theorem single_add (a : G) (b₁ b₂ : k) : single a (b₁ + b₂) = single a b₁ + single a b₂ :=
  Finsupp.single_add a b₁ b₂

@[simp]
theorem sum_single_index {N} [AddCommMonoid N] {a : G} {b : k} {h : G → k → N}
    (h_zero : h a 0 = 0) :
    (single a b).sum h = h a b := Finsupp.sum_single_index h_zero

@[simp]
theorem sum_single (f : k[G]) : f.sum single = f :=
  Finsupp.sum_single f

theorem single_apply {a a' : G} {b : k} [Decidable (a = a')] :
    single a b a' = if a = a' then b else 0 :=
  Finsupp.single_apply

@[simp]
theorem single_eq_zero {a : G} {b : k} : single a b = 0 ↔ b = 0 := Finsupp.single_eq_zero

abbrev mapDomain {G' : Type*} (f : G → G') (v : k[G]) : k[G'] :=
  Finsupp.mapDomain f v

theorem mapDomain_sum {k' G' : Type*} [Semiring k'] {f : G → G'} {s : AddMonoidAlgebra k' G}
    {v : G → k' → k[G]} :
    mapDomain f (s.sum v) = s.sum fun a b => mapDomain f (v a b) :=
  Finsupp.mapDomain_sum

theorem mapDomain_single {G' : Type*} {f : G → G'} {a : G} {b : k} :
    mapDomain f (single a b) = single (f a) b :=
  Finsupp.mapDomain_single

/-- 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`. -/
def liftNC (f : k →+ R) (g : Multiplicative G → R) : k[G] →+ R :=
  liftAddHom fun x : G => (AddMonoidHom.mulRight (g <| Multiplicative.ofAdd x)).comp f
#align add_monoid_algebra.lift_nc AddMonoidAlgebra.liftNC

@[simp]
theorem liftNC_single (f : k →+ R) (g : Multiplicative G → R) (a : G) (b : k) :
    liftNC f g (single a b) = f b * g (Multiplicative.ofAdd a) :=
  liftAddHom_apply_single _ _ _
#align add_monoid_algebra.lift_nc_single AddMonoidAlgebra.liftNC_single

end

section Mul

variable [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.) -/
instance hasMul : Mul k[G] :=
  ⟨fun f g => f.sum fun a₁ b₁ => g.sum fun a₂ b₂ => single (a₁ + a₂) (b₁ * b₂)⟩
#align add_monoid_algebra.has_mul AddMonoidAlgebra.hasMul

theorem mul_def {f g : k[G]} :
    f * g = f.sum fun a₁ b₁ => g.sum fun a₂ b₂ => single (a₁ + a₂) (b₁ * b₂) :=
  rfl
#align add_monoid_algebra.mul_def AddMonoidAlgebra.mul_def

instance nonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring k[G] :=
  { Finsupp.instAddCommMonoid with
    -- Porting note: `refine` & `exact` are required because `simp` behaves differently.
    left_distrib := fun f g h => by
      haveI := Classical.decEq G
      simp only [mul_def]
      refine Eq.trans (congr_arg (sum f) (funext₂ fun a₁ b₁ => sum_add_index ?_ ?_)) ?_ <;>
        simp only [mul_add, mul_zero, single_zero, single_add, forall_true_iff, sum_add]
    right_distrib := fun f g h => by
      haveI := Classical.decEq G
      simp only [mul_def]
      refine Eq.trans (sum_add_index ?_ ?_) ?_ <;>
        simp only [add_mul, zero_mul, single_zero, single_add, forall_true_iff, sum_zero, sum_add]
    zero_mul := fun f => by
      simp only [mul_def]
      exact sum_zero_index
    mul_zero := fun f => by
      simp only [mul_def]
      exact Eq.trans (congr_arg (sum f) (funext₂ fun a₁ b₁ => sum_zero_index)) sum_zero
    nsmul := fun n f => n • f
    -- Porting note: `ext` → `refine Finsupp.ext fun _ => ?_`
    nsmul_zero := by
      intros
      refine Finsupp.ext fun _ => ?_
      simp [-nsmul_eq_mul, add_smul]
    nsmul_succ := by
      intros
      refine Finsupp.ext fun _ => ?_
      simp [-nsmul_eq_mul, add_smul] }
#align add_monoid_algebra.non_unital_non_assoc_semiring AddMonoidAlgebra.nonUnitalNonAssocSemiring

variable [Semiring R]

theorem liftNC_mul {g_hom : Type*}
    [FunLike g_hom (Multiplicative G) R] [MulHomClass g_hom (Multiplicative G) R]
    (f : k →+* R) (g : g_hom) (a b : k[G])
    (h_comm : ∀ {x y}, y ∈ a.support → Commute (f (b x)) (g <| Multiplicative.ofAdd y)) :
    liftNC (f : k →+ R) g (a * b) = liftNC (f : k →+ R) g a * liftNC (f : k →+ R) g b :=
  (MonoidAlgebra.liftNC_mul f g _ _ @h_comm : _)
#align add_monoid_algebra.lift_nc_mul AddMonoidAlgebra.liftNC_mul

end Mul

section One

variable [Semiring k] [Zero G] [NonAssocSemiring R]

/-- The unit of the multiplication is `single 1 1`, i.e. the function
  that is `1` at `0` and zero elsewhere. -/
instance one : One k[G] :=
  ⟨single 0 1⟩
#align add_monoid_algebra.has_one AddMonoidAlgebra.one

theorem one_def : (1 : k[G]) = single 0 1 :=
  rfl
#align add_monoid_algebra.one_def AddMonoidAlgebra.one_def

@[simp]
theorem liftNC_one {g_hom : Type*}
    [FunLike g_hom (Multiplicative G) R] [OneHomClass g_hom (Multiplicative G) R]
    (f : k →+* R) (g : g_hom) : liftNC (f : k →+ R) g 1 = 1 :=
  (MonoidAlgebra.liftNC_one f g : _)
#align add_monoid_algebra.lift_nc_one AddMonoidAlgebra.liftNC_one

end One

section Semigroup

variable [Semiring k] [AddSemigroup G]

instance nonUnitalSemiring : NonUnitalSemiring k[G] :=
  { AddMonoidAlgebra.nonUnitalNonAssocSemiring with
    mul_assoc := fun f g h => by
      -- Porting note: `reducible` cannot be `local` so proof gets long.
      simp only [mul_def]
      rw [sum_sum_index]; congr; ext a₁ b₁
      rw [sum_sum_index, sum_sum_index]; congr; ext a₂ b₂
      rw [sum_sum_index, sum_single_index]; congr; ext a₃ b₃
      rw [sum_single_index, mul_assoc, add_assoc]
      all_goals simp only [single_zero, single_add, forall_true_iff, add_mul,
        mul_add, zero_mul, mul_zero, sum_zero, sum_add] }
#align add_monoid_algebra.non_unital_semiring AddMonoidAlgebra.nonUnitalSemiring

end Semigroup

section MulOneClass

variable [Semiring k] [AddZeroClass G]

instance nonAssocSemiring : NonAssocSemiring k[G] :=
  { AddMonoidAlgebra.nonUnitalNonAssocSemiring with
    natCast := fun n => single 0 n
    natCast_zero := by simp
    natCast_succ := fun _ => by simp; rfl
    one_mul := fun f => by
      simp only [mul_def, one_def, sum_single_index, zero_mul, single_zero, sum_zero, zero_add,
        one_mul, sum_single]
    mul_one := fun f => by
      simp only [mul_def, one_def, sum_single_index, mul_zero, single_zero, sum_zero, add_zero,
        mul_one, sum_single] }
#align add_monoid_algebra.non_assoc_semiring AddMonoidAlgebra.nonAssocSemiring

theorem natCast_def (n : ℕ) : (n : k[G]) = single (0 : G) (n : k) :=
  rfl
#align add_monoid_algebra.nat_cast_def AddMonoidAlgebra.natCast_def

end MulOneClass

/-! #### Semiring structure -/


section Semiring

instance smulZeroClass [Semiring k] [SMulZeroClass R k] : SMulZeroClass R k[G] :=
  Finsupp.smulZeroClass
#align add_monoid_algebra.smul_zero_class AddMonoidAlgebra.smulZeroClass

variable [Semiring k] [AddMonoid G]

instance semiring : Semiring k[G] :=
  { AddMonoidAlgebra.nonUnitalSemiring,
    AddMonoidAlgebra.nonAssocSemiring with }
#align add_monoid_algebra.semiring AddMonoidAlgebra.semiring

variable [Semiring R]

/-- `liftNC` as a `RingHom`, for when `f` and `g` commute -/
def liftNCRingHom (f : k →+* R) (g : Multiplicative G →* R) (h_comm : ∀ x y, Commute (f x) (g y)) :
    k[G] →+* R :=
  { liftNC (f : k →+ R) g with
    map_one' := liftNC_one _ _
    map_mul' := fun _a _b => liftNC_mul _ _ _ _ fun {_ _} _ => h_comm _ _ }
#align add_monoid_algebra.lift_nc_ring_hom AddMonoidAlgebra.liftNCRingHom

end Semiring

instance nonUnitalCommSemiring [CommSemiring k] [AddCommSemigroup G] :
    NonUnitalCommSemiring k[G] :=
  { AddMonoidAlgebra.nonUnitalSemiring with
    mul_comm := @mul_comm (MonoidAlgebra k <| Multiplicative G) _ }
#align add_monoid_algebra.non_unital_comm_semiring AddMonoidAlgebra.nonUnitalCommSemiring

instance nontrivial [Semiring k] [Nontrivial k] [Nonempty G] : Nontrivial k[G] :=
  Finsupp.instNontrivial
#align add_monoid_algebra.nontrivial AddMonoidAlgebra.nontrivial

/-! #### Derived instances -/


section DerivedInstances

instance commSemiring [CommSemiring k] [AddCommMonoid G] : CommSemiring k[G] :=
  { AddMonoidAlgebra.nonUnitalCommSemiring, AddMonoidAlgebra.semiring with }
#align add_monoid_algebra.comm_semiring AddMonoidAlgebra.commSemiring

instance unique [Semiring k] [Subsingleton k] : Unique k[G] :=
  Finsupp.uniqueOfRight
#align add_monoid_algebra.unique AddMonoidAlgebra.unique

instance addCommGroup [Ring k] : AddCommGroup k[G] :=
  Finsupp.instAddCommGroup
#align add_monoid_algebra.add_comm_group AddMonoidAlgebra.addCommGroup

instance nonUnitalNonAssocRing [Ring k] [Add G] : NonUnitalNonAssocRing k[G] :=
  { AddMonoidAlgebra.addCommGroup, AddMonoidAlgebra.nonUnitalNonAssocSemiring with }
#align add_monoid_algebra.non_unital_non_assoc_ring AddMonoidAlgebra.nonUnitalNonAssocRing

instance nonUnitalRing [Ring k] [AddSemigroup G] : NonUnitalRing k[G] :=
  { AddMonoidAlgebra.addCommGroup, AddMonoidAlgebra.nonUnitalSemiring with }
#align add_monoid_algebra.non_unital_ring AddMonoidAlgebra.nonUnitalRing

instance nonAssocRing [Ring k] [AddZeroClass G] : NonAssocRing k[G] :=
  { AddMonoidAlgebra.addCommGroup,
    AddMonoidAlgebra.nonAssocSemiring with
    intCast := fun z => single 0 (z : k)
    -- Porting note: Both were `simpa`.
    intCast_ofNat := fun n => by simp; rfl
    intCast_negSucc := fun n => by simp; rfl }
#align add_monoid_algebra.non_assoc_ring AddMonoidAlgebra.nonAssocRing

theorem intCast_def [Ring k] [AddZeroClass G] (z : ℤ) :
    (z : k[G]) = single (0 : G) (z : k) :=
  rfl
#align add_monoid_algebra.int_cast_def AddMonoidAlgebra.intCast_def

instance ring [Ring k] [AddMonoid G] : Ring k[G] :=
  { AddMonoidAlgebra.nonAssocRing, AddMonoidAlgebra.semiring with }
#align add_monoid_algebra.ring AddMonoidAlgebra.ring

instance nonUnitalCommRing [CommRing k] [AddCommSemigroup G] :
    NonUnitalCommRing k[G] :=
  { AddMonoidAlgebra.nonUnitalCommSemiring, AddMonoidAlgebra.nonUnitalRing with }
#align add_monoid_algebra.non_unital_comm_ring AddMonoidAlgebra.nonUnitalCommRing

instance commRing [CommRing k] [AddCommMonoid G] : CommRing k[G] :=
  { AddMonoidAlgebra.nonUnitalCommRing, AddMonoidAlgebra.ring with }
#align add_monoid_algebra.comm_ring AddMonoidAlgebra.commRing

variable {S : Type*}

instance distribSMul [Semiring k] [DistribSMul R k] : DistribSMul R k[G] :=
  Finsupp.distribSMul G k
#align add_monoid_algebra.distrib_smul AddMonoidAlgebra.distribSMul

instance distribMulAction [Monoid R] [Semiring k] [DistribMulAction R k] :
    DistribMulAction R k[G] :=
  Finsupp.distribMulAction G k
#align add_monoid_algebra.distrib_mul_action AddMonoidAlgebra.distribMulAction

instance faithfulSMul [Semiring k] [SMulZeroClass R k] [FaithfulSMul R k] [Nonempty G] :
    FaithfulSMul R k[G] :=
  Finsupp.faithfulSMul
#align add_monoid_algebra.faithful_smul AddMonoidAlgebra.faithfulSMul

instance module [Semiring R] [Semiring k] [Module R k] : Module R k[G] :=
  Finsupp.module G k
#align add_monoid_algebra.module AddMonoidAlgebra.module

instance isScalarTower [Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMul R S]
    [IsScalarTower R S k] : IsScalarTower R S k[G] :=
  Finsupp.isScalarTower G k
#align add_monoid_algebra.is_scalar_tower AddMonoidAlgebra.isScalarTower

instance smulCommClass [Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMulCommClass R S k] :
    SMulCommClass R S k[G] :=
  Finsupp.smulCommClass G k
#align add_monoid_algebra.smul_comm_tower AddMonoidAlgebra.smulCommClass

instance isCentralScalar [Semiring k] [SMulZeroClass R k] [SMulZeroClass Rᵐᵒᵖ k]
    [IsCentralScalar R k] : IsCentralScalar R k[G] :=
  Finsupp.isCentralScalar G k
#align add_monoid_algebra.is_central_scalar AddMonoidAlgebra.isCentralScalar

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


end DerivedInstances

section MiscTheorems

variable [Semiring k]

theorem mul_apply [DecidableEq G] [Add G] (f g : k[G]) (x : G) :
    (f * g) x = f.sum fun a₁ b₁ => g.sum fun a₂ b₂ => if a₁ + a₂ = x then b₁ * b₂ else 0 :=
  @MonoidAlgebra.mul_apply k (Multiplicative G) _ _ _ _ _ _
#align add_monoid_algebra.mul_apply AddMonoidAlgebra.mul_apply

theorem mul_apply_antidiagonal [Add G] (f g : k[G]) (x : G) (s : Finset (G × G))
    (hs : ∀ {p : G × G}, p ∈ s ↔ p.1 + p.2 = x) : (f * g) x = ∑ p in s, f p.1 * g p.2 :=
  @MonoidAlgebra.mul_apply_antidiagonal k (Multiplicative G) _ _ _ _ _ s @hs
#align add_monoid_algebra.mul_apply_antidiagonal AddMonoidAlgebra.mul_apply_antidiagonal

theorem single_mul_single [Add G] {a₁ a₂ : G} {b₁ b₂ : k} :
    single a₁ b₁ * single a₂ b₂ = single (a₁ + a₂) (b₁ * b₂) :=
  @MonoidAlgebra.single_mul_single k (Multiplicative G) _ _ _ _ _ _
#align add_monoid_algebra.single_mul_single AddMonoidAlgebra.single_mul_single

theorem single_commute_single [Add G] {a₁ a₂ : G} {b₁ b₂ : k}
    (ha : AddCommute a₁ a₂) (hb : Commute b₁ b₂) :
    Commute (single a₁ b₁) (single a₂ b₂) :=
  @MonoidAlgebra.single_commute_single k (Multiplicative G) _ _ _ _ _ _ ha hb

-- This should be a `@[simp]` lemma, but the simp_nf linter times out if we add this.
-- Probably the correct fix is to make a `[Add]MonoidAlgebra.single` with the correct type,
-- instead of relying on `Finsupp.single`.
theorem single_pow [AddMonoid G] {a : G} {b : k} : ∀ n : ℕ, single a b ^ n = single (n • a) (b ^ n)
  | 0 => by
    simp only [pow_zero, zero_nsmul]
    rfl
  | n + 1 => by
    rw [pow_succ, pow_succ, single_pow n, single_mul_single, add_nsmul, one_nsmul]
#align add_monoid_algebra.single_pow AddMonoidAlgebra.single_pow

/-- Like `Finsupp.mapDomain_zero`, but for the `1` we define in this file -/
@[simp]
theorem mapDomain_one {α : Type*} {β : Type*} {α₂ : Type*} [Semiring β] [Zero α] [Zero α₂]
    {F : Type*} [FunLike F α α₂] [ZeroHomClass F α α₂] (f : F) :
    (mapDomain f (1 : AddMonoidAlgebra β α) : AddMonoidAlgebra β α₂) =
      (1 : AddMonoidAlgebra β α₂) :=
  by simp_rw [one_def, mapDomain_single, map_zero]
#align add_monoid_algebra.map_domain_one AddMonoidAlgebra.mapDomain_one

/-- Like `Finsupp.mapDomain_add`, but for the convolutive multiplication we define in this file -/
theorem mapDomain_mul {α : Type*} {β : Type*} {α₂ : Type*} [Semiring β] [Add α] [Add α₂]
    {F : Type*} [FunLike F α α₂] [AddHomClass F α α₂] (f : F) (x y : AddMonoidAlgebra β α) :
    mapDomain f (x * y) = mapDomain f x * mapDomain f y := by
  simp_rw [mul_def, mapDomain_sum, mapDomain_single, map_add]
  rw [Finsupp.sum_mapDomain_index]
  · congr
    ext a b
    rw [Finsupp.sum_mapDomain_index]
    · simp
    · simp [mul_add]
  · simp
  · simp [add_mul]
#align add_monoid_algebra.map_domain_mul AddMonoidAlgebra.mapDomain_mul

section

variable (k G)

/-- The embedding of an additive magma into its additive magma algebra. -/
@[simps]
def ofMagma [Add G] : Multiplicative G →ₙ* k[G] where
  toFun a := single a 1
  map_mul' a b := by simp only [mul_def, mul_one, sum_single_index, single_eq_zero, mul_zero]; rfl
#align add_monoid_algebra.of_magma AddMonoidAlgebra.ofMagma
#align add_monoid_algebra.of_magma_apply AddMonoidAlgebra.ofMagma_apply

/-- Embedding of a magma with zero into its magma algebra. -/
def of [AddZeroClass G] : Multiplicative G →* k[G] :=
  { ofMagma k G with
    toFun := fun a => single a 1
    map_one' := rfl }
#align add_monoid_algebra.of AddMonoidAlgebra.of

/-- Embedding of a magma with zero `G`, into its magma algebra, having `G` as source. -/
def of' : G → k[G] := fun a => single a 1
#align add_monoid_algebra.of' AddMonoidAlgebra.of'

end

@[simp]
theorem of_apply [AddZeroClass G] (a : Multiplicative G) :
    of k G a = single (Multiplicative.toAdd a) 1 :=
  rfl
#align add_monoid_algebra.of_apply AddMonoidAlgebra.of_apply

@[simp]
theorem of'_apply (a : G) : of' k G a = single a 1 :=
  rfl
#align add_monoid_algebra.of'_apply AddMonoidAlgebra.of'_apply

theorem of'_eq_of [AddZeroClass G] (a : G) : of' k G a = of k G (.ofAdd a) := rfl
#align add_monoid_algebra.of'_eq_of AddMonoidAlgebra.of'_eq_of

theorem of_injective [Nontrivial k] [AddZeroClass G] : Function.Injective (of k G) :=
  MonoidAlgebra.of_injective
#align add_monoid_algebra.of_injective AddMonoidAlgebra.of_injective

theorem of'_commute [Semiring k] [AddZeroClass G] {a : G} (h : ∀ a', AddCommute a a')
    (f : AddMonoidAlgebra k G) :
    Commute (of' k G a) f :=
  MonoidAlgebra.of_commute (G := Multiplicative G) h f

/-- `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`.
-/
@[simps]
def singleHom [AddZeroClass G] : k × Multiplicative G →* k[G] where
  toFun a := single (Multiplicative.toAdd a.2) a.1
  map_one' := rfl
  map_mul' _a _b := single_mul_single.symm
#align add_monoid_algebra.single_hom AddMonoidAlgebra.singleHom
#align add_monoid_algebra.single_hom_apply AddMonoidAlgebra.singleHom_apply

theorem mul_single_apply_aux [Add G] (f : k[G]) (r : k) (x y z : G)
    (H : ∀ a, a + x = z ↔ a = y) : (f * single x r) z = f y * r :=
  @MonoidAlgebra.mul_single_apply_aux k (Multiplicative G) _ _ _ _ _ _ _ H
#align add_monoid_algebra.mul_single_apply_aux AddMonoidAlgebra.mul_single_apply_aux

theorem mul_single_zero_apply [AddZeroClass G] (f : k[G]) (r : k) (x : G) :
    (f * single (0 : G) r) x = f x * r :=
  f.mul_single_apply_aux r _ _ _ fun a => by rw [add_zero]
#align add_monoid_algebra.mul_single_zero_apply AddMonoidAlgebra.mul_single_zero_apply

theorem mul_single_apply_of_not_exists_add [Add G] (r : k) {g g' : G} (x : k[G])
    (h : ¬∃ d, g' = d + g) : (x * single g r) g' = 0 :=
  @MonoidAlgebra.mul_single_apply_of_not_exists_mul k (Multiplicative G) _ _ _ _ _ _ h
#align add_monoid_algebra.mul_single_apply_of_not_exists_add AddMonoidAlgebra.mul_single_apply_of_not_exists_add

theorem single_mul_apply_aux [Add G] (f : k[G]) (r : k) (x y z : G)
    (H : ∀ a, x + a = y ↔ a = z) : (single x r * f) y = r * f z :=
  @MonoidAlgebra.single_mul_apply_aux k (Multiplicative G) _ _ _ _ _ _ _ H
#align add_monoid_algebra.single_mul_apply_aux AddMonoidAlgebra.single_mul_apply_aux

theorem single_zero_mul_apply [AddZeroClass G] (f : k[G]) (r : k) (x : G) :
    (single (0 : G) r * f) x = r * f x :=
  f.single_mul_apply_aux r _ _ _ fun a => by rw [zero_add]
#align add_monoid_algebra.single_zero_mul_apply AddMonoidAlgebra.single_zero_mul_apply

theorem single_mul_apply_of_not_exists_add [Add G] (r : k) {g g' : G} (x : k[G])
    (h : ¬∃ d, g' = g + d) : (single g r * x) g' = 0 :=
  @MonoidAlgebra.single_mul_apply_of_not_exists_mul k (Multiplicative G) _ _ _ _ _ _ h
#align add_monoid_algebra.single_mul_apply_of_not_exists_add AddMonoidAlgebra.single_mul_apply_of_not_exists_add

theorem mul_single_apply [AddGroup G] (f : k[G]) (r : k) (x y : G) :
    (f * single x r) y = f (y - x) * r :=
  (sub_eq_add_neg y x).symm ▸ @MonoidAlgebra.mul_single_apply k (Multiplicative G) _ _ _ _ _ _
#align add_monoid_algebra.mul_single_apply AddMonoidAlgebra.mul_single_apply

theorem single_mul_apply [AddGroup G] (r : k) (x : G) (f : k[G]) (y : G) :
    (single x r * f) y = r * f (-x + y) :=
  @MonoidAlgebra.single_mul_apply k (Multiplicative G) _ _ _ _ _ _
#align add_monoid_algebra.single_mul_apply AddMonoidAlgebra.single_mul_apply

theorem liftNC_smul {R : Type*} [AddZeroClass G] [Semiring R] (f : k →+* R)
    (g : Multiplicative G →* R) (c : k) (φ : MonoidAlgebra k G) :
    liftNC (f : k →+ R) g (c • φ) = f c * liftNC (f : k →+ R) g φ :=
  @MonoidAlgebra.liftNC_smul k (Multiplicative G) _ _ _ _ f g c φ
#align add_monoid_algebra.lift_nc_smul AddMonoidAlgebra.liftNC_smul

theorem induction_on [AddMonoid G] {p : k[G] → Prop} (f : k[G])
    (hM : ∀ g, p (of k G (Multiplicative.ofAdd g)))
    (hadd : ∀ f g : k[G], p f → p g → p (f + g))
    (hsmul : ∀ (r : k) (f), p f → p (r • f)) : p f := by
  refine' Finsupp.induction_linear f _ (fun f g hf hg => hadd f g hf hg) fun g r => _
  · simpa using hsmul 0 (of k G (Multiplicative.ofAdd 0)) (hM 0)
  · convert hsmul r (of k G (Multiplicative.ofAdd g)) (hM g)
    -- Porting note: Was `simp only`.
    rw [of_apply, toAdd_ofAdd, smul_single', mul_one]
#align add_monoid_algebra.induction_on AddMonoidAlgebra.induction_on

/-- 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. -/
@[simps]
def mapDomainRingHom (k : Type*) [Semiring k] {H F : Type*} [AddMonoid G] [AddMonoid H]
    [FunLike F G H] [AddMonoidHomClass F G H] (f : F) : k[G] →+* k[H] :=
  { (Finsupp.mapDomain.addMonoidHom f : MonoidAlgebra k G →+ MonoidAlgebra k H) with
    map_one' := mapDomain_one f
    map_mul' := fun x y => mapDomain_mul f x y }
#align add_monoid_algebra.map_domain_ring_hom AddMonoidAlgebra.mapDomainRingHom
#align add_monoid_algebra.map_domain_ring_hom_apply AddMonoidAlgebra.mapDomainRingHom_apply

end MiscTheorems

end AddMonoidAlgebra

/-!
#### 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` -/
protected def AddMonoidAlgebra.toMultiplicative [Semiring k] [Add G] :
    AddMonoidAlgebra k G ≃+* MonoidAlgebra k (Multiplicative G) :=
  { Finsupp.domCongr
      Multiplicative.ofAdd with
    toFun := equivMapDomain Multiplicative.ofAdd
    map_mul' := fun x y => by
      -- Porting note: added `dsimp only`; `beta_reduce` alone is not sufficient
      dsimp only
      repeat' rw [equivMapDomain_eq_mapDomain (M := k)]
      dsimp [Multiplicative.ofAdd]
      exact MonoidAlgebra.mapDomain_mul (α := Multiplicative G) (β := k)
        (MulHom.id (Multiplicative G)) x y }
#align add_monoid_algebra.to_multiplicative AddMonoidAlgebra.toMultiplicative

/-- The equivalence between `MonoidAlgebra` and `AddMonoidAlgebra` in terms of `Additive` -/
protected def MonoidAlgebra.toAdditive [Semiring k] [Mul G] :
    MonoidAlgebra k G ≃+* AddMonoidAlgebra k (Additive G) :=
  { Finsupp.domCongr Additive.ofMul with
    toFun := equivMapDomain Additive.ofMul
    map_mul' := fun x y => by
      -- Porting note: added `dsimp only`; `beta_reduce` alone is not sufficient
      dsimp only
      repeat' rw [equivMapDomain_eq_mapDomain (M := k)]
      dsimp [Additive.ofMul]
      convert MonoidAlgebra.mapDomain_mul (β := k) (MulHom.id G) x y }
#align monoid_algebra.to_additive MonoidAlgebra.toAdditive

namespace AddMonoidAlgebra

variable {k G H}

/-! #### Non-unital, non-associative algebra structure -/


section NonUnitalNonAssocAlgebra

variable (k) [Semiring k] [DistribSMul R k] [Add G]

instance isScalarTower_self [IsScalarTower R k k] :
    IsScalarTower R k[G] k[G] :=
  @MonoidAlgebra.isScalarTower_self k (Multiplicative G) R _ _ _ _
#align add_monoid_algebra.is_scalar_tower_self AddMonoidAlgebra.isScalarTower_self

/-- Note that if `k` is a `CommSemiring` then we have `SMulCommClass k k k` and so we can take
`R = k` in the below. In other words, if the coefficients are commutative amongst themselves, they
also commute with the algebra multiplication. -/
instance smulCommClass_self [SMulCommClass R k k] :
    SMulCommClass R k[G] k[G] :=
  @MonoidAlgebra.smulCommClass_self k (Multiplicative G) R _ _ _ _
#align add_monoid_algebra.smul_comm_class_self AddMonoidAlgebra.smulCommClass_self

instance smulCommClass_symm_self [SMulCommClass k R k] :
    SMulCommClass k[G] R k[G] :=
  @MonoidAlgebra.smulCommClass_symm_self k (Multiplicative G) R _ _ _ _
#align add_monoid_algebra.smul_comm_class_symm_self AddMonoidAlgebra.smulCommClass_symm_self

variable {A : Type u₃} [NonUnitalNonAssocSemiring A]

/-- A non_unital `k`-algebra homomorphism from `k[G]` is uniquely defined by its
values on the functions `single a 1`. -/
theorem nonUnitalAlgHom_ext [DistribMulAction k A] {φ₁ φ₂ : k[G] →ₙₐ[k] A}
    (h : ∀ x, φ₁ (single x 1) = φ₂ (single x 1)) : φ₁ = φ₂ :=
  @MonoidAlgebra.nonUnitalAlgHom_ext k (Multiplicative G) _ _ _ _ _ φ₁ φ₂ h
#align add_monoid_algebra.non_unital_alg_hom_ext AddMonoidAlgebra.nonUnitalAlgHom_ext

/-- See note [partially-applied ext lemmas]. -/
@[ext high]
theorem nonUnitalAlgHom_ext' [DistribMulAction k A] {φ₁ φ₂ : k[G] →ₙₐ[k] A}
    (h : φ₁.toMulHom.comp (ofMagma k G) = φ₂.toMulHom.comp (ofMagma k G)) : φ₁ = φ₂ :=
  @MonoidAlgebra.nonUnitalAlgHom_ext' k (Multiplicative G) _ _ _ _ _ φ₁ φ₂ h
#align add_monoid_algebra.non_unital_alg_hom_ext' AddMonoidAlgebra.nonUnitalAlgHom_ext'

/-- 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. -/
@[simps apply_apply symm_apply]
def liftMagma [Module k A] [IsScalarTower k A A] [SMulCommClass k A A] :
    (Multiplicative G →ₙ* A) ≃ (k[G] →ₙₐ[k] A) :=
  { (MonoidAlgebra.liftMagma k : (Multiplicative G →ₙ* A) ≃ (_ →ₙₐ[k] A)) with
    toFun := fun f =>
      { (MonoidAlgebra.liftMagma k f : _) with
        toFun := fun a => sum a fun m t => t • f (Multiplicative.ofAdd m) }
    invFun := fun F => F.toMulHom.comp (ofMagma k G) }
#align add_monoid_algebra.lift_magma AddMonoidAlgebra.liftMagma
#align add_monoid_algebra.lift_magma_apply_apply AddMonoidAlgebra.liftMagma_apply_apply
#align add_monoid_algebra.lift_magma_symm_apply AddMonoidAlgebra.liftMagma_symm_apply

end NonUnitalNonAssocAlgebra

/-! #### Algebra structure -/


section Algebra

-- attribute [local reducible] MonoidAlgebra -- Porting note: `reducible` cannot be `local`.

/-- `Finsupp.single 0` as a `RingHom` -/
@[simps]
def singleZeroRingHom [Semiring k] [AddMonoid G] : k →+* k[G] :=
  { Finsupp.singleAddHom 0 with
    map_one' := rfl
    -- Porting note (#10691): Was `rw`.
    map_mul' := fun x y => by simp only [singleAddHom, single_mul_single, zero_add] }
#align add_monoid_algebra.single_zero_ring_hom AddMonoidAlgebra.singleZeroRingHom
#align add_monoid_algebra.single_zero_ring_hom_apply AddMonoidAlgebra.singleZeroRingHom_apply

/-- If two ring homomorphisms from `k[G]` are equal on all `single a 1`
and `single 0 b`, then they are equal. -/
theorem ringHom_ext {R} [Semiring k] [AddMonoid G] [Semiring R] {f g : k[G] →+* R}
    (h₀ : ∀ b, f (single 0 b) = g (single 0 b)) (h_of : ∀ a, f (single a 1) = g (single a 1)) :
    f = g :=
  @MonoidAlgebra.ringHom_ext k (Multiplicative G) R _ _ _ _ _ h₀ h_of
#align add_monoid_algebra.ring_hom_ext AddMonoidAlgebra.ringHom_ext

/-- 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]. -/
@[ext high]
theorem ringHom_ext' {R} [Semiring k] [AddMonoid G] [Semiring R] {f g : k[G] →+* R}
    (h₁ : f.comp singleZeroRingHom = g.comp singleZeroRingHom)
    (h_of : (f : k[G] →* R).comp (of k G) = (g : k[G] →* R).comp (of k G)) :
    f = g :=
  ringHom_ext (RingHom.congr_fun h₁) (DFunLike.congr_fun h_of)
#align add_monoid_algebra.ring_hom_ext' AddMonoidAlgebra.ringHom_ext'

section Opposite

open Finsupp MulOpposite

variable [Semiring k]

/-- The opposite of an `R[I]` is ring equivalent to
the `AddMonoidAlgebra Rᵐᵒᵖ I` over the opposite ring, taking elements to their opposite. -/
@[simps! (config := { simpRhs := true }) apply symm_apply]
protected noncomputable def opRingEquiv [AddCommMonoid G] :
    k[G]ᵐᵒᵖ ≃+* kᵐᵒᵖ[G] :=
  { MulOpposite.opAddEquiv.symm.trans
      (Finsupp.mapRange.addEquiv (MulOpposite.opAddEquiv : k ≃+ kᵐᵒᵖ)) with
    map_mul' := by
      -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
      rw [Equiv.toFun_as_coe, AddEquiv.toEquiv_eq_coe]; erw [AddEquiv.coe_toEquiv]
      rw [← AddEquiv.coe_toAddMonoidHom]
      refine Iff.mpr (AddMonoidHom.map_mul_iff (R := k[G]ᵐᵒᵖ) (S := kᵐᵒᵖ[G]) _) ?_
      -- Porting note: Was `ext`.
      refine AddMonoidHom.mul_op_ext _ _ <| addHom_ext' fun i₁ => AddMonoidHom.ext fun r₁ =>
        AddMonoidHom.mul_op_ext _ _ <| addHom_ext' fun i₂ => AddMonoidHom.ext fun r₂ => ?_
      -- Porting note: `reducible` cannot be `local` so proof gets long.
      dsimp
      -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
      erw [AddEquiv.trans_apply, AddEquiv.trans_apply, AddEquiv.trans_apply,
        MulOpposite.opAddEquiv_symm_apply]; rw [MulOpposite.unop_mul (α := k[G])]
      dsimp
      -- This was not needed before leanprover/lean4#2644
      erw [mapRange_single, single_mul_single, mapRange_single, mapRange_single]
      simp only [mapRange_single, single_mul_single, ← op_mul, add_comm] }
#align add_monoid_algebra.op_ring_equiv AddMonoidAlgebra.opRingEquiv
#align add_monoid_algebra.op_ring_equiv_apply AddMonoidAlgebra.opRingEquiv_apply
#align add_monoid_algebra.op_ring_equiv_symm_apply AddMonoidAlgebra.opRingEquiv_symm_apply

-- @[simp] -- Porting note (#10618): simp can prove this
theorem opRingEquiv_single [AddCommMonoid G] (r : k) (x : G) :
    AddMonoidAlgebra.opRingEquiv (op (single x r)) = single x (op r) := by simp
#align add_monoid_algebra.op_ring_equiv_single AddMonoidAlgebra.opRingEquiv_single

-- @[simp] -- Porting note (#10618): simp can prove this
theorem opRingEquiv_symm_single [AddCommMonoid G] (r : kᵐᵒᵖ) (x : Gᵐᵒᵖ) :
    AddMonoidAlgebra.opRingEquiv.symm (single x r) = op (single x r.unop) := by simp
#align add_monoid_algebra.op_ring_equiv_symm_single AddMonoidAlgebra.opRingEquiv_symm_single

end Opposite

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

In particular this provides the instance `Algebra k k[G]`.
-/
instance algebra [CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] :
    Algebra R k[G] :=
  { singleZeroRingHom.comp (algebraMap R k) with
    -- Porting note: `ext` → `refine Finsupp.ext fun _ => ?_`
    smul_def' := fun r a => by
      refine Finsupp.ext fun _ => ?_
      -- Porting note: Newly required.
      rw [Finsupp.coe_smul]
      simp [single_zero_mul_apply, Algebra.smul_def, Pi.smul_apply]
    commutes' := fun r f => by
      refine Finsupp.ext fun _ => ?_
      simp [single_zero_mul_apply, mul_single_zero_apply, Algebra.commutes] }
#align add_monoid_algebra.algebra AddMonoidAlgebra.algebra

/-- `Finsupp.single 0` as an `AlgHom` -/
@[simps! apply]
def singleZeroAlgHom [CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] : k →ₐ[R] k[G] :=
  { singleZeroRingHom with
    commutes' := fun r => by
      -- Porting note: `ext` → `refine Finsupp.ext fun _ => ?_`
      refine Finsupp.ext fun _ => ?_
      simp
      rfl }
#align add_monoid_algebra.single_zero_alg_hom AddMonoidAlgebra.singleZeroAlgHom
#align add_monoid_algebra.single_zero_alg_hom_apply AddMonoidAlgebra.singleZeroAlgHom_apply

@[simp]
theorem coe_algebraMap [CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] :
    (algebraMap R k[G] : R → k[G]) = single 0 ∘ algebraMap R k :=
  rfl
#align add_monoid_algebra.coe_algebra_map AddMonoidAlgebra.coe_algebraMap

end Algebra

section lift

variable [CommSemiring k] [AddMonoid G]
variable {A : Type u₃} [Semiring A] [Algebra k A] {B : Type*} [Semiring B] [Algebra k B]

/-- `liftNCRingHom` as an `AlgHom`, for when `f` is an `AlgHom` -/
def liftNCAlgHom (f : A →ₐ[k] B) (g : Multiplicative G →* B) (h_comm : ∀ x y, Commute (f x) (g y)) :
    A[G] →ₐ[k] B :=
  { liftNCRingHom (f : A →+* B) g h_comm with
    commutes' := by simp [liftNCRingHom] }
#align add_monoid_algebra.lift_nc_alg_hom AddMonoidAlgebra.liftNCAlgHom

/-- A `k`-algebra homomorphism from `k[G]` is uniquely defined by its
values on the functions `single a 1`. -/
theorem algHom_ext ⦃φ₁ φ₂ : k[G] →ₐ[k] A⦄
    (h : ∀ x, φ₁ (single x 1) = φ₂ (single x 1)) : φ₁ = φ₂ :=
  @MonoidAlgebra.algHom_ext k (Multiplicative G) _ _ _ _ _ _ _ h
#align add_monoid_algebra.alg_hom_ext AddMonoidAlgebra.algHom_ext

/-- See note [partially-applied ext lemmas]. -/
@[ext high]
theorem algHom_ext' ⦃φ₁ φ₂ : k[G] →ₐ[k] A⦄
    (h : (φ₁ : k[G] →* A).comp (of k G) = (φ₂ : k[G] →* A).comp (of k G)) :
    φ₁ = φ₂ :=
  algHom_ext <| DFunLike.congr_fun h
#align add_monoid_algebra.alg_hom_ext' AddMonoidAlgebra.algHom_ext'

variable (k G A)

/-- Any monoid homomorphism `G →* A` can be lifted to an algebra homomorphism
`k[G] →ₐ[k] A`. -/
def lift : (Multiplicative G →* A) ≃ (k[G] →ₐ[k] A) :=
  { @MonoidAlgebra.lift k (Multiplicative G) _ _ A _ _ with
    invFun := fun f => (f : k[G] →* A).comp (of k G)
    toFun := fun F =>
      { @MonoidAlgebra.lift k (Multiplicative G) _ _ A _ _ F with
        toFun := liftNCAlgHom (Algebra.ofId k A) F fun _ _ => Algebra.commutes _ _ } }
#align add_monoid_algebra.lift AddMonoidAlgebra.lift

variable {k G A}

theorem lift_apply' (F : Multiplicative G →* A) (f : MonoidAlgebra k G) :
    lift k G A F f = f.sum fun a b => algebraMap k A b * F (Multiplicative.ofAdd a) :=
  rfl
#align add_monoid_algebra.lift_apply' AddMonoidAlgebra.lift_apply'

theorem lift_apply (F : Multiplicative G →* A) (f : MonoidAlgebra k G) :
    lift k G A F f = f.sum fun a b => b • F (Multiplicative.ofAdd a) := by
  simp only [lift_apply', Algebra.smul_def]
#align add_monoid_algebra.lift_apply AddMonoidAlgebra.lift_apply

theorem lift_def (F : Multiplicative G →* A) :
    ⇑(lift k G A F) = liftNC ((algebraMap k A : k →+* A) : k →+ A) F :=
  rfl
#align add_monoid_algebra.lift_def AddMonoidAlgebra.lift_def

@[simp]
theorem lift_symm_apply (F : k[G] →ₐ[k] A) (x : Multiplicative G) :
    (lift k G A).symm F x = F (single (Multiplicative.toAdd x) 1) :=
  rfl
#align add_monoid_algebra.lift_symm_apply AddMonoidAlgebra.lift_symm_apply

theorem lift_of (F : Multiplicative G →* A) (x : Multiplicative G) :
    lift k G A F (of k G x) = F x := MonoidAlgebra.lift_of F x
#align add_monoid_algebra.lift_of AddMonoidAlgebra.lift_of

@[simp]
theorem lift_single (F : Multiplicative G →* A) (a b) :
    lift k G A F (single a b) = b • F (Multiplicative.ofAdd a) :=
  MonoidAlgebra.lift_single F (.ofAdd a) b
#align add_monoid_algebra.lift_single AddMonoidAlgebra.lift_single

lemma lift_of' (F : Multiplicative G →* A) (x : G) :
    lift k G A F (of' k G x) = F (Multiplicative.ofAdd x) :=
  lift_of F x

theorem lift_unique' (F : k[G] →ₐ[k] A) :
    F = lift k G A ((F : k[G] →* A).comp (of k G)) :=
  ((lift k G A).apply_symm_apply F).symm
#align add_monoid_algebra.lift_unique' AddMonoidAlgebra.lift_unique'

/-- Decomposition of a `k`-algebra homomorphism from `MonoidAlgebra k G` by
its values on `F (single a 1)`. -/
theorem lift_unique (F : k[G] →ₐ[k] A) (f : MonoidAlgebra k G) :
    F f = f.sum fun a b => b • F (single a 1) := by
  conv_lhs =>
    rw [lift_unique' F]
    simp [lift_apply]
#align add_monoid_algebra.lift_unique AddMonoidAlgebra.lift_unique

theorem algHom_ext_iff {φ₁ φ₂ : k[G] →ₐ[k] A} :
    (∀ x, φ₁ (Finsupp.single x 1) = φ₂ (Finsupp.single x 1)) ↔ φ₁ = φ₂ :=
  ⟨fun h => algHom_ext h, by rintro rfl _; rfl⟩
#align add_monoid_algebra.alg_hom_ext_iff AddMonoidAlgebra.algHom_ext_iff

end lift

section

-- attribute [local reducible] MonoidAlgebra -- Porting note: `reducible` cannot be `local`.

universe ui

variable {ι : Type ui}

theorem prod_single [CommSemiring k] [AddCommMonoid G] {s : Finset ι} {a : ι → G} {b : ι → k} :
    (∏ i in s, single (a i) (b i)) = single (∑ i in s, a i) (∏ i in s, b i) :=
  Finset.cons_induction_on s rfl fun a s has ih => by
    rw [prod_cons has, ih, single_mul_single, sum_cons has, prod_cons has]
#align add_monoid_algebra.prod_single AddMonoidAlgebra.prod_single

end

theorem mapDomain_algebraMap (A : Type*) {H F : Type*} [CommSemiring k] [Semiring A] [Algebra k A]
    [AddMonoid G] [AddMonoid H] [FunLike F G H] [AddMonoidHomClass F G H]
    (f : F) (r : k) :
    mapDomain f (algebraMap k A[G] r) = algebraMap k A[H] r :=
  by simp only [Function.comp_apply, mapDomain_single, AddMonoidAlgebra.coe_algebraMap, map_zero]
#align add_monoid_algebra.map_domain_algebra_map AddMonoidAlgebra.mapDomain_algebraMap

/-- 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. -/
@[simps apply]
def mapDomainNonUnitalAlgHom (k A : Type*) [CommSemiring k] [Semiring A] [Algebra k A]
    {G H F : Type*} [Add G] [Add H] [FunLike F G H] [AddHomClass F G H] (f : F) :
    A[G] →ₙₐ[k] A[H] :=
  { (Finsupp.mapDomain.addMonoidHom f : MonoidAlgebra A G →+ MonoidAlgebra A H) with
    map_mul' := fun x y => mapDomain_mul f x y
    map_smul' := fun r x => mapDomain_smul r x }
#align add_monoid_algebra.map_domain_non_unital_alg_hom AddMonoidAlgebra.mapDomainNonUnitalAlgHom
#align add_monoid_algebra.map_domain_non_unital_alg_hom_apply AddMonoidAlgebra.mapDomainNonUnitalAlgHom_apply

/-- 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. -/
@[simps!]
def mapDomainAlgHom (k A : Type*) [CommSemiring k] [Semiring A] [Algebra k A] [AddMonoid G]
    {H F : Type*} [AddMonoid H] [FunLike F G H] [AddMonoidHomClass F G H] (f : F) :
    A[G] →ₐ[k] A[H] :=
  { mapDomainRingHom A f with commutes' := mapDomain_algebraMap A f }
#align add_monoid_algebra.map_domain_alg_hom AddMonoidAlgebra.mapDomainAlgHom
#align add_monoid_algebra.map_domain_alg_hom_apply AddMonoidAlgebra.mapDomainAlgHom_apply

variable (k A)
variable [CommSemiring k] [AddMonoid G] [AddMonoid H] [Semiring A] [Algebra k A]


/-- If `e : G ≃* H` is a multiplicative equivalence between two monoids, then
`AddMonoidAlgebra.domCongr e` is an algebra equivalence between their monoid algebras. -/
def domCongr (e : G ≃+ H) : A[G] ≃ₐ[k] A[H] :=
  AlgEquiv.ofLinearEquiv
    (Finsupp.domLCongr e : (G →₀ A) ≃ₗ[k] (H →₀ A))
    ((equivMapDomain_eq_mapDomain _ _).trans <| mapDomain_one e)
    (fun f g => (equivMapDomain_eq_mapDomain _ _).trans <| (mapDomain_mul e f g).trans <|
        congr_arg₂ _ (equivMapDomain_eq_mapDomain _ _).symm (equivMapDomain_eq_mapDomain _ _).symm)

theorem domCongr_toAlgHom (e : G ≃+ H) : (domCongr k A e).toAlgHom = mapDomainAlgHom k A e :=
  AlgHom.ext fun _ => equivMapDomain_eq_mapDomain _ _

@[simp] theorem domCongr_apply (e : G ≃+ H) (f : MonoidAlgebra A G) (h : H) :
    domCongr k A e f h = f (e.symm h) :=
  rfl

@[simp] theorem domCongr_support (e : G ≃+ H) (f : MonoidAlgebra A G) :
    (domCongr k A e f).support = f.support.map e :=
  rfl

@[simp] theorem domCongr_single (e : G ≃+ H) (g : G) (a : A) :
    domCongr k A e (single g a) = single (e g) a :=
  Finsupp.equivMapDomain_single _ _ _

@[simp] theorem domCongr_refl : domCongr k A (AddEquiv.refl G) = AlgEquiv.refl :=
  AlgEquiv.ext fun _ => Finsupp.ext fun _ => rfl

@[simp] theorem domCongr_symm (e : G ≃+ H) : (domCongr k A e).symm = domCongr k A e.symm := rfl

end AddMonoidAlgebra

variable [CommSemiring R]

/-- The algebra equivalence between `AddMonoidAlgebra` and `MonoidAlgebra` in terms of
`Multiplicative`. -/
def AddMonoidAlgebra.toMultiplicativeAlgEquiv [Semiring k] [Algebra R k] [AddMonoid G] :
    AddMonoidAlgebra k G ≃ₐ[R] MonoidAlgebra k (Multiplicative G) :=
  { AddMonoidAlgebra.toMultiplicative k G with
    commutes' := fun r => by simp [AddMonoidAlgebra.toMultiplicative] }
#align add_monoid_algebra.to_multiplicative_alg_equiv AddMonoidAlgebra.toMultiplicativeAlgEquiv

/-- The algebra equivalence between `MonoidAlgebra` and `AddMonoidAlgebra` in terms of
`Additive`. -/
def MonoidAlgebra.toAdditiveAlgEquiv [Semiring k] [Algebra R k] [Monoid G] :
    MonoidAlgebra k G ≃ₐ[R] AddMonoidAlgebra k (Additive G) :=
  { MonoidAlgebra.toAdditive k G with commutes' := fun r => by simp [MonoidAlgebra.toAdditive] }
#align monoid_algebra.to_additive_alg_equiv MonoidAlgebra.toAdditiveAlgEquiv