# Documentation

Mathlib.Algebra.Ring.Opposite

# Ring structures on the multiplicative opposite #

instance MulOpposite.distrib (α : Type u) [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance MulOpposite.mulZeroClass (α : Type u) [inst : ] :
Equations
instance MulOpposite.mulZeroOneClass (α : Type u) [inst : ] :
Equations
instance MulOpposite.semigroupWithZero (α : Type u) [inst : ] :
Equations
instance MulOpposite.monoidWithZero (α : Type u) [inst : ] :
Equations
instance MulOpposite.nonUnitalNonAssocSemiring (α : Type u) [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance MulOpposite.nonUnitalSemiring (α : Type u) [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance MulOpposite.nonAssocSemiring (α : Type u) [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance MulOpposite.semiring (α : Type u) [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance MulOpposite.nonUnitalCommSemiring (α : Type u) [inst : ] :
Equations
instance MulOpposite.commSemiring (α : Type u) [inst : ] :
Equations
instance MulOpposite.nonUnitalNonAssocRing (α : Type u) [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance MulOpposite.nonUnitalRing (α : Type u) [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance MulOpposite.nonAssocRing (α : Type u) [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance MulOpposite.ring (α : Type u) [inst : Ring α] :
Equations
instance MulOpposite.nonUnitalCommRing (α : Type u) [inst : ] :
Equations
instance MulOpposite.commRing (α : Type u) [inst : ] :
Equations
instance MulOpposite.noZeroDivisors (α : Type u) [inst : Zero α] [inst : Mul α] [inst : ] :
Equations
instance MulOpposite.isDomain (α : Type u) [inst : Ring α] [inst : ] :
Equations
instance MulOpposite.groupWithZero (α : Type u) [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance AddOpposite.distrib (α : Type u) [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance AddOpposite.mulZeroClass (α : Type u) [inst : ] :
Equations
instance AddOpposite.mulZeroOneClass (α : Type u) [inst : ] :
Equations
instance AddOpposite.semigroupWithZero (α : Type u) [inst : ] :
Equations
instance AddOpposite.monoidWithZero (α : Type u) [inst : ] :
Equations
instance AddOpposite.nonUnitalNonAssocSemiring (α : Type u) [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance AddOpposite.nonUnitalSemiring (α : Type u) [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance AddOpposite.nonAssocSemiring (α : Type u) [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance AddOpposite.semiring (α : Type u) [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance AddOpposite.nonUnitalCommSemiring (α : Type u) [inst : ] :
Equations
instance AddOpposite.commSemiring (α : Type u) [inst : ] :
Equations
instance AddOpposite.nonUnitalNonAssocRing (α : Type u) [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance AddOpposite.nonUnitalRing (α : Type u) [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance AddOpposite.nonAssocRing (α : Type u) [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance AddOpposite.ring (α : Type u) [inst : Ring α] :
Equations
instance AddOpposite.nonUnitalCommRing (α : Type u) [inst : ] :
Equations
instance AddOpposite.commRing (α : Type u) [inst : ] :
Equations
instance AddOpposite.noZeroDivisors (α : Type u) [inst : Zero α] [inst : Mul α] [inst : ] :
Equations
instance AddOpposite.isDomain (α : Type u) [inst : Ring α] [inst : ] :
Equations
instance AddOpposite.groupWithZero (α : Type u) [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem NonUnitalRingHom.toOpposite_apply {R : Type u_1} {S : Type u_2} [inst : ] [inst : ] (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) :
↑() = MulOpposite.op f
def NonUnitalRingHom.toOpposite {R : Type u_1} {S : Type u_2} [inst : ] [inst : ] (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) :

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ᵐᵒᵖ.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem NonUnitalRingHom.fromOpposite_apply {R : Type u_1} {S : Type u_2} [inst : ] [inst : ] (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) :
↑() = f MulOpposite.unop
def NonUnitalRingHom.fromOpposite {R : Type u_1} {S : Type u_2} [inst : ] [inst : ] (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) :

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ᵐᵒᵖ.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem NonUnitalRingHom.op_symm_apply_apply {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (f : ) :
∀ (a : α), ↑(↑(Equiv.symm NonUnitalRingHom.op) f) a = ZeroHom.toFun (↑(AddMonoidHom.mulUnop ())) a
@[simp]
theorem NonUnitalRingHom.op_apply_apply {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (f : α →ₙ+* β) :
∀ (a : αᵐᵒᵖ), ↑(NonUnitalRingHom.op f) a = ZeroHom.toFun (↑(AddMonoidHom.mulOp ())) a
def NonUnitalRingHom.op {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] :
(α →ₙ+* β) ()

A non-unital ring hom α →ₙ+* β can equivalently be viewed as a non-unital ring hom αᵐᵒᵖ →+* βᵐᵒᵖ. This is the action of the (fully faithful) ᵐᵒᵖ-functor on morphisms.

Equations
• One or more equations did not get rendered due to their size.
def NonUnitalRingHom.unop {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] :
() (α →ₙ+* β)

The 'unopposite' of a non-unital ring hom αᵐᵒᵖ →ₙ+* βᵐᵒᵖ. Inverse to NonUnitalRingHom.op.

Equations
@[simp]
theorem RingHom.toOpposite_apply {R : Type u_1} {S : Type u_2} [inst : ] [inst : ] (f : R →+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) :
↑() = MulOpposite.op f
def RingHom.toOpposite {R : Type u_1} {S : Type u_2} [inst : ] [inst : ] (f : R →+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) :

A ring homomorphism f : R →+* S such that f x commutes with f y for all x, y defines a ring homomorphism to Sᵐᵒᵖ.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem RingHom.fromOpposite_apply {R : Type u_1} {S : Type u_2} [inst : ] [inst : ] (f : R →+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) :
↑() = f MulOpposite.unop
def RingHom.fromOpposite {R : Type u_1} {S : Type u_2} [inst : ] [inst : ] (f : R →+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) :

A ring homomorphism f : R →+* S such that f x commutes with f y for all x, y defines a ring homomorphism from Rᵐᵒᵖ.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem RingHom.op_apply_apply_unop {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (f : α →+* β) :
∀ (a : αᵐᵒᵖ), (↑(RingHom.op f) a).unop = f a.unop
@[simp]
theorem RingHom.op_symm_apply_apply {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (f : ) :
∀ (a : α), ↑(↑(Equiv.symm RingHom.op) f) a = (f { unop := a }).unop
def RingHom.op {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] :
(α →+* β) ()

A ring hom α →+* β can equivalently be viewed as a ring hom αᵐᵒᵖ →+* βᵐᵒᵖ. This is the action of the (fully faithful) ᵐᵒᵖ-functor on morphisms.

Equations
• One or more equations did not get rendered due to their size.
def RingHom.unop {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] :
() (α →+* β)

The 'unopposite' of a ring hom αᵐᵒᵖ →+* βᵐᵒᵖ. Inverse to RingHom.op.

Equations