mathlib documentation

algebra.ring.opposite

Ring structures on the multiplicative opposite #

@[protected, instance]
def mul_opposite.distrib (α : Type u) [distrib α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
def mul_opposite.is_domain (α : Type u) [ring α] [is_domain α] :
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 monoid homomorphism f : R →* S such that f x commutes with f y for all x, y defines a monoid homomorphism from Rᵐᵒᵖ.

Equations
@[simp]
theorem ring_hom.op_apply_apply {α : Type u_1} {β : Type u_2} [non_assoc_semiring α] [non_assoc_semiring β] (f : α →+* β) (ᾰ : αᵐᵒᵖ) :
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]
theorem ring_hom.op_symm_apply_apply {α : Type u_1} {β : Type u_2} [non_assoc_semiring α] [non_assoc_semiring β] (f : αᵐᵒᵖ →+* βᵐᵒᵖ) (ᾰ : α) :
@[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