Documentation

Mathlib.Algebra.Ring.Opposite

Ring structures on the multiplicative opposite #

instance MulOpposite.distrib (α : Type u) [Distrib α] :

Distrib αᵐᵒᵖ

instance MulOpposite.mulZeroClass (α : Type u) [MulZeroClass α] :

MulZeroClass αᵐᵒᵖ

instance MulOpposite.mulZeroOneClass (α : Type u) [MulZeroOneClass α] :

MulZeroOneClass αᵐᵒᵖ

instance MulOpposite.semigroupWithZero (α : Type u) [SemigroupWithZero α] :

SemigroupWithZero αᵐᵒᵖ

instance MulOpposite.monoidWithZero (α : Type u) [MonoidWithZero α] :

MonoidWithZero αᵐᵒᵖ

instance MulOpposite.nonUnitalNonAssocSemiring (α : Type u) [NonUnitalNonAssocSemiring α] :

NonUnitalNonAssocSemiring αᵐᵒᵖ

instance MulOpposite.nonUnitalSemiring (α : Type u) [NonUnitalSemiring α] :

NonUnitalSemiring αᵐᵒᵖ

instance MulOpposite.nonAssocSemiring (α : Type u) [NonAssocSemiring α] :

NonAssocSemiring αᵐᵒᵖ

instance MulOpposite.semiring (α : Type u) [Semiring α] :

Semiring αᵐᵒᵖ

instance MulOpposite.nonUnitalCommSemiring (α : Type u) [NonUnitalCommSemiring α] :

NonUnitalCommSemiring αᵐᵒᵖ

instance MulOpposite.commSemiring (α : Type u) [CommSemiring α] :

CommSemiring αᵐᵒᵖ

instance MulOpposite.nonUnitalNonAssocRing (α : Type u) [NonUnitalNonAssocRing α] :

NonUnitalNonAssocRing αᵐᵒᵖ

instance MulOpposite.nonUnitalRing (α : Type u) [NonUnitalRing α] :

NonUnitalRing αᵐᵒᵖ

instance MulOpposite.nonAssocRing (α : Type u) [NonAssocRing α] :

NonAssocRing αᵐᵒᵖ

instance MulOpposite.ring (α : Type u) [Ring α] :

Ring αᵐᵒᵖ

instance MulOpposite.nonUnitalCommRing (α : Type u) [NonUnitalCommRing α] :

NonUnitalCommRing αᵐᵒᵖ

instance MulOpposite.commRing (α : Type u) [CommRing α] :

CommRing αᵐᵒᵖ

instance MulOpposite.noZeroDivisors (α : Type u) [Zero α] [Mul α] [NoZeroDivisors α] :

NoZeroDivisors αᵐᵒᵖ

instance MulOpposite.isDomain (α : Type u) [Ring α] [IsDomain α] :

IsDomain αᵐᵒᵖ

instance MulOpposite.groupWithZero (α : Type u) [GroupWithZero α] :

GroupWithZero αᵐᵒᵖ

instance AddOpposite.distrib (α : Type u) [Distrib α] :

Distrib αᵃᵒᵖ

instance AddOpposite.mulZeroClass (α : Type u) [MulZeroClass α] :

MulZeroClass αᵃᵒᵖ

instance AddOpposite.mulZeroOneClass (α : Type u) [MulZeroOneClass α] :

MulZeroOneClass αᵃᵒᵖ

instance AddOpposite.semigroupWithZero (α : Type u) [SemigroupWithZero α] :

SemigroupWithZero αᵃᵒᵖ

instance AddOpposite.monoidWithZero (α : Type u) [MonoidWithZero α] :

MonoidWithZero αᵃᵒᵖ

instance AddOpposite.nonUnitalNonAssocSemiring (α : Type u) [NonUnitalNonAssocSemiring α] :

NonUnitalNonAssocSemiring αᵃᵒᵖ

instance AddOpposite.nonUnitalSemiring (α : Type u) [NonUnitalSemiring α] :

NonUnitalSemiring αᵃᵒᵖ

instance AddOpposite.nonAssocSemiring (α : Type u) [NonAssocSemiring α] :

NonAssocSemiring αᵃᵒᵖ

instance AddOpposite.semiring (α : Type u) [Semiring α] :

Semiring αᵃᵒᵖ

instance AddOpposite.nonUnitalCommSemiring (α : Type u) [NonUnitalCommSemiring α] :

NonUnitalCommSemiring αᵃᵒᵖ

instance AddOpposite.commSemiring (α : Type u) [CommSemiring α] :

CommSemiring αᵃᵒᵖ

instance AddOpposite.nonUnitalNonAssocRing (α : Type u) [NonUnitalNonAssocRing α] :

NonUnitalNonAssocRing αᵃᵒᵖ

instance AddOpposite.nonUnitalRing (α : Type u) [NonUnitalRing α] :

NonUnitalRing αᵃᵒᵖ

instance AddOpposite.nonAssocRing (α : Type u) [NonAssocRing α] :

NonAssocRing αᵃᵒᵖ

instance AddOpposite.ring (α : Type u) [Ring α] :

Ring αᵃᵒᵖ

instance AddOpposite.nonUnitalCommRing (α : Type u) [NonUnitalCommRing α] :

NonUnitalCommRing αᵃᵒᵖ

instance AddOpposite.commRing (α : Type u) [CommRing α] :

CommRing αᵃᵒᵖ

instance AddOpposite.noZeroDivisors (α : Type u) [Zero α] [Mul α] [NoZeroDivisors α] :

NoZeroDivisors αᵃᵒᵖ

instance AddOpposite.isDomain (α : Type u) [Ring α] [IsDomain α] :

IsDomain αᵃᵒᵖ

instance AddOpposite.groupWithZero (α : Type u) [GroupWithZero α] :

GroupWithZero αᵃᵒᵖ

@[simp]

theorem NonUnitalRingHom.toOpposite_apply {R : Type u_1} {S : Type u_2} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (↑f x) (↑f y)) :

↑(NonUnitalRingHom.toOpposite f hf) = MulOpposite.op ∘ ↑f

def NonUnitalRingHom.toOpposite {R : Type u_1} {S : Type u_2} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (↑f x) (↑f y)) :

R →ₙ+* Sᵐᵒᵖ

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

Instances For

@[simp]

theorem NonUnitalRingHom.fromOpposite_apply {R : Type u_1} {S : Type u_2} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (↑f x) (↑f y)) :

↑(NonUnitalRingHom.fromOpposite f hf) = ↑f ∘ MulOpposite.unop

def NonUnitalRingHom.fromOpposite {R : Type u_1} {S : Type u_2} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (↑f x) (↑f y)) :

Rᵐᵒᵖ →ₙ+* S

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

Instances For

@[simp]

theorem NonUnitalRingHom.op_apply_apply {α : Type u_1} {β : Type u_2} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) :

∀ (a : αᵐᵒᵖ), ↑(↑NonUnitalRingHom.op f) a = ZeroHom.toFun (↑(↑AddMonoidHom.mulOp (NonUnitalRingHom.toAddMonoidHom f))) a

@[simp]

theorem NonUnitalRingHom.op_symm_apply_apply {α : Type u_1} {β : Type u_2} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : αᵐᵒᵖ →ₙ+* βᵐᵒᵖ) :

∀ (a : α), ↑(↑NonUnitalRingHom.op.symm f) a = ZeroHom.toFun (↑(↑AddMonoidHom.mulUnop (NonUnitalRingHom.toAddMonoidHom f))) a

def NonUnitalRingHom.op {α : Type u_1} {β : Type u_2} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] :

(α →ₙ+* β) ≃ (αᵐᵒᵖ →ₙ+* βᵐᵒᵖ)

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.

Instances For

def NonUnitalRingHom.unop {α : Type u_1} {β : Type u_2} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] :

(αᵐᵒᵖ →ₙ+* βᵐᵒᵖ) ≃ (α →ₙ+* β)

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

Instances For

@[simp]

theorem RingHom.toOpposite_apply {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (hf : ∀ (x y : R), Commute (↑f x) (↑f y)) :

↑(RingHom.toOpposite f hf) = MulOpposite.op ∘ ↑f

def RingHom.toOpposite {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (hf : ∀ (x y : R), Commute (↑f x) (↑f y)) :

R →+* Sᵐᵒᵖ

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

Instances For

@[simp]

theorem RingHom.fromOpposite_apply {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (hf : ∀ (x y : R), Commute (↑f x) (↑f y)) :

↑(RingHom.fromOpposite f hf) = ↑f ∘ MulOpposite.unop

def RingHom.fromOpposite {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (hf : ∀ (x y : R), Commute (↑f x) (↑f y)) :

Rᵐᵒᵖ →+* S

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

Instances For

@[simp]

theorem RingHom.op_symm_apply_apply {α : Type u_1} {β : Type u_2} [NonAssocSemiring α] [NonAssocSemiring β] (f : αᵐᵒᵖ →+* βᵐᵒᵖ) :

∀ (a : α), ↑(↑RingHom.op.symm f) a = MulOpposite.unop (↑f (MulOpposite.op a))

@[simp]

theorem RingHom.op_apply_apply {α : Type u_1} {β : Type u_2} [NonAssocSemiring α] [NonAssocSemiring β] (f : α →+* β) :

∀ (a : αᵐᵒᵖ), ↑(↑RingHom.op f) a = MulOpposite.op (↑f (MulOpposite.unop a))

def RingHom.op {α : Type u_1} {β : Type u_2} [NonAssocSemiring α] [NonAssocSemiring β] :

(α →+* β) ≃ (αᵐᵒᵖ →+* βᵐᵒᵖ)

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

Instances For

def RingHom.unop {α : Type u_1} {β : Type u_2} [NonAssocSemiring α] [NonAssocSemiring β] :

(αᵐᵒᵖ →+* βᵐᵒᵖ) ≃ (α →+* β)

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

Instances For