mathlib3 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.

source
@[protected, instance]
def mul_opposite.distrib (α : Type u) [distrib α] :
distrib αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.mul_zero_class (α : Type u) [mul_zero_class α] :
mul_zero_class αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.mul_zero_one_class (α : Type u) [mul_zero_one_class α] :
mul_zero_one_class αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.semigroup_with_zero (α : Type u) [semigroup_with_zero α] :
semigroup_with_zero αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.monoid_with_zero (α : Type u) [monoid_with_zero α] :
monoid_with_zero αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.non_unital_non_assoc_semiring (α : Type u) [non_unital_non_assoc_semiring α] :
non_unital_non_assoc_semiring αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.non_unital_semiring (α : Type u) [non_unital_semiring α] :
non_unital_semiring αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.non_assoc_semiring (α : Type u) [non_assoc_semiring α] :
non_assoc_semiring αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.semiring (α : Type u) [semiring α] :
semiring αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.non_unital_comm_semiring (α : Type u) [non_unital_comm_semiring α] :
non_unital_comm_semiring αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.comm_semiring (α : Type u) [comm_semiring α] :
comm_semiring αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.non_unital_non_assoc_ring (α : Type u) [non_unital_non_assoc_ring α] :
non_unital_non_assoc_ring αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.non_unital_ring (α : Type u) [non_unital_ring α] :
non_unital_ring αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.non_assoc_ring (α : Type u) [non_assoc_ring α] :
non_assoc_ring αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.ring (α : Type u) [ring α] :
ring αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.non_unital_comm_ring (α : Type u) [non_unital_comm_ring α] :
non_unital_comm_ring αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.comm_ring (α : Type u) [comm_ring α] :
comm_ring αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.no_zero_divisors (α : Type u) [has_zero α] [has_mul α] [no_zero_divisors α] :
no_zero_divisors αᵐᵒᵖ
source
@[protected, instance]
def mul_opposite.is_domain (α : Type u) [ring α] [is_domain α] :
is_domain αᵐᵒᵖ
source
@[protected, instance]
def mul_opposite.group_with_zero (α : Type u) [group_with_zero α] :
group_with_zero αᵐᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.distrib (α : Type u) [distrib α] :
distrib αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.mul_zero_class (α : Type u) [mul_zero_class α] :
mul_zero_class αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.mul_zero_one_class (α : Type u) [mul_zero_one_class α] :
mul_zero_one_class αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.semigroup_with_zero (α : Type u) [semigroup_with_zero α] :
semigroup_with_zero αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.monoid_with_zero (α : Type u) [monoid_with_zero α] :
monoid_with_zero αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.non_unital_non_assoc_semiring (α : Type u) [non_unital_non_assoc_semiring α] :
non_unital_non_assoc_semiring αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.non_unital_semiring (α : Type u) [non_unital_semiring α] :
non_unital_semiring αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.non_assoc_semiring (α : Type u) [non_assoc_semiring α] :
non_assoc_semiring αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.semiring (α : Type u) [semiring α] :
semiring αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.non_unital_comm_semiring (α : Type u) [non_unital_comm_semiring α] :
non_unital_comm_semiring αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.comm_semiring (α : Type u) [comm_semiring α] :
comm_semiring αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.non_unital_non_assoc_ring (α : Type u) [non_unital_non_assoc_ring α] :
non_unital_non_assoc_ring αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.non_unital_ring (α : Type u) [non_unital_ring α] :
non_unital_ring αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.non_assoc_ring (α : Type u) [non_assoc_ring α] :
non_assoc_ring αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.ring (α : Type u) [ring α] :
ring αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.non_unital_comm_ring (α : Type u) [non_unital_comm_ring α] :
non_unital_comm_ring αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.comm_ring (α : Type u) [comm_ring α] :
comm_ring αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.no_zero_divisors (α : Type u) [has_zero α] [has_mul α] [no_zero_divisors α] :
no_zero_divisors αᵃᵒᵖ
source
@[protected, instance]
def add_opposite.is_domain (α : Type u) [ring α] [is_domain α] :
is_domain αᵃᵒᵖ
source
@[protected, instance]
def add_opposite.group_with_zero (α : Type u) [group_with_zero α] :
group_with_zero αᵃᵒᵖ
Equations
source
def non_unital_ring_hom.to_opposite {R : Type u_1} {S : Type u_2} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring 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ᵐᵒᵖ.

Equations
source
@[simp]
theorem non_unital_ring_hom.to_opposite_to_fun {R : Type u_1} {S : Type u_2} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] (f : R →ₙ+* S) (hf : ∀ (x y : R), commute (⇑f x) (⇑f y)) :
⇑(f.to_opposite hf) = mul_opposite.op ∘ ⇑f
source
def non_unital_ring_hom.from_opposite {R : Type u_1} {S : Type u_2} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring 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ᵐᵒᵖ.

Equations
source
@[simp]
theorem non_unital_ring_hom.from_opposite_to_fun {R : Type u_1} {S : Type u_2} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] (f : R →ₙ+* S) (hf : ∀ (x y : R), commute (⇑f x) (⇑f y)) :
⇑(f.from_opposite hf) = ⇑f ∘ mul_opposite.unop
source
@[simp]
theorem non_unital_ring_hom.op_symm_apply_to_fun {α : Type u_1} {β : Type u_2} [non_unital_non_assoc_semiring α] [non_unital_non_assoc_semiring β] (f : αᵐᵒᵖ →ₙ+* βᵐᵒᵖ) (ᾰ : α) :
⇑(⇑(non_unital_ring_hom.op.symm) f) ᾰ = (⇑add_monoid_hom.mul_unop f.to_add_monoid_hom).to_fun ᾰ
source
def non_unital_ring_hom.op {α : Type u_1} {β : Type u_2} [non_unital_non_assoc_semiring α] [non_unital_non_assoc_semiring β] :
(α →ₙ+* β) ≃ (αᵐᵒᵖ →ₙ+* βᵐᵒᵖ)

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
source
@[simp]
theorem non_unital_ring_hom.op_apply_to_fun {α : Type u_1} {β : Type u_2} [non_unital_non_assoc_semiring α] [non_unital_non_assoc_semiring β] (f : α →ₙ+* β) (ᾰ : αᵐᵒᵖ) :
⇑(⇑non_unital_ring_hom.op f) ᾰ = (⇑add_monoid_hom.mul_op f.to_add_monoid_hom).to_fun ᾰ
source
@[simp]
def non_unital_ring_hom.unop {α : Type u_1} {β : Type u_2} [non_unital_non_assoc_semiring α] [non_unital_non_assoc_semiring β] :
(αᵐᵒᵖ →ₙ+* βᵐᵒᵖ) ≃ (α →ₙ+* β)

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

Equations
source
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)) :
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ᵐᵒᵖ.

Equations
source
@[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)) :
⇑(f.to_opposite hf) = mul_opposite.op ∘ ⇑f
source
@[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)) :
⇑(f.from_opposite hf) = ⇑f ∘ mul_opposite.unop
source
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)) :
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ᵐᵒᵖ.

Equations
source
@[simp]
theorem ring_hom.op_apply_apply {α : Type u_1} {β : Type u_2} [non_assoc_semiring α] [non_assoc_semiring β] (f : α →+* β) (ᾰ : αᵐᵒᵖ) :
⇑(⇑ring_hom.op f) ᾰ = (⇑add_monoid_hom.mul_op f.to_add_monoid_hom).to_fun ᾰ
source
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
source
@[simp]
theorem ring_hom.op_symm_apply_apply {α : Type u_1} {β : Type u_2} [non_assoc_semiring α] [non_assoc_semiring β] (f : αᵐᵒᵖ →+* βᵐᵒᵖ) (ᾰ : α) :
⇑(⇑(ring_hom.op.symm) f) ᾰ = (⇑add_monoid_hom.mul_unop f.to_add_monoid_hom).to_fun ᾰ
source
@[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