mathlib documentation

algebra.opposites

Algebraic operations on αᵒᵖ #

This file records several basic facts about the opposite of an algebraic structure, e.g. the opposite of a ring is a ring (with multiplication x * y = yx). Use is made of the identity functions op : α → αᵒᵖ and unop : αᵒᵖ → α.

source
@[instance]
def opposite.has_add (α : Type u) [has_add α] :
has_add αᵒᵖ
Equations
source
@[instance]
def opposite.has_sub (α : Type u) [has_sub α] :
has_sub αᵒᵖ
Equations
source
@[instance]
def opposite.add_semigroup (α : Type u) [add_semigroup α] :
add_semigroup αᵒᵖ
Equations
source
@[instance]
def opposite.add_left_cancel_semigroup (α : Type u) [add_left_cancel_semigroup α] :
add_left_cancel_semigroup αᵒᵖ
Equations
source
@[instance]
def opposite.add_right_cancel_semigroup (α : Type u) [add_right_cancel_semigroup α] :
add_right_cancel_semigroup αᵒᵖ
Equations
source
@[instance]
def opposite.add_comm_semigroup (α : Type u) [add_comm_semigroup α] :
add_comm_semigroup αᵒᵖ
Equations
source
@[instance]
def opposite.has_zero (α : Type u) [has_zero α] :
has_zero αᵒᵖ
Equations
source
@[instance]
def opposite.nontrivial (α : Type u) [nontrivial α] :
nontrivial αᵒᵖ
source
@[simp]
theorem opposite.unop_eq_zero_iff {α : Type u_1} [has_zero α] (a : αᵒᵖ) :
opposite.unop a = 0 ↔ a = 0
source
@[simp]
theorem opposite.op_eq_zero_iff {α : Type u_1} [has_zero α] (a : α) :
opposite.op a = 0 ↔ a = 0
source
theorem opposite.unop_ne_zero_iff {α : Type u_1} [has_zero α] (a : αᵒᵖ) :
opposite.unop a ≠ 0 ↔ a ≠ 0
source
theorem opposite.op_ne_zero_iff {α : Type u_1} [has_zero α] (a : α) :
opposite.op a ≠ 0 ↔ a ≠ 0
source
@[instance]
def opposite.add_zero_class (α : Type u) [add_zero_class α] :
add_zero_class αᵒᵖ
Equations
source
@[instance]
def opposite.add_monoid (α : Type u) [add_monoid α] :
add_monoid αᵒᵖ
Equations
source
@[instance]
def opposite.add_comm_monoid (α : Type u) [add_comm_monoid α] :
add_comm_monoid αᵒᵖ
Equations
source
@[instance]
def opposite.has_neg (α : Type u) [has_neg α] :
has_neg αᵒᵖ
Equations
source
@[instance]
def opposite.add_group (α : Type u) [add_group α] :
add_group αᵒᵖ
Equations
source
@[instance]
def opposite.add_comm_group (α : Type u) [add_comm_group α] :
add_comm_group αᵒᵖ
Equations
source
@[instance]
def opposite.has_mul (α : Type u) [has_mul α] :
has_mul αᵒᵖ
Equations
source
@[instance]
def opposite.semigroup (α : Type u) [semigroup α] :
semigroup αᵒᵖ
Equations
source
@[instance]
def opposite.left_cancel_semigroup (α : Type u) [right_cancel_semigroup α] :
left_cancel_semigroup αᵒᵖ
Equations
source
@[instance]
def opposite.right_cancel_semigroup (α : Type u) [left_cancel_semigroup α] :
right_cancel_semigroup αᵒᵖ
Equations
source
@[instance]
def opposite.comm_semigroup (α : Type u) [comm_semigroup α] :
comm_semigroup αᵒᵖ
Equations
source
@[instance]
def opposite.has_one (α : Type u) [has_one α] :
has_one αᵒᵖ
Equations
source
@[simp]
theorem opposite.unop_eq_one_iff {α : Type u_1} [has_one α] (a : αᵒᵖ) :
opposite.unop a = 1 ↔ a = 1
source
@[simp]
theorem opposite.op_eq_one_iff {α : Type u_1} [has_one α] (a : α) :
opposite.op a = 1 ↔ a = 1
source
@[instance]
def opposite.mul_one_class (α : Type u) [mul_one_class α] :
mul_one_class αᵒᵖ
Equations
source
@[instance]
def opposite.monoid (α : Type u) [monoid α] :
monoid αᵒᵖ
Equations
source
@[instance]
def opposite.comm_monoid (α : Type u) [comm_monoid α] :
comm_monoid αᵒᵖ
Equations
source
@[instance]
def opposite.has_inv (α : Type u) [has_inv α] :
has_inv αᵒᵖ
Equations
source
@[instance]
def opposite.group (α : Type u) [group α] :
group αᵒᵖ
Equations
source
@[instance]
def opposite.comm_group (α : Type u) [comm_group α] :
comm_group αᵒᵖ
Equations
source
@[instance]
def opposite.distrib (α : Type u) [distrib α] :
distrib αᵒᵖ
Equations
source
@[instance]
def opposite.mul_zero_class (α : Type u) [mul_zero_class α] :
mul_zero_class αᵒᵖ
Equations
source
@[instance]
def opposite.mul_zero_one_class (α : Type u) [mul_zero_one_class α] :
mul_zero_one_class αᵒᵖ
Equations
source
@[instance]
def opposite.semigroup_with_zero (α : Type u) [semigroup_with_zero α] :
semigroup_with_zero αᵒᵖ
Equations
source
@[instance]
def opposite.monoid_with_zero (α : Type u) [monoid_with_zero α] :
monoid_with_zero αᵒᵖ
Equations
source
@[instance]
def opposite.non_unital_non_assoc_semiring (α : Type u) [non_unital_non_assoc_semiring α] :
non_unital_non_assoc_semiring αᵒᵖ
Equations
source
@[instance]
def opposite.non_unital_semiring (α : Type u) [non_unital_semiring α] :
non_unital_semiring αᵒᵖ
Equations
source
@[instance]
def opposite.non_assoc_semiring (α : Type u) [non_assoc_semiring α] :
non_assoc_semiring αᵒᵖ
Equations
source
@[instance]
def opposite.semiring (α : Type u) [semiring α] :
semiring αᵒᵖ
Equations
source
@[instance]
def opposite.ring (α : Type u) [ring α] :
ring αᵒᵖ
Equations
source
@[instance]
def opposite.comm_ring (α : Type u) [comm_ring α] :
comm_ring αᵒᵖ
Equations
source
@[instance]
def opposite.no_zero_divisors (α : Type u) [has_zero α] [has_mul α] [no_zero_divisors α] :
no_zero_divisors αᵒᵖ
source
@[instance]
def opposite.integral_domain (α : Type u) [integral_domain α] :
integral_domain αᵒᵖ
Equations
source
@[instance]
def opposite.group_with_zero (α : Type u) [group_with_zero α] :
group_with_zero αᵒᵖ
Equations
source
@[instance]
def opposite.division_ring (α : Type u) [division_ring α] :
division_ring αᵒᵖ
Equations
source
@[instance]
def opposite.field (α : Type u) [field α] :
field αᵒᵖ
Equations
source
@[instance]
def opposite.has_scalar (α : Type u) (R : Type u_1) [has_scalar R α] :
has_scalar R αᵒᵖ
Equations
source
@[instance]
def opposite.mul_action (α : Type u) (R : Type u_1) [monoid R] [mul_action R α] :
mul_action R αᵒᵖ
Equations
source
@[instance]
def opposite.distrib_mul_action (α : Type u) (R : Type u_1) [monoid R] [add_monoid α] [distrib_mul_action R α] :
distrib_mul_action R αᵒᵖ
Equations
source
@[instance]
def opposite.monoid.to_opposite_mul_action (α : Type u) [monoid α] :
mul_action αᵒᵖ α

Like monoid.to_mul_action, but multiplies on the right.

Equations
source
theorem opposite.op_smul_eq_mul (α : Type u) [monoid α] {a a' : α} :
opposite.op a • a' = a' * a
source
@[simp]
theorem opposite.op_zero (α : Type u) [has_zero α] :
opposite.op 0 = 0
source
@[simp]
theorem opposite.unop_zero (α : Type u) [has_zero α] :
opposite.unop 0 = 0
source
@[simp]
theorem opposite.op_one (α : Type u) [has_one α] :
opposite.op 1 = 1
source
@[simp]
theorem opposite.unop_one (α : Type u) [has_one α] :
opposite.unop 1 = 1
source
@[simp]
theorem opposite.op_add {α : Type u} [has_add α] (x y : α) :
opposite.op (x + y) = opposite.op x + opposite.op y
source
@[simp]
theorem opposite.unop_add {α : Type u} [has_add α] (x y : αᵒᵖ) :
opposite.unop (x + y) = opposite.unop x + opposite.unop y
source
@[simp]
theorem opposite.op_neg {α : Type u} [has_neg α] (x : α) :
opposite.op (-x) = -opposite.op x
source
@[simp]
theorem opposite.unop_neg {α : Type u} [has_neg α] (x : αᵒᵖ) :
opposite.unop (-x) = -opposite.unop x
source
@[simp]
theorem opposite.op_mul {α : Type u} [has_mul α] (x y : α) :
opposite.op (x * y) = (opposite.op y) * opposite.op x
source
@[simp]
theorem opposite.unop_mul {α : Type u} [has_mul α] (x y : αᵒᵖ) :
opposite.unop (x * y) = (opposite.unop y) * opposite.unop x
source
@[simp]
theorem opposite.op_inv {α : Type u} [has_inv α] (x : α) :
opposite.op x⁻¹ = (opposite.op x)⁻¹
source
@[simp]
theorem opposite.unop_inv {α : Type u} [has_inv α] (x : αᵒᵖ) :
opposite.unop x⁻¹ = (opposite.unop x)⁻¹
source
@[simp]
theorem opposite.op_sub {α : Type u} [add_group α] (x y : α) :
opposite.op (x - y) = opposite.op x - opposite.op y
source
@[simp]
theorem opposite.unop_sub {α : Type u} [add_group α] (x y : αᵒᵖ) :
opposite.unop (x - y) = opposite.unop x - opposite.unop y
source
@[simp]
theorem opposite.op_smul {α : Type u} {R : Type u_1} [has_scalar R α] (c : R) (a : α) :
opposite.op (c • a) = c • opposite.op a
source
@[simp]
theorem opposite.unop_smul {α : Type u} {R : Type u_1} [has_scalar R α] (c : R) (a : αᵒᵖ) :
opposite.unop (c • a) = c • opposite.unop a
source
theorem opposite.semiconj_by.op {α : Type u} [has_mul α] {a x y : α} (h : semiconj_by a x y) :
semiconj_by (opposite.op a) (opposite.op y) (opposite.op x)
source
theorem opposite.semiconj_by.unop {α : Type u} [has_mul α] {a x y : αᵒᵖ} (h : semiconj_by a x y) :
semiconj_by (opposite.unop a) (opposite.unop y) (opposite.unop x)
source
@[simp]
theorem opposite.semiconj_by_op {α : Type u} [has_mul α] {a x y : α} :
semiconj_by (opposite.op a) (opposite.op y) (opposite.op x) ↔ semiconj_by a x y
source
@[simp]
theorem opposite.semiconj_by_unop {α : Type u} [has_mul α] {a x y : αᵒᵖ} :
semiconj_by (opposite.unop a) (opposite.unop y) (opposite.unop x) ↔ semiconj_by a x y
source
theorem opposite.commute.op {α : Type u} [has_mul α] {x y : α} (h : commute x y) :
commute (opposite.op x) (opposite.op y)
source
theorem opposite.commute.unop {α : Type u} [has_mul α] {x y : αᵒᵖ} (h : commute x y) :
commute (opposite.unop x) (opposite.unop y)
source
@[simp]
theorem opposite.commute_op {α : Type u} [has_mul α] {x y : α} :
commute (opposite.op x) (opposite.op y) ↔ commute x y
source
@[simp]
theorem opposite.commute_unop {α : Type u} [has_mul α] {x y : αᵒᵖ} :
commute (opposite.unop x) (opposite.unop y) ↔ commute x y
source
def opposite.op_add_equiv {α : Type u} [has_add α] :
α ≃+ αᵒᵖ

The function op is an additive equivalence.

Equations
source
@[simp]
theorem opposite.coe_op_add_equiv {α : Type u} [has_add α] :
⇑opposite.op_add_equiv = opposite.op
source
@[simp]
theorem opposite.coe_op_add_equiv_symm {α : Type u} [has_add α] :
⇑(opposite.op_add_equiv.symm) = opposite.unop
source
@[simp]
theorem opposite.op_add_equiv_to_equiv {α : Type u} [has_add α] :
opposite.op_add_equiv.to_equiv = opposite.equiv_to_opposite
source
@[simp]
theorem mul_equiv.inv'_symm_apply (G : Type u_1) [group G] :
⇑((mul_equiv.inv' G).symm) = has_inv.inv ∘ opposite.unop
source
@[simp]
theorem mul_equiv.inv'_apply (G : Type u_1) [group G] :
⇑(mul_equiv.inv' G) = opposite.op ∘ has_inv.inv
source
def mul_equiv.inv' (G : Type u_1) [group G] :
G ≃* Gᵒᵖ

Inversion on a group is a mul_equiv to the opposite group. When G is commutative, there is mul_equiv.inv.

Equations
source
@[simp]
theorem monoid_hom.to_opposite_apply {R : Type u_1} {S : Type u_2} [mul_one_class R] [mul_one_class S] (f : R →* S) (hf : ∀ (x y : R), commute (⇑f x) (⇑f y)) :
⇑(f.to_opposite hf) = opposite.op ∘ ⇑f
source
def monoid_hom.to_opposite {R : Type u_1} {S : Type u_2} [mul_one_class R] [mul_one_class 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 to Sᵒᵖ.

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) = opposite.op ∘ ⇑f
source
def units.op_equiv {R : Type u_1} [monoid R] :
units Rᵒᵖ ≃* (units R)ᵒᵖ

The units of the opposites are equivalent to the opposites of the units.

Equations
source
@[simp]
theorem units.coe_unop_op_equiv {R : Type u_1} [monoid R] (u : units Rᵒᵖ) :
↑(opposite.unop (⇑units.op_equiv u)) = opposite.unop ↑u
source
@[simp]
theorem units.coe_op_equiv_symm {R : Type u_1} [monoid R] (u : (units R)ᵒᵖ) :
↑(⇑(units.op_equiv.symm) u) = opposite.op ↑(opposite.unop u)
source
def monoid_hom.op {α : Type u_1} {β : Type u_2} [mul_one_class α] [mul_one_class β] :
(α →* β) ≃ (αᵒᵖ →* βᵒᵖ)

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

Equations
source
@[simp]
theorem monoid_hom.op_apply_apply {α : Type u_1} {β : Type u_2} [mul_one_class α] [mul_one_class β] (f : α →* β) (ᾰ : αᵒᵖ) :
⇑(⇑monoid_hom.op f) ᾰ = (opposite.op ∘ ⇑f ∘ opposite.unop) ᾰ
source
@[simp]
theorem monoid_hom.op_symm_apply_apply {α : Type u_1} {β : Type u_2} [mul_one_class α] [mul_one_class β] (f : αᵒᵖ →* βᵒᵖ) (ᾰ : α) :
⇑(⇑(monoid_hom.op.symm) f) ᾰ = (opposite.unop ∘ ⇑f ∘ opposite.op) ᾰ
source
@[simp]
def monoid_hom.unop {α : Type u_1} {β : Type u_2} [mul_one_class α] [mul_one_class β] :
(αᵒᵖ →* βᵒᵖ) ≃ (α →* β)

The 'unopposite' of a monoid hom αᵒᵖ →* βᵒᵖ. Inverse to monoid_hom.op.

Equations
source
def add_monoid_hom.op {α : Type u_1} {β : Type u_2} [add_zero_class α] [add_zero_class β] :
(α →+ β) ≃ (αᵒᵖ →+ βᵒᵖ)

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

Equations
source
@[simp]
theorem add_monoid_hom.op_apply_apply {α : Type u_1} {β : Type u_2} [add_zero_class α] [add_zero_class β] (f : α →+ β) (ᾰ : αᵒᵖ) :
⇑(⇑add_monoid_hom.op f) ᾰ = (opposite.op ∘ ⇑f ∘ opposite.unop) ᾰ
source
@[simp]
theorem add_monoid_hom.op_symm_apply_apply {α : Type u_1} {β : Type u_2} [add_zero_class α] [add_zero_class β] (f : αᵒᵖ →+ βᵒᵖ) (ᾰ : α) :
⇑(⇑(add_monoid_hom.op.symm) f) ᾰ = (opposite.unop ∘ ⇑f ∘ opposite.op) ᾰ
source
@[simp]
def add_monoid_hom.unop {α : Type u_1} {β : Type u_2} [add_zero_class α] [add_zero_class β] :
(αᵒᵖ →+ βᵒᵖ) ≃ (α →+ β)

The 'unopposite' of an additive monoid hom αᵒᵖ →+ βᵒᵖ. Inverse to add_monoid_hom.op.

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