Documentation

Mathlib.Algebra.MonoidAlgebra.Opposite

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
    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
        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))