doc-next-gen

Mathlib.Algebra.Ring.Opposite

Module docstring

{"# Ring structures on the multiplicative opposite "}

MulOpposite.instDistrib instance
[Distrib R] : Distrib Rᵐᵒᵖ
Full source 
instance instDistrib [Distrib R] : Distrib Rᵐᵒᵖ where
  left_distrib _ _ _ := unop_injective <| add_mul _ _ _
  right_distrib _ _ _ := unop_injective <| mul_add _ _ _
Distributivity in the Multiplicative Opposite
Informal description
For any type $R$ with a distributive multiplication over addition, the multiplicative opposite $R^\text{op}$ also inherits a distributive multiplication over addition, where the multiplication is reversed.
MulOpposite.instNonUnitalNonAssocSemiring instance
[NonUnitalNonAssocSemiring R] : NonUnitalNonAssocSemiring Rᵐᵒᵖ
Full source 
instance instNonUnitalNonAssocSemiring [NonUnitalNonAssocSemiring R] :
    NonUnitalNonAssocSemiring Rᵐᵒᵖ where
  __ := instAddCommMonoid
  __ := instDistrib
  __ := instMulZeroClass
Non-unital Non-associative Semiring Structure on the Multiplicative Opposite
Informal description
For any non-unital non-associative semiring $R$, the multiplicative opposite $R^\text{op}$ also forms a non-unital non-associative semiring, where the multiplication is reversed.
MulOpposite.instNonAssocSemiring instance
[NonAssocSemiring R] : NonAssocSemiring Rᵐᵒᵖ
Full source 
instance instNonAssocSemiring [NonAssocSemiring R] : NonAssocSemiring Rᵐᵒᵖ where
  __ := instNonUnitalNonAssocSemiring
  __ := instMulZeroOneClass
  __ := instAddCommMonoidWithOne
Non-associative Semiring Structure on the Multiplicative Opposite
Informal description
For any non-associative semiring $R$, the multiplicative opposite $R^\text{op}$ also forms a non-associative semiring, where the multiplication is reversed.
MulOpposite.instNonUnitalCommSemiring instance
[NonUnitalCommSemiring R] : NonUnitalCommSemiring Rᵐᵒᵖ
Full source 
instance instNonUnitalCommSemiring [NonUnitalCommSemiring R] : NonUnitalCommSemiring Rᵐᵒᵖ where
  __ := instNonUnitalSemiring
  __ := instCommSemigroup
Non-unital Commutative Semiring Structure on the Multiplicative Opposite
Informal description
For any non-unital commutative semiring $R$, the multiplicative opposite $R^\text{op}$ is also a non-unital commutative semiring, with multiplication defined by $\text{op}(x) \cdot \text{op}(y) = \text{op}(y \cdot x)$ for all $x, y \in R$.
MulOpposite.instCommSemiring instance
[CommSemiring R] : CommSemiring Rᵐᵒᵖ
Full source 
instance instCommSemiring [CommSemiring R] : CommSemiring Rᵐᵒᵖ where
  __ := instSemiring
  __ := instCommMonoid
Commutative Semiring Structure on the Multiplicative Opposite
Informal description
For any commutative semiring $R$, the multiplicative opposite $R^\text{op}$ is also a commutative semiring, where the multiplication is reversed.
MulOpposite.instNonUnitalNonAssocRing instance
[NonUnitalNonAssocRing R] : NonUnitalNonAssocRing Rᵐᵒᵖ
Full source 
instance instNonUnitalNonAssocRing [NonUnitalNonAssocRing R] : NonUnitalNonAssocRing Rᵐᵒᵖ where
  __ := instAddCommGroup
  __ := instNonUnitalNonAssocSemiring
Non-unital Non-associative Ring Structure on the Multiplicative Opposite
Informal description
For any non-unital non-associative ring $R$, the multiplicative opposite $R^\text{op}$ is also a non-unital non-associative ring, where the multiplication is reversed.
MulOpposite.instNonUnitalRing instance
[NonUnitalRing R] : NonUnitalRing Rᵐᵒᵖ
Full source 
instance instNonUnitalRing [NonUnitalRing R] : NonUnitalRing Rᵐᵒᵖ where
  __ := instNonUnitalNonAssocRing
  __ := instNonUnitalSemiring
Non-unital Ring Structure on the Multiplicative Opposite
Informal description
For any non-unital ring $R$, the multiplicative opposite $R^\text{op}$ is also a non-unital ring, where the multiplication is reversed. That is, for any $x, y \in R$, the multiplication in $R^\text{op}$ satisfies $\text{op}(x * y) = \text{op}(y) * \text{op}(x)$, where $\text{op} : R \to R^\text{op}$ is the canonical embedding.
MulOpposite.instNonAssocRing instance
[NonAssocRing R] : NonAssocRing Rᵐᵒᵖ
Full source 
instance instNonAssocRing [NonAssocRing R] : NonAssocRing Rᵐᵒᵖ where
  __ := instNonUnitalNonAssocRing
  __ := instNonAssocSemiring
  __ := instAddCommGroupWithOne
Non-associative Ring Structure on the Multiplicative Opposite
Informal description
For any non-associative ring $R$, the multiplicative opposite $R^\text{op}$ is also a non-associative ring, where the multiplication is reversed. That is, for any $x, y \in R$, the multiplication in $R^\text{op}$ satisfies $\text{op}(x * y) = \text{op}(y) * \text{op}(x)$, where $\text{op} : R \to R^\text{op}$ is the canonical embedding.
MulOpposite.instRing instance
[Ring R] : Ring Rᵐᵒᵖ
Full source 
instance instRing [Ring R] : Ring Rᵐᵒᵖ where
  __ := instSemiring
  __ := instAddCommGroupWithOne
Ring Structure on the Multiplicative Opposite
Informal description
For any ring $R$, the multiplicative opposite $R^\text{op}$ is also a ring, where the multiplication is reversed. That is, for any $x, y \in R$, the multiplication in $R^\text{op}$ satisfies $\text{op}(x * y) = \text{op}(y) * \text{op}(x)$, where $\text{op} : R \to R^\text{op}$ is the canonical embedding.
MulOpposite.instNonUnitalCommRing instance
[NonUnitalCommRing R] : NonUnitalCommRing Rᵐᵒᵖ
Full source 
instance instNonUnitalCommRing [NonUnitalCommRing R] : NonUnitalCommRing Rᵐᵒᵖ where
  __ := instNonUnitalRing
  __ := instNonUnitalCommSemiring
Non-unital Commutative Ring Structure on the Multiplicative Opposite
Informal description
For any non-unital commutative ring $R$, the multiplicative opposite $R^\text{op}$ is also a non-unital commutative ring, with multiplication defined by $\text{op}(x) \cdot \text{op}(y) = \text{op}(y \cdot x)$ for all $x, y \in R$.
MulOpposite.instCommRing instance
[CommRing R] : CommRing Rᵐᵒᵖ
Full source 
instance instCommRing [CommRing R] : CommRing Rᵐᵒᵖ where
  __ := instRing
  __ := instCommMonoid
Commutative Ring Structure on the Multiplicative Opposite
Informal description
For any commutative ring $R$, the multiplicative opposite $R^\text{op}$ is also a commutative ring, where the multiplication is defined by $\text{op}(x) \cdot \text{op}(y) = \text{op}(x \cdot y)$ for all $x, y \in R$.
MulOpposite.instIsDomain instance
[Ring R] [IsDomain R] : IsDomain Rᵐᵒᵖ
Full source 
instance instIsDomain [Ring R] [IsDomain R] : IsDomain Rᵐᵒᵖ :=
  NoZeroDivisors.to_isDomain _
Multiplicative Opposite of a Domain is a Domain
Informal description
For any ring $R$ that is a domain (i.e., a nontrivial ring with no zero divisors), the multiplicative opposite ring $R^\text{op}$ is also a domain.
AddOpposite.instDistrib instance
[Distrib R] : Distrib Rᵃᵒᵖ
Full source 
instance instDistrib [Distrib R] : Distrib Rᵃᵒᵖ where
  left_distrib _ _ _ := unop_injective <| mul_add _ _ _
  right_distrib _ _ _ := unop_injective <| add_mul _ _ _
Distributive Structure on the Additive Opposite
Informal description
For any type $R$ equipped with multiplication and addition operations that satisfy the distributive property, the additive opposite $R^{\text{aop}}$ also inherits a distributive structure. Specifically, the multiplication in $R^{\text{aop}}$ is both left and right distributive over addition, mirroring the distributive properties of the original structure $R$.
AddOpposite.instNonUnitalNonAssocSemiring instance
[NonUnitalNonAssocSemiring R] : NonUnitalNonAssocSemiring Rᵃᵒᵖ
Full source 
instance instNonUnitalNonAssocSemiring [NonUnitalNonAssocSemiring R] :
    NonUnitalNonAssocSemiring Rᵃᵒᵖ where
  __ := instAddCommMonoid
  __ := instDistrib
  __ := instMulZeroClass
Non-unital Non-associative Semiring Structure on the Additive Opposite
Informal description
For any non-unital non-associative semiring $R$, the additive opposite $R^{\text{aop}}$ also forms a non-unital non-associative semiring. This means that $R^{\text{aop}}$ inherits the additive commutative monoid structure, distributive property, and multiplicative zero properties from $R$, but with the order of operations reversed in the additive structure.
AddOpposite.instNonUnitalSemiring instance
[NonUnitalSemiring R] : NonUnitalSemiring Rᵃᵒᵖ
Full source 
instance instNonUnitalSemiring [NonUnitalSemiring R] : NonUnitalSemiring Rᵃᵒᵖ where
  __ := instNonUnitalNonAssocSemiring
  __ := instSemigroupWithZero
Non-unital Semiring Structure on the Additive Opposite
Informal description
For any non-unital semiring $R$, the additive opposite $R^{\text{aop}}$ also forms a non-unital semiring. This means that $R^{\text{aop}}$ inherits the additive commutative monoid structure, associative multiplication, distributive property, and multiplicative zero properties from $R$, but with the order of operations reversed in the additive structure.
AddOpposite.instNonAssocSemiring instance
[NonAssocSemiring R] : NonAssocSemiring Rᵃᵒᵖ
Full source 
instance instNonAssocSemiring [NonAssocSemiring R] : NonAssocSemiring Rᵃᵒᵖ where
  __ := instNonUnitalNonAssocSemiring
  __ := instMulZeroOneClass
  __ := instAddCommMonoidWithOne
Non-associative Semiring Structure on the Additive Opposite
Informal description
For any non-associative semiring $R$, the additive opposite $R^{\text{aop}}$ is also a non-associative semiring. This means that $R^{\text{aop}}$ inherits the additive commutative monoid structure with one, the multiplicative zero and identity properties, and the distributive properties from $R$, but with the order of operations reversed in the additive structure.
AddOpposite.instSemiring instance
[Semiring R] : Semiring Rᵃᵒᵖ
Full source 
instance instSemiring [Semiring R] : Semiring Rᵃᵒᵖ where
  __ := instNonUnitalSemiring
  __ := instNonAssocSemiring
  __ := instMonoidWithZero
Semiring Structure on the Additive Opposite
Informal description
For any semiring $R$, the additive opposite $R^{\text{aop}}$ is also a semiring. This means that $R^{\text{aop}}$ inherits all the semiring structure from $R$, including the additive commutative monoid structure, multiplicative monoid with zero structure, and the distributive properties, but with the order of operations reversed in the additive structure.
AddOpposite.instNonUnitalCommSemiring instance
[NonUnitalCommSemiring R] : NonUnitalCommSemiring Rᵃᵒᵖ
Full source 
instance instNonUnitalCommSemiring [NonUnitalCommSemiring R] : NonUnitalCommSemiring Rᵃᵒᵖ where
  __ := instNonUnitalSemiring
  __ := instCommSemigroup
Non-unital Commutative Semiring Structure on the Additive Opposite
Informal description
For any non-unital commutative semiring $R$, the additive opposite $R^{\text{aop}}$ is also a non-unital commutative semiring. This means that $R^{\text{aop}}$ inherits the additive commutative monoid structure, commutative multiplicative semigroup structure, distributive properties, and multiplicative zero properties from $R$, but with the order of operations reversed in the additive structure.
AddOpposite.instCommSemiring instance
[CommSemiring R] : CommSemiring Rᵃᵒᵖ
Full source 
instance instCommSemiring [CommSemiring R] : CommSemiring Rᵃᵒᵖ where
  __ := instSemiring
  __ := instCommMonoid
Commutative Semiring Structure on the Additive Opposite
Informal description
For any commutative semiring $R$, the additive opposite $R^{\text{aop}}$ is also a commutative semiring. This means that $R^{\text{aop}}$ inherits all the semiring structure from $R$, including the additive commutative monoid structure, commutative multiplicative monoid structure, and the distributive properties, but with the order of operations reversed in the additive structure.
AddOpposite.instNonUnitalNonAssocRing instance
[NonUnitalNonAssocRing R] : NonUnitalNonAssocRing Rᵃᵒᵖ
Full source 
instance instNonUnitalNonAssocRing [NonUnitalNonAssocRing R] : NonUnitalNonAssocRing Rᵃᵒᵖ where
  __ := instAddCommGroup
  __ := instNonUnitalNonAssocSemiring
Non-unital Non-associative Ring Structure on the Additive Opposite
Informal description
For any non-unital non-associative ring $R$, the additive opposite $R^{\text{aop}}$ also forms a non-unital non-associative ring. This means that $R^{\text{aop}}$ inherits the additive commutative group structure, multiplicative semigroup structure, and distributive properties from $R$, but with the order of operations reversed in the additive structure.
AddOpposite.instNonUnitalRing instance
[NonUnitalRing R] : NonUnitalRing Rᵃᵒᵖ
Full source 
instance instNonUnitalRing [NonUnitalRing R] : NonUnitalRing Rᵃᵒᵖ where
  __ := instNonUnitalNonAssocRing
  __ := instNonUnitalSemiring
Non-unital Ring Structure on the Additive Opposite
Informal description
For any non-unital ring $R$, the additive opposite $R^{\text{aop}}$ also forms a non-unital ring. This means that $R^{\text{aop}}$ inherits the additive commutative group structure, associative multiplication, and distributive properties from $R$, but with the order of operations reversed in the additive structure.
AddOpposite.instNonAssocRing instance
[NonAssocRing R] : NonAssocRing Rᵃᵒᵖ
Full source 
instance instNonAssocRing [NonAssocRing R] : NonAssocRing Rᵃᵒᵖ where
  __ := instNonUnitalNonAssocRing
  __ := instNonAssocSemiring
  __ := instAddCommGroupWithOne
Non-associative Ring Structure on the Additive Opposite
Informal description
For any non-associative ring $R$, the additive opposite $R^{\text{aop}}$ is also a non-associative ring. This means that $R^{\text{aop}}$ inherits the additive commutative group structure with one, the multiplicative identity property, and the distributive properties from $R$, but with the order of operations reversed in the additive structure.
AddOpposite.instRing instance
[Ring R] : Ring Rᵃᵒᵖ
Full source 
instance instRing [Ring R] : Ring Rᵃᵒᵖ where
  __ := instSemiring
  __ := instAddCommGroupWithOne
Ring Structure on the Additive Opposite
Informal description
For any ring $R$, the additive opposite $R^{\text{aop}}$ is also a ring. This means that $R^{\text{aop}}$ inherits all the ring structure from $R$, including the additive commutative group structure, multiplicative monoid with one structure, and the distributive properties, but with the order of operations reversed in the additive structure.
AddOpposite.instNonUnitalCommRing instance
[NonUnitalCommRing R] : NonUnitalCommRing Rᵃᵒᵖ
Full source 
instance instNonUnitalCommRing [NonUnitalCommRing R] : NonUnitalCommRing Rᵃᵒᵖ where
  __ := instNonUnitalRing
  __ := instNonUnitalCommSemiring
Non-unital Commutative Ring Structure on the Additive Opposite
Informal description
For any non-unital commutative ring $R$, the additive opposite $R^{\text{aop}}$ is also a non-unital commutative ring. This means that $R^{\text{aop}}$ inherits the additive commutative group structure, commutative multiplication, and distributive properties from $R$, but with the order of operations reversed in the additive structure.
AddOpposite.instCommRing instance
[CommRing R] : CommRing Rᵃᵒᵖ
Full source 
instance instCommRing [CommRing R] : CommRing Rᵃᵒᵖ where
  __ := instRing
  __ := instCommMonoid
Commutative Ring Structure on the Additive Opposite
Informal description
For any commutative ring $R$, the additive opposite $R^{\text{aop}}$ is also a commutative ring. This means that $R^{\text{aop}}$ inherits all the ring structure from $R$, including the additive commutative group structure, commutative multiplication, and distributive properties, but with the order of operations reversed in the additive structure.
AddOpposite.instIsDomain instance
[Ring R] [IsDomain R] : IsDomain Rᵃᵒᵖ
Full source 
instance instIsDomain [Ring R] [IsDomain R] : IsDomain Rᵃᵒᵖ :=
  NoZeroDivisors.to_isDomain _
Domain Property of the Additive Opposite Ring
Informal description
For any domain $R$, the additive opposite $R^{\text{aop}}$ is also a domain. This means that $R^{\text{aop}}$ inherits the property of being a nontrivial semiring where multiplication by any nonzero element is cancellative on both sides.
NonUnitalRingHom.toOpposite definition
{R S : Type*} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : ∀ x y, Commute (f x) (f y)) : R →ₙ+* Sᵐᵒᵖ
Full source 
/-- A non-unital ring homomorphism `f : R →ₙ+* S` such that `f x` commutes with `f y` for all `x, y`
defines a non-unital ring homomorphism to `Sᵐᵒᵖ`. -/
@[simps -fullyApplied]
def NonUnitalRingHom.toOpposite {R S : Type*} [NonUnitalNonAssocSemiring R]
    [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : ∀ x y, Commute (f x) (f y)) : R →ₙ+* Sᵐᵒᵖ :=
  { ((opAddEquiv : S ≃+ Sᵐᵒᵖ).toAddMonoidHom.comp ↑f : R →+ Sᵐᵒᵖ), f.toMulHom.toOpposite hf with
    toFun := MulOpposite.opMulOpposite.op ∘ f }
Non-unital ring homomorphism to multiplicative opposite
Informal description
Given a non-unital ring homomorphism \( f \colon R \to S \) between non-unital non-associative semirings \( R \) and \( S \), if \( f(x) \) commutes with \( f(y) \) for all \( x, y \in R \), then \( f \) induces a non-unital ring homomorphism from \( R \) to the multiplicative opposite \( S^\text{op} \), defined by composing \( f \) with the canonical map \( \text{op} \colon S \to S^\text{op} \).
NonUnitalRingHom.fromOpposite definition
{R S : Type*} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : ∀ x y, Commute (f x) (f y)) : Rᵐᵒᵖ →ₙ+* S
Full source 
/-- A non-unital ring homomorphism `f : R →ₙ* S` such that `f x` commutes with `f y` for all `x, y`
defines a non-unital ring homomorphism from `Rᵐᵒᵖ`. -/
@[simps -fullyApplied]
def NonUnitalRingHom.fromOpposite {R S : Type*} [NonUnitalNonAssocSemiring R]
    [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : ∀ x y, Commute (f x) (f y)) : RᵐᵒᵖRᵐᵒᵖ →ₙ+* S :=
  { (f.toAddMonoidHom.comp (opAddEquiv : R ≃+ Rᵐᵒᵖ).symm.toAddMonoidHom : RᵐᵒᵖRᵐᵒᵖ →+ S),
    f.toMulHom.fromOpposite hf with toFun := f ∘ MulOpposite.unop }
Non-unital ring homomorphism from the multiplicative opposite
Informal description
Given a non-unital ring homomorphism \( f \colon R \to S \) between non-unital non-associative semirings \( R \) and \( S \), if \( f(x) \) commutes with \( f(y) \) for all \( x, y \in R \), then \( f \) induces a non-unital ring homomorphism from the multiplicative opposite \( R^\text{op} \) to \( S \), defined by composing \( f \) with the canonical projection \( \text{unop} \colon R^\text{op} \to R \).
NonUnitalRingHom.op definition
{R S} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] : (R →ₙ+* S) ≃ (Rᵐᵒᵖ →ₙ+* Sᵐᵒᵖ)
Full source 
/-- A non-unital ring hom `R →ₙ+* S` can equivalently be viewed as a non-unital ring hom
`Rᵐᵒᵖ →+* Sᵐᵒᵖ`. This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms. -/
@[simps]
def NonUnitalRingHom.op {R S} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] :
    (R →ₙ+* S) ≃ (Rᵐᵒᵖ →ₙ+* Sᵐᵒᵖ) where
  toFun f := { AddMonoidHom.mulOp f.toAddMonoidHom, MulHom.op f.toMulHom with }
  invFun f := { AddMonoidHom.mulUnop f.toAddMonoidHom, MulHom.unop f.toMulHom with }
  left_inv _ := rfl
  right_inv _ := rfl
Equivalence of non-unital ring homomorphisms via multiplicative opposites
Informal description
The equivalence between non-unital ring homomorphisms $f \colon R \to S$ and non-unital ring homomorphisms $f^\text{op} \colon R^\text{op} \to S^\text{op}$, where $R^\text{op}$ and $S^\text{op}$ denote the multiplicative opposites of $R$ and $S$ respectively. Specifically, this defines: 1. A function that takes a non-unital ring homomorphism $f \colon R \to S$ and constructs a homomorphism $f^\text{op} \colon R^\text{op} \to S^\text{op}$ by composing with the opposite operations. 2. An inverse function that reverses this process. 3. Proofs that these operations are mutual inverses.
NonUnitalRingHom.unop definition
{R S} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] : (Rᵐᵒᵖ →ₙ+* Sᵐᵒᵖ) ≃ (R →ₙ+* S)
Full source 
/-- The 'unopposite' of a non-unital ring hom `Rᵐᵒᵖ →ₙ+* Sᵐᵒᵖ`. Inverse to
`NonUnitalRingHom.op`. -/
@[simp]
def NonUnitalRingHom.unop {R S} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] :
    (Rᵐᵒᵖ →ₙ+* Sᵐᵒᵖ) ≃ (R →ₙ+* S) :=
  NonUnitalRingHom.op.symm
Inverse of the opposite operation for non-unital ring homomorphisms
Informal description
The inverse of the operation that converts a non-unital ring homomorphism $f \colon R \to S$ into a homomorphism $f^\text{op} \colon R^\text{op} \to S^\text{op}$ between their multiplicative opposites. Specifically, this function takes a homomorphism $g \colon R^\text{op} \to S^\text{op}$ and returns the original homomorphism $f \colon R \to S$ by reversing the opposite operation.
RingHom.toOpposite definition
{R S : Type*} [Semiring R] [Semiring S] (f : R →+* S) (hf : ∀ x y, Commute (f x) (f y)) : R →+* Sᵐᵒᵖ
Full source 
/-- A ring homomorphism `f : R →+* S` such that `f x` commutes with `f y` for all `x, y` defines
a ring homomorphism to `Sᵐᵒᵖ`. -/
@[simps -fullyApplied]
def RingHom.toOpposite {R S : Type*} [Semiring R] [Semiring S] (f : R →+* S)
    (hf : ∀ x y, Commute (f x) (f y)) : R →+* Sᵐᵒᵖ :=
  { ((opAddEquiv : S ≃+ Sᵐᵒᵖ).toAddMonoidHom.comp ↑f : R →+ Sᵐᵒᵖ), f.toMonoidHom.toOpposite hf with
    toFun := MulOpposite.opMulOpposite.op ∘ f }
Semiring homomorphism to multiplicative opposite via commuting elements
Informal description
Given a semiring homomorphism \( f \colon R \to S \) between semirings \( R \) and \( S \), such that \( f(x) \) commutes with \( f(y) \) for all \( x, y \in R \), there exists a semiring homomorphism from \( R \) to the multiplicative opposite \( S^\text{op} \) defined by composing \( f \) with the canonical map \( \text{op} \colon S \to S^\text{op} \).
RingHom.fromOpposite definition
{R S : Type*} [Semiring R] [Semiring S] (f : R →+* S) (hf : ∀ x y, Commute (f x) (f y)) : Rᵐᵒᵖ →+* S
Full source 
/-- A ring homomorphism `f : R →+* S` such that `f x` commutes with `f y` for all `x, y` defines
a ring homomorphism from `Rᵐᵒᵖ`. -/
@[simps -fullyApplied]
def RingHom.fromOpposite {R S : Type*} [Semiring R] [Semiring S] (f : R →+* S)
    (hf : ∀ x y, Commute (f x) (f y)) : RᵐᵒᵖRᵐᵒᵖ →+* S :=
  { (f.toAddMonoidHom.comp (opAddEquiv : R ≃+ Rᵐᵒᵖ).symm.toAddMonoidHom : RᵐᵒᵖRᵐᵒᵖ →+ S),
    f.toMonoidHom.fromOpposite hf with toFun := f ∘ MulOpposite.unop }
Semiring homomorphism from multiplicative opposite induced by commuting homomorphism
Informal description
Given a semiring homomorphism \( f \colon R \to S \) between semirings \( R \) and \( S \) such that \( f(x) \) commutes with \( f(y) \) for all \( x, y \in R \), there exists a semiring homomorphism from the multiplicative opposite \( R^\text{op} \) to \( S \) defined by composing \( f \) with the canonical projection \( \text{unop} \colon R^\text{op} \to R \).
RingHom.op definition
{R S} [NonAssocSemiring R] [NonAssocSemiring S] : (R →+* S) ≃ (Rᵐᵒᵖ →+* Sᵐᵒᵖ)
Full source 
/-- A ring hom `R →+* S` can equivalently be viewed as a ring hom `Rᵐᵒᵖ →+* Sᵐᵒᵖ`. This is the
action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms. -/
@[simps!]
def RingHom.op {R S} [NonAssocSemiring R] [NonAssocSemiring S] :
    (R →+* S) ≃ (Rᵐᵒᵖ →+* Sᵐᵒᵖ) where
  toFun f := { AddMonoidHom.mulOp f.toAddMonoidHom, MonoidHom.op f.toMonoidHom with }
  invFun f := { AddMonoidHom.mulUnop f.toAddMonoidHom, MonoidHom.unop f.toMonoidHom with }
  left_inv _ := rfl
  right_inv _ := rfl
Ring homomorphism equivalence via opposites
Informal description
The equivalence between ring homomorphisms $R \to^* S$ and ring homomorphisms $R^\text{op} \to^* S^\text{op}$, where $R^\text{op}$ denotes the multiplicative opposite of $R$. Specifically, this defines: 1. A function that takes a ring homomorphism $f: R \to S$ and constructs a ring homomorphism $f^\text{op}: R^\text{op} \to S^\text{op}$ by composing with the opposite operations. 2. An inverse function that reverses this process. 3. Proofs that these operations are mutual inverses.
RingHom.unop definition
{R S} [NonAssocSemiring R] [NonAssocSemiring S] : (Rᵐᵒᵖ →+* Sᵐᵒᵖ) ≃ (R →+* S)
Full source 
/-- The 'unopposite' of a ring hom `Rᵐᵒᵖ →+* Sᵐᵒᵖ`. Inverse to `RingHom.op`. -/
@[simp]
def RingHom.unop {R S} [NonAssocSemiring R] [NonAssocSemiring S] : (Rᵐᵒᵖ →+* Sᵐᵒᵖ) ≃ (R →+* S) :=
  RingHom.op.symm
Inverse of the ring homomorphism opposite equivalence
Informal description
The inverse of the equivalence `RingHom.op`, which converts a ring homomorphism between multiplicative opposites $R^\text{op} \to^* S^\text{op}$ back to a ring homomorphism between the original rings $R \to^* S$.