# Monoid algebras and the opposite ring #

### Multiplicative monoids #

source
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.

Instances For

source
@[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✝))
source
@[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✝))
source
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)
source
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 #

source
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' := ⋯ }

Instances For

source
@[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✝)
source
@[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✝)
source
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)
source
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))