Group Rings

We construct the Group ring R[G] given a group G and a ring R, both having decidable equality. The ring structures is constructed using the (implicit) universal property of R-modules. As a check on our definitions, R[G] is proved to be a Ring.

We first define multiplication on formal sums. We prove many properties that are used both to show invariance under elementary moves and to prove that R[G] is a ring.

Multiplication on formal sums

def LeanPool.Polylean.FormalSum.mulMonom {R : Type} [Ring R] {G : Type} [Group G] (b : R) (h : G) : FormalSum R G → FormalSum R G

multiplication by a monomial

Equations

• LeanPool.Polylean.FormalSum.mulMonom b h [] = []
• LeanPool.Polylean.FormalSum.mulMonom b h ((a, g) :: tail) = (a * b, g * h) :: LeanPool.Polylean.FormalSum.mulMonom b h tail

def LeanPool.Polylean.FormalSum.mul {R : Type} [Ring R] {G : Type} [Group G] (fst : FormalSum R G) : FormalSum R G → FormalSum R G

multiplication for formal sums

Equations

• fst.mul [] = []
• fst.mul ((a, g) :: tail) = LeanPool.Polylean.FormalSum.mulMonom a g fst ++ fst.mul tail

Properties of multiplication on formal sums

theorem LeanPool.Polylean.GroupRing.mul_monom_zero {R : Type} [Ring R] {G : Type} [Group G] [DecidableEq G] (g x₀ : G) (s : FormalSum R G) : (FormalSum.mulMonom 0 g s).coords x₀ = 0

theorem LeanPool.Polylean.GroupRing.mul_monom_dist {R : Type} [Ring R] {G : Type} [Group G] [DecidableEq G] (b : R) (h x₀ : G) (s₁ s₂ : FormalSum R G) : (FormalSum.mulMonom b h (s₁ ++ s₂)).coords x₀ = (FormalSum.mulMonom b h s₁).coords x₀ + (FormalSum.mulMonom b h s₂).coords x₀

theorem LeanPool.Polylean.GroupRing.mul_dist {R : Type} [Ring R] {G : Type} [Group G] [DecidableEq G] (x₀ : G) (s₁ s₂ s₃ : FormalSum R G) : (s₁.mul (s₂ ++ s₃)).coords x₀ = (s₁.mul s₂).coords x₀ + (s₁.mul s₃).coords x₀

theorem LeanPool.Polylean.GroupRing.mul_monom_monom_assoc {R : Type} [Ring R] {G : Type} [Group G] [DecidableEq G] {x : G} (a b : R) (h x₀ : G) (s : FormalSum R G) : (FormalSum.mulMonom b h (FormalSum.mulMonom a x s)).coords x₀ = (FormalSum.mulMonom (a * b) (x * h) s).coords x₀

theorem LeanPool.Polylean.GroupRing.mul_monom_assoc {R : Type} [Ring R] {G : Type} [Group G] [DecidableEq G] (b : R) (h x₀ : G) (s₁ s₂ : FormalSum R G) : (FormalSum.mulMonom b h (s₁.mul s₂)).coords x₀ = (s₁.mul (FormalSum.mulMonom b h s₂)).coords x₀

theorem LeanPool.Polylean.GroupRing.mul_monom_add {R : Type} [Ring R] {G : Type} [Group G] [DecidableEq G] (b₁ b₂ : R) (h x₀ : G) (s : FormalSum R G) : (FormalSum.mulMonom (b₁ + b₂) h s).coords x₀ = (FormalSum.mulMonom b₁ h s).coords x₀ + (FormalSum.mulMonom b₂ h s).coords x₀

theorem LeanPool.Polylean.GroupRing.mul_zero_cons {R : Type} [Ring R] [DecidableEq R] {G : Type} [Group G] [DecidableEq G] {h : G} (s t : FormalSum R G) : s.mul ((0, h) :: t) ≈ s.mul t

multiplication equivalent when adding term with 0 coefficient

Induced product on the quotient

def LeanPool.Polylean.GroupRing.mulAux {R : Type} [Ring R] [DecidableEq R] {G : Type} [Group G] [DecidableEq G] : FormalSum R G → R[G] → R[G]

Quotient in second argument for group ring multiplication

Equations

• LeanPool.Polylean.GroupRing.mulAux s = Quotient.lift (fun (x : LeanPool.Polylean.FormalSum R G) => ⟦s.mul x⟧) ⋯

theorem LeanPool.Polylean.GroupRing.mul_monom_invariant {R : Type} [Ring R] [DecidableEq R] {G : Type} [Group G] [DecidableEq G] (b : R) (h x₀ : G) (s₁ s₂ : FormalSum R G) (rel : ElementaryMove R G s₁ s₂) : (FormalSum.mulMonom b h s₁).coords x₀ = (FormalSum.mulMonom b h s₂).coords x₀

invariance under moves of multiplication by monomials

theorem LeanPool.Polylean.GroupRing.first_arg_invariant {R : Type} [Ring R] [DecidableEq R] {G : Type} [Group G] [DecidableEq G] (s₁ s₂ t : FormalSum R G) (rel : ElementaryMove R G s₁ s₂) : s₁.mul t ≈ s₂.mul t

invariance under moves for the first argument for multipilication

theorem LeanPool.Polylean.GroupRing.first_arg_invariant_nil {R : Type} [Ring R] [DecidableEq R] {G : Type} [Group G] [DecidableEq G] (s₁ s₂ : FormalSum R G) (rel : ElementaryMove R G s₁ s₂) : s₁.mul [] ≈ s₂.mul []

The empty right factor is preserved by elementary moves in the first factor.

def LeanPool.Polylean.GroupRing.mul {R : Type} [Ring R] [DecidableEq R] {G : Type} [Group G] [DecidableEq G] : R[G] → R[G] → R[G]

multiplication for free modules

Equations

• LeanPool.Polylean.GroupRing.mul = Quotient.lift (fun (s : LeanPool.Polylean.FormalSum R G) (t : R[G]) => LeanPool.Polylean.GroupRing.mulAux s t) ⋯

The Ring Structure

@[implicit_reducible]

instance LeanPool.Polylean.GroupRing.groupRingMul {R : Type} [Ring R] [DecidableEq R] {G : Type} [Group G] [DecidableEq G] : Mul (R[G])

Equations

• LeanPool.Polylean.GroupRing.groupRingMul = { mul := LeanPool.Polylean.GroupRing.mul }

@[implicit_reducible]

instance LeanPool.Polylean.GroupRing.instOneFreeModule {R : Type} [Ring R] [DecidableEq R] {G : Type} [Group G] [DecidableEq G] : One (R[G])

Equations

• LeanPool.Polylean.GroupRing.instOneFreeModule = { one := ⟦[(1, 1)]⟧ }

@[implicit_reducible]

instance LeanPool.Polylean.GroupRing.instAddCommGroupFreeModule {R : Type} [Ring R] [DecidableEq R] {G : Type} [DecidableEq G] : AddCommGroup (R[G])

Equations

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

@[implicit_reducible]

instance LeanPool.Polylean.GroupRing.instRingFreeModule {R : Type} [Ring R] [DecidableEq R] {G : Type} [Group G] [DecidableEq G] : Ring (R[G])

The group ring is a ring

Equations

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

Inclusions of the group and ring into the group ring

@[implicit_reducible]

instance LeanPool.Polylean.groupRingMul {R G : Type} [Ring R] [DecidableEq G] [DecidableEq R] : HMul R G (R[G])

Product R → G → R[G], r ↦ g ↦ r ⬝ g; used only in verification results.

Equations

• LeanPool.Polylean.groupRingMul = { hMul := fun (r : R) (g : G) => ⟦[(r, g)]⟧ }

theorem LeanPool.Polylean.groupRingMul_apply {R G : Type} [Ring R] [DecidableEq G] [DecidableEq R] (r : R) (g : G) : r * g = ⟦[(r, g)]⟧

Scalar multiplication by a group element is represented by the singleton formal sum.

def LeanPool.Polylean.groupInclusionHom {R : Type} [Ring R] [DecidableEq R] (G : Type) [Group G] [DecidableEq G] : G →* R[G]

Monoid homomorphism from G to R[G] given by g ↦ 1 ⬝ g

Equations

• LeanPool.Polylean.groupInclusionHom G = { toFun := LeanPool.Polylean.baseInclusion 1, map_one' := ⋯, map_mul' := ⋯ }

theorem LeanPool.Polylean.groupInclusionHom_formula {R : Type} [Ring R] [DecidableEq R] (G : Type) [Group G] [DecidableEq G] : (↑(groupInclusionHom G)).toFun = fun (g : G) => 1 * g

As a function groupInclusionHom is g ↦ 1 ⬝ g

theorem LeanPool.Polylean.groupInclusionHom_injective' {R : Type} [Ring R] [DecidableEq R] {G : Type} [Group G] [DecidableEq G] (hR : 1 ≠ 0) : Function.Injective ⇑(groupInclusionHom G)

The monoid homomorphism G → R[G], g ↦ 1 ⬝ g is injective if 1 ≠ 0 in R.

theorem LeanPool.Polylean.groupInclusionHom_injective {F : Type} [Field F] [DecidableEq F] (G : Type) [Group G] [DecidableEq G] : Function.Injective ⇑(groupInclusionHom G)

For a field F the monoid homomorphism G → F[G], g ↦ 1 ⬝ g is injective.

def LeanPool.Polylean.ringInclusionHom {R : Type} [Ring R] [DecidableEq R] (G : Type) [Group G] [DecidableEq G] : R →+* R[G]

The ring homomorphism R → R[G] given by a ↦ a ⬝ 1

Equations

• LeanPool.Polylean.ringInclusionHom G = { toFun := LeanPool.Polylean.coeffInclusion 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem LeanPool.Polylean.ringInclusionHom_formula {R : Type} [Ring R] [DecidableEq R] (G : Type) [Group G] [DecidableEq G] : (↑↑(ringInclusionHom G)).toFun = fun (r : R) => r * 1

As a function, ringInclusionHom is r ↦ r ⬝ 1

theorem LeanPool.Polylean.ringInclusionHom_injective' {R : Type} [Ring R] [DecidableEq R] (G : Type) [Group G] [DecidableEq G] : Function.Injective ⇑(ringInclusionHom G)

The ring homomorphism R → R[G] given by a ↦ a ⬝ 1 is injective