Monoid algebras and the opposite ring

Multiplicative monoids

noncomputable def MonoidAlgebra.opRingEquiv {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] : (MonoidAlgebra k G)ᵐᵒᵖ ≃+* MonoidAlgebra kᵐᵒᵖ Gᵐᵒᵖ

The opposite of a MonoidAlgebra R I equivalent as a ring to the MonoidAlgebra Rᵐᵒᵖ Iᵐᵒᵖ over the opposite ring, taking elements to their opposite.

Equations

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

@[simp]

theorem MonoidAlgebra.opRingEquiv_apply {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] (a✝ : (G →₀ k)ᵐᵒᵖ) : MonoidAlgebra.opRingEquiv a✝ = Finsupp.equivMapDomain MulOpposite.opEquiv (Finsupp.mapRange MulOpposite.op ⋯ (MulOpposite.unop a✝))

@[simp]

theorem MonoidAlgebra.opRingEquiv_symm_apply {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] (a✝ : Gᵐᵒᵖ →₀ kᵐᵒᵖ) : MonoidAlgebra.opRingEquiv.symm a✝ = MulOpposite.op (Finsupp.mapRange MulOpposite.unop ⋯ (Finsupp.equivMapDomain MulOpposite.opEquiv.symm a✝))

theorem MonoidAlgebra.opRingEquiv_single {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] (r : k) (x : G) : MonoidAlgebra.opRingEquiv (MulOpposite.op (single x r)) = single (MulOpposite.op x) (MulOpposite.op r)

theorem MonoidAlgebra.opRingEquiv_symm_single {k : Type u₁} {G : Type u₂} [Semiring k] [Mul G] (r : kᵐᵒᵖ) (x : Gᵐᵒᵖ) : MonoidAlgebra.opRingEquiv.symm (single x r) = MulOpposite.op (single (MulOpposite.unop x) (MulOpposite.unop r))

Additive monoids

noncomputable def AddMonoidAlgebra.opRingEquiv {k : Type u₁} {G : Type u₂} [Semiring k] [AddCommMagma G] : (AddMonoidAlgebra k G)ᵐᵒᵖ ≃+* AddMonoidAlgebra kᵐᵒᵖ G

The opposite of an R[I] is ring equivalent to the AddMonoidAlgebra Rᵐᵒᵖ I over the opposite ring, taking elements to their opposite.

Equations

• AddMonoidAlgebra.opRingEquiv = { toEquiv := (MulOpposite.opAddEquiv.symm.trans (Finsupp.mapRange.addEquiv MulOpposite.opAddEquiv)).toEquiv, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

theorem AddMonoidAlgebra.opRingEquiv_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddCommMagma G] (a✝ : (G →₀ k)ᵐᵒᵖ) : AddMonoidAlgebra.opRingEquiv a✝ = Finsupp.mapRange MulOpposite.op ⋯ (MulOpposite.unop a✝)

@[simp]

theorem AddMonoidAlgebra.opRingEquiv_symm_apply {k : Type u₁} {G : Type u₂} [Semiring k] [AddCommMagma G] (a✝ : G →₀ kᵐᵒᵖ) : AddMonoidAlgebra.opRingEquiv.symm a✝ = MulOpposite.op (Finsupp.mapRange MulOpposite.unop ⋯ a✝)

theorem AddMonoidAlgebra.opRingEquiv_single {k : Type u₁} {G : Type u₂} [Semiring k] [AddCommMagma G] (r : k) (x : G) : AddMonoidAlgebra.opRingEquiv (MulOpposite.op (single x r)) = single x (MulOpposite.op r)

theorem AddMonoidAlgebra.opRingEquiv_symm_single {k : Type u₁} {G : Type u₂} [Semiring k] [AddCommMagma G] (r : kᵐᵒᵖ) (x : Gᵐᵒᵖ) : AddMonoidAlgebra.opRingEquiv.symm (single x r) = MulOpposite.op (single x (MulOpposite.unop r))