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 αᵐᵒᵖ #

source
@[protected, instance]
def add_opposite.has_nat_cast (α : Type u) [has_nat_cast α] :
has_nat_cast αᵃᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.has_nat_cast (α : Type u) [has_nat_cast α] :
has_nat_cast αᵐᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.has_int_cast (α : Type u) [has_int_cast α] :
has_int_cast αᵃᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.has_int_cast (α : Type u) [has_int_cast α] :
has_int_cast αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.add_semigroup (α : Type u) [add_semigroup α] :
add_semigroup αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.add_left_cancel_semigroup (α : Type u) [add_left_cancel_semigroup α] :
add_left_cancel_semigroup αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.add_right_cancel_semigroup (α : Type u) [add_right_cancel_semigroup α] :
add_right_cancel_semigroup αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.add_comm_semigroup (α : Type u) [add_comm_semigroup α] :
add_comm_semigroup αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.add_zero_class (α : Type u) [add_zero_class α] :
add_zero_class αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.add_monoid (α : Type u) [add_monoid α] :
add_monoid αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.add_comm_monoid (α : Type u) [add_comm_monoid α] :
add_comm_monoid αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.add_monoid_with_one (α : Type u) [add_monoid_with_one α] :
add_monoid_with_one αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.add_comm_monoid_with_one (α : Type u) [add_comm_monoid_with_one α] :
add_comm_monoid_with_one αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.sub_neg_monoid (α : Type u) [sub_neg_monoid α] :
sub_neg_monoid αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.add_group (α : Type u) [add_group α] :
add_group αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.add_comm_group (α : Type u) [add_comm_group α] :
add_comm_group αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.add_group_with_one (α : Type u) [add_group_with_one α] :
add_group_with_one αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.add_comm_group_with_one (α : Type u) [add_comm_group_with_one α] :
add_comm_group_with_one αᵐᵒᵖ
Equations

Multiplicative structures on αᵐᵒᵖ #

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

source
@[protected, instance]
def add_opposite.add_semigroup (α : Type u) [add_semigroup α] :
add_semigroup αᵃᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.semigroup (α : Type u) [semigroup α] :
semigroup αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.left_cancel_semigroup (α : Type u) [right_cancel_semigroup α] :
left_cancel_semigroup αᵐᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.left_cancel_add_semigroup (α : Type u) [add_right_cancel_semigroup α] :
add_left_cancel_semigroup αᵃᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.right_cancel_semigroup (α : Type u) [left_cancel_semigroup α] :
right_cancel_semigroup αᵐᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.right_cancel_add_semigroup (α : Type u) [add_left_cancel_semigroup α] :
add_right_cancel_semigroup αᵃᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.comm_semigroup (α : Type u) [comm_semigroup α] :
comm_semigroup αᵐᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.add_comm_semigroup (α : Type u) [add_comm_semigroup α] :
add_comm_semigroup αᵃᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.mul_one_class (α : Type u) [mul_one_class α] :
mul_one_class αᵐᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.add_zero_class (α : Type u) [add_zero_class α] :
add_zero_class αᵃᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.monoid (α : Type u) [monoid α] :
monoid αᵐᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.add_monoid (α : Type u) [add_monoid α] :
add_monoid αᵃᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.left_cancel_monoid (α : Type u) [right_cancel_monoid α] :
left_cancel_monoid αᵐᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.left_cancel_add_monoid (α : Type u) [add_right_cancel_monoid α] :
add_left_cancel_monoid αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.right_cancel_add_monoid (α : Type u) [add_left_cancel_monoid α] :
add_right_cancel_monoid αᵃᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.right_cancel_monoid (α : Type u) [left_cancel_monoid α] :
right_cancel_monoid αᵐᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.cancel_add_monoid (α : Type u) [add_cancel_monoid α] :
add_cancel_monoid αᵃᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.cancel_monoid (α : Type u) [cancel_monoid α] :
cancel_monoid αᵐᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.add_comm_monoid (α : Type u) [add_comm_monoid α] :
add_comm_monoid αᵃᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.comm_monoid (α : Type u) [comm_monoid α] :
comm_monoid αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.cancel_comm_monoid (α : Type u) [cancel_comm_monoid α] :
cancel_comm_monoid αᵐᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.cancel_add_comm_monoid (α : Type u) [add_cancel_comm_monoid α] :
add_cancel_comm_monoid αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.sub_neg_monoid (α : Type u) [sub_neg_monoid α] :
sub_neg_monoid αᵃᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.div_inv_monoid (α : Type u) [div_inv_monoid α] :
div_inv_monoid αᵐᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.subtraction_monoid (α : Type u) [subtraction_monoid α] :
subtraction_monoid αᵃᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.division_monoid (α : Type u) [division_monoid α] :
division_monoid αᵐᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.division_comm_monoid (α : Type u) [division_comm_monoid α] :
division_comm_monoid αᵐᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.subtraction_comm_monoid (α : Type u) [subtraction_comm_monoid α] :
subtraction_comm_monoid αᵃᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.group (α : Type u) [group α] :
group αᵐᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.add_group (α : Type u) [add_group α] :
add_group αᵃᵒᵖ
Equations
source
@[protected, instance]
def mul_opposite.comm_group (α : Type u) [comm_group α] :
comm_group αᵐᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.add_comm_group (α : Type u) [add_comm_group α] :
add_comm_group αᵃᵒᵖ
Equations
source
@[simp, norm_cast]
theorem mul_opposite.op_nat_cast {α : Type u} [has_nat_cast α] (n : ℕ) :
mul_opposite.op ↑n = ↑n
source
@[simp, norm_cast]
theorem add_opposite.op_nat_cast {α : Type u} [has_nat_cast α] (n : ℕ) :
add_opposite.op ↑n = ↑n
source
@[simp, norm_cast]
theorem mul_opposite.op_int_cast {α : Type u} [has_int_cast α] (n : ℤ) :
mul_opposite.op ↑n = ↑n
source
@[simp, norm_cast]
theorem add_opposite.op_int_cast {α : Type u} [has_int_cast α] (n : ℤ) :
add_opposite.op ↑n = ↑n
source
@[simp, norm_cast]
theorem mul_opposite.unop_nat_cast {α : Type u} [has_nat_cast α] (n : ℕ) :
mul_opposite.unop ↑n = ↑n
source
@[simp, norm_cast]
theorem add_opposite.unop_nat_cast {α : Type u} [has_nat_cast α] (n : ℕ) :
add_opposite.unop ↑n = ↑n
source
@[simp, norm_cast]
theorem add_opposite.unop_int_cast {α : Type u} [has_int_cast α] (n : ℤ) :
add_opposite.unop ↑n = ↑n
source
@[simp, norm_cast]
theorem mul_opposite.unop_int_cast {α : Type u} [has_int_cast α] (n : ℤ) :
mul_opposite.unop ↑n = ↑n
source
@[simp]
theorem add_opposite.unop_sub {α : Type u} [sub_neg_monoid α] (x y : αᵃᵒᵖ) :
add_opposite.unop (x - y) = -add_opposite.unop y + add_opposite.unop x
source
@[simp]
theorem mul_opposite.unop_div {α : Type u} [div_inv_monoid α] (x y : αᵐᵒᵖ) :
mul_opposite.unop (x / y) = (mul_opposite.unop y)⁻¹ * mul_opposite.unop x
source
@[simp]
theorem add_opposite.op_sub {α : Type u} [sub_neg_monoid α] (x y : α) :
add_opposite.op (x - y) = -add_opposite.op y + add_opposite.op x
source
@[simp]
theorem mul_opposite.op_div {α : Type u} [div_inv_monoid α] (x y : α) :
mul_opposite.op (x / y) = (mul_opposite.op y)⁻¹ * mul_opposite.op x
source
@[simp]
theorem add_opposite.semiconj_by_op {α : Type u} [has_add α] {a x y : α} :
add_semiconj_by (add_opposite.op a) (add_opposite.op y) (add_opposite.op x) ↔ add_semiconj_by a x y
source
@[simp]
theorem mul_opposite.semiconj_by_op {α : Type u} [has_mul α] {a x y : α} :
semiconj_by (mul_opposite.op a) (mul_opposite.op y) (mul_opposite.op x) ↔ semiconj_by a x y
source
@[simp]
theorem add_opposite.semiconj_by_unop {α : Type u} [has_add α] {a x y : αᵃᵒᵖ} :
add_semiconj_by (add_opposite.unop a) (add_opposite.unop y) (add_opposite.unop x) ↔ add_semiconj_by a x y
source
@[simp]
theorem mul_opposite.semiconj_by_unop {α : Type u} [has_mul α] {a x y : αᵐᵒᵖ} :
semiconj_by (mul_opposite.unop a) (mul_opposite.unop y) (mul_opposite.unop x) ↔ semiconj_by a x y
source
theorem semiconj_by.op {α : Type u} [has_mul α] {a x y : α} (h : semiconj_by a x y) :
semiconj_by (mul_opposite.op a) (mul_opposite.op y) (mul_opposite.op x)
source
theorem add_semiconj_by.op {α : Type u} [has_add α] {a x y : α} (h : add_semiconj_by a x y) :
add_semiconj_by (add_opposite.op a) (add_opposite.op y) (add_opposite.op x)
source
theorem semiconj_by.unop {α : Type u} [has_mul α] {a x y : αᵐᵒᵖ} (h : semiconj_by a x y) :
semiconj_by (mul_opposite.unop a) (mul_opposite.unop y) (mul_opposite.unop x)
source
theorem add_semiconj_by.unop {α : Type u} [has_add α] {a x y : αᵃᵒᵖ} (h : add_semiconj_by a x y) :
add_semiconj_by (add_opposite.unop a) (add_opposite.unop y) (add_opposite.unop x)
source
theorem commute.op {α : Type u} [has_mul α] {x y : α} (h : commute x y) :
commute (mul_opposite.op x) (mul_opposite.op y)
source
theorem add_commute.op {α : Type u} [has_add α] {x y : α} (h : add_commute x y) :
add_commute (add_opposite.op x) (add_opposite.op y)
source
theorem add_opposite.commute.unop {α : Type u} [has_add α] {x y : αᵃᵒᵖ} (h : add_commute x y) :
add_commute (add_opposite.unop x) (add_opposite.unop y)
source
theorem mul_opposite.commute.unop {α : Type u} [has_mul α] {x y : αᵐᵒᵖ} (h : commute x y) :
commute (mul_opposite.unop x) (mul_opposite.unop y)
source
@[simp]
theorem add_opposite.commute_op {α : Type u} [has_add α] {x y : α} :
add_commute (add_opposite.op x) (add_opposite.op y) ↔ add_commute x y
source
@[simp]
theorem mul_opposite.commute_op {α : Type u} [has_mul α] {x y : α} :
commute (mul_opposite.op x) (mul_opposite.op y) ↔ commute x y
source
@[simp]
theorem mul_opposite.commute_unop {α : Type u} [has_mul α] {x y : αᵐᵒᵖ} :
commute (mul_opposite.unop x) (mul_opposite.unop y) ↔ commute x y
source
@[simp]
theorem add_opposite.commute_unop {α : Type u} [has_add α] {x y : αᵃᵒᵖ} :
add_commute (add_opposite.unop x) (add_opposite.unop y) ↔ add_commute x y
source
@[simp]
theorem mul_opposite.op_add_equiv_symm_apply {α : Type u} [has_add α] :
⇑(mul_opposite.op_add_equiv.symm) = mul_opposite.unop
source
def mul_opposite.op_add_equiv {α : Type u} [has_add α] :
α ≃+ αᵐᵒᵖ

The function mul_opposite.op is an additive equivalence.

Equations
source
@[simp]
theorem mul_opposite.op_add_equiv_apply {α : Type u} [has_add α] :
⇑mul_opposite.op_add_equiv = mul_opposite.op
source
@[simp]
theorem mul_opposite.op_add_equiv_to_equiv {α : Type u} [has_add α] :
mul_opposite.op_add_equiv.to_equiv = mul_opposite.op_equiv

Multiplicative structures on αᵃᵒᵖ #

source
@[protected, instance]
def add_opposite.semigroup (α : Type u) [semigroup α] :
semigroup αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.left_cancel_semigroup (α : Type u) [left_cancel_semigroup α] :
left_cancel_semigroup αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.right_cancel_semigroup (α : Type u) [right_cancel_semigroup α] :
right_cancel_semigroup αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.comm_semigroup (α : Type u) [comm_semigroup α] :
comm_semigroup αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.mul_one_class (α : Type u) [mul_one_class α] :
mul_one_class αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.has_pow (α : Type u) {β : Type u_1} [has_pow α β] :
has_pow αᵃᵒᵖ β
Equations
source
@[simp]
theorem add_opposite.op_pow (α : Type u) {β : Type u_1} [has_pow α β] (a : α) (b : β) :
add_opposite.op (a ^ b) = add_opposite.op a ^ b
source
@[simp]
theorem add_opposite.unop_pow (α : Type u) {β : Type u_1} [has_pow α β] (a : αᵃᵒᵖ) (b : β) :
add_opposite.unop (a ^ b) = add_opposite.unop a ^ b
source
@[protected, instance]
def add_opposite.monoid (α : Type u) [monoid α] :
monoid αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.comm_monoid (α : Type u) [comm_monoid α] :
comm_monoid αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.div_inv_monoid (α : Type u) [div_inv_monoid α] :
div_inv_monoid αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.group (α : Type u) [group α] :
group αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.comm_group (α : Type u) [comm_group α] :
comm_group αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.add_comm_monoid_with_one (α : Type u) [add_comm_monoid_with_one α] :
add_comm_monoid_with_one αᵃᵒᵖ
Equations
source
@[protected, instance]
def add_opposite.add_comm_group_with_one (α : Type u) [add_comm_group_with_one α] :
add_comm_group_with_one αᵃᵒᵖ
Equations
source
@[simp]
theorem add_opposite.op_mul_equiv_apply {α : Type u} [has_mul α] :
⇑add_opposite.op_mul_equiv = add_opposite.op
source
@[simp]
theorem add_opposite.op_mul_equiv_symm_apply {α : Type u} [has_mul α] :
⇑(add_opposite.op_mul_equiv.symm) = add_opposite.unop
source
def add_opposite.op_mul_equiv {α : Type u} [has_mul α] :
α ≃* αᵃᵒᵖ

The function add_opposite.op is a multiplicative equivalence.

Equations
source
@[simp]
theorem add_opposite.op_mul_equiv_to_equiv {α : Type u} [has_mul α] :
add_opposite.op_mul_equiv.to_equiv = add_opposite.op_equiv
source
@[simp]
theorem add_equiv.neg'_symm_apply (G : Type u_1) [subtraction_monoid G] :
⇑((add_equiv.neg' G).symm) = ⇑((equiv.trans (equiv.neg G) add_opposite.op_equiv).symm)
source
@[simp]
theorem mul_equiv.inv'_symm_apply (G : Type u_1) [division_monoid G] :
⇑((mul_equiv.inv' G).symm) = ⇑((equiv.trans (equiv.inv G) mul_opposite.op_equiv).symm)
source
def add_equiv.neg' (G : Type u_1) [subtraction_monoid G] :
G ≃+ Gᵃᵒᵖ

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

Equations
source
@[simp]
theorem add_equiv.neg'_apply (G : Type u_1) [subtraction_monoid G] :
⇑(add_equiv.neg' G) = add_opposite.op ∘ has_neg.neg
source
@[simp]
theorem mul_equiv.inv'_apply (G : Type u_1) [division_monoid G] :
⇑(mul_equiv.inv' G) = mul_opposite.op ∘ has_inv.inv
source
def mul_equiv.inv' (G : Type u_1) [division_monoid 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 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)) :
⇑(f.to_opposite hf) = mul_opposite.op ∘ ⇑f
source
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)) :
add_hom M Nᵃᵒᵖ

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
source
@[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)) :
⇑(f.to_opposite hf) = add_opposite.op ∘ ⇑f
source
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)) :
M →ₙ* Nᵐᵒᵖ

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
source
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)) :
add_hom Mᵃᵒᵖ N

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
source
@[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)) :
⇑(f.from_opposite hf) = ⇑f ∘ add_opposite.unop
source
@[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)) :
⇑(f.from_opposite hf) = ⇑f ∘ mul_opposite.unop
source
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)) :
Mᵐᵒᵖ →ₙ* N

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
source
@[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)) :
⇑(f.to_opposite hf) = add_opposite.op ∘ ⇑f
source
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)) :
M →+ Nᵃᵒᵖ

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
source
@[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)) :
⇑(f.to_opposite hf) = mul_opposite.op ∘ ⇑f
source
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)) :
M →* Nᵐᵒᵖ

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
source
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)) :
Mᵃᵒᵖ →+ N

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
source
@[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)) :
⇑(f.from_opposite hf) = ⇑f ∘ add_opposite.unop
source
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)) :
Mᵐᵒᵖ →* N

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
source
@[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)) :
⇑(f.from_opposite hf) = ⇑f ∘ mul_opposite.unop
source
def add_units.op_equiv {M : Type u_1} [add_monoid M] :
add_units Mᵃᵒᵖ ≃+ (add_units M)ᵃᵒᵖ

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

Equations
source
def units.op_equiv {M : Type u_1} [monoid M] :
Mᵐᵒᵖˣ ≃* Mˣᵐᵒᵖ

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

Equations
source
@[simp]
theorem add_units.coe_unop_op_equiv {M : Type u_1} [add_monoid M] (u : add_units Mᵃᵒᵖ) :
↑(add_opposite.unop (⇑add_units.op_equiv u)) = add_opposite.unop ↑u
source
@[simp]
theorem units.coe_unop_op_equiv {M : Type u_1} [monoid M] (u : Mᵐᵒᵖˣ) :
↑(mul_opposite.unop (⇑units.op_equiv u)) = mul_opposite.unop ↑u
source
@[simp]
theorem add_units.coe_op_equiv_symm {M : Type u_1} [add_monoid M] (u : (add_units M)ᵃᵒᵖ) :
↑(⇑(add_units.op_equiv.symm) u) = add_opposite.op ↑(add_opposite.unop u)
source
@[simp]
theorem units.coe_op_equiv_symm {M : Type u_1} [monoid M] (u : Mˣᵐᵒᵖ) :
↑(⇑(units.op_equiv.symm) u) = mul_opposite.op ↑(mul_opposite.unop u)
source
theorem is_add_unit.op {M : Type u_1} [add_monoid M] {m : M} (h : is_add_unit m) :
is_add_unit (add_opposite.op m)
source
theorem is_unit.op {M : Type u_1} [monoid M] {m : M} (h : is_unit m) :
is_unit (mul_opposite.op m)
source
theorem is_unit.unop {M : Type u_1} [monoid M] {m : Mᵐᵒᵖ} (h : is_unit m) :
is_unit (mul_opposite.unop m)
source
theorem is_add_unit.unop {M : Type u_1} [add_monoid M] {m : Mᵃᵒᵖ} (h : is_add_unit m) :
is_add_unit (add_opposite.unop m)
source
@[simp]
theorem is_add_unit_op {M : Type u_1} [add_monoid M] {m : M} :
is_add_unit (add_opposite.op m) ↔ is_add_unit m
source
@[simp]
theorem is_unit_op {M : Type u_1} [monoid M] {m : M} :
is_unit (mul_opposite.op m) ↔ is_unit m
source
@[simp]
theorem is_unit_unop {M : Type u_1} [monoid M] {m : Mᵐᵒᵖ} :
is_unit (mul_opposite.unop m) ↔ is_unit m
source
@[simp]
theorem is_add_unit_unop {M : Type u_1} [add_monoid M] {m : Mᵃᵒᵖ} :
is_add_unit (add_opposite.unop m) ↔ is_add_unit m
source
@[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ᵃᵒᵖ) :
⇑(⇑add_hom.op f) ᾰ = (add_opposite.op ∘ ⇑f ∘ add_opposite.unop) ᾰ
source
@[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) :
⇑(⇑(mul_hom.op.symm) f) ᾰ = (mul_opposite.unop ∘ ⇑f ∘ mul_opposite.op) ᾰ
source
def add_hom.op {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] :
add_hom M N ≃ add_hom Mᵃᵒᵖ 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
source
def mul_hom.op {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] :
(M →ₙ* N) ≃ (Mᵐᵒᵖ →ₙ* 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
source
@[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ᵐᵒᵖ) :
⇑(⇑mul_hom.op f) ᾰ = (mul_opposite.op ∘ ⇑f ∘ mul_opposite.unop) ᾰ
source
@[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) :
⇑(⇑(add_hom.op.symm) f) ᾰ = (add_opposite.unop ∘ ⇑f ∘ add_opposite.op) ᾰ
source
@[simp]
def mul_hom.unop {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] :
(Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ) ≃ (M →ₙ* N)

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

Equations
source
@[simp]
def add_hom.unop {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] :
add_hom Mᵃᵒᵖ Nᵃᵒᵖ ≃ add_hom M N

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

Equations
source
@[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ᵐᵒᵖ) :
⇑(⇑add_hom.mul_op f) ᾰ = (mul_opposite.op ∘ ⇑f ∘ mul_opposite.unop) ᾰ
source
@[simp]
theorem add_hom.mul_op_symm_apply_apply {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : add_hom Mᵐᵒᵖ Nᵐᵒᵖ) (ᾰ : M) :
⇑(⇑(add_hom.mul_op.symm) f) ᾰ = (mul_opposite.unop ∘ ⇑f ∘ mul_opposite.op) ᾰ
source
def add_hom.mul_op {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] :
add_hom M N ≃ add_hom Mᵐᵒᵖ 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
source
@[simp]
def add_hom.mul_unop {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] :
add_hom αᵐᵒᵖ βᵐᵒᵖ ≃ add_hom α β

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

Equations
source
def add_monoid_hom.op {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :
(M →+ N) ≃ (Mᵃᵒᵖ →+ 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
source
def monoid_hom.op {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :
(M →* N) ≃ (Mᵐᵒᵖ →* 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
source
@[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ᵐᵒᵖ) :
⇑(⇑monoid_hom.op f) ᾰ = (mul_opposite.op ∘ ⇑f ∘ mul_opposite.unop) ᾰ
source
@[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) :
⇑(⇑(monoid_hom.op.symm) f) ᾰ = (mul_opposite.unop ∘ ⇑f ∘ mul_opposite.op) ᾰ
source
@[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ᵃᵒᵖ) :
⇑(⇑add_monoid_hom.op f) ᾰ = (add_opposite.op ∘ ⇑f ∘ add_opposite.unop) ᾰ
source
@[simp]
theorem add_monoid_hom.op_symm_apply_apply {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) (ᾰ : M) :
⇑(⇑(add_monoid_hom.op.symm) f) ᾰ = (add_opposite.unop ∘ ⇑f ∘ add_opposite.op) ᾰ
source
@[simp]
def add_monoid_hom.unop {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :
(Mᵃᵒᵖ →+ Nᵃᵒᵖ) ≃ (M →+ N)

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

Equations
source
@[simp]
def monoid_hom.unop {M : Type u_1} {N : Type u_2} [mul_one_class M] [mul_one_class N] :
(Mᵐᵒᵖ →* Nᵐᵒᵖ) ≃ (M →* N)

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

Equations
source
def add_monoid_hom.mul_op {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] :
(M →+ N) ≃ (Mᵐᵒᵖ →+ 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
source
@[simp]
theorem add_monoid_hom.mul_op_symm_apply_apply {M : Type u_1} {N : Type u_2} [add_zero_class M] [add_zero_class N] (f : Mᵐᵒᵖ →+ Nᵐᵒᵖ) (ᾰ : M) :
⇑(⇑(add_monoid_hom.mul_op.symm) f) ᾰ = (mul_opposite.unop ∘ ⇑f ∘ mul_opposite.op) ᾰ
source
@[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ᵐᵒᵖ) :
⇑(⇑add_monoid_hom.mul_op f) ᾰ = (mul_opposite.op ∘ ⇑f ∘ mul_opposite.unop) ᾰ
source
@[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
source
@[simp]
theorem add_equiv.mul_op_apply {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] (f : α ≃+ β) :
⇑add_equiv.mul_op f = mul_opposite.op_add_equiv.symm.trans (f.trans mul_opposite.op_add_equiv)
source
@[simp]
theorem add_equiv.mul_op_symm_apply {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] (f : αᵐᵒᵖ ≃+ βᵐᵒᵖ) :
⇑(add_equiv.mul_op.symm) f = mul_opposite.op_add_equiv.trans (f.trans mul_opposite.op_add_equiv.symm)
source
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
source
@[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
source
@[simp]
theorem add_equiv.op_symm_apply_symm_apply {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) (ᾰ : β) :
⇑((⇑(add_equiv.op.symm) f).symm) ᾰ = (add_opposite.unop ∘ ⇑(f.symm) ∘ add_opposite.op) ᾰ
source
@[simp]
theorem mul_equiv.op_symm_apply_apply {α : Type u_1} {β : Type u_2} [has_mul α] [has_mul β] (f : αᵐᵒᵖ ≃* βᵐᵒᵖ) (ᾰ : α) :
⇑(⇑(mul_equiv.op.symm) f) ᾰ = (mul_opposite.unop ∘ ⇑f ∘ mul_opposite.op) ᾰ
source
@[simp]
theorem mul_equiv.op_symm_apply_symm_apply {α : Type u_1} {β : Type u_2} [has_mul α] [has_mul β] (f : αᵐᵒᵖ ≃* βᵐᵒᵖ) (ᾰ : β) :
⇑((⇑(mul_equiv.op.symm) f).symm) ᾰ = (mul_opposite.unop ∘ ⇑(f.symm) ∘ mul_opposite.op) ᾰ
source
def add_equiv.op {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] :
α ≃+ β ≃ (αᵃᵒᵖ ≃+ βᵃᵒᵖ)

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

Equations
source
@[simp]
theorem add_equiv.op_apply_symm_apply {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] (f : α ≃+ β) (ᾰ : βᵃᵒᵖ) :
⇑((⇑add_equiv.op f).symm) ᾰ = (add_opposite.op ∘ ⇑(f.symm) ∘ add_opposite.unop) ᾰ
source
@[simp]
theorem add_equiv.op_symm_apply_apply {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) (ᾰ : α) :
⇑(⇑(add_equiv.op.symm) f) ᾰ = (add_opposite.unop ∘ ⇑f ∘ add_opposite.op) ᾰ
source
def mul_equiv.op {α : Type u_1} {β : Type u_2} [has_mul α] [has_mul β] :
α ≃* β ≃ (αᵐᵒᵖ ≃* βᵐᵒᵖ)

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

Equations
source
@[simp]
theorem mul_equiv.op_apply_symm_apply {α : Type u_1} {β : Type u_2} [has_mul α] [has_mul β] (f : α ≃* β) (ᾰ : βᵐᵒᵖ) :
⇑((⇑mul_equiv.op f).symm) ᾰ = (mul_opposite.op ∘ ⇑(f.symm) ∘ mul_opposite.unop) ᾰ
source
@[simp]
theorem mul_equiv.op_apply_apply {α : Type u_1} {β : Type u_2} [has_mul α] [has_mul β] (f : α ≃* β) (ᾰ : αᵐᵒᵖ) :
⇑(⇑mul_equiv.op f) ᾰ = (mul_opposite.op ∘ ⇑f ∘ mul_opposite.unop) ᾰ
source
@[simp]
theorem add_equiv.op_apply_apply {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] (f : α ≃+ β) (ᾰ : αᵃᵒᵖ) :
⇑(⇑add_equiv.op f) ᾰ = (add_opposite.op ∘ ⇑f ∘ add_opposite.unop) ᾰ
source
@[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
source
@[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
source
@[ext]
theorem add_monoid_hom.mul_op_ext {α : Type u_1} {β : Type u_2} [add_zero_class α] [add_zero_class β] (f g : αᵐᵒᵖ →+ β) (h : f.comp mul_opposite.op_add_equiv.to_add_monoid_hom = g.comp mul_opposite.op_add_equiv.to_add_monoid_hom) :
f = g

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