mathlib3 documentation

algebra.group.opposite

Group structures on the multiplicative and additive opposites #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Additive structures on αᵐᵒᵖ #

@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations

Multiplicative structures on αᵐᵒᵖ #

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

@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp]
@[simp]
theorem semiconj_by.op {α : 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) :
@[simp]
@[simp]
theorem mul_opposite.commute_op {α : Type u} [has_mul α] {x y : α} :

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 : β) :

The function add_opposite.op is a multiplicative equivalence.

Equations

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

Equations

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

Equations
@[simp]
theorem mul_hom.to_opposite_apply {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) (hf : (x y : M), commute (f x) (f y)) :
def add_hom.to_opposite {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) (hf : (x y : M), add_commute (f x) (f y)) :

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

Equations
@[simp]
theorem add_hom.to_opposite_apply {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) (hf : (x y : M), add_commute (f x) (f y)) :
def mul_hom.to_opposite {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) (hf : (x y : M), commute (f x) (f y)) :

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

Equations
def add_hom.from_opposite {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) (hf : (x y : M), add_commute (f x) (f y)) :

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

Equations
@[simp]
theorem add_hom.from_opposite_apply {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) (hf : (x y : M), add_commute (f x) (f y)) :
@[simp]
theorem mul_hom.from_opposite_apply {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) (hf : (x y : M), commute (f x) (f y)) :
def mul_hom.from_opposite {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) (hf : (x y : M), commute (f x) (f y)) :

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

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

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

Equations
theorem is_add_unit.op {M : Type u_1} [add_monoid M] {m : M} (h : is_add_unit m) :
theorem is_unit.op {M : Type u_1} [monoid M] {m : M} (h : is_unit m) :
theorem is_unit.unop {M : Type u_1} [monoid M] {m : Mᵐᵒᵖ} (h : is_unit m) :
@[simp]
theorem is_add_unit_op {M : Type u_1} [add_monoid M] {m : M} :
@[simp]
theorem is_unit_op {M : Type u_1} [monoid M] {m : M} :
@[simp]
theorem is_unit_unop {M : Type u_1} [monoid M] {m : Mᵐᵒᵖ} :
@[simp]
theorem add_hom.op_apply_apply {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) (ᾰ : Mᵃᵒᵖ) :
@[simp]
theorem mul_hom.op_symm_apply_apply {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ) (ᾰ : M) :
def add_hom.op {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] :

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

Equations
def mul_hom.op {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] :

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

Equations
@[simp]
theorem mul_hom.op_apply_apply {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) (ᾰ : Mᵐᵒᵖ) :
@[simp]
theorem add_hom.op_symm_apply_apply {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom Mᵃᵒᵖ Nᵃᵒᵖ) (ᾰ : M) :
@[simp]
def mul_hom.unop {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] :

The 'unopposite' of a semigroup homomorphism Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ. Inverse to mul_hom.op.

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

The 'unopposite' of an additive semigroup homomorphism Mᵃᵒᵖ →ₙ+ Nᵃᵒᵖ. Inverse to add_hom.op.

Equations
@[simp]
theorem add_hom.mul_op_apply_apply {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom M N) (ᾰ : Mᵐᵒᵖ) :
@[simp]
def add_hom.mul_op {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] :

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

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

The 'unopposite' of an additive semigroup hom αᵐᵒᵖ →+ βᵐᵒᵖ. Inverse to add_hom.mul_op.

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

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