Inversion on commutative group rings

7 fully proved

Group Ring

DefinitionInversion on a group ring#✓fully proved

Let \(R\) be a commutative ring and \(G\) a commutative group. The inversion of the group ring \(R[G]\) is the ring automorphism of \(R[G]\) induced by the group automorphism \(g \mapsto g^{-1}\) of \(G\): it sends \(\sum_g r_g\, g\) to \(\sum_g r_g\, g^{-1}\).

def inversion : MonoidAlgebra R G ≃+* MonoidAlgebra R G :=
  MonoidAlgebra.mapDomainRingEquiv R (MulEquiv.inv G)

Used by 4

Used byGroup-ring inversion is an involution · Inversion on basis elements · Twisting twice by inversion recovers the module · Scalar action on the inversion twist

TheoremInversion on basis elements#✓fully proved

Let \(R\) be a commutative ring and \(G\) a commutative group. For every \(g \in G\) and \(r \in R\), the inversion of the group ring \(R[G]\) sends \(r\, g\) to \(r\, g^{-1}\).

@[simp]
theorem inversion_single (g : G) (r : R) :
    inversion R G (MonoidAlgebra.single g r) = MonoidAlgebra.single g⁻¹ r

Uses 1

Statement usesInversion on a group ring

TheoremGroup-ring inversion is an involution#✓fully proved

Let \(R\) be a commutative ring, \(G\) a commutative group and \(\iota\) the inversion of the group ring \(R[G]\). For every \(x \in R[G]\), \(\iota(\iota(x)) = x\).

@[simp]
theorem inversion_involution (x : MonoidAlgebra R G) : inversion R G (inversion R G x) = x

Uses 1 · Used by 1

Statement usesInversion on a group ring

Used byTwisting twice by inversion recovers the module

StructureInversion twist of a group-ring module#✓fully proved

Let \(R\) be a commutative ring, \(G\) a commutative group and \(A\) a module over the group ring \(R[G]\). The inversion twist of \(A\) is a copy of \(A\) with the same addition, on which \(r \in R[G]\) acts by \(a \mapsto \iota(r) \cdot a\), where \(\iota\) is the inversion of \(R[G]\) and \(\cdot\) is the original action on \(A\).

As a bare type, the inversion twist of any type \(A\) is a copy of \(A\); the addition and the action above are defined when \(A\) is an \(R[G]\)-module.

@[ext]
structure InversionTwist (A : Type*) where
  of ::
  val : A

Used by 3

Used byUnderlying bijection of the inversion twist · Twisting twice by inversion recovers the module · Scalar action on the inversion twist

Inversion Twist

DefinitionUnderlying bijection of the inversion twist#✓fully proved

For every type \(A\), the map sending an element of the inversion twist of \(A\) to its underlying element of \(A\) is a bijection, whose inverse sends \(a \in A\) to its copy in the twist.

def equiv (A : Type*) : InversionTwist A ≃ A where
  toFun := val
  invFun := of
  left_inv _ := rfl
  right_inv _ := rfl

Uses 1 · Used by 1

Statement usesInversion twist of a group-ring module

Used byTwisting twice by inversion recovers the module

TheoremScalar action on the inversion twist#✓fully proved

Let \(R\) be a commutative ring, \(G\) a commutative group and \(A\) a module over the group ring \(R[G]\). For every \(r \in R[G]\) and every element \(a\) of the inversion twist of \(A\), with underlying element \(\bar a \in A\), the underlying element of \(r \cdot a\) is \(\iota(r) \cdot \bar a\), where \(\iota\) is the inversion of \(R[G]\) and \(\cdot\) on the right is the original action on \(A\).

@[simp]
theorem val_smul (r : MonoidAlgebra R G) (a : InversionTwist A) :
    (r • a).val = inversion R G r • a.val

Uses 2

Statement usesInversion twist of a group-ring module · Inversion on a group ring

DefinitionTwisting twice by inversion recovers the module#✓fully proved

Let \(R\) be a commutative ring, \(G\) a commutative group and \(A\) a module over the group ring \(R[G]\). The map sending an element of the inversion twist of the inversion twist of \(A\) to its underlying element of \(A\) is an \(R[G]\)-linear isomorphism.

def twistTwistEquiv : InversionTwist (InversionTwist A) ≃ₗ[MonoidAlgebra R G] A where
  toFun a := a.val.val
  invFun a := of (of a)
  left_inv _ := rfl
  right_inv _ := rfl
  map_add' _ _ := rfl
  map_smul' r a := by
    change inversion R G (inversion R G r) • a.val.val = r • a.val.val
    rw [inversion_involution]

Uses 4

Statement usesInversion twist of a group-ring module · Underlying bijection of the inversion twist · Inversion on a group ring · Group-ring inversion is an involution

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.