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.

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.

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