Mathlib.Algebra.Algebra.Opposite

MulOpposite.instAlgebra instance

: Algebra R Aᵐᵒᵖ

Full source

instance instAlgebra : Algebra R Aᵐᵒᵖ where
  algebraMap := (algebraMap R A).toOpposite fun _ _ => Algebra.commutes _ _
  smul_def' c x := unop_injective <| by
    simp only [unop_smul, RingHom.toOpposite_apply, Function.comp_apply, unop_mul, op_mul,
      Algebra.smul_def, Algebra.commutes, op_unop, unop_op]
  commutes' r := MulOpposite.rec' fun x => by
    simp only [RingHom.toOpposite_apply, Function.comp_apply, ← op_mul, Algebra.commutes]

Algebra Structure on the Multiplicative Opposite

Informal description

For any commutative semiring $R$ and semiring $A$ with an $R$-algebra structure, the multiplicative opposite $A^\text{op}$ inherits an $R$-algebra structure, where the scalar multiplication is defined via the original algebra structure on $A$.

MulOpposite.algebraMap_apply theorem

(c : R) : algebraMap R Aᵐᵒᵖ c = op (algebraMap R A c)

Full source

@[simp]
theorem algebraMap_apply (c : R) : algebraMap R Aᵐᵒᵖ c = op (algebraMap R A c) :=
  rfl

Algebra Map in Multiplicative Opposite Equals Opposite of Original Algebra Map

Informal description

For any commutative semiring $R$ and semiring $A$ with an $R$-algebra structure, the algebra map $\text{algebraMap} : R \to A^\text{op}$ satisfies $\text{algebraMap}_{R,A^\text{op}}(c) = \text{op}(\text{algebraMap}_{R,A}(c))$ for any $c \in R$, where $\text{op} : A \to A^\text{op}$ is the canonical embedding into the multiplicative opposite algebra.

AlgEquiv.opOp definition

: A ≃ₐ[R] Aᵐᵒᵖᵐᵒᵖ

Full source

/-- An algebra is isomorphic to the opposite of its opposite. -/
@[simps!]
def opOp : A ≃ₐ[R] Aᵐᵒᵖᵐᵒᵖ where
  __ := RingEquiv.opOp A
  commutes' _ := rfl

Algebra isomorphism between an algebra and its double multiplicative opposite

Informal description

For any commutative semiring $ R $ and $ R $-algebra $ A $, there is an algebra isomorphism between $ A $ and the double multiplicative opposite $ A^{\text{op}\text{op}} $. This isomorphism preserves both the algebra structure and the scalar multiplication by elements of $ R $.

AlgEquiv.toRingEquiv_opOp theorem

: (opOp R A : A ≃+* Aᵐᵒᵖᵐᵒᵖ) = RingEquiv.opOp A

Full source

@[simp] theorem toRingEquiv_opOp : (opOp R A : A ≃+* Aᵐᵒᵖᵐᵒᵖ) = RingEquiv.opOp A := rfl

Ring Equivalence Underlying Double Opposite Algebra Isomorphism

Informal description

The underlying ring equivalence of the algebra isomorphism between an $R$-algebra $A$ and its double multiplicative opposite $A^{\text{op}\text{op}}$ is equal to the canonical ring equivalence between $A$ and $A^{\text{op}\text{op}}$.

AlgHom.fromOpposite definition

(f : A →ₐ[R] B) (hf : ∀ x y, Commute (f x) (f y)) : Aᵐᵒᵖ →ₐ[R] B

Full source

/--
An algebra homomorphism `f : A →ₐ[R] B` such that `f x` commutes with `f y` for all `x, y` defines
an algebra homomorphism from `Aᵐᵒᵖ`. -/
@[simps -fullyApplied]
def fromOpposite (f : A →ₐ[R] B) (hf : ∀ x y, Commute (f x) (f y)) : AᵐᵒᵖAᵐᵒᵖ →ₐ[R] B :=
  { f.toRingHom.fromOpposite hf with
    toFun := f ∘ unop
    commutes' := fun r => f.commutes r }

Algebra homomorphism from multiplicative opposite induced by commuting homomorphism

Informal description

Given an algebra homomorphism $ f \colon A \to B $ over a commutative semiring $ R $, such that $ f(x) $ commutes with $ f(y) $ for all $ x, y \in A $, there exists an algebra homomorphism from the multiplicative opposite $ A^\text{op} $ to $ B $ defined by composing $ f $ with the canonical projection $ \text{unop} \colon A^\text{op} \to A $.

AlgHom.toLinearMap_fromOpposite theorem

 (f : A →ₐ[R] B) (hf : ∀ x y, Commute (f x) (f y)) :
  (f.fromOpposite hf).toLinearMap = f.toLinearMap ∘ₗ (opLinearEquiv R (M := A)).symm

Full source

@[simp]
theorem toLinearMap_fromOpposite (f : A →ₐ[R] B) (hf : ∀ x y, Commute (f x) (f y)) :
    (f.fromOpposite hf).toLinearMap = f.toLinearMap ∘ₗ (opLinearEquiv R (M := A)).symm :=
  rfl

Linear map decomposition for algebra homomorphism from opposite algebra

Informal description

Let $R$ be a commutative semiring, and let $A$ and $B$ be $R$-algebras. Given an $R$-algebra homomorphism $f \colon A \to B$ such that $f(x)$ commutes with $f(y)$ for all $x, y \in A$, the linear map associated to the induced homomorphism $f^\text{op} \colon A^\text{op} \to B$ (where $A^\text{op}$ is the multiplicative opposite algebra of $A$) is equal to the composition of the linear map associated to $f$ with the inverse of the canonical linear equivalence $\text{op} \colon A \to A^\text{op}$. In symbols: $$(f^\text{op})_\text{lin} = f_\text{lin} \circ \text{op}^{-1}$$

AlgHom.toRingHom_fromOpposite theorem

 (f : A →ₐ[R] B) (hf : ∀ x y, Commute (f x) (f y)) : (f.fromOpposite hf : Aᵐᵒᵖ →+* B) = (f : A →+* B).fromOpposite hf

Full source

@[simp]
theorem toRingHom_fromOpposite (f : A →ₐ[R] B) (hf : ∀ x y, Commute (f x) (f y)) :
    (f.fromOpposite hf : AᵐᵒᵖAᵐᵒᵖ →+* B) = (f : A →+* B).fromOpposite hf :=
  rfl

Compatibility of Ring Homomorphism Construction from Opposite Algebra with Underlying Homomorphism

Informal description

Let $R$ be a commutative semiring, and let $A$ and $B$ be semirings with an $R$-algebra structure. Given an algebra homomorphism $f \colon A \to B$ such that $f(x)$ and $f(y)$ commute for all $x, y \in A$, the ring homomorphism induced by $f$ from the multiplicative opposite algebra $A^\text{op}$ to $B$ coincides with the ring homomorphism obtained by applying the `fromOpposite` construction to the underlying ring homomorphism of $f$.

AlgHom.toOpposite definition

(f : A →ₐ[R] B) (hf : ∀ x y, Commute (f x) (f y)) : A →ₐ[R] Bᵐᵒᵖ

Full source

/--
An algebra homomorphism `f : A →ₐ[R] B` such that `f x` commutes with `f y` for all `x, y` defines
an algebra homomorphism to `Bᵐᵒᵖ`. -/
@[simps -fullyApplied]
def toOpposite (f : A →ₐ[R] B) (hf : ∀ x y, Commute (f x) (f y)) : A →ₐ[R] Bᵐᵒᵖ :=
  { f.toRingHom.toOpposite hf with
    toFun := opop ∘ f
    commutes' := fun r => unop_injective <| f.commutes r }

Algebra homomorphism to the multiplicative opposite via commuting elements

Informal description

Given an algebra homomorphism $ f \colon A \to B $ over a commutative semiring $ R $, if $ f(x) $ commutes with $ f(y) $ for all $ x, y \in A $, then $ f $ induces an algebra homomorphism $ A \to B^\text{op} $ to the multiplicative opposite algebra, defined by composing $ f $ with the canonical map $ \text{op} \colon B \to B^\text{op} $.

AlgHom.toLinearMap_toOpposite theorem

 (f : A →ₐ[R] B) (hf : ∀ x y, Commute (f x) (f y)) :
  (f.toOpposite hf).toLinearMap = (opLinearEquiv R : B ≃ₗ[R] Bᵐᵒᵖ) ∘ₗ f.toLinearMap

Full source

@[simp]
theorem toLinearMap_toOpposite (f : A →ₐ[R] B) (hf : ∀ x y, Commute (f x) (f y)) :
    (f.toOpposite hf).toLinearMap = (opLinearEquiv R : B ≃ₗ[R] Bᵐᵒᵖ) ∘ₗ f.toLinearMap :=
  rfl

Linear map decomposition for algebra homomorphism to opposite via commuting elements

Informal description

Let $R$ be a commutative semiring, and let $A$ and $B$ be semirings with $R$-algebra structures. Given an algebra homomorphism $f \colon A \to B$ such that $f(x)$ commutes with $f(y)$ for all $x, y \in A$, the linear map associated to the induced homomorphism $f \colon A \to B^\text{op}$ is equal to the composition of the linear equivalence $\text{op} \colon B \simeq_R B^\text{op}$ with the linear map associated to $f$.

AlgHom.toRingHom_toOpposite theorem

 (f : A →ₐ[R] B) (hf : ∀ x y, Commute (f x) (f y)) : (f.toOpposite hf : A →+* Bᵐᵒᵖ) = (f : A →+* B).toOpposite hf

Full source

@[simp]
theorem toRingHom_toOpposite (f : A →ₐ[R] B) (hf : ∀ x y, Commute (f x) (f y)) :
    (f.toOpposite hf : A →+* Bᵐᵒᵖ) = (f : A →+* B).toOpposite hf :=
  rfl

Compatibility of Opposite Algebra Homomorphism with Underlying Ring Homomorphism

Informal description

Let $A$ and $B$ be $R$-algebras over a commutative semiring $R$, and let $f : A \to B$ be an algebra homomorphism such that $f(x)$ commutes with $f(y)$ for all $x, y \in A$. Then the ring homomorphism $f^\text{op} : A \to B^\text{op}$ obtained by composing $f$ with the canonical map $\text{op} : B \to B^\text{op}$ is equal to the ring homomorphism obtained by first viewing $f$ as a ring homomorphism $A \to B$ and then applying the $\text{op}$ construction.

AlgHom.op definition

: (A →ₐ[R] B) ≃ (Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ)

Full source

/-- An algebra hom `A →ₐ[R] B` can equivalently be viewed as an algebra hom `Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ`.
This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms. -/
@[simps!]
protected def op : (A →ₐ[R] B) ≃ (Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ) where
  toFun f := { RingHom.op f.toRingHom with commutes' := fun r => unop_injective <| f.commutes r }
  invFun f := { RingHom.unop f.toRingHom with commutes' := fun r => op_injective <| f.commutes r }
  left_inv _f := AlgHom.ext fun _a => rfl
  right_inv _f := AlgHom.ext fun _a => rfl

Algebra homomorphism equivalence via opposites

Informal description

The equivalence between algebra homomorphisms $A \to_{R} B$ and algebra homomorphisms $A^\text{op} \to_{R} B^\text{op}$, where $A^\text{op}$ and $B^\text{op}$ denote the multiplicative opposites of $A$ and $B$ respectively. Specifically, this defines: 1. A function that takes an algebra homomorphism $f: A \to B$ and constructs an algebra homomorphism $f^\text{op}: A^\text{op} \to B^\text{op}$ by composing with the opposite operations. 2. An inverse function that reverses this process. 3. Proofs that these operations are mutual inverses.

AlgHom.toRingHom_op theorem

(f : A →ₐ[R] B) : f.op.toRingHom = RingHom.op f.toRingHom

Full source

theorem toRingHom_op (f : A →ₐ[R] B) : f.op.toRingHom = RingHom.op f.toRingHom :=
  rfl

Compatibility of Opposite Algebra Homomorphism with Underlying Ring Homomorphism

Informal description

For any algebra homomorphism $f \colon A \to_{R} B$, the underlying ring homomorphism of the opposite algebra homomorphism $f^\text{op} \colon A^\text{op} \to_{R} B^\text{op}$ is equal to the opposite of the underlying ring homomorphism of $f$.

AlgHom.unop abbrev

: (Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ) ≃ (A →ₐ[R] B)

Full source

/-- The 'unopposite' of an algebra hom `Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ`. Inverse to `RingHom.op`. -/
abbrev unop : (Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ) ≃ (A →ₐ[R] B) := AlgHom.op.symm

Inverse Equivalence of Algebra Homomorphisms via Opposites

Informal description

The equivalence between algebra homomorphisms $A^\text{op} \to_{R} B^\text{op}$ and algebra homomorphisms $A \to_{R} B$, where $A^\text{op}$ and $B^\text{op}$ denote the multiplicative opposites of $A$ and $B$ respectively. Specifically, this defines: 1. A function that takes an algebra homomorphism $f: A^\text{op} \to B^\text{op}$ and constructs an algebra homomorphism $f^\text{unop}: A \to B$ by reversing the opposite operations. 2. An inverse function that reverses this process. 3. Proofs that these operations are mutual inverses.

AlgHom.toRingHom_unop theorem

(f : Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ) : f.unop.toRingHom = RingHom.unop f.toRingHom

Full source

theorem toRingHom_unop (f : AᵐᵒᵖAᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ) : f.unop.toRingHom = RingHom.unop f.toRingHom :=
  rfl

Compatibility of Unopposite Algebra Homomorphism with Underlying Ring Homomorphism

Informal description

For any algebra homomorphism $f \colon A^\text{op} \to_R B^\text{op}$ between the multiplicative opposites of $R$-algebras $A$ and $B$, the underlying ring homomorphism of $f^\text{unop} \colon A \to_R B$ is equal to the inverse of the underlying ring homomorphism of $f$ under the ring homomorphism opposite equivalence.

AlgHom.opComm definition

: (A →ₐ[R] Bᵐᵒᵖ) ≃ (Aᵐᵒᵖ →ₐ[R] B)

Full source

/-- Swap the `ᵐᵒᵖ` on an algebra hom to the opposite side. -/
@[simps!]
def opComm : (A →ₐ[R] Bᵐᵒᵖ) ≃ (Aᵐᵒᵖ →ₐ[R] B) :=
  AlgHom.op.trans <| AlgEquiv.refl.arrowCongr (AlgEquiv.opOp R B).symm

Algebra homomorphism equivalence with swapped opposites

Informal description

The equivalence between algebra homomorphisms $A \to_{R} B^\text{op}$ and algebra homomorphisms $A^\text{op} \to_{R} B$, where $A^\text{op}$ and $B^\text{op}$ denote the multiplicative opposites of $A$ and $B$ respectively. Specifically, this defines: 1. A bijection that swaps the side on which the opposite algebra lies in the homomorphism. 2. The equivalence is constructed by composing the `AlgHom.op` equivalence with an isomorphism involving the double opposite of $B$.

AlgEquiv.op definition

: (A ≃ₐ[R] B) ≃ Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ

Full source

/-- An algebra iso `A ≃ₐ[R] B` can equivalently be viewed as an algebra iso `Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ`.
This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms. -/
@[simps!]
def op : (A ≃ₐ[R] B) ≃ Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ where
  toFun f :=
    { RingEquiv.op f.toRingEquiv with
      commutes' := fun r => MulOpposite.unop_injective <| f.commutes r }
  invFun f :=
    { RingEquiv.unop f.toRingEquiv with
      commutes' := fun r => MulOpposite.op_injective <| f.commutes r }
  left_inv _f := AlgEquiv.ext fun _a => rfl
  right_inv _f := AlgEquiv.ext fun _a => rfl

Algebra isomorphism between multiplicative opposites

Informal description

The function maps an algebra isomorphism $f : A \simeq_{R} B$ between $R$-algebras $A$ and $B$ to an algebra isomorphism $A^\text{op} \simeq_{R} B^\text{op}$ between their multiplicative opposites. Specifically: 1. The forward direction applies the opposite operation to both the domain and codomain of $f$, preserving the algebra structure. 2. The inverse direction reverses this process, converting an isomorphism between opposites back to an isomorphism between the original algebras. 3. These operations are mutual inverses, establishing a bijection between the two types of isomorphisms.

AlgEquiv.toAlgHom_op theorem

(f : A ≃ₐ[R] B) : (AlgEquiv.op f).toAlgHom = AlgHom.op f.toAlgHom

Full source

theorem toAlgHom_op (f : A ≃ₐ[R] B) :
    (AlgEquiv.op f).toAlgHom = AlgHom.op f.toAlgHom :=
  rfl

Compatibility of Opposite Algebra Isomorphism with Underlying Homomorphism

Informal description

For any algebra isomorphism $f : A \simeq_{R} B$ between $R$-algebras $A$ and $B$, the underlying algebra homomorphism of the opposite algebra isomorphism $\text{op}(f)$ is equal to the opposite of the underlying algebra homomorphism of $f$. In symbols, this means: \[ (\text{op}(f)).\text{toAlgHom} = \text{op}(f.\text{toAlgHom}) \]

AlgEquiv.toRingEquiv_op theorem

(f : A ≃ₐ[R] B) : (AlgEquiv.op f).toRingEquiv = RingEquiv.op f.toRingEquiv

Full source

theorem toRingEquiv_op (f : A ≃ₐ[R] B) :
    (AlgEquiv.op f).toRingEquiv = RingEquiv.op f.toRingEquiv :=
  rfl

Ring Equivalence of Opposite Algebra Isomorphism Equals Opposite of Ring Equivalence

Informal description

For any algebra isomorphism $f : A \simeq_{R} B$ between $R$-algebras $A$ and $B$, the underlying ring equivalence of the opposite algebra isomorphism $\text{op}(f)$ is equal to the opposite of the underlying ring equivalence of $f$. That is, $(\text{op}(f))_{\text{ring}} = \text{op}(f_{\text{ring}})$.

AlgEquiv.unop abbrev

: (Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) ≃ A ≃ₐ[R] B

Full source

/-- The 'unopposite' of an algebra iso `Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ`. Inverse to `AlgEquiv.op`. -/
abbrev unop : (Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) ≃ A ≃ₐ[R] B := AlgEquiv.op.symm

Inverse of the Algebra Isomorphism between Multiplicative Opposites

Informal description

Given two $R$-algebras $A$ and $B$, there is a bijection between algebra isomorphisms $A^\text{op} \simeq_R B^\text{op}$ of their multiplicative opposites and algebra isomorphisms $A \simeq_R B$ of the original algebras. Specifically, the function `AlgEquiv.unop` maps an isomorphism $f : A^\text{op} \simeq_R B^\text{op}$ to an isomorphism $A \simeq_R B$ by reversing the opposite operation on both the domain and codomain.

AlgEquiv.toAlgHom_unop theorem

(f : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) : f.unop.toAlgHom = AlgHom.unop f.toAlgHom

Full source

theorem toAlgHom_unop (f : AᵐᵒᵖAᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) : f.unop.toAlgHom = AlgHom.unop f.toAlgHom :=
  rfl

Compatibility of Unop with Underlying Homomorphism for Algebra Isomorphisms between Opposites

Informal description

Let $A$ and $B$ be $R$-algebras, and let $f: A^\text{op} \simeq_R B^\text{op}$ be an algebra isomorphism between their multiplicative opposites. Then the underlying algebra homomorphism of $f^\text{unop}$ (the inverse of $f$ under the opposite operation) is equal to the inverse of the underlying algebra homomorphism of $f$ under the opposite operation. In symbols, if we denote the underlying algebra homomorphism of an isomorphism $g$ as $g_\text{hom}$, then: $$(f^\text{unop})_\text{hom} = (f_\text{hom})^\text{unop}$$

AlgEquiv.toRingEquiv_unop theorem

(f : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) : (AlgEquiv.unop f).toRingEquiv = RingEquiv.unop f.toRingEquiv

Full source

theorem toRingEquiv_unop (f : AᵐᵒᵖAᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) :
    (AlgEquiv.unop f).toRingEquiv = RingEquiv.unop f.toRingEquiv :=
  rfl

Compatibility of unop operations between algebra and ring equivalences

Informal description

Let $A$ and $B$ be $R$-algebras, and let $f : A^\text{op} \simeq_R B^\text{op}$ be an algebra isomorphism between their multiplicative opposites. Then the underlying ring equivalence of the isomorphism $\text{unop}(f) : A \simeq_R B$ is equal to the ring equivalence obtained by applying $\text{RingEquiv.unop}$ to the underlying ring equivalence of $f$.

AlgEquiv.opComm definition

: (A ≃ₐ[R] Bᵐᵒᵖ) ≃ (Aᵐᵒᵖ ≃ₐ[R] B)

Full source

/-- Swap the `ᵐᵒᵖ` on an algebra isomorphism to the opposite side. -/
@[simps!]
def opComm : (A ≃ₐ[R] Bᵐᵒᵖ) ≃ (Aᵐᵒᵖ ≃ₐ[R] B) :=
  AlgEquiv.op.trans <| AlgEquiv.refl.equivCongr (opOp R B).symm

Equivalence between algebra isomorphisms involving multiplicative opposites

Informal description

The equivalence between algebra isomorphisms from an $R$-algebra $A$ to the multiplicative opposite of an $R$-algebra $B$ and algebra isomorphisms from the multiplicative opposite of $A$ to $B$. Specifically, this equivalence is constructed by: 1. First applying the `AlgEquiv.op` operation to convert an isomorphism $A \simeq B^\text{op}$ into an isomorphism $A^\text{op} \simeq B^{\text{op}\text{op}}$. 2. Then composing with the isomorphism $(B^\text{op})^\text{op} \simeq B$ given by the double opposite isomorphism. This establishes a natural bijection between the two types of algebra isomorphisms.

AlgEquiv.moduleEndSelf definition

: Aᵐᵒᵖ ≃ₐ[R] Module.End A A

Full source

/-- The canonical algebra isomorphism from `Aᵐᵒᵖ` to `Module.End A A` induced by the right
multiplication. -/
@[simps!] def moduleEndSelf : AᵐᵒᵖAᵐᵒᵖ ≃ₐ[R] Module.End A A where
  __ := RingEquiv.moduleEndSelf A
  commutes' _ := by ext; simp [Algebra.algebraMap_eq_smul_one]

Algebra isomorphism between opposite algebra and endomorphism algebra via right multiplication

Informal description

The canonical algebra isomorphism from the multiplicative opposite algebra $A^\text{op}$ to the algebra of linear endomorphisms $\text{End}_A(A)$, induced by right multiplication. Specifically, it maps each element $a \in A^\text{op}$ to the endomorphism $x \mapsto x \cdot a$ for $x \in A$.

AlgEquiv.moduleEndSelfOp definition

: A ≃ₐ[R] Module.End Aᵐᵒᵖ A

Full source

/-- The canonical algebra isomorphism from `A` to `Module.End Aᵐᵒᵖ A` induced by the left
multiplication. -/
@[simps!] def moduleEndSelfOp : A ≃ₐ[R] Module.End Aᵐᵒᵖ A where
  __ := RingEquiv.moduleEndSelfOp A
  commutes' _ := by ext; simp [Algebra.algebraMap_eq_smul_one]

Algebra isomorphism between an algebra and its opposite module endomorphisms

Informal description

The canonical algebra isomorphism from an $R$-algebra $A$ to the algebra of linear endomorphisms of the multiplicative opposite $A^\text{op}$ as an $A$-module, induced by left multiplication. Specifically, it maps each element $a \in A$ to the linear endomorphism $\lambda x \mapsto a \cdot x$ on $A^\text{op}$.

AlgEquiv.toOpposite definition

: A ≃ₐ[R] Aᵐᵒᵖ

Full source

/-- A commutative algebra is isomorphic to its opposite. -/
@[simps!]
def toOpposite : A ≃ₐ[R] Aᵐᵒᵖ where
  __ := RingEquiv.toOpposite A
  commutes' _r := rfl

Algebra isomorphism to the multiplicative opposite

Informal description

Given a commutative semiring $R$ and a commutative $R$-algebra $A$, the algebra isomorphism $\text{toOpposite}$ maps $A$ to its multiplicative opposite $A^\text{op}$. This isomorphism preserves both the ring structure and the $R$-algebra structure, where multiplication in $A^\text{op}$ is defined by $\text{op}(x) \cdot \text{op}(y) = \text{op}(y \cdot x)$ for all $x, y \in A$.

AlgEquiv.toRingEquiv_toOpposite theorem

: (toOpposite R A : A ≃+* Aᵐᵒᵖ) = RingEquiv.toOpposite A

Full source

@[simp] lemma toRingEquiv_toOpposite : (toOpposite R A : A ≃+* Aᵐᵒᵖ) = RingEquiv.toOpposite A := rfl

Equality of Underlying Ring Equivalences in the Algebra Isomorphism to the Opposite

Informal description

For a commutative semiring $R$ and a commutative $R$-algebra $A$, the underlying ring equivalence of the algebra isomorphism $\text{toOpposite} : A \simeq_{\text{Alg}[R]} A^\text{op}$ is equal to the ring equivalence $\text{RingEquiv.toOpposite} : A \simeq_{+*} A^\text{op}$.

AlgEquiv.toLinearEquiv_toOpposite theorem

: toLinearEquiv (toOpposite R A) = opLinearEquiv R

Full source

@[simp] lemma toLinearEquiv_toOpposite : toLinearEquiv (toOpposite R A) = opLinearEquiv R := rfl

Linear Equivalence of Algebra Isomorphism to Multiplicative Opposite

Informal description

For a commutative semiring $R$ and a commutative $R$-algebra $A$, the linear equivalence associated with the algebra isomorphism $\text{toOpposite} \colon A \simeq_{\text{Alg}_R} A^\text{op}$ is equal to the linear equivalence $\text{opLinearEquiv}_R \colon M \simeq_{\text{Lin}_R} M^\text{op}$.

Main definitions