Documentation

Mathlib.Algebra.MonoidAlgebra.Opposite

Monoid algebras and the opposite ring #

source
🔸 coverage
noncomputable def MonoidAlgebra.opRingEquiv {R : Type u_1} {M : Type u_2} [Semiring R] [Mul M] :
(MonoidAlgebra R M)ᵐᵒᵖ ≃+* MonoidAlgebra Rᵐᵒᵖ Mᵐᵒᵖ

The opposite of a monoid algebra is equivalent as a ring to the opposite monoid algebra over the opposite ring.

Equations
    Instances For
      source
      🔸 coverage
      noncomputable def AddMonoidAlgebra.opRingEquiv {R : Type u_1} {M : Type u_2} [Semiring R] [Add M] :
      (AddMonoidAlgebra R M)ᵐᵒᵖ ≃+* AddMonoidAlgebra Rᵐᵒᵖ Mᵃᵒᵖ

      The opposite of a monoid algebra is equivalent as a ring to the opposite monoid algebra over the opposite ring.

      Equations
        Instances For
          source
          📐 coverage
          @[simp]
          theorem AddMonoidAlgebra.opRingEquiv_symm_apply {R : Type u_1} {M : Type u_2} [Semiring R] [Add M] (a✝ : Mᵃᵒᵖ →₀ Rᵐᵒᵖ) :
          AddMonoidAlgebra.opRingEquiv.symm a✝ = MulOpposite.op (Finsupp.mapRange MulOpposite.unop ⋯ (Finsupp.equivMapDomain AddOpposite.opEquiv.symm a✝))
          source
          📐 coverage
          @[simp]
          theorem MonoidAlgebra.opRingEquiv_symm_apply {R : Type u_1} {M : Type u_2} [Semiring R] [Mul M] (a✝ : Mᵐᵒᵖ →₀ Rᵐᵒᵖ) :
          MonoidAlgebra.opRingEquiv.symm a✝ = MulOpposite.op (Finsupp.mapRange MulOpposite.unop ⋯ (Finsupp.equivMapDomain MulOpposite.opEquiv.symm a✝))
          source
          📐 coverage
          @[simp]
          theorem AddMonoidAlgebra.opRingEquiv_apply {R : Type u_1} {M : Type u_2} [Semiring R] [Add M] (a✝ : (M →₀ R)ᵐᵒᵖ) :
          AddMonoidAlgebra.opRingEquiv a✝ = Finsupp.equivMapDomain AddOpposite.opEquiv (Finsupp.mapRange MulOpposite.op ⋯ (MulOpposite.unop a✝))
          source
          📐 coverage
          @[simp]
          theorem MonoidAlgebra.opRingEquiv_apply {R : Type u_1} {M : Type u_2} [Semiring R] [Mul M] (a✝ : (M →₀ R)ᵐᵒᵖ) :
          MonoidAlgebra.opRingEquiv a✝ = Finsupp.equivMapDomain MulOpposite.opEquiv (Finsupp.mapRange MulOpposite.op ⋯ (MulOpposite.unop a✝))
          source
          📐 coverage
          theorem MonoidAlgebra.opRingEquiv_single {R : Type u_1} {M : Type u_2} [Semiring R] [Mul M] (r : R) (x : M) :
          MonoidAlgebra.opRingEquiv (MulOpposite.op (single x r)) = single (MulOpposite.op x) (MulOpposite.op r)
          source
          📐 coverage
          theorem AddMonoidAlgebra.opRingEquiv_single {R : Type u_1} {M : Type u_2} [Semiring R] [Add M] (r : R) (x : M) :
          AddMonoidAlgebra.opRingEquiv (MulOpposite.op (single x r)) = single (AddOpposite.op x) (MulOpposite.op r)
          source
          📐 coverage
          theorem MonoidAlgebra.opRingEquiv_symm_single {R : Type u_1} {M : Type u_2} [Semiring R] [Mul M] (r : Rᵐᵒᵖ) (x : Mᵐᵒᵖ) :
          MonoidAlgebra.opRingEquiv.symm (single x r) = MulOpposite.op (single (MulOpposite.unop x) (MulOpposite.unop r))
          source
          📐 coverage
          theorem AddMonoidAlgebra.opRingEquiv_symm_single {R : Type u_1} {M : Type u_2} [Semiring R] [Add M] (r : Rᵐᵒᵖ) (x : Mᵃᵒᵖ) :
          AddMonoidAlgebra.opRingEquiv.symm (single x r) = MulOpposite.op (single (AddOpposite.unop x) (MulOpposite.unop r))