Documentation

Mathlib.Algebra.MonoidAlgebra.Opposite

Monoid algebras and the opposite ring #

source
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
  • One or more equations did not get rendered due to their size.
Instances For
    source
    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
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem AddMonoidAlgebra.opRingEquiv_apply {R : Type u_1} {M : Type u_2} [Semiring R] [Add M] (a✝ : (AddMonoidAlgebra R M)ᵐᵒᵖ) :
      AddMonoidAlgebra.opRingEquiv a✝ = (mapAddEquiv Mᵃᵒᵖ MulOpposite.opAddEquiv) ((mapDomainAddEquiv R AddOpposite.opEquiv) (MulOpposite.unop a✝))
      source
      @[simp]
      theorem MonoidAlgebra.opRingEquiv_apply {R : Type u_1} {M : Type u_2} [Semiring R] [Mul M] (a✝ : (MonoidAlgebra R M)ᵐᵒᵖ) :
      MonoidAlgebra.opRingEquiv a✝ = (mapAddEquiv Mᵐᵒᵖ MulOpposite.opAddEquiv) ((mapDomainAddEquiv R MulOpposite.opEquiv) (MulOpposite.unop a✝))
      source
      @[simp]
      theorem AddMonoidAlgebra.opRingEquiv_symm_apply {R : Type u_1} {M : Type u_2} [Semiring R] [Add M] (a✝ : AddMonoidAlgebra Rᵐᵒᵖ Mᵃᵒᵖ) :
      AddMonoidAlgebra.opRingEquiv.symm a✝ = MulOpposite.op ((mapDomainAddEquiv R AddOpposite.opEquiv.symm) ((mapAddEquiv Mᵃᵒᵖ MulOpposite.opAddEquiv.symm) a✝))
      source
      @[simp]
      theorem MonoidAlgebra.opRingEquiv_symm_apply {R : Type u_1} {M : Type u_2} [Semiring R] [Mul M] (a✝ : MonoidAlgebra Rᵐᵒᵖ Mᵐᵒᵖ) :
      MonoidAlgebra.opRingEquiv.symm a✝ = MulOpposite.op ((mapDomainAddEquiv R MulOpposite.opEquiv.symm) ((mapAddEquiv Mᵐᵒᵖ MulOpposite.opAddEquiv.symm) a✝))
      source
      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
      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
      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
      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))