mathlib documentation

algebra.group.opposite

Group structures on the multiplicative and additive opposites #

Additive structures on αᵐᵒᵖ #

Multiplicative structures on αᵐᵒᵖ #

We also generate additive structures on αᵃᵒᵖ using to_additive

@[protected, instance]
def mul_opposite.semigroup (α : Type u) [semigroup α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def mul_opposite.monoid (α : Type u) [monoid α] :
Equations
@[simp]
@[simp]
theorem mul_opposite.semiconj_by_op {α : Type u} [has_mul α] {a x y : α} :
theorem semiconj_by.op {α : Type u} [has_mul α] {a x y : α} (h : semiconj_by a x y) :
theorem add_semiconj_by.op {α : Type u} [has_add α] {a x y : α} (h : add_semiconj_by a x y) :
theorem semiconj_by.unop {α : Type u} [has_mul α] {a x y : αᵐᵒᵖ} (h : semiconj_by a x y) :
theorem commute.op {α : Type u} [has_mul α] {x y : α} (h : commute x y) :
theorem add_commute.op {α : Type u} [has_add α] {x y : α} (h : add_commute x y) :
theorem mul_opposite.commute.unop {α : Type u} [has_mul α] {x y : αᵐᵒᵖ} (h : commute x y) :
@[simp]
theorem add_opposite.commute_op {α : Type u} [has_add α] {x y : α} :
@[simp]
theorem mul_opposite.commute_op {α : Type u} [has_mul α] {x y : α} :
@[simp]
def mul_opposite.op_add_equiv {α : Type u} [has_add α] :

The function mul_opposite.op is an additive equivalence.

Equations

Multiplicative structures on αᵃᵒᵖ #

@[protected, instance]
def add_opposite.has_pow (α : Type u) {β : Type u_1} [has_pow α β] :
Equations
@[simp]
theorem add_opposite.op_pow (α : Type u) {β : Type u_1} [has_pow α β] (a : α) (b : β) :
@[simp]
theorem add_opposite.unop_pow (α : Type u) {β : Type u_1} [has_pow α β] (a : αᵃᵒᵖ) (b : β) :
def add_opposite.op_mul_equiv {α : Type u} [has_mul α] :

The function add_opposite.op is a multiplicative equivalence.

Equations
def add_equiv.neg' (G : Type u_1) [add_group G] :

Negation on an additive group is an add_equiv to the opposite group. When G is commutative, there is add_equiv.inv.

Equations
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 add_monoid_hom.to_opposite_apply {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) (hf : ∀ (x y : M), add_commute (f x) (f y)) :
def add_monoid_hom.to_opposite {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) (hf : ∀ (x y : M), add_commute (f x) (f y)) :

An additive monoid homomorphism f : M →+ N such that f x additively commutes with f y for all x, y defines an additive monoid homomorphism to Sᵃᵒᵖ.

Equations
@[simp]
theorem monoid_hom.to_opposite_apply {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (f : M →* N) (hf : ∀ (x y : M), commute (f x) (f y)) :
def monoid_hom.to_opposite {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (f : M →* N) (hf : ∀ (x y : M), commute (f x) (f y)) :

A monoid homomorphism f : M →* N such that f x commutes with f y for all x, y defines a monoid homomorphism to Nᵐᵒᵖ.

Equations
def add_monoid_hom.from_opposite {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) (hf : ∀ (x y : M), add_commute (f x) (f y)) :

An additive monoid homomorphism f : M →+ N such that f x additively commutes with f y for all x, y defines an additive monoid homomorphism from Mᵃᵒᵖ.

Equations
@[simp]
theorem add_monoid_hom.from_opposite_apply {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) (hf : ∀ (x y : M), add_commute (f x) (f y)) :
def monoid_hom.from_opposite {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (f : M →* N) (hf : ∀ (x y : M), commute (f x) (f y)) :

A monoid homomorphism f : M →* N such that f x commutes with f y for all x, y defines a monoid homomorphism from Mᵐᵒᵖ.

Equations
@[simp]
theorem monoid_hom.from_opposite_apply {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (f : M →* N) (hf : ∀ (x y : M), commute (f x) (f y)) :

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

Equations
def units.op_equiv {M : Type u_1} [monoid M] :

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

Equations
def add_monoid_hom.op {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :

An additive monoid homomorphism M →+ N can equivalently be viewed as an additive monoid homomorphism Mᵃᵒᵖ →+ Nᵃᵒᵖ. This is the action of the (fully faithful) ᵃᵒᵖ-functor on morphisms.

Equations
def monoid_hom.op {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :

A monoid homomorphism M →* N can equivalently be viewed as a monoid homomorphism Mᵐᵒᵖ →* Nᵐᵒᵖ. This is the action of the (fully faithful) ᵐᵒᵖ-functor on morphisms.

Equations
@[simp]
theorem monoid_hom.op_apply_apply {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (f : M →* N) (ᾰ : Mᵐᵒᵖ) :
@[simp]
theorem monoid_hom.op_symm_apply_apply {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] (f : Mᵐᵒᵖ →* Nᵐᵒᵖ) (ᾰ : M) :
@[simp]
theorem add_monoid_hom.op_apply_apply {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) (ᾰ : Mᵃᵒᵖ) :
@[simp]
@[simp]
def add_monoid_hom.unop {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :

The 'unopposite' of an additive monoid homomorphism Mᵃᵒᵖ →+ Nᵃᵒᵖ. Inverse to add_monoid_hom.op.

Equations
@[simp]
def monoid_hom.unop {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :

The 'unopposite' of a monoid homomorphism Mᵐᵒᵖ →* Nᵐᵒᵖ. Inverse to monoid_hom.op.

Equations
def add_monoid_hom.mul_op {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :

An additive homomorphism M →+ N can equivalently be viewed as an additive homomorphism Mᵐᵒᵖ →+ Nᵐᵒᵖ. This is the action of the (fully faithful) ᵐᵒᵖ-functor on morphisms.

Equations
@[simp]
theorem add_monoid_hom.mul_op_apply_apply {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : M →+ N) (ᾰ : Mᵐᵒᵖ) :
@[simp]
def add_monoid_hom.mul_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.mul_op.

Equations
@[simp]
theorem add_equiv.mul_op_apply {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] (f : α ≃+ β) :
def add_equiv.mul_op {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] :

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

Equations
@[simp]
def add_equiv.mul_unop {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] :

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

Equations
@[simp]
theorem add_equiv.op_symm_apply_symm_apply {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) (ᾰ : β) :
@[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 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_apply_symm_apply {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] (f : α ≃+ β) (ᾰ : βᵃᵒᵖ) :
@[simp]
theorem add_equiv.op_symm_apply_apply {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] (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]
theorem add_equiv.op_apply_apply {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] (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
@[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
@[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'.