Monoid algebras

Multiplicative monoids

Non-unital, non-associative algebra structure

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

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

theorem MonoidAlgebra.nonUnitalAlgHom_ext' (k : Type u₁) {G : Type u₂} [Semiring k] [Mul G] {A : Type u₃} [NonUnitalNonAssocSemiring A] [DistribMulAction k A] {φ₁ φ₂ : MonoidAlgebra k G →ₙₐ[k] A} (h : φ₁.toMulHom.comp (MonoidAlgebra.ofMagma k G) = φ₂.toMulHom.comp (MonoidAlgebra.ofMagma k G)) : φ₁ = φ₂

See note [partially-applied ext lemmas].

def MonoidAlgebra.liftMagma (k : Type u₁) {G : Type u₂} [Semiring k] [Mul G] {A : Type u₃} [NonUnitalNonAssocSemiring A] [Module k A] [IsScalarTower k A A] [SMulCommClass k A A] : (G →ₙ* A) ≃ (MonoidAlgebra k G →ₙₐ[k] A)

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

Equations

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

@[simp]

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

@[simp]

theorem MonoidAlgebra.liftMagma_symm_apply (k : Type u₁) {G : Type u₂} [Semiring k] [Mul G] {A : Type u₃} [NonUnitalNonAssocSemiring A] [Module k A] [IsScalarTower k A A] [SMulCommClass k A A] (F : MonoidAlgebra k G →ₙₐ[k] A) : (MonoidAlgebra.liftMagma k).symm F = F.toMulHom.comp (MonoidAlgebra.ofMagma k G)

Algebra structure

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

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

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

Equations

• MonoidAlgebra.algebra = Algebra.mk (MonoidAlgebra.singleOneRingHom.comp (algebraMap k A)) ⋯ ⋯

def MonoidAlgebra.singleOneAlgHom {k : Type u₁} {G : Type u₂} {A : Type u_3} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] : A →ₐ[k] MonoidAlgebra A G

Finsupp.single 1 as an AlgHom

Equations

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

@[simp]

theorem MonoidAlgebra.singleOneAlgHom_apply {k : Type u₁} {G : Type u₂} {A : Type u_3} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] (a✝ : A) : MonoidAlgebra.singleOneAlgHom a✝ = Finsupp.single 1 a✝

@[simp]

theorem MonoidAlgebra.coe_algebraMap {k : Type u₁} {G : Type u₂} {A : Type u_3} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] : ⇑(algebraMap k (MonoidAlgebra A G)) = MonoidAlgebra.single 1 ∘ ⇑(algebraMap k A)

theorem MonoidAlgebra.single_eq_algebraMap_mul_of {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] (a : G) (b : k) : MonoidAlgebra.single a b = (algebraMap k (MonoidAlgebra k G)) b * (MonoidAlgebra.of k G) a

theorem MonoidAlgebra.single_algebraMap_eq_algebraMap_mul_of {k : Type u₁} {G : Type u₂} {A : Type u_3} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] (a : G) (b : k) : MonoidAlgebra.single a ((algebraMap k A) b) = (algebraMap k (MonoidAlgebra A G)) b * (MonoidAlgebra.of A G) a

def MonoidAlgebra.liftNCAlgHom {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] {B : Type u_3} [Semiring B] [Algebra k B] (f : A →ₐ[k] B) (g : G →* B) (h_comm : ∀ (x : A) (y : G), Commute (f x) (g y)) : MonoidAlgebra A G →ₐ[k] 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' := ⋯ }

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

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

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

See note [partially-applied ext lemmas].

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

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

Equations

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

theorem MonoidAlgebra.lift_apply' {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : G →* A) (f : MonoidAlgebra k G) : ((MonoidAlgebra.lift k G A) F) f = Finsupp.sum f fun (a : G) (b : k) => (algebraMap k A) b * F a

theorem MonoidAlgebra.lift_apply {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : G →* A) (f : MonoidAlgebra k G) : ((MonoidAlgebra.lift k G A) F) f = Finsupp.sum f fun (a : G) (b : k) => b • F a

theorem MonoidAlgebra.lift_def {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : G →* A) : ⇑((MonoidAlgebra.lift k G A) F) = ⇑(MonoidAlgebra.liftNC ↑(algebraMap k A) ⇑F)

@[simp]

theorem MonoidAlgebra.lift_symm_apply {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : MonoidAlgebra k G →ₐ[k] A) (x : G) : ((MonoidAlgebra.lift k G A).symm F) x = F (MonoidAlgebra.single x 1)

@[simp]

theorem MonoidAlgebra.lift_single {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : G →* A) (a : G) (b : k) : ((MonoidAlgebra.lift k G A) F) (MonoidAlgebra.single a b) = b • F a

theorem MonoidAlgebra.lift_of {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : G →* A) (x : G) : ((MonoidAlgebra.lift k G A) F) ((MonoidAlgebra.of k G) x) = F x

theorem MonoidAlgebra.lift_unique' {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : MonoidAlgebra k G →ₐ[k] A) : F = (MonoidAlgebra.lift k G A) ((↑F).comp (MonoidAlgebra.of k G))

theorem MonoidAlgebra.lift_unique {k : Type u₁} {G : Type u₂} [CommSemiring k] [Monoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : MonoidAlgebra k G →ₐ[k] A) (f : MonoidAlgebra k G) : F f = Finsupp.sum f fun (a : G) (b : k) => b • F (MonoidAlgebra.single a 1)

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

def MonoidAlgebra.mapDomainNonUnitalAlgHom (k : Type u_4) (A : Type u_5) [CommSemiring k] [Semiring A] [Algebra k A] {G : Type u_6} {H : Type u_7} {F : Type u_8} [Mul G] [Mul H] [FunLike F G H] [MulHomClass F G H] (f : F) : MonoidAlgebra A G →ₙₐ[k] MonoidAlgebra A H

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

Equations

• MonoidAlgebra.mapDomainNonUnitalAlgHom k A f = { toFun := (↑(Finsupp.mapDomain.addMonoidHom ⇑f)).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

@[simp]

theorem MonoidAlgebra.mapDomainNonUnitalAlgHom_apply (k : Type u_4) (A : Type u_5) [CommSemiring k] [Semiring A] [Algebra k A] {G : Type u_6} {H : Type u_7} {F : Type u_8} [Mul G] [Mul H] [FunLike F G H] [MulHomClass F G H] (f : F) (a✝ : G →₀ A) : (MonoidAlgebra.mapDomainNonUnitalAlgHom k A f) a✝ = (↑(Finsupp.mapDomain.addMonoidHom ⇑f)).toFun a✝

theorem MonoidAlgebra.mapDomain_algebraMap {k : Type u₁} {G : Type u₂} {H : Type u_1} [CommSemiring k] [Monoid G] [Monoid H] (A : Type u₃) [Semiring A] [Algebra k A] {F : Type u_4} [FunLike F G H] [MonoidHomClass F G H] (f : F) (r : k) : MonoidAlgebra.mapDomain (⇑f) ((algebraMap k (MonoidAlgebra A G)) r) = (algebraMap k (MonoidAlgebra A H)) r

def MonoidAlgebra.mapDomainAlgHom {G : Type u₂} [Monoid G] (k : Type u_4) (A : Type u_5) [CommSemiring k] [Semiring A] [Algebra k A] {H : Type u_6} {F : Type u_7} [Monoid H] [FunLike F G H] [MonoidHomClass F G H] (f : F) : MonoidAlgebra A G →ₐ[k] MonoidAlgebra A H

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

Equations

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

@[simp]

theorem MonoidAlgebra.mapDomainAlgHom_apply {G : Type u₂} [Monoid G] (k : Type u_4) (A : Type u_5) [CommSemiring k] [Semiring A] [Algebra k A] {H : Type u_6} {F : Type u_7} [Monoid H] [FunLike F G H] [MonoidHomClass F G H] (f : F) (a✝ : G →₀ A) : (MonoidAlgebra.mapDomainAlgHom k A f) a✝ = Finsupp.mapDomain (⇑f) a✝

@[simp]

theorem MonoidAlgebra.mapDomainAlgHom_id {G : Type u₂} [Monoid G] (k : Type u_4) (A : Type u_5) [CommSemiring k] [Semiring A] [Algebra k A] : MonoidAlgebra.mapDomainAlgHom k A (MonoidHom.id G) = AlgHom.id k (MonoidAlgebra A G)

@[simp]

theorem MonoidAlgebra.mapDomainAlgHom_comp (k : Type u_4) (A : Type u_5) {G₁ : Type u_6} {G₂ : Type u_7} {G₃ : Type u_8} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G₁] [Monoid G₂] [Monoid G₃] (f : G₁ →* G₂) (g : G₂ →* G₃) : MonoidAlgebra.mapDomainAlgHom k A (g.comp f) = (MonoidAlgebra.mapDomainAlgHom k A g).comp (MonoidAlgebra.mapDomainAlgHom k A f)

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

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

Equations

• MonoidAlgebra.domCongr k A e = AlgEquiv.ofLinearEquiv (Finsupp.domLCongr ↑e) ⋯ ⋯

theorem MonoidAlgebra.domCongr_toAlgHom (k : Type u₁) {G : Type u₂} {H : Type u_1} [CommSemiring k] [Monoid G] [Monoid H] (A : Type u₃) [Semiring A] [Algebra k A] (e : G ≃* H) : ↑(MonoidAlgebra.domCongr k A e) = MonoidAlgebra.mapDomainAlgHom k A e

@[simp]

theorem MonoidAlgebra.domCongr_apply (k : Type u₁) {G : Type u₂} {H : Type u_1} [CommSemiring k] [Monoid G] [Monoid H] (A : Type u₃) [Semiring A] [Algebra k A] (e : G ≃* H) (f : MonoidAlgebra A G) (h : H) : ((MonoidAlgebra.domCongr k A e) f) h = f (e.symm h)

@[simp]

theorem MonoidAlgebra.domCongr_support (k : Type u₁) {G : Type u₂} {H : Type u_1} [CommSemiring k] [Monoid G] [Monoid H] (A : Type u₃) [Semiring A] [Algebra k A] (e : G ≃* H) (f : MonoidAlgebra A G) : ((MonoidAlgebra.domCongr k A e) f).support = Finset.map (↑e).toEmbedding f.support

@[simp]

theorem MonoidAlgebra.domCongr_single (k : Type u₁) {G : Type u₂} {H : Type u_1} [CommSemiring k] [Monoid G] [Monoid H] (A : Type u₃) [Semiring A] [Algebra k A] (e : G ≃* H) (g : G) (a : A) : (MonoidAlgebra.domCongr k A e) (MonoidAlgebra.single g a) = MonoidAlgebra.single (e g) a

@[simp]

theorem MonoidAlgebra.domCongr_refl (k : Type u₁) {G : Type u₂} [CommSemiring k] [Monoid G] (A : Type u₃) [Semiring A] [Algebra k A] : MonoidAlgebra.domCongr k A (MulEquiv.refl G) = AlgEquiv.refl

@[simp]

theorem MonoidAlgebra.domCongr_symm (k : Type u₁) {G : Type u₂} {H : Type u_1} [CommSemiring k] [Monoid G] [Monoid H] (A : Type u₃) [Semiring A] [Algebra k A] (e : G ≃* H) : (MonoidAlgebra.domCongr k A e).symm = MonoidAlgebra.domCongr k A e.symm

def MonoidAlgebra.GroupSMul.linearMap (k : Type u₁) {G : Type u₂} [Monoid G] [CommSemiring k] (V : Type u₃) [AddCommMonoid V] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] (g : G) : V →ₗ[k] V

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

Equations

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

@[simp]

theorem MonoidAlgebra.GroupSMul.linearMap_apply (k : Type u₁) {G : Type u₂} [Monoid G] [CommSemiring k] (V : Type u₃) [AddCommMonoid V] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] (g : G) (v : V) : (MonoidAlgebra.GroupSMul.linearMap k V g) v = MonoidAlgebra.single g 1 • v

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

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

Equations

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

@[simp]

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

Non-unital, non-associative algebra structure

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

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

theorem AddMonoidAlgebra.nonUnitalAlgHom_ext' (k : Type u₁) {G : Type u₂} [Semiring k] [Add G] {A : Type u₃} [NonUnitalNonAssocSemiring A] [DistribMulAction k A] {φ₁ φ₂ : AddMonoidAlgebra k G →ₙₐ[k] A} (h : φ₁.toMulHom.comp (AddMonoidAlgebra.ofMagma k G) = φ₂.toMulHom.comp (AddMonoidAlgebra.ofMagma k G)) : φ₁ = φ₂

See note [partially-applied ext lemmas].

def AddMonoidAlgebra.liftMagma (k : Type u₁) {G : Type u₂} [Semiring k] [Add G] {A : Type u₃} [NonUnitalNonAssocSemiring A] [Module k A] [IsScalarTower k A A] [SMulCommClass k A A] : (Multiplicative G →ₙ* A) ≃ (AddMonoidAlgebra k G →ₙₐ[k] A)

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

Equations

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

@[simp]

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

@[simp]

theorem AddMonoidAlgebra.liftMagma_symm_apply (k : Type u₁) {G : Type u₂} [Semiring k] [Add G] {A : Type u₃} [NonUnitalNonAssocSemiring A] [Module k A] [IsScalarTower k A A] [SMulCommClass k A A] (F : AddMonoidAlgebra k G →ₙₐ[k] A) : (AddMonoidAlgebra.liftMagma k).symm F = F.toMulHom.comp (AddMonoidAlgebra.ofMagma k G)

Algebra structure

instance AddMonoidAlgebra.algebra {k : Type u₁} {G : Type u₂} {R : Type u_2} [CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] : Algebra R (AddMonoidAlgebra k G)

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

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

Equations

• AddMonoidAlgebra.algebra = Algebra.mk (AddMonoidAlgebra.singleZeroRingHom.comp (algebraMap R k)) ⋯ ⋯

def AddMonoidAlgebra.singleZeroAlgHom {k : Type u₁} {G : Type u₂} {R : Type u_2} [CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] : k →ₐ[R] AddMonoidAlgebra k G

Finsupp.single 0 as an AlgHom

Equations

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

@[simp]

theorem AddMonoidAlgebra.singleZeroAlgHom_apply {k : Type u₁} {G : Type u₂} {R : Type u_2} [CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] (a✝ : k) : AddMonoidAlgebra.singleZeroAlgHom a✝ = Finsupp.single 0 a✝

@[simp]

theorem AddMonoidAlgebra.coe_algebraMap {k : Type u₁} {G : Type u₂} {R : Type u_2} [CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] : ⇑(algebraMap R (AddMonoidAlgebra k G)) = AddMonoidAlgebra.single 0 ∘ ⇑(algebraMap R k)

def AddMonoidAlgebra.liftNCAlgHom {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] {B : Type u_3} [Semiring B] [Algebra k B] (f : A →ₐ[k] B) (g : Multiplicative G →* B) (h_comm : ∀ (x : A) (y : Multiplicative G), Commute (f x) (g y)) : AddMonoidAlgebra A G →ₐ[k] 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' := ⋯ }

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

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

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

See note [partially-applied ext lemmas].

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

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

Equations

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

theorem AddMonoidAlgebra.lift_apply' {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : Multiplicative G →* A) (f : MonoidAlgebra k G) : ((AddMonoidAlgebra.lift k G A) F) f = Finsupp.sum f fun (a : G) (b : k) => (algebraMap k A) b * F (Multiplicative.ofAdd a)

theorem AddMonoidAlgebra.lift_apply {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : Multiplicative G →* A) (f : MonoidAlgebra k G) : ((AddMonoidAlgebra.lift k G A) F) f = Finsupp.sum f fun (a : G) (b : k) => b • F (Multiplicative.ofAdd a)

theorem AddMonoidAlgebra.lift_def {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : Multiplicative G →* A) : ⇑((AddMonoidAlgebra.lift k G A) F) = ⇑(AddMonoidAlgebra.liftNC ↑(algebraMap k A) ⇑F)

@[simp]

theorem AddMonoidAlgebra.lift_symm_apply {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : AddMonoidAlgebra k G →ₐ[k] A) (x : Multiplicative G) : ((AddMonoidAlgebra.lift k G A).symm F) x = F (AddMonoidAlgebra.single (Multiplicative.toAdd x) 1)

theorem AddMonoidAlgebra.lift_of {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : Multiplicative G →* A) (x : Multiplicative G) : ((AddMonoidAlgebra.lift k G A) F) ((AddMonoidAlgebra.of k G) x) = F x

@[simp]

theorem AddMonoidAlgebra.lift_single {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : Multiplicative G →* A) (a : G) (b : k) : ((AddMonoidAlgebra.lift k G A) F) (AddMonoidAlgebra.single a b) = b • F (Multiplicative.ofAdd a)

theorem AddMonoidAlgebra.lift_of' {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : Multiplicative G →* A) (x : G) : ((AddMonoidAlgebra.lift k G A) F) (AddMonoidAlgebra.of' k G x) = F (Multiplicative.ofAdd x)

theorem AddMonoidAlgebra.lift_unique' {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : AddMonoidAlgebra k G →ₐ[k] A) : F = (AddMonoidAlgebra.lift k G A) ((↑F).comp (AddMonoidAlgebra.of k G))

theorem AddMonoidAlgebra.lift_unique {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] (F : AddMonoidAlgebra k G →ₐ[k] A) (f : MonoidAlgebra k G) : F f = Finsupp.sum f fun (a : G) (b : k) => b • F (AddMonoidAlgebra.single a 1)

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

theorem AddMonoidAlgebra.algHom_ext_iff {k : Type u₁} {G : Type u₂} [CommSemiring k] [AddMonoid G] {A : Type u₃} [Semiring A] [Algebra k A] {φ₁ φ₂ : AddMonoidAlgebra k G →ₐ[k] A} : (∀ (x : G), φ₁ (Finsupp.single x 1) = φ₂ (Finsupp.single x 1)) ↔ φ₁ = φ₂

theorem AddMonoidAlgebra.mapDomain_algebraMap {k : Type u₁} {G : Type u₂} (A : Type u_3) {H : Type u_4} {F : Type u_5} [CommSemiring k] [Semiring A] [Algebra k A] [AddMonoid G] [AddMonoid H] [FunLike F G H] [AddMonoidHomClass F G H] (f : F) (r : k) : AddMonoidAlgebra.mapDomain (⇑f) ((algebraMap k (AddMonoidAlgebra A G)) r) = (algebraMap k (AddMonoidAlgebra A H)) r

def AddMonoidAlgebra.mapDomainNonUnitalAlgHom (k : Type u_3) (A : Type u_4) [CommSemiring k] [Semiring A] [Algebra k A] {G : Type u_5} {H : Type u_6} {F : Type u_7} [Add G] [Add H] [FunLike F G H] [AddHomClass F G H] (f : F) : AddMonoidAlgebra A G →ₙₐ[k] AddMonoidAlgebra A H

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

Equations

• AddMonoidAlgebra.mapDomainNonUnitalAlgHom k A f = { toFun := (↑(Finsupp.mapDomain.addMonoidHom ⇑f)).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

@[simp]

theorem AddMonoidAlgebra.mapDomainNonUnitalAlgHom_apply (k : Type u_3) (A : Type u_4) [CommSemiring k] [Semiring A] [Algebra k A] {G : Type u_5} {H : Type u_6} {F : Type u_7} [Add G] [Add H] [FunLike F G H] [AddHomClass F G H] (f : F) (a✝ : G →₀ A) : (AddMonoidAlgebra.mapDomainNonUnitalAlgHom k A f) a✝ = (↑(Finsupp.mapDomain.addMonoidHom ⇑f)).toFun a✝

def AddMonoidAlgebra.mapDomainAlgHom {G : Type u₂} (k : Type u_3) (A : Type u_4) [CommSemiring k] [Semiring A] [Algebra k A] [AddMonoid G] {H : Type u_5} {F : Type u_6} [AddMonoid H] [FunLike F G H] [AddMonoidHomClass F G H] (f : F) : AddMonoidAlgebra A G →ₐ[k] AddMonoidAlgebra A H

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

Equations

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

@[simp]

theorem AddMonoidAlgebra.mapDomainAlgHom_apply {G : Type u₂} (k : Type u_3) (A : Type u_4) [CommSemiring k] [Semiring A] [Algebra k A] [AddMonoid G] {H : Type u_5} {F : Type u_6} [AddMonoid H] [FunLike F G H] [AddMonoidHomClass F G H] (f : F) (a✝ : G →₀ A) : (AddMonoidAlgebra.mapDomainAlgHom k A f) a✝ = Finsupp.mapDomain (⇑f) a✝

@[simp]

theorem AddMonoidAlgebra.mapDomainAlgHom_id {G : Type u₂} (k : Type u_3) (A : Type u_4) [CommSemiring k] [Semiring A] [Algebra k A] [AddMonoid G] : AddMonoidAlgebra.mapDomainAlgHom k A (AddMonoidHom.id G) = AlgHom.id k (AddMonoidAlgebra A G)

@[simp]

theorem AddMonoidAlgebra.mapDomainAlgHom_comp (k : Type u_3) (A : Type u_4) {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [CommSemiring k] [Semiring A] [Algebra k A] [AddMonoid G₁] [AddMonoid G₂] [AddMonoid G₃] (f : G₁ →+ G₂) (g : G₂ →+ G₃) : AddMonoidAlgebra.mapDomainAlgHom k A (g.comp f) = (AddMonoidAlgebra.mapDomainAlgHom k A g).comp (AddMonoidAlgebra.mapDomainAlgHom k A f)

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

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

Equations

• AddMonoidAlgebra.domCongr k A e = AlgEquiv.ofLinearEquiv (Finsupp.domLCongr ↑e) ⋯ ⋯

theorem AddMonoidAlgebra.domCongr_toAlgHom (k : Type u₁) {G : Type u₂} {H : Type u_1} (A : Type u_3) [CommSemiring k] [AddMonoid G] [AddMonoid H] [Semiring A] [Algebra k A] (e : G ≃+ H) : ↑(AddMonoidAlgebra.domCongr k A e) = AddMonoidAlgebra.mapDomainAlgHom k A e

@[simp]

theorem AddMonoidAlgebra.domCongr_apply (k : Type u₁) {G : Type u₂} {H : Type u_1} (A : Type u_3) [CommSemiring k] [AddMonoid G] [AddMonoid H] [Semiring A] [Algebra k A] (e : G ≃+ H) (f : MonoidAlgebra A G) (h : H) : ((AddMonoidAlgebra.domCongr k A e) f) h = f (e.symm h)

@[simp]

theorem AddMonoidAlgebra.domCongr_support (k : Type u₁) {G : Type u₂} {H : Type u_1} (A : Type u_3) [CommSemiring k] [AddMonoid G] [AddMonoid H] [Semiring A] [Algebra k A] (e : G ≃+ H) (f : MonoidAlgebra A G) : ((AddMonoidAlgebra.domCongr k A e) f).support = Finset.map (↑e).toEmbedding f.support

@[simp]

theorem AddMonoidAlgebra.domCongr_single (k : Type u₁) {G : Type u₂} {H : Type u_1} (A : Type u_3) [CommSemiring k] [AddMonoid G] [AddMonoid H] [Semiring A] [Algebra k A] (e : G ≃+ H) (g : G) (a : A) : (AddMonoidAlgebra.domCongr k A e) (AddMonoidAlgebra.single g a) = AddMonoidAlgebra.single (e g) a

@[simp]

theorem AddMonoidAlgebra.domCongr_refl (k : Type u₁) {G : Type u₂} (A : Type u_3) [CommSemiring k] [AddMonoid G] [Semiring A] [Algebra k A] : AddMonoidAlgebra.domCongr k A (AddEquiv.refl G) = AlgEquiv.refl

@[simp]

theorem AddMonoidAlgebra.domCongr_symm (k : Type u₁) {G : Type u₂} {H : Type u_1} (A : Type u_3) [CommSemiring k] [AddMonoid G] [AddMonoid H] [Semiring A] [Algebra k A] (e : G ≃+ H) : (AddMonoidAlgebra.domCongr k A e).symm = AddMonoidAlgebra.domCongr k A e.symm

def AddMonoidAlgebra.toMultiplicativeAlgEquiv (k : Type u₁) (G : Type u₂) {R : Type u_2} [CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] : AddMonoidAlgebra k G ≃ₐ[R] MonoidAlgebra k (Multiplicative G)

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

Equations

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

def MonoidAlgebra.toAdditiveAlgEquiv (k : Type u₁) (G : Type u₂) {R : Type u_2} [CommSemiring R] [Semiring k] [Algebra R k] [Monoid G] : MonoidAlgebra k G ≃ₐ[R] AddMonoidAlgebra k (Additive G)

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

Equations

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