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 : αᵒᵖ → α.

@[instance]
def opposite.has_zero (α : Type u) [has_zero α] :
Equations
@[instance]
def opposite.has_one (α : Type u) [has_one α] :
Equations
@[instance]
def opposite.has_add (α : Type u) [has_add α] :
Equations
@[instance]
def opposite.has_sub (α : Type u) [has_sub α] :
Equations
@[instance]
def opposite.has_neg (α : Type u) [has_neg α] :
Equations
@[instance]
def opposite.has_mul (α : Type u) [has_mul α] :
Equations
@[instance]
def opposite.has_inv (α : Type u) [has_inv α] :
Equations
@[instance]
def opposite.has_scalar (α : Type u) (R : Type u_1) [has_scalar R α] :
Equations
@[simp]
theorem opposite.op_zero (α : Type u) [has_zero α] :
@[simp]
theorem opposite.unop_zero (α : Type u) [has_zero α] :
@[simp]
theorem opposite.op_one (α : Type u) [has_one α] :
@[simp]
theorem opposite.unop_one (α : Type u) [has_one α] :
@[simp]
theorem opposite.op_add {α : Type u} [has_add α] (x y : α) :
@[simp]
theorem opposite.unop_add {α : Type u} [has_add α] (x y : αᵒᵖ) :
@[simp]
theorem opposite.op_neg {α : Type u} [has_neg α] (x : α) :
@[simp]
theorem opposite.unop_neg {α : Type u} [has_neg α] (x : αᵒᵖ) :
@[simp]
theorem opposite.op_mul {α : Type u} [has_mul α] (x y : α) :
@[simp]
theorem opposite.unop_mul {α : Type u} [has_mul α] (x y : αᵒᵖ) :
@[simp]
theorem opposite.op_inv {α : Type u} [has_inv α] (x : α) :
@[simp]
theorem opposite.unop_inv {α : Type u} [has_inv α] (x : αᵒᵖ) :
@[simp]
theorem opposite.op_sub {α : Type u} [add_group α] (x y : α) :
@[simp]
theorem opposite.unop_sub {α : Type u} [add_group α] (x y : αᵒᵖ) :
@[simp]
theorem opposite.op_smul {α : Type u} {R : Type u_1} [has_scalar R α] (c : R) (a : α) :
@[simp]
theorem opposite.unop_smul {α : Type u} {R : Type u_1} [has_scalar R α] (c : R) (a : αᵒᵖ) :
@[instance]
def opposite.nontrivial (α : Type u) [nontrivial α] :
@[simp]
theorem opposite.unop_eq_zero_iff {α : Type u_1} [has_zero α] (a : αᵒᵖ) :
@[simp]
theorem opposite.op_eq_zero_iff {α : Type u_1} [has_zero α] (a : α) :
opposite.op a = 0 a = 0
theorem opposite.unop_ne_zero_iff {α : Type u_1} [has_zero α] (a : αᵒᵖ) :
theorem opposite.op_ne_zero_iff {α : Type u_1} [has_zero α] (a : α) :
@[instance]
Equations
@[instance]
def opposite.semigroup (α : Type u) [semigroup α] :
Equations
@[simp]
theorem opposite.unop_eq_one_iff {α : Type u_1} [has_one α] (a : αᵒᵖ) :
@[simp]
theorem opposite.op_eq_one_iff {α : Type u_1} [has_one α] (a : α) :
opposite.op a = 1 a = 1
@[instance]
Equations
@[instance]
def opposite.monoid (α : Type u) [monoid α] :
Equations
@[instance]
def opposite.comm_monoid (α : Type u) [comm_monoid α] :
Equations
@[instance]
Equations
@[instance]
def opposite.distrib (α : Type u) [distrib α] :
Equations
@[instance]
Equations
@[instance]
@[instance]
def opposite.mul_action (α : Type u) (R : Type u_1) [monoid R] [mul_action R α] :
Equations
@[instance]
def opposite.is_scalar_tower (α : Type u) {M : Type u_1} {N : Type u_2} [has_scalar M N] [has_scalar M α] [has_scalar N α] [is_scalar_tower M N α] :
@[instance]
def opposite.smul_comm_class (α : Type u) {M : Type u_1} {N : Type u_2} [has_scalar M α] [has_scalar N α] [smul_comm_class M N α] :
@[instance]
def has_mul.to_has_opposite_scalar (α : Type u) [has_mul α] :

Like has_mul.to_has_scalar, but multiplies on the right.

See also monoid.to_opposite_mul_action and monoid_with_zero.to_opposite_mul_action.

Equations
@[simp]
theorem opposite.op_smul_eq_mul (α : Type u) [has_mul α] {a a' : α} :
opposite.op a a' = a' * a
@[instance]
@[instance]
@[instance]
def monoid.to_opposite_mul_action (α : Type u) [monoid α] :

Like monoid.to_mul_action, but multiplies on the right.

Equations
@[instance]
def is_scalar_tower.opposite_mid {M : Type u_1} {N : Type u_2} [monoid N] [has_scalar M N] [smul_comm_class M N N] :
@[instance]
def smul_comm_class.opposite_mid {M : Type u_1} {N : Type u_2} [monoid N] [has_scalar M N] [is_scalar_tower M N N] :
@[instance]

monoid.to_opposite_mul_action is faithful on cancellative monoids.

@[instance]

monoid.to_opposite_mul_action is faithful on nontrivial cancellative monoids with zero.

theorem opposite.semiconj_by.op {α : Type u} [has_mul α] {a x y : α} (h : semiconj_by a x y) :
theorem opposite.semiconj_by.unop {α : Type u} [has_mul α] {a x y : αᵒᵖ} (h : semiconj_by a x y) :
@[simp]
theorem opposite.semiconj_by_op {α : Type u} [has_mul α] {a x y : α} :
@[simp]
theorem opposite.semiconj_by_unop {α : Type u} [has_mul α] {a x y : αᵒᵖ} :
theorem opposite.commute.op {α : Type u} [has_mul α] {x y : α} (h : commute x y) :
theorem opposite.commute.unop {α : Type u} [has_mul α] {x y : αᵒᵖ} (h : commute x y) :
@[simp]
theorem opposite.commute_op {α : Type u} [has_mul α] {x y : α} :
@[simp]
theorem opposite.commute_unop {α : Type u} [has_mul α] {x y : αᵒᵖ} :
def opposite.op_add_equiv {α : Type u} [has_add α] :

The function op is an additive equivalence.

Equations
@[simp]
def mul_equiv.inv' (G : Type u_1) [group G] :

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

Equations
@[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)) :
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)) :

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
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)) :
def units.op_equiv {R : Type u_1} [monoid R] :

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

Equations
@[simp]
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
@[simp]
theorem monoid_hom.op_apply_apply {α : Type u_1} {β : Type u_2} [mul_one_class α] [mul_one_class β] (f : α →* β) (ᾰ : αᵒᵖ) :
@[simp]
theorem monoid_hom.op_symm_apply_apply {α : Type u_1} {β : Type u_2} [mul_one_class α] [mul_one_class β] (f : αᵒᵖ →* βᵒᵖ) (ᾰ : α) :
@[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
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
@[simp]
theorem add_monoid_hom.op_apply_apply {α : Type u_1} {β : Type u_2} [add_zero_class α] [add_zero_class β] (f : α →+ β) (ᾰ : αᵒᵖ) :
@[simp]
theorem add_monoid_hom.op_symm_apply_apply {α : Type u_1} {β : Type u_2} [add_zero_class α] [add_zero_class β] (f : αᵒᵖ →+ βᵒᵖ) (ᾰ : α) :
@[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
@[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
def add_equiv.op {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] :
α ≃+ β ᵒᵖ ≃+ βᵒᵖ)

A iso α ≃+ β can equivalently be viewed as an iso αᵒᵖ ≃+ βᵒᵖ.

Equations
@[simp]
theorem add_equiv.op_symm_apply {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] (f : αᵒᵖ ≃+ βᵒᵖ) :
@[simp]
theorem add_equiv.op_apply {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] (f : α ≃+ β) :
@[simp]
def add_equiv.unop {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] :
αᵒᵖ ≃+ βᵒᵖ ≃+ β)

The 'unopposite' of an iso αᵒᵖ ≃+ βᵒᵖ. Inverse to add_equiv.op.

Equations
@[simp]
theorem mul_equiv.op_symm_apply_apply {α : Type u_1} {β : Type u_2} [has_mul α] [has_mul β] (f : αᵒᵖ ≃* βᵒᵖ) (ᾰ : α) :
@[simp]
theorem mul_equiv.op_symm_apply_symm_apply {α : Type u_1} {β : Type u_2} [has_mul α] [has_mul β] (f : αᵒᵖ ≃* βᵒᵖ) (ᾰ : β) :
def mul_equiv.op {α : Type u_1} {β : Type u_2} [has_mul α] [has_mul β] :
α ≃* β ᵒᵖ ≃* βᵒᵖ)

A iso α ≃* β can equivalently be viewed as an iso αᵒᵖ ≃+ βᵒᵖ.

Equations
@[simp]
theorem mul_equiv.op_apply_symm_apply {α : Type u_1} {β : Type u_2} [has_mul α] [has_mul β] (f : α ≃* β) (ᾰ : βᵒᵖ) :
@[simp]
theorem mul_equiv.op_apply_apply {α : Type u_1} {β : Type u_2} [has_mul α] [has_mul β] (f : α ≃* β) (ᾰ : αᵒᵖ) :
@[simp]
def mul_equiv.unop {α : Type u_1} {β : Type u_2} [has_mul α] [has_mul β] :
αᵒᵖ ≃* βᵒᵖ ≃* β)

The 'unopposite' of an iso αᵒᵖ ≃* βᵒᵖ. Inverse to mul_equiv.op.

Equations
@[ext]

This ext lemma change equalities on αᵒᵖ →+ β to equalities on α →+ β. This is useful because there are often ext lemmas for specific αs that will apply to an equality of α →+ β such as finsupp.add_hom_ext'.