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

ink

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

multiplication by a monomial

Equations

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

ink

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

multiplication for formal sums

Equations

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

Properties of multiplication on formal sums

ink

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

multiplication by the zero monomial

ink

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

distributivity of multiplication by a monomial

ink

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

right distributivity

ink

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

associativity with two terms monomials

ink

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

associativity with one term a monomial

ink

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

left distributivity for multiplication by a monomial

ink

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

multiplication equivalent when adding term with 0 coefficient

Induced product on the quotient

ink

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

Quotient in second argument for group ring multiplication

Equations

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

ink

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

invariance under moves of multiplication by monomials

ink

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

invariance under moves for the first argument for multipilication

ink

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

multiplication for free modules

Equations

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

The Ring Structure

ink

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

Equations

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

ink

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

Equations

• GroupRing.instOneFreeModule = { one := Quotient.mk (formalSumSetoid R G) [(1, 1)] }

ink

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

Equations

• GroupRing.instAddCommGroupFreeModule = AddCommGroup.mk (_ : ∀ (x₁ x₂ : R[G]), x₁ + x₂ = x₂ + x₁)

ink

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

The group ring is a ring

Equations

• GroupRing.instRingFreeModule = Ring.mk zsmulRec (_ : ∀ (x : R[G]), -1 • x + x = Quotient.mk (formalSumSetoid R G) [])