Algebra structure on monoid algebras

Multiplicative monoids

Non-unital, non-associative algebra structure

theorem MonoidAlgebra.nonUnitalAlgHom_ext (R : Type u_1) {A : Type u_4} {M : Type u_7} [Semiring R] [Mul M] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] {φ₁ φ₂ : MonoidAlgebra R M →ₙₐ[R] A} (h : ∀ (x : M), φ₁ (single x 1) = φ₂ (single x 1)) : φ₁ = φ₂

A non-unital R-algebra homomorphism from R[M] is uniquely defined by its values on the monomials single a 1.

theorem AddMonoidAlgebra.nonUnitalAlgHom_ext (R : Type u_1) {A : Type u_4} {M : Type u_7} [Semiring R] [Add M] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] {φ₁ φ₂ : AddMonoidAlgebra R M →ₙₐ[R] A} (h : ∀ (x : M), φ₁ (single x 1) = φ₂ (single x 1)) : φ₁ = φ₂

A non-unital R-algebra homomorphism from R[M] is uniquely defined by its values on the monomials single a 1.

theorem MonoidAlgebra.nonUnitalAlgHom_ext' (R : Type u_1) {A : Type u_4} {M : Type u_7} [Semiring R] [Mul M] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] {φ₁ φ₂ : MonoidAlgebra R M →ₙₐ[R] A} (h : φ₁.toMulHom.comp (ofMagma R M) = φ₂.toMulHom.comp (ofMagma R M)) : φ₁ = φ₂

See note [partially-applied ext lemmas].

theorem MonoidAlgebra.nonUnitalAlgHom_ext'_iff {R : Type u_1} {A : Type u_4} {M : Type u_7} [Semiring R] [Mul M] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] {φ₁ φ₂ : MonoidAlgebra R M →ₙₐ[R] A} : φ₁ = φ₂ ↔ φ₁.toMulHom.comp (ofMagma R M) = φ₂.toMulHom.comp (ofMagma R M)

def MonoidAlgebra.liftMagma (R : Type u_1) {A : Type u_4} {M : Type u_7} [Semiring R] [Mul M] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : (M →ₙ* A) ≃ (MonoidAlgebra R M →ₙₐ[R] A)

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

Equations

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

@[simp]

theorem MonoidAlgebra.liftMagma_apply_apply (R : Type u_1) {A : Type u_4} {M : Type u_7} [Semiring R] [Mul M] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (f : M →ₙ* A) (a : MonoidAlgebra R M) : ((liftMagma R) f) a = Finsupp.sum a fun (m : M) (t : R) => t • f m

@[simp]

theorem MonoidAlgebra.liftMagma_symm_apply (R : Type u_1) {A : Type u_4} {M : Type u_7} [Semiring R] [Mul M] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (F : MonoidAlgebra R M →ₙₐ[R] A) : (liftMagma R).symm F = F.toMulHom.comp (ofMagma R M)

Algebra structure

instance MonoidAlgebra.algebra {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] : Algebra R (MonoidAlgebra A M)

The instance Algebra R A[M] whenever we have Algebra R A.

In particular this provides the instance Algebra R R[M].

Equations

• MonoidAlgebra.algebra = { toSMul := MonoidAlgebra.smulZeroClass.toSMul, algebraMap := MonoidAlgebra.singleOneRingHom.comp (algebraMap R A), commutes' := ⋯, smul_def' := ⋯ }

instance AddMonoidAlgebra.algebra {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [Semiring A] [Algebra R A] [AddMonoid M] : Algebra R (AddMonoidAlgebra A M)

The instance Algebra R R[M] whenever we have Algebra R R.

In particular this provides the instance Algebra R R[M].

Equations

• AddMonoidAlgebra.algebra = { toSMul := AddMonoidAlgebra.smulZeroClass.toSMul, algebraMap := AddMonoidAlgebra.singleZeroRingHom.comp (algebraMap R A), commutes' := ⋯, smul_def' := ⋯ }

def MonoidAlgebra.singleOneAlgHom {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] : A →ₐ[R] MonoidAlgebra A M

MonoidAlgebra.single 1 as an AlgHom

Equations

• MonoidAlgebra.singleOneAlgHom = { toRingHom := MonoidAlgebra.singleOneRingHom, commutes' := ⋯ }

def AddMonoidAlgebra.singleZeroAlgHom {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [Semiring A] [Algebra R A] [AddMonoid M] : A →ₐ[R] AddMonoidAlgebra A M

AddMonoidAlgebra.single 0 as an AlgHom

Equations

• AddMonoidAlgebra.singleZeroAlgHom = { toRingHom := AddMonoidAlgebra.singleZeroRingHom, commutes' := ⋯ }

@[simp]

theorem MonoidAlgebra.singleOneAlgHom_apply {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] (a✝ : A) : singleOneAlgHom a✝ = single 1 a✝

@[simp]

theorem AddMonoidAlgebra.singleZeroAlgHom_apply {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [Semiring A] [Algebra R A] [AddMonoid M] (a✝ : A) : singleZeroAlgHom a✝ = single 0 a✝

@[simp]

theorem MonoidAlgebra.coe_algebraMap {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] : ⇑(algebraMap R (MonoidAlgebra A M)) = single 1 ∘ ⇑(algebraMap R A)

@[simp]

theorem AddMonoidAlgebra.coe_algebraMap {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [Semiring A] [Algebra R A] [AddMonoid M] : ⇑(algebraMap R (AddMonoidAlgebra A M)) = single 0 ∘ ⇑(algebraMap R A)

theorem MonoidAlgebra.single_eq_algebraMap_mul_of {R : Type u_1} {M : Type u_7} [CommSemiring R] [Monoid M] (m : M) (r : R) : single m r = (algebraMap R (MonoidAlgebra R M)) r * (of R M) m

theorem MonoidAlgebra.single_algebraMap_eq_algebraMap_mul_of {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] (m : M) (r : R) : single m ((algebraMap R A) r) = (algebraMap R (MonoidAlgebra A M)) r * (of A M) m

instance MonoidAlgebra.isLocalHom_singleOneAlgHom {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] : IsLocalHom singleOneAlgHom

instance AddMonoidAlgebra.isLocalHom_singleZeroAlgHom {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [Semiring A] [Algebra R A] [AddMonoid M] : IsLocalHom singleZeroAlgHom

instance MonoidAlgebra.isLocalHom_algebraMap {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] [IsLocalHom (algebraMap R A)] : IsLocalHom (algebraMap R (MonoidAlgebra A M))

instance AddMonoidAlgebra.isLocalHom_algebraMap {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [Semiring A] [Algebra R A] [AddMonoid M] [IsLocalHom (algebraMap R A)] : IsLocalHom (algebraMap R (AddMonoidAlgebra A M))

def MonoidAlgebra.uniqueAlgEquiv (R : Type u_1) {A : Type u_4} (M : Type u_7) [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] [Unique M] : MonoidAlgebra A M ≃ₐ[R] A

The trivial monoid algebra is the base ring.

Equations

• MonoidAlgebra.uniqueAlgEquiv R M = { toEquiv := (MonoidAlgebra.uniqueRingEquiv M).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

def AddMonoidAlgebra.uniqueAlgEquiv (R : Type u_1) {A : Type u_4} (M : Type u_7) [CommSemiring R] [Semiring A] [Algebra R A] [AddMonoid M] [Unique M] : AddMonoidAlgebra A M ≃ₐ[R] A

The trivial monoid algebra is the base ring.

Equations

• AddMonoidAlgebra.uniqueAlgEquiv R M = { toEquiv := (AddMonoidAlgebra.uniqueRingEquiv M).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

def MonoidAlgebra.curryAlgEquiv (R : Type u_1) {A : Type u_4} {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] [Monoid N] [DecidableEq M] : MonoidAlgebra A (M × N) ≃ₐ[R] MonoidAlgebra (MonoidAlgebra A N) M

A product monoid algebra is a nested monoid algebra.

Equations

• MonoidAlgebra.curryAlgEquiv R = { toEquiv := MonoidAlgebra.curryRingEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

def AddMonoidAlgebra.curryAlgEquiv (R : Type u_1) {A : Type u_4} {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [AddMonoid M] [AddMonoid N] [DecidableEq M] : AddMonoidAlgebra A (M × N) ≃ₐ[R] AddMonoidAlgebra (AddMonoidAlgebra A N) M

A product monoid algebra is a nested monoid algebra.

Equations

• AddMonoidAlgebra.curryAlgEquiv R = { toEquiv := AddMonoidAlgebra.curryRingEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem MonoidAlgebra.curryAlgEquiv_single {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] [Monoid N] [DecidableEq M] (m : M) (n : N) (a : A) : (curryAlgEquiv R) (single (m, n) a) = single m (single n a)

@[simp]

theorem AddMonoidAlgebra.curryAlgEquiv_single {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [AddMonoid M] [AddMonoid N] [DecidableEq M] (m : M) (n : N) (a : A) : (curryAlgEquiv R) (single (m, n) a) = single m (single n a)

@[simp]

theorem MonoidAlgebra.curryAlgEquiv_symm_single {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] [Monoid N] [DecidableEq M] (m : M) (n : N) (a : A) : (curryAlgEquiv R).symm (single m (single n a)) = single (m, n) a

@[simp]

theorem AddMonoidAlgebra.curryAlgEquiv_symm_single {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [AddMonoid M] [AddMonoid N] [DecidableEq M] (m : M) (n : N) (a : A) : (curryAlgEquiv R).symm (single m (single n a)) = single (m, n) a

def MonoidAlgebra.liftNCAlgHom {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Monoid M] (f : A →ₐ[R] B) (g : M →* B) (h_comm : ∀ (x : A) (y : M), Commute (f x) (g y)) : MonoidAlgebra A M →ₐ[R] B

liftNCRingHom as an AlgHom, for when f is an AlgHom

Equations

• MonoidAlgebra.liftNCAlgHom f g h_comm = { toRingHom := MonoidAlgebra.liftNCRingHom (↑f) g h_comm, commutes' := ⋯ }

@[simp]

theorem MonoidAlgebra.coe_liftNCAlgHom {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Monoid M] (f : A →ₐ[R] B) (g : M →* B) (h_comm : ∀ (x : A) (y : M), Commute (f x) (g y)) : ⇑(liftNCAlgHom f g h_comm) = ⇑(liftNC ↑f ⇑g)

theorem MonoidAlgebra.algHom_ext {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] ⦃φ₁ φ₂ : MonoidAlgebra R M →ₐ[R] A⦄ (h : ∀ (x : M), φ₁ (single x 1) = φ₂ (single x 1)) : φ₁ = φ₂

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

theorem AddMonoidAlgebra.algHom_ext {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [Semiring A] [Algebra R A] [AddMonoid M] ⦃φ₁ φ₂ : AddMonoidAlgebra R M →ₐ[R] A⦄ (h : ∀ (x : M), φ₁ (single x 1) = φ₂ (single x 1)) : φ₁ = φ₂

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

theorem MonoidAlgebra.algHom_ext' {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] ⦃φ₁ φ₂ : MonoidAlgebra R M →ₐ[R] A⦄ (h : (↑φ₁).comp (of R M) = (↑φ₂).comp (of R M)) : φ₁ = φ₂

See note [partially-applied ext lemmas].

theorem MonoidAlgebra.algHom_ext'_iff {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] {φ₁ φ₂ : MonoidAlgebra R M →ₐ[R] A} : φ₁ = φ₂ ↔ (↑φ₁).comp (of R M) = (↑φ₂).comp (of R M)

def MonoidAlgebra.lift (R : Type u_1) (A : Type u_4) (M : Type u_7) [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] : (M →* A) ≃ (MonoidAlgebra R M →ₐ[R] A)

Any monoid homomorphism M →* A can be lifted to an algebra homomorphism R[M] →ₐ[R] A.

Equations

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

theorem MonoidAlgebra.lift_apply' {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] (F : M →* A) (f : MonoidAlgebra R M) : ((lift R A M) F) f = Finsupp.sum f fun (a : M) (b : R) => (algebraMap R A) b * F a

theorem MonoidAlgebra.lift_apply {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] (F : M →* A) (f : MonoidAlgebra R M) : ((lift R A M) F) f = Finsupp.sum f fun (a : M) (b : R) => b • F a

theorem MonoidAlgebra.lift_def {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] (F : M →* A) : ⇑((lift R A M) F) = ⇑(liftNC ↑(algebraMap R A) ⇑F)

@[simp]

theorem MonoidAlgebra.lift_symm_apply {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] (F : MonoidAlgebra R M →ₐ[R] A) (m : M) : ((lift R A M).symm F) m = F (single m 1)

@[simp]

theorem MonoidAlgebra.lift_single {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] (F : M →* A) (a : M) (b : R) : ((lift R A M) F) (single a b) = b • F a

theorem MonoidAlgebra.lift_of {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] (F : M →* A) (m : M) : ((lift R A M) F) ((of R M) m) = F m

theorem MonoidAlgebra.lift_unique' {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] (F : MonoidAlgebra R M →ₐ[R] A) : F = (lift R A M) ((↑F).comp (of R M))

theorem MonoidAlgebra.lift_unique {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] (F : MonoidAlgebra R M →ₐ[R] A) (f : MonoidAlgebra R M) : F f = Finsupp.sum f fun (a : M) (b : R) => b • F (single a 1)

Decomposition of a R-algebra homomorphism from R[M] by its values on F (single a 1).

def MonoidAlgebra.mapDomainNonUnitalAlgHom {M : Type u_7} {N : Type u_8} (R : Type u_10) (A : Type u_11) [CommSemiring R] [Semiring A] [Algebra R A] [Mul M] [Mul N] (f : M →ₙ* N) : MonoidAlgebra A M →ₙₐ[R] MonoidAlgebra A N

If f : M → N is a homomorphism between two magmas, then MonoidAlgebra.mapDomain f is a non-unital algebra homomorphism between their magma algebras.

Equations

• MonoidAlgebra.mapDomainNonUnitalAlgHom R A f = { toFun := (MonoidAlgebra.mapDomainNonUnitalRingHom A f).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

def AddMonoidAlgebra.mapDomainNonUnitalAlgHom {M : Type u_7} {N : Type u_8} (R : Type u_10) (A : Type u_11) [CommSemiring R] [Semiring A] [Algebra R A] [Add M] [Add N] (f : M →ₙ+ N) : AddMonoidAlgebra A M →ₙₐ[R] AddMonoidAlgebra A N

If f : M → N is a homomorphism between two additive magmas, then AddMonoidAlgebra.mapDomain f is a non-unital algebra homomorphism between their additive magma algebras.

Equations

• AddMonoidAlgebra.mapDomainNonUnitalAlgHom R A f = { toFun := (AddMonoidAlgebra.mapDomainNonUnitalRingHom A f).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

@[simp]

theorem AddMonoidAlgebra.mapDomainNonUnitalAlgHom_apply {M : Type u_7} {N : Type u_8} (R : Type u_10) (A : Type u_11) [CommSemiring R] [Semiring A] [Algebra R A] [Add M] [Add N] (f : M →ₙ+ N) (a✝ : AddMonoidAlgebra A M) : (mapDomainNonUnitalAlgHom R A f) a✝ = (mapDomainNonUnitalRingHom A f).toFun a✝

@[simp]

theorem MonoidAlgebra.mapDomainNonUnitalAlgHom_apply {M : Type u_7} {N : Type u_8} (R : Type u_10) (A : Type u_11) [CommSemiring R] [Semiring A] [Algebra R A] [Mul M] [Mul N] (f : M →ₙ* N) (a✝ : MonoidAlgebra A M) : (mapDomainNonUnitalAlgHom R A f) a✝ = (mapDomainNonUnitalRingHom A f).toFun a✝

theorem MonoidAlgebra.mapDomain_algebraMap {R : Type u_1} (A : Type u_4) {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] [Monoid N] {F : Type u_10} [FunLike F M N] [MonoidHomClass F M N] (f : F) (r : R) : mapDomain (⇑f) ((algebraMap R (MonoidAlgebra A M)) r) = (algebraMap R (MonoidAlgebra A N)) r

theorem AddMonoidAlgebra.mapDomain_algebraMap {R : Type u_1} (A : Type u_4) {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [AddMonoid M] [AddMonoid N] {F : Type u_10} [FunLike F M N] [AddMonoidHomClass F M N] (f : F) (r : R) : mapDomain (⇑f) ((algebraMap R (AddMonoidAlgebra A M)) r) = (algebraMap R (AddMonoidAlgebra A N)) r

def MonoidAlgebra.mapDomainAlgHom (R : Type u_1) (A : Type u_4) {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] [Monoid N] (f : M →* N) : MonoidAlgebra A M →ₐ[R] MonoidAlgebra A N

If f : M → N is a monoid homomorphism, then MonoidAlgebra.mapDomain f is an algebra homomorphism between their monoid algebras.

Equations

• MonoidAlgebra.mapDomainAlgHom R A f = { toRingHom := MonoidAlgebra.mapDomainRingHom A f, commutes' := ⋯ }

def AddMonoidAlgebra.mapDomainAlgHom (R : Type u_1) (A : Type u_4) {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [AddMonoid M] [AddMonoid N] (f : M →+ N) : AddMonoidAlgebra A M →ₐ[R] AddMonoidAlgebra A N

If f : M → N is an additive monoid homomorphism, then MonoidAlgebra.mapDomain f is an algebra homomorphism between their additive monoid algebras.

Equations

• AddMonoidAlgebra.mapDomainAlgHom R A f = { toRingHom := AddMonoidAlgebra.mapDomainRingHom A f, commutes' := ⋯ }

@[simp]

theorem MonoidAlgebra.mapDomainAlgHom_apply (R : Type u_1) (A : Type u_4) {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] [Monoid N] (f : M →* N) (x : MonoidAlgebra A M) : (mapDomainAlgHom R A f) x = mapDomain (⇑f) x

@[simp]

theorem AddMonoidAlgebra.mapDomainAlgHom_apply (R : Type u_1) (A : Type u_4) {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [AddMonoid M] [AddMonoid N] (f : M →+ N) (x : AddMonoidAlgebra A M) : (mapDomainAlgHom R A f) x = mapDomain (⇑f) x

@[simp]

theorem MonoidAlgebra.mapDomainAlgHom_id {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] : mapDomainAlgHom R A (MonoidHom.id M) = AlgHom.id R (MonoidAlgebra A M)

@[simp]

theorem AddMonoidAlgebra.mapDomainAlgHom_id {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [Semiring A] [Algebra R A] [AddMonoid M] : mapDomainAlgHom R A (AddMonoidHom.id M) = AlgHom.id R (AddMonoidAlgebra A M)

@[simp]

theorem MonoidAlgebra.mapDomainAlgHom_comp {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} {O : Type u_9} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] [Monoid N] [Monoid O] (f : M →* N) (g : N →* O) : mapDomainAlgHom R A (g.comp f) = (mapDomainAlgHom R A g).comp (mapDomainAlgHom R A f)

@[simp]

theorem AddMonoidAlgebra.mapDomainAlgHom_comp {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} {O : Type u_9} [CommSemiring R] [Semiring A] [Algebra R A] [AddMonoid M] [AddMonoid N] [AddMonoid O] (f : M →+ N) (g : N →+ O) : mapDomainAlgHom R A (g.comp f) = (mapDomainAlgHom R A g).comp (mapDomainAlgHom R A f)

def MonoidAlgebra.domCongr (R : Type u_1) (A : Type u_4) {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] [Monoid N] (e : M ≃* N) : MonoidAlgebra A M ≃ₐ[R] MonoidAlgebra A N

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

Equations

• MonoidAlgebra.domCongr R A e = { toEquiv := (MonoidAlgebra.mapDomainRingEquiv A e).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

def AddMonoidAlgebra.domCongr (R : Type u_1) (A : Type u_4) {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [AddMonoid M] [AddMonoid N] (e : M ≃+ N) : AddMonoidAlgebra A M ≃ₐ[R] AddMonoidAlgebra A N

If e : M ≃+ N is an additive equivalence between two additive monoids, then AddMonoidAlgebra.domCongr e is an algebra equivalence between their additive monoid algebras.

Equations

• AddMonoidAlgebra.domCongr R A e = { toEquiv := (AddMonoidAlgebra.mapDomainRingEquiv A e).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem MonoidAlgebra.domCongr_apply {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] [Monoid N] (e : M ≃* N) (x : MonoidAlgebra A M) (n : N) : ((domCongr R A e) x) n = x (e.symm n)

@[simp]

theorem AddMonoidAlgebra.domCongr_apply {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [AddMonoid M] [AddMonoid N] (e : M ≃+ N) (x : AddMonoidAlgebra A M) (n : N) : ((domCongr R A e) x) n = x (e.symm n)

theorem MonoidAlgebra.domCongr_toAlgHom {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] [Monoid N] (e : M ≃* N) : ↑(domCongr R A e) = mapDomainAlgHom R A ↑e

theorem AddMonoidAlgebra.domCongr_toAlgHom {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [AddMonoid M] [AddMonoid N] (e : M ≃+ N) : ↑(domCongr R A e) = mapDomainAlgHom R A ↑e

@[simp]

theorem MonoidAlgebra.domCongr_support {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] [Monoid N] (e : M ≃* N) (f : MonoidAlgebra A M) : ((domCongr R A e) f).support = Finset.map (↑e).toEmbedding f.support

@[simp]

theorem AddMonoidAlgebra.domCongr_support {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [AddMonoid M] [AddMonoid N] (e : M ≃+ N) (f : AddMonoidAlgebra A M) : ((domCongr R A e) f).support = Finset.map (↑e).toEmbedding f.support

@[simp]

theorem MonoidAlgebra.domCongr_single {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] [Monoid N] (e : M ≃* N) (m : M) (a : A) : (domCongr R A e) (single m a) = single (e m) a

@[simp]

theorem AddMonoidAlgebra.domCongr_single {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [AddMonoid M] [AddMonoid N] (e : M ≃+ N) (m : M) (a : A) : (domCongr R A e) (single m a) = single (e m) a

@[simp]

theorem MonoidAlgebra.domCongr_comp_lsingle {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] [Monoid N] (e : M ≃* N) (m : M) : (domCongr R A e).toLinearMap ∘ₗ lsingle m = lsingle (e m)

@[simp]

theorem AddMonoidAlgebra.domCongr_comp_lsingle {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [AddMonoid M] [AddMonoid N] (e : M ≃+ N) (m : M) : (domCongr R A e).toLinearMap ∘ₗ lsingle m = lsingle (e m)

@[simp]

theorem MonoidAlgebra.domCongr_refl {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] : domCongr R A (MulEquiv.refl M) = AlgEquiv.refl

@[simp]

theorem AddMonoidAlgebra.domCongr_refl {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [Semiring A] [Algebra R A] [AddMonoid M] : domCongr R A (AddEquiv.refl M) = AlgEquiv.refl

@[simp]

theorem MonoidAlgebra.domCongr_symm {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] [Monoid N] (e : M ≃* N) : (domCongr R A e).symm = domCongr R A e.symm

@[simp]

theorem AddMonoidAlgebra.domCongr_symm {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [AddMonoid M] [AddMonoid N] (e : M ≃+ N) : (domCongr R A e).symm = domCongr R A e.symm

def MonoidAlgebra.commAlgEquiv (R : Type u_1) {A : Type u_4} {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] [Monoid N] [DecidableEq M] [DecidableEq N] : MonoidAlgebra (MonoidAlgebra A M) N ≃ₐ[R] MonoidAlgebra (MonoidAlgebra A N) M

Nested monoid algebras can be taken in an arbitrary order.

Equations

• MonoidAlgebra.commAlgEquiv R = (MonoidAlgebra.curryAlgEquiv R).symm.trans ((MonoidAlgebra.domCongr R A MulEquiv.prodComm).trans (MonoidAlgebra.curryAlgEquiv R))

def AddMonoidAlgebra.commAlgEquiv (R : Type u_1) {A : Type u_4} {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [AddMonoid M] [AddMonoid N] [DecidableEq M] [DecidableEq N] : AddMonoidAlgebra (AddMonoidAlgebra A M) N ≃ₐ[R] AddMonoidAlgebra (AddMonoidAlgebra A N) M

Nested monoid algebras can be taken in an arbitrary order.

Equations

• AddMonoidAlgebra.commAlgEquiv R = (AddMonoidAlgebra.curryAlgEquiv R).symm.trans ((AddMonoidAlgebra.domCongr R A AddEquiv.prodComm).trans (AddMonoidAlgebra.curryAlgEquiv R))

@[simp]

theorem MonoidAlgebra.symm_commAlgEquiv {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] [Monoid N] [DecidableEq M] [DecidableEq N] : (commAlgEquiv R).symm = commAlgEquiv R

@[simp]

theorem AddMonoidAlgebra.symm_commAlgEquiv {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [AddMonoid M] [AddMonoid N] [DecidableEq M] [DecidableEq N] : (commAlgEquiv R).symm = commAlgEquiv R

@[simp]

theorem MonoidAlgebra.commAlgEquiv_single_single {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] [Monoid N] [DecidableEq M] [DecidableEq N] (m : M) (n : N) (a : A) : (commAlgEquiv R) (single m (single n a)) = single n (single m a)

@[simp]

theorem AddMonoidAlgebra.commAlgEquiv_single_single {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [AddMonoid M] [AddMonoid N] [DecidableEq M] [DecidableEq N] (m : M) (n : N) (a : A) : (commAlgEquiv R) (single m (single n a)) = single n (single m a)

@[simp]

theorem MonoidAlgebra.mapDomainRingHom_comp_algebraMap {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] [Monoid N] (f : M →* N) : (mapDomainRingHom A f).comp (algebraMap R (MonoidAlgebra A M)) = algebraMap R (MonoidAlgebra A N)

@[simp]

theorem AddMonoidAlgebra.mapDomainRingHom_comp_algebraMap {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [CommSemiring R] [Semiring A] [Algebra R A] [AddMonoid M] [AddMonoid N] (f : M →+ N) : (mapDomainRingHom A f).comp (algebraMap R (AddMonoidAlgebra A M)) = algebraMap R (AddMonoidAlgebra A N)

@[simp]

theorem MonoidAlgebra.mapRangeRingHom_comp_algebraMap {R : Type u_1} {S : Type u_2} {M : Type u_7} [CommSemiring R] [CommSemiring S] [Monoid M] (f : R →+* S) : (mapRangeRingHom M f).comp (algebraMap R (MonoidAlgebra R M)) = (algebraMap S (MonoidAlgebra S M)).comp f

@[simp]

theorem AddMonoidAlgebra.mapRangeRingHom_comp_algebraMap {R : Type u_1} {S : Type u_2} {M : Type u_7} [CommSemiring R] [CommSemiring S] [AddMonoid M] (f : R →+* S) : (mapRangeRingHom M f).comp (algebraMap R (AddMonoidAlgebra R M)) = (algebraMap S (AddMonoidAlgebra S M)).comp f

noncomputable def MonoidAlgebra.mapRangeAlgHom {R : Type u_1} {A : Type u_4} {B : Type u_5} (M : Type u_7) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Monoid M] (f : A →ₐ[R] B) : MonoidAlgebra A M →ₐ[R] MonoidAlgebra B M

The algebra homomorphism of monoid algebras induced by a homomorphism of the base algebras.

Equations

• MonoidAlgebra.mapRangeAlgHom M f = { toRingHom := MonoidAlgebra.mapRangeRingHom M ↑f, commutes' := ⋯ }

noncomputable def AddMonoidAlgebra.mapRangeAlgHom {R : Type u_1} {A : Type u_4} {B : Type u_5} (M : Type u_7) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddMonoid M] (f : A →ₐ[R] B) : AddMonoidAlgebra A M →ₐ[R] AddMonoidAlgebra B M

The algebra homomorphism of additive monoid algebras induced by a homomorphism of the base algebras.

Equations

• AddMonoidAlgebra.mapRangeAlgHom M f = { toRingHom := AddMonoidAlgebra.mapRangeRingHom M ↑f, commutes' := ⋯ }

@[simp]

theorem MonoidAlgebra.toRingHom_mapRangeAlgHom {R : Type u_1} {A : Type u_4} {B : Type u_5} (M : Type u_7) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Monoid M] (f : A →ₐ[R] B) : ↑(mapRangeAlgHom M f) = mapRangeRingHom M f.toRingHom

@[simp]

theorem AddMonoidAlgebra.toRingHom_mapRangeAlgHom {R : Type u_1} {A : Type u_4} {B : Type u_5} (M : Type u_7) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddMonoid M] (f : A →ₐ[R] B) : ↑(mapRangeAlgHom M f) = mapRangeRingHom M f.toRingHom

@[simp]

theorem MonoidAlgebra.mapRangeAlgHom_apply {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Monoid M] (f : A →ₐ[R] B) (x : MonoidAlgebra A M) (m : M) : ((mapRangeAlgHom M f) x) m = f (x m)

@[simp]

theorem AddMonoidAlgebra.mapRangeAlgHom_apply {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddMonoid M] (f : A →ₐ[R] B) (x : AddMonoidAlgebra A M) (m : M) : ((mapRangeAlgHom M f) x) m = f (x m)

@[simp]

theorem MonoidAlgebra.mapRangeAlgHom_single {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Monoid M] (f : A →ₐ[R] B) (m : M) (a : A) : (mapRangeAlgHom M f) (single m a) = single m (f a)

@[simp]

theorem AddMonoidAlgebra.mapRangeAlgHom_single {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddMonoid M] (f : A →ₐ[R] B) (m : M) (a : A) : (mapRangeAlgHom M f) (single m a) = single m (f a)

noncomputable def MonoidAlgebra.mapRangeAlgEquiv (R : Type u_1) {A : Type u_4} {B : Type u_5} (M : Type u_7) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Monoid M] (e : A ≃ₐ[R] B) : MonoidAlgebra A M ≃ₐ[R] MonoidAlgebra B M

The algebra isomorphism of monoid algebras induced by an isomorphism of the base algebras.

Equations

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

noncomputable def AddMonoidAlgebra.mapRangeAlgEquiv (R : Type u_1) {A : Type u_4} {B : Type u_5} (M : Type u_7) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddMonoid M] (e : A ≃ₐ[R] B) : AddMonoidAlgebra A M ≃ₐ[R] AddMonoidAlgebra B M

The algebra isomorphism of additive monoid algebras induced by an isomorphism of the base algebras.

Equations

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

@[simp]

theorem AddMonoidAlgebra.mapRangeAlgEquiv_apply (R : Type u_1) {A : Type u_4} {B : Type u_5} (M : Type u_7) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddMonoid M] (e : A ≃ₐ[R] B) (a✝ : AddMonoidAlgebra A M) : (mapRangeAlgEquiv R M e) a✝ = (↑↑(mapRangeAlgHom M ↑e).toRingHom).toFun a✝

@[simp]

theorem MonoidAlgebra.mapRangeAlgEquiv_apply (R : Type u_1) {A : Type u_4} {B : Type u_5} (M : Type u_7) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Monoid M] (e : A ≃ₐ[R] B) (a✝ : MonoidAlgebra A M) : (mapRangeAlgEquiv R M e) a✝ = (↑↑(mapRangeAlgHom M ↑e).toRingHom).toFun a✝

@[simp]

theorem MonoidAlgebra.symm_mapRangeAlgEquiv {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Monoid M] (e : A ≃ₐ[R] B) : (mapRangeAlgEquiv R M e).symm = mapRangeAlgEquiv R M e.symm

@[simp]

theorem AddMonoidAlgebra.symm_mapRangeAlgEquiv {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [AddMonoid M] (e : A ≃ₐ[R] B) : (mapRangeAlgEquiv R M e).symm = mapRangeAlgEquiv R M e.symm

@[simp]

theorem MonoidAlgebra.mapRangeAlgEquiv_trans {R : Type u_1} {A : Type u_4} {B : Type u_5} {C : Type u_6} {M : Type u_7} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B] [Algebra R C] [Monoid M] (e₁ : A ≃ₐ[R] B) (e₂ : B ≃ₐ[R] C) : mapRangeAlgEquiv R M (e₁.trans e₂) = (mapRangeAlgEquiv R M e₁).trans (mapRangeAlgEquiv R M e₂)

@[simp]

theorem AddMonoidAlgebra.mapRangeAlgEquiv_trans {R : Type u_1} {A : Type u_4} {B : Type u_5} {C : Type u_6} {M : Type u_7} [CommSemiring R] [Semiring A] [Semiring B] [Semiring C] [Algebra R A] [Algebra R B] [Algebra R C] [AddMonoid M] (e₁ : A ≃ₐ[R] B) (e₂ : B ≃ₐ[R] C) : mapRangeAlgEquiv R M (e₁.trans e₂) = (mapRangeAlgEquiv R M e₁).trans (mapRangeAlgEquiv R M e₂)

def MonoidAlgebra.GroupSMul.linearMap (R : Type u_1) {M : Type u_7} [Monoid M] [CommSemiring R] (V : Type u_10) [AddCommMonoid V] [Module R V] [Module (MonoidAlgebra R M) V] [IsScalarTower R (MonoidAlgebra R M) V] (g : M) : V →ₗ[R] V

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

Equations

• MonoidAlgebra.GroupSMul.linearMap R V g = { toFun := fun (v : V) => MonoidAlgebra.single g 1 • v, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem MonoidAlgebra.GroupSMul.linearMap_apply (R : Type u_1) {M : Type u_7} [Monoid M] [CommSemiring R] (V : Type u_10) [AddCommMonoid V] [Module R V] [Module (MonoidAlgebra R M) V] [IsScalarTower R (MonoidAlgebra R M) V] (g : M) (v : V) : (linearMap R V g) v = single g 1 • v

def MonoidAlgebra.equivariantOfLinearOfComm {R : Type u_1} {M : Type u_7} [Monoid M] [CommSemiring R] {V : Type u_10} {W : Type u_11} [AddCommMonoid V] [Module R V] [Module (MonoidAlgebra R M) V] [IsScalarTower R (MonoidAlgebra R M) V] [AddCommMonoid W] [Module R W] [Module (MonoidAlgebra R M) W] [IsScalarTower R (MonoidAlgebra R M) W] (f : V →ₗ[R] W) (h : ∀ (g : M) (v : V), f (single g 1 • v) = single g 1 • f v) : V →ₗ[MonoidAlgebra R M] W

Build a R[M]-linear map from a R-linear map and evidence that it is M-equivariant.

Equations

• MonoidAlgebra.equivariantOfLinearOfComm f h = { toFun := ⇑f, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem MonoidAlgebra.equivariantOfLinearOfComm_apply {R : Type u_1} {M : Type u_7} [Monoid M] [CommSemiring R] {V : Type u_10} {W : Type u_11} [AddCommMonoid V] [Module R V] [Module (MonoidAlgebra R M) V] [IsScalarTower R (MonoidAlgebra R M) V] [AddCommMonoid W] [Module R W] [Module (MonoidAlgebra R M) W] [IsScalarTower R (MonoidAlgebra R M) W] (f : V →ₗ[R] W) (h : ∀ (g : M) (v : V), f (single g 1 • v) = single g 1 • f v) (v : V) : (equivariantOfLinearOfComm f h) v = f v

@[reducible, inline]

noncomputable abbrev MonoidAlgebra.algebraMonoidAlgebra {R : Type u_1} {S : Type u_2} {M : Type u_7} [CommMonoid M] [CommSemiring R] [CommSemiring S] [Algebra R S] : Algebra (MonoidAlgebra R M) (MonoidAlgebra S M)

If S is an R-algebra, then S[M] is a R[M] algebra.

Warning: This produces a diamond for Algebra R[M] S[M][M] and another one for Algebra R[M] R[M]. That's why it is not a global instance.

Equations

• MonoidAlgebra.algebraMonoidAlgebra = (MonoidAlgebra.mapRangeRingHom M (algebraMap R S)).toAlgebra

@[reducible, inline]

noncomputable abbrev AddMonoidAlgebra.algebraAddMonoidAlgebra {R : Type u_1} {S : Type u_2} {M : Type u_7} [AddCommMonoid M] [CommSemiring R] [CommSemiring S] [Algebra R S] : Algebra (AddMonoidAlgebra R M) (AddMonoidAlgebra S M)

If S is an R-algebra, then S[M] is an R[M]-algebra.

Warning: This produces a diamond for Algebra R[M] S[M][M] and another one for Algebra R[M] R[M]. That's why it is not a global instance.

Equations

• AddMonoidAlgebra.algebraAddMonoidAlgebra = (AddMonoidAlgebra.mapRangeRingHom M (algebraMap R S)).toAlgebra

@[simp]

theorem MonoidAlgebra.algebraMap_def {R : Type u_1} {S : Type u_2} {M : Type u_7} [CommMonoid M] [CommSemiring R] [CommSemiring S] [Algebra R S] : algebraMap (MonoidAlgebra R M) (MonoidAlgebra S M) = mapRangeRingHom M (algebraMap R S)

@[simp]

theorem AddMonoidAlgebra.algebraMap_def {R : Type u_1} {S : Type u_2} {M : Type u_7} [AddCommMonoid M] [CommSemiring R] [CommSemiring S] [Algebra R S] : algebraMap (AddMonoidAlgebra R M) (AddMonoidAlgebra S M) = mapRangeRingHom M (algebraMap R S)

theorem MonoidAlgebra.isScalarTower_monoidAlgebra {R : Type u_1} {S : Type u_2} {T : Type u_3} {M : Type u_7} [CommMonoid M] [CommSemiring R] [CommSemiring S] [Algebra R S] [CommSemiring T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] : IsScalarTower R (MonoidAlgebra S M) (MonoidAlgebra T M)

theorem AddMonoidAlgebra.vaddAssocClass_addMonoidAlgebra {R : Type u_1} {S : Type u_2} {T : Type u_3} {M : Type u_7} [AddCommMonoid M] [CommSemiring R] [CommSemiring S] [Algebra R S] [CommSemiring T] [Algebra R T] [Algebra S T] [IsScalarTower R S T] : IsScalarTower R (AddMonoidAlgebra S M) (AddMonoidAlgebra T M)

Non-unital, non-associative algebra structure

theorem AddMonoidAlgebra.nonUnitalAlgHom_ext' (R : Type u_1) {A : Type u_4} {M : Type u_7} [Semiring R] [Add M] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] {φ₁ φ₂ : AddMonoidAlgebra R M →ₙₐ[R] A} (h : φ₁.toMulHom.comp (ofMagma R M) = φ₂.toMulHom.comp (ofMagma R M)) : φ₁ = φ₂

See note [partially-applied ext lemmas].

theorem AddMonoidAlgebra.nonUnitalAlgHom_ext'_iff {R : Type u_1} {A : Type u_4} {M : Type u_7} [Semiring R] [Add M] [NonUnitalNonAssocSemiring A] [DistribMulAction R A] {φ₁ φ₂ : AddMonoidAlgebra R M →ₙₐ[R] A} : φ₁ = φ₂ ↔ φ₁.toMulHom.comp (ofMagma R M) = φ₂.toMulHom.comp (ofMagma R M)

def AddMonoidAlgebra.liftMagma (R : Type u_1) {A : Type u_4} {M : Type u_7} [Semiring R] [Add M] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : (Multiplicative M →ₙ* A) ≃ (AddMonoidAlgebra R M →ₙₐ[R] A)

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

Equations

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

@[simp]

theorem AddMonoidAlgebra.liftMagma_apply_apply (R : Type u_1) {A : Type u_4} {M : Type u_7} [Semiring R] [Add M] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (f : Multiplicative M →ₙ* A) (a : AddMonoidAlgebra R M) : ((liftMagma R) f) a = Finsupp.sum a fun (m : M) (t : R) => t • f (Multiplicative.ofAdd m)

@[simp]

theorem AddMonoidAlgebra.liftMagma_symm_apply (R : Type u_1) {A : Type u_4} {M : Type u_7} [Semiring R] [Add M] [NonUnitalNonAssocSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (f : AddMonoidAlgebra R M →ₙₐ[R] A) : (liftMagma R).symm f = f.toMulHom.comp (ofMagma R M)

Algebra structure

def AddMonoidAlgebra.liftNCAlgHom {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [CommSemiring R] [AddMonoid M] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (f : A →ₐ[R] B) (g : Multiplicative M →* B) (h_comm : ∀ (x : A) (y : Multiplicative M), Commute (f x) (g y)) : AddMonoidAlgebra A M →ₐ[R] B

liftNCRingHom as an AlgHom, for when f is an AlgHom

Equations

• AddMonoidAlgebra.liftNCAlgHom f g h_comm = { toRingHom := AddMonoidAlgebra.liftNCRingHom (↑f) g h_comm, commutes' := ⋯ }

@[simp]

theorem AddMonoidAlgebra.coe_liftNCAlgHom {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [CommSemiring R] [AddMonoid M] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (f : A →ₐ[R] B) (g : Multiplicative M →* B) (h_comm : ∀ (x : A) (y : Multiplicative M), Commute (f x) (g y)) : ⇑(liftNCAlgHom f g h_comm) = ⇑(liftNC ↑f ⇑g)

theorem AddMonoidAlgebra.algHom_ext' {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [AddMonoid M] [Semiring A] [Algebra R A] ⦃φ₁ φ₂ : AddMonoidAlgebra R M →ₐ[R] A⦄ (h : (↑φ₁).comp (of R M) = (↑φ₂).comp (of R M)) : φ₁ = φ₂

See note [partially-applied ext lemmas].

theorem AddMonoidAlgebra.algHom_ext'_iff {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [AddMonoid M] [Semiring A] [Algebra R A] {φ₁ φ₂ : AddMonoidAlgebra R M →ₐ[R] A} : φ₁ = φ₂ ↔ (↑φ₁).comp (of R M) = (↑φ₂).comp (of R M)

def AddMonoidAlgebra.lift (R : Type u_1) (A : Type u_4) (M : Type u_7) [CommSemiring R] [AddMonoid M] [Semiring A] [Algebra R A] : (Multiplicative M →* A) ≃ (AddMonoidAlgebra R M →ₐ[R] A)

Any monoid homomorphism M →* A can be lifted to an algebra homomorphism R[M] →ₐ[R] A.

Equations

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

theorem AddMonoidAlgebra.lift_apply' {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [AddMonoid M] [Semiring A] [Algebra R A] (F : Multiplicative M →* A) (f : AddMonoidAlgebra R M) : ((lift R A M) F) f = Finsupp.sum f fun (a : M) (b : R) => (algebraMap R A) b * F (Multiplicative.ofAdd a)

theorem AddMonoidAlgebra.lift_apply {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [AddMonoid M] [Semiring A] [Algebra R A] (F : Multiplicative M →* A) (f : AddMonoidAlgebra R M) : ((lift R A M) F) f = Finsupp.sum f fun (a : M) (b : R) => b • F (Multiplicative.ofAdd a)

theorem AddMonoidAlgebra.lift_def {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [AddMonoid M] [Semiring A] [Algebra R A] (F : Multiplicative M →* A) : ⇑((lift R A M) F) = ⇑(liftNC ↑(algebraMap R A) ⇑F)

@[simp]

theorem AddMonoidAlgebra.lift_symm_apply {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [AddMonoid M] [Semiring A] [Algebra R A] (F : AddMonoidAlgebra R M →ₐ[R] A) (x : Multiplicative M) : ((lift R A M).symm F) x = F (single (Multiplicative.toAdd x) 1)

theorem AddMonoidAlgebra.lift_of {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [AddMonoid M] [Semiring A] [Algebra R A] (F : Multiplicative M →* A) (x : Multiplicative M) : ((lift R A M) F) ((of R M) x) = F x

@[simp]

theorem AddMonoidAlgebra.lift_single {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [AddMonoid M] [Semiring A] [Algebra R A] (F : Multiplicative M →* A) (a : M) (b : R) : ((lift R A M) F) (single a b) = b • F (Multiplicative.ofAdd a)

theorem AddMonoidAlgebra.lift_of' {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [AddMonoid M] [Semiring A] [Algebra R A] (F : Multiplicative M →* A) (x : M) : ((lift R A M) F) (of' R M x) = F (Multiplicative.ofAdd x)

theorem AddMonoidAlgebra.lift_unique' {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [AddMonoid M] [Semiring A] [Algebra R A] (F : AddMonoidAlgebra R M →ₐ[R] A) : F = (lift R A M) ((↑F).comp (of R M))

theorem AddMonoidAlgebra.lift_unique {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [AddMonoid M] [Semiring A] [Algebra R A] (F : AddMonoidAlgebra R M →ₐ[R] A) (f : AddMonoidAlgebra R M) : F f = Finsupp.sum f fun (a : M) (b : R) => b • F (single a 1)

Decomposition of a R-algebra homomorphism from R[M] by its values on F (single a 1).

theorem AddMonoidAlgebra.algHom_ext_iff {R : Type u_1} {A : Type u_4} {M : Type u_7} [CommSemiring R] [AddMonoid M] [Semiring A] [Algebra R A] {φ₁ φ₂ : AddMonoidAlgebra R M →ₐ[R] A} : (∀ (x : M), φ₁ (single x 1) = φ₂ (single x 1)) ↔ φ₁ = φ₂

def AddMonoidAlgebra.toMultiplicativeAlgEquiv {R : Type u_1} (A : Type u_4) (M : Type u_7) [CommSemiring R] [Semiring A] [Algebra R A] [AddMonoid M] : AddMonoidAlgebra A M ≃ₐ[R] MonoidAlgebra A (Multiplicative M)

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

Equations

• AddMonoidAlgebra.toMultiplicativeAlgEquiv A M = { toEquiv := (AddMonoidAlgebra.toMultiplicative A M).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

def MonoidAlgebra.toAdditiveAlgEquiv {R : Type u_1} (A : Type u_4) (M : Type u_7) [CommSemiring R] [Semiring A] [Algebra R A] [Monoid M] : MonoidAlgebra A M ≃ₐ[R] AddMonoidAlgebra A (Additive M)

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

Equations

• MonoidAlgebra.toAdditiveAlgEquiv A M = { toEquiv := (MonoidAlgebra.toAdditive A M).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }