Basic facts about monoid algebras

General facts about the monoid algebra R[G] that use only its basis elements single g r, and none of the further theory built on it.

Main results

• TauCeti.single_sub_one_ne_zero: over a nontrivial ring, the difference single g 1 - 1 between the basis element at g and the unit is nonzero when g ≠ 1.
• MonoidAlgebra.coeff_one_mul_comm: the coefficient at the identity of xy equals that of yx in a group algebra over a commutative semiring.
• The IsMulCommutative (MonoidAlgebra R M) instance: the monoid algebra of a commutative magma over a commutative semiring is commutative, as a mixin on the existing ring structure.
• TauCeti.MonoidAlgebra.mem_ideal_smul_top_iff: an element of R[M] lies in I • R[M] exactly when its coefficients lie in I, and TauCeti.MonoidAlgebra.mapRingHom_eq_zero_iff: the kernel of the coefficientwise map along f : R →+* S is ker f • R[M].

References

Injectivity of single in its index is Mathlib's MonoidAlgebra.single_left_injective.

instance TauCeti.instIsMulCommutativeMonoidAlgebra {R : Type u_1} [CommSemiring R] {M : Type u_2} [Mul M] [IsMulCommutative M] : IsMulCommutative (MonoidAlgebra R M)

The monoid algebra of a commutative magma over a commutative semiring is commutative. This is the mixin form of Mathlib's MonoidAlgebra.nonUnitalCommSemiring, for a multiplication that is commutative without carrying a CommSemigroup instance.

theorem MonoidAlgebra.exists_eq_nsmul_of_dvd_coeff {R : Type u_1} [Semiring R] {M : Type u_2} {n : ℕ} {x : MonoidAlgebra R M} (h : ∀ (m : M), ↑n ∣ x.coeff m) : ∃ (y : MonoidAlgebra R M), x = n • y

An element of R[M] all of whose coefficients are divisible by n is n times an element.

theorem TauCeti.single_sub_one_ne_zero {R : Type u_1} [Ring R] {G : Type u_2} [One G] [Nontrivial R] {g : G} (hg : g ≠ 1) : MonoidAlgebra.single g 1 - 1 ≠ 0

Over a nontrivial ring, the difference single g 1 - 1 between the basis element at g and the unit is nonzero when g ≠ 1.

@[simp]

theorem TauCeti.MonoidAlgebra.mem_ideal_smul_top_iff {R : Type u_3} [CommSemiring R] {M : Type u_4} {I : Ideal R} {x : MonoidAlgebra R M} : x ∈ I • ⊤ ↔ ∀ (m : M), x.coeff m ∈ I

An element of R[M] lies in I • R[M] exactly when all of its coefficients lie in I.

@[simp]

theorem TauCeti.MonoidAlgebra.mapRingHom_eq_zero_iff {R : Type u_3} [CommSemiring R] {M : Type u_4} [Monoid M] {S : Type u_5} [Semiring S] (f : R →+* S) {x : MonoidAlgebra R M} : (MonoidAlgebra.mapRingHom M f) x = 0 ↔ x ∈ RingHom.ker f • ⊤

Applying a ring homomorphism f to the coefficients kills exactly ker f • R[M].

theorem MonoidAlgebra.coeff_one_mul_comm {R : Type u_1} [CommSemiring R] {G : Type u_2} [Group G] (x y : MonoidAlgebra R G) : (x * y).coeff 1 = (y * x).coeff 1

The coefficient at the identity is symmetric under swapping the factors in a group algebra over a commutative semiring.