mathlib documentation

algebra.ring.opposite

Ring structures on the multiplicative opposite #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]

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

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

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
@[simp]

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

Equations
def ring_hom.to_opposite {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (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
@[simp]
theorem ring_hom.to_opposite_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)) :
@[simp]
theorem ring_hom.from_opposite_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)) :
def ring_hom.from_opposite {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (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
@[simp]
def ring_hom.op {α : Type u_1} {β : Type u_2} [non_assoc_semiring α] [non_assoc_semiring β] :

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

Equations
@[simp]
def ring_hom.unop {α : Type u_1} {β : Type u_2} [non_assoc_semiring α] [non_assoc_semiring β] :

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

Equations