mathlib documentation

algebra.ring.opposite

Ring structures on the multiplicative opposite #

@[protected, instance]

def mul_opposite.distrib (α : Type u) [distrib α] :

distrib αᵐᵒᵖ

Equations

mul_opposite.distrib α = {mul := has_mul.mul (mul_opposite.has_mul α), add := has_add.add (mul_opposite.has_add α), left_distrib := _, right_distrib := _}

@[protected, instance]

def mul_opposite.mul_zero_class (α : Type u) [mul_zero_class α] :

mul_zero_class αᵐᵒᵖ

Equations

mul_opposite.mul_zero_class α = {mul := has_mul.mul (mul_opposite.has_mul α), zero := 0, zero_mul := _, mul_zero := _}

@[protected, instance]

def mul_opposite.mul_zero_one_class (α : Type u) [mul_zero_one_class α] :

mul_zero_one_class αᵐᵒᵖ

Equations

mul_opposite.mul_zero_one_class α = {one := mul_one_class.one (mul_opposite.mul_one_class α), mul := mul_zero_class.mul (mul_opposite.mul_zero_class α), one_mul := _, mul_one := _, zero := mul_zero_class.zero (mul_opposite.mul_zero_class α), zero_mul := _, mul_zero := _}

@[protected, instance]

def mul_opposite.semigroup_with_zero (α : Type u) [semigroup_with_zero α] :

semigroup_with_zero αᵐᵒᵖ

Equations

mul_opposite.semigroup_with_zero α = {mul := semigroup.mul (mul_opposite.semigroup α), mul_assoc := _, zero := mul_zero_class.zero (mul_opposite.mul_zero_class α), zero_mul := _, mul_zero := _}

@[protected, instance]

def mul_opposite.monoid_with_zero (α : Type u) [monoid_with_zero α] :

monoid_with_zero αᵐᵒᵖ

Equations

mul_opposite.monoid_with_zero α = {mul := monoid.mul (mul_opposite.monoid α), mul_assoc := _, one := monoid.one (mul_opposite.monoid α), one_mul := _, mul_one := _, npow := monoid.npow (mul_opposite.monoid α), npow_zero' := _, npow_succ' := _, zero := mul_zero_one_class.zero (mul_opposite.mul_zero_one_class α), zero_mul := _, mul_zero := _}

@[protected, instance]

def mul_opposite.non_unital_non_assoc_semiring (α : Type u) [non_unital_non_assoc_semiring α] :

non_unital_non_assoc_semiring αᵐᵒᵖ

Equations

mul_opposite.non_unital_non_assoc_semiring α = {add := add_comm_monoid.add (mul_opposite.add_comm_monoid α), add_assoc := _, zero := add_comm_monoid.zero (mul_opposite.add_comm_monoid α), zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul (mul_opposite.add_comm_monoid α), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := mul_zero_class.mul (mul_opposite.mul_zero_class α), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _}

@[protected, instance]

def mul_opposite.non_unital_semiring (α : Type u) [non_unital_semiring α] :

non_unital_semiring αᵐᵒᵖ

Equations

mul_opposite.non_unital_semiring α = {add := non_unital_non_assoc_semiring.add (mul_opposite.non_unital_non_assoc_semiring α), add_assoc := _, zero := semigroup_with_zero.zero (mul_opposite.semigroup_with_zero α), zero_add := _, add_zero := _, nsmul := non_unital_non_assoc_semiring.nsmul (mul_opposite.non_unital_non_assoc_semiring α), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semigroup_with_zero.mul (mul_opposite.semigroup_with_zero α), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _}

@[protected, instance]

def mul_opposite.non_assoc_semiring (α : Type u) [non_assoc_semiring α] :

non_assoc_semiring αᵐᵒᵖ

Equations

mul_opposite.non_assoc_semiring α = {add := non_unital_non_assoc_semiring.add (mul_opposite.non_unital_non_assoc_semiring α), add_assoc := _, zero := mul_zero_one_class.zero (mul_opposite.mul_zero_one_class α), zero_add := _, add_zero := _, nsmul := non_unital_non_assoc_semiring.nsmul (mul_opposite.non_unital_non_assoc_semiring α), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := mul_zero_one_class.mul (mul_opposite.mul_zero_one_class α), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, one := mul_zero_one_class.one (mul_opposite.mul_zero_one_class α), one_mul := _, mul_one := _}

@[protected, instance]

def mul_opposite.semiring (α : Type u) [semiring α] :

semiring αᵐᵒᵖ

Equations

mul_opposite.semiring α = {add := non_unital_semiring.add (mul_opposite.non_unital_semiring α), add_assoc := _, zero := non_unital_semiring.zero (mul_opposite.non_unital_semiring α), zero_add := _, add_zero := _, nsmul := non_unital_semiring.nsmul (mul_opposite.non_unital_semiring α), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := non_unital_semiring.mul (mul_opposite.non_unital_semiring α), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := non_assoc_semiring.one (mul_opposite.non_assoc_semiring α), one_mul := _, mul_one := _, npow := monoid_with_zero.npow (mul_opposite.monoid_with_zero α), npow_zero' := _, npow_succ' := _}

@[protected, instance]

def mul_opposite.comm_semiring (α : Type u) [comm_semiring α] :

comm_semiring αᵐᵒᵖ

Equations

mul_opposite.comm_semiring α = {add := semiring.add (mul_opposite.semiring α), add_assoc := _, zero := semiring.zero (mul_opposite.semiring α), zero_add := _, add_zero := _, nsmul := semiring.nsmul (mul_opposite.semiring α), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul (mul_opposite.semiring α), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := semiring.one (mul_opposite.semiring α), one_mul := _, mul_one := _, npow := semiring.npow (mul_opposite.semiring α), npow_zero' := _, npow_succ' := _, mul_comm := _}

@[protected, instance]

def mul_opposite.ring (α : Type u) [ring α] :

ring αᵐᵒᵖ

Equations

mul_opposite.ring α = {add := add_comm_group.add (mul_opposite.add_comm_group α), add_assoc := _, zero := add_comm_group.zero (mul_opposite.add_comm_group α), zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul (mul_opposite.add_comm_group α), nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg (mul_opposite.add_comm_group α), sub := add_comm_group.sub (mul_opposite.add_comm_group α), sub_eq_add_neg := _, zsmul := add_comm_group.zsmul (mul_opposite.add_comm_group α), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := monoid.mul (mul_opposite.monoid α), mul_assoc := _, one := monoid.one (mul_opposite.monoid α), one_mul := _, mul_one := _, npow := monoid.npow (mul_opposite.monoid α), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}

@[protected, instance]

def mul_opposite.comm_ring (α : Type u) [comm_ring α] :

comm_ring αᵐᵒᵖ

Equations

mul_opposite.comm_ring α = {add := ring.add (mul_opposite.ring α), add_assoc := _, zero := ring.zero (mul_opposite.ring α), zero_add := _, add_zero := _, nsmul := ring.nsmul (mul_opposite.ring α), nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg (mul_opposite.ring α), sub := ring.sub (mul_opposite.ring α), sub_eq_add_neg := _, zsmul := ring.zsmul (mul_opposite.ring α), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := ring.mul (mul_opposite.ring α), mul_assoc := _, one := ring.one (mul_opposite.ring α), one_mul := _, mul_one := _, npow := ring.npow (mul_opposite.ring α), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}

@[protected, instance]

def mul_opposite.no_zero_divisors (α : Type u) [has_zero α] [has_mul α] [no_zero_divisors α] :

no_zero_divisors αᵐᵒᵖ

@[protected, instance]

def mul_opposite.is_domain (α : Type u) [ring α] [is_domain α] :

is_domain αᵐᵒᵖ

@[protected, instance]

def mul_opposite.group_with_zero (α : Type u) [group_with_zero α] :

group_with_zero αᵐᵒᵖ

Equations

mul_opposite.group_with_zero α = {mul := monoid_with_zero.mul (mul_opposite.monoid_with_zero α), mul_assoc := _, one := monoid_with_zero.one (mul_opposite.monoid_with_zero α), one_mul := _, mul_one := _, npow := monoid_with_zero.npow (mul_opposite.monoid_with_zero α), npow_zero' := _, npow_succ' := _, zero := monoid_with_zero.zero (mul_opposite.monoid_with_zero α), zero_mul := _, mul_zero := _, inv := div_inv_monoid.inv (mul_opposite.div_inv_monoid α), div := div_inv_monoid.div (mul_opposite.div_inv_monoid α), div_eq_mul_inv := _, zpow := div_inv_monoid.zpow (mul_opposite.div_inv_monoid α), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}

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

f.to_opposite hf = {to_fun := mul_opposite.op ∘ ⇑f, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

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

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

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 monoid homomorphism f : R →* S such that f x commutes with f y for all x, y defines a monoid homomorphism from Rᵐᵒᵖ.

Equations

f.from_opposite hf = {to_fun := ⇑f ∘ mul_opposite.unop, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

@[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.op f.to_add_monoid_hom).to_fun ᾰ

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

ring_hom.op = {to_fun := λ (f : α →+* β), {to_fun := (⇑add_monoid_hom.op f.to_add_monoid_hom).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, inv_fun := λ (f : αᵐᵒᵖ →+* βᵐᵒᵖ), {to_fun := (⇑add_monoid_hom.unop f.to_add_monoid_hom).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, left_inv := _, right_inv := _}

@[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.unop f.to_add_monoid_hom).to_fun ᾰ

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

ring_hom.unop = ring_hom.op.symm