# mathlibdocumentation

algebra.ring.opposite

# Ring structures on the multiplicative opposite #

@[protected, instance]
def mul_opposite.distrib (α : Type u) [distrib α] :
Equations
@[protected, instance]
def mul_opposite.mul_zero_class (α : Type u)  :
Equations
@[protected, instance]
def mul_opposite.mul_zero_one_class (α : Type u)  :
Equations
@[protected, instance]
def mul_opposite.semigroup_with_zero (α : Type u)  :
Equations
@[protected, instance]
def mul_opposite.monoid_with_zero (α : Type u)  :
Equations
@[protected, instance]
Equations
@[protected, instance]
def mul_opposite.non_unital_semiring (α : Type u)  :
Equations
@[protected, instance]
def mul_opposite.non_assoc_semiring (α : Type u)  :
Equations
@[protected, instance]
def mul_opposite.semiring (α : Type u) [semiring α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def mul_opposite.comm_semiring (α : Type u)  :
Equations
@[protected, instance]
Equations
@[protected, instance]
def mul_opposite.non_unital_ring (α : Type u)  :
Equations
@[protected, instance]
def mul_opposite.non_assoc_ring (α : Type u)  :
Equations
@[protected, instance]
def mul_opposite.ring (α : Type u) [ring α] :
Equations
@[protected, instance]
def mul_opposite.non_unital_comm_ring (α : Type u)  :
Equations
@[protected, instance]
def mul_opposite.comm_ring (α : Type u) [comm_ring α] :
Equations
@[protected, instance]
def mul_opposite.no_zero_divisors (α : Type u) [has_zero α] [has_mul α]  :
@[protected, instance]
def mul_opposite.is_domain (α : Type u) [ring α] [is_domain α] :
@[protected, instance]
def mul_opposite.group_with_zero (α : Type u)  :
Equations
@[protected, instance]
def add_opposite.distrib (α : Type u) [distrib α] :
Equations
@[protected, instance]
def add_opposite.mul_zero_class (α : Type u)  :
Equations
@[protected, instance]
def add_opposite.mul_zero_one_class (α : Type u)  :
Equations
@[protected, instance]
def add_opposite.semigroup_with_zero (α : Type u)  :
Equations
@[protected, instance]
def add_opposite.monoid_with_zero (α : Type u)  :
Equations
@[protected, instance]
Equations
@[protected, instance]
def add_opposite.non_unital_semiring (α : Type u)  :
Equations
@[protected, instance]
def add_opposite.non_assoc_semiring (α : Type u)  :
Equations
@[protected, instance]
def add_opposite.semiring (α : Type u) [semiring α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def add_opposite.comm_semiring (α : Type u)  :
Equations
@[protected, instance]
Equations
@[protected, instance]
def add_opposite.non_unital_ring (α : Type u)  :
Equations
@[protected, instance]
def add_opposite.non_assoc_ring (α : Type u)  :
Equations
@[protected, instance]
def add_opposite.ring (α : Type u) [ring α] :
Equations
@[protected, instance]
def add_opposite.non_unital_comm_ring (α : Type u)  :
Equations
@[protected, instance]
def add_opposite.comm_ring (α : Type u) [comm_ring α] :
Equations
@[protected, instance]
def add_opposite.no_zero_divisors (α : Type u) [has_zero α] [has_mul α]  :
@[protected, instance]
def add_opposite.is_domain (α : Type u) [ring α] [is_domain α] :
@[protected, instance]
def add_opposite.group_with_zero (α : Type u)  :
Equations
def non_unital_ring_hom.to_opposite {R : Type u_1} {S : Type u_2} (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
@[simp]
theorem non_unital_ring_hom.to_opposite_to_fun {R : Type u_1} {S : Type u_2} (f : R →ₙ+* S) (hf : ∀ (x y : R), commute (f x) (f y)) :
def non_unital_ring_hom.from_opposite {R : Type u_1} {S : Type u_2} (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
@[simp]
theorem non_unital_ring_hom.from_opposite_to_fun {R : Type u_1} {S : Type u_2} (f : R →ₙ+* S) (hf : ∀ (x y : R), commute (f x) (f y)) :
@[simp]
theorem non_unital_ring_hom.op_symm_apply_to_fun {α : Type u_1} {β : Type u_2} (f : αᵐᵒᵖ →ₙ+* βᵐᵒᵖ) (ᾰ : α) :
def non_unital_ring_hom.op {α : Type u_1} {β : Type u_2}  :

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]
theorem non_unital_ring_hom.op_apply_to_fun {α : Type u_1} {β : Type u_2} (f : α →ₙ+* β) (ᾰ : αᵐᵒᵖ) :
@[simp]
def non_unital_ring_hom.unop {α : Type u_1} {β : Type u_2}  :

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]
theorem ring_hom.op_apply_apply {α : Type u_1} {β : Type u_2} (f : α →+* β) (ᾰ : αᵐᵒᵖ) :
def ring_hom.op {α : Type u_1} {β : Type u_2}  :

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

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

Equations