Group structures on the multiplicative opposite #
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
- mul_opposite.add_comm_semigroup α = {add := add_semigroup.add (mul_opposite.add_semigroup α), add_assoc := _, add_comm := _}
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
- mul_opposite.add_comm_monoid α = {add := add_monoid.add (mul_opposite.add_monoid α), add_assoc := _, zero := add_monoid.zero (mul_opposite.add_monoid α), zero_add := _, add_zero := _, nsmul := add_monoid.nsmul (mul_opposite.add_monoid α), nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
- mul_opposite.add_comm_group α = {add := add_group.add (mul_opposite.add_group α), add_assoc := _, zero := add_group.zero (mul_opposite.add_group α), zero_add := _, add_zero := _, nsmul := add_group.nsmul (mul_opposite.add_group α), nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg (mul_opposite.add_group α), sub := add_group.sub (mul_opposite.add_group α), sub_eq_add_neg := _, zsmul := add_group.zsmul (mul_opposite.add_group α), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
@[protected, instance]
Equations
- mul_opposite.semigroup α = {mul := has_mul.mul (mul_opposite.has_mul α), mul_assoc := _}
@[protected, instance]
Equations
- mul_opposite.left_cancel_semigroup α = {mul := semigroup.mul (mul_opposite.semigroup α), mul_assoc := _, mul_left_cancel := _}
@[protected, instance]
Equations
- mul_opposite.right_cancel_semigroup α = {mul := semigroup.mul (mul_opposite.semigroup α), mul_assoc := _, mul_right_cancel := _}
@[protected, instance]
Equations
- mul_opposite.comm_semigroup α = {mul := semigroup.mul (mul_opposite.semigroup α), mul_assoc := _, mul_comm := _}
@[protected, instance]
Equations
- mul_opposite.mul_one_class α = {one := 1, mul := has_mul.mul (mul_opposite.has_mul α), one_mul := _, mul_one := _}
@[protected, instance]
Equations
- mul_opposite.monoid α = {mul := semigroup.mul (mul_opposite.semigroup α), mul_assoc := _, one := mul_one_class.one (mul_opposite.mul_one_class α), one_mul := _, mul_one := _, npow := λ (n : ℕ) (x : αᵐᵒᵖ), mul_opposite.op (mul_opposite.unop x ^ n), npow_zero' := _, npow_succ' := _}
@[protected, instance]
Equations
- mul_opposite.left_cancel_monoid α = {mul := left_cancel_semigroup.mul (mul_opposite.left_cancel_semigroup α), mul_assoc := _, mul_left_cancel := _, one := monoid.one (mul_opposite.monoid α), one_mul := _, mul_one := _, npow := monoid.npow (mul_opposite.monoid α), npow_zero' := _, npow_succ' := _}
@[protected, instance]
Equations
- mul_opposite.right_cancel_monoid α = {mul := right_cancel_semigroup.mul (mul_opposite.right_cancel_semigroup α), mul_assoc := _, mul_right_cancel := _, one := monoid.one (mul_opposite.monoid α), one_mul := _, mul_one := _, npow := monoid.npow (mul_opposite.monoid α), npow_zero' := _, npow_succ' := _}
@[protected, instance]
Equations
- mul_opposite.cancel_monoid α = {mul := right_cancel_monoid.mul (mul_opposite.right_cancel_monoid α), mul_assoc := _, mul_left_cancel := _, one := right_cancel_monoid.one (mul_opposite.right_cancel_monoid α), one_mul := _, mul_one := _, npow := right_cancel_monoid.npow (mul_opposite.right_cancel_monoid α), npow_zero' := _, npow_succ' := _, mul_right_cancel := _}
@[protected, instance]
Equations
- mul_opposite.comm_monoid α = {mul := monoid.mul (mul_opposite.monoid α), mul_assoc := _, one := monoid.one (mul_opposite.monoid α), one_mul := _, mul_one := _, npow := monoid.npow (mul_opposite.monoid α), npow_zero' := _, npow_succ' := _, mul_comm := _}
@[protected, instance]
Equations
- mul_opposite.cancel_comm_monoid α = {mul := cancel_monoid.mul (mul_opposite.cancel_monoid α), mul_assoc := _, mul_left_cancel := _, one := cancel_monoid.one (mul_opposite.cancel_monoid α), one_mul := _, mul_one := _, npow := cancel_monoid.npow (mul_opposite.cancel_monoid α), npow_zero' := _, npow_succ' := _, mul_comm := _}
@[protected, instance]
Equations
- mul_opposite.div_inv_monoid α = {mul := monoid.mul (mul_opposite.monoid α), mul_assoc := _, one := monoid.one (mul_opposite.monoid α), one_mul := _, mul_one := _, npow := monoid.npow (mul_opposite.monoid α), npow_zero' := _, npow_succ' := _, inv := has_inv.inv (mul_opposite.has_inv α), div := λ (a b : αᵐᵒᵖ), monoid.mul a b⁻¹, div_eq_mul_inv := _, zpow := λ (n : ℤ) (x : αᵐᵒᵖ), mul_opposite.op (mul_opposite.unop x ^ n), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _}
@[protected, instance]
Equations
- mul_opposite.group α = {mul := div_inv_monoid.mul (mul_opposite.div_inv_monoid α), mul_assoc := _, one := div_inv_monoid.one (mul_opposite.div_inv_monoid α), one_mul := _, mul_one := _, npow := div_inv_monoid.npow (mul_opposite.div_inv_monoid α), npow_zero' := _, npow_succ' := _, inv := div_inv_monoid.inv (mul_opposite.div_inv_monoid α), div := div_inv_monoid.div (mul_opposite.div_inv_monoid α), div_eq_mul_inv := _, zpow := div_inv_monoid.zpow (mul_opposite.div_inv_monoid α), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}
@[protected, instance]
Equations
- mul_opposite.comm_group α = {mul := group.mul (mul_opposite.group α), mul_assoc := _, one := group.one (mul_opposite.group α), one_mul := _, mul_one := _, npow := group.npow (mul_opposite.group α), npow_zero' := _, npow_succ' := _, inv := group.inv (mul_opposite.group α), div := group.div (mul_opposite.group α), div_eq_mul_inv := _, zpow := group.zpow (mul_opposite.group α), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}
theorem
mul_opposite.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)
theorem
mul_opposite.semiconj_by.unop
{α : Type u}
[has_mul α]
{a x y : αᵐᵒᵖ}
(h : semiconj_by a x y) :
@[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
@[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
theorem
mul_opposite.commute.op
{α : Type u}
[has_mul α]
{x y : α}
(h : commute x y) :
commute (mul_opposite.op x) (mul_opposite.op y)
@[simp]
theorem
mul_opposite.commute_op
{α : Type u}
[has_mul α]
{x y : α} :
commute (mul_opposite.op x) (mul_opposite.op y) ↔ commute x y
@[simp]
theorem
mul_opposite.commute_unop
{α : Type u}
[has_mul α]
{x y : αᵐᵒᵖ} :
commute (mul_opposite.unop x) (mul_opposite.unop y) ↔ commute x y
@[simp]
The function unop is an additive equivalence.
Equations
- mul_opposite.op_add_equiv = {to_fun := mul_opposite.op_equiv.to_fun, inv_fun := mul_opposite.op_equiv.inv_fun, left_inv := _, right_inv := _, map_add' := _}
@[simp]
@[simp]
@[simp]
theorem
mul_equiv.inv'_symm_apply
(G : Type u_1)
[group G] :
⇑((mul_equiv.inv' G).symm) = ⇑((equiv.trans (equiv.inv G) mul_opposite.op_equiv).symm)
@[simp]
Inversion on a group is a mul_equiv to the opposite group. When G is commutative, there is
mul_equiv.inv.
Equations
- mul_equiv.inv' G = {to_fun := (equiv.trans (equiv.inv G) mul_opposite.op_equiv).to_fun, inv_fun := (equiv.trans (equiv.inv G) mul_opposite.op_equiv).inv_fun, left_inv := _, right_inv := _, map_mul' := _}
@[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) = mul_opposite.op ∘ ⇑f
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
- f.to_opposite hf = {to_fun := mul_opposite.op ∘ ⇑f, map_one' := _, map_mul' := _}
def
monoid_hom.from_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 from Rᵐᵒᵖ.
Equations
- f.from_opposite hf = {to_fun := ⇑f ∘ mul_opposite.unop, map_one' := _, map_mul' := _}
@[simp]
theorem
monoid_hom.from_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.from_opposite hf) = ⇑f ∘ mul_opposite.unop
The units of the opposites are equivalent to the opposites of the units.
Equations
- units.op_equiv = {to_fun := λ (u : units Rᵐᵒᵖ), mul_opposite.op {val := mul_opposite.unop ↑u, inv := mul_opposite.unop ↑u⁻¹, val_inv := _, inv_val := _}, inv_fun := mul_opposite.rec (λ (u : units R), {val := mul_opposite.op ↑u, inv := mul_opposite.op ↑u⁻¹, val_inv := _, inv_val := _}), left_inv := _, right_inv := _, map_mul' := _}
@[simp]
@[simp]
theorem
units.coe_op_equiv_symm
{R : Type u_1}
[monoid R]
(u : (units R)ᵐᵒᵖ) :
↑(⇑(units.op_equiv.symm) u) = mul_opposite.op ↑(mul_opposite.unop u)
A hom α →* β can equivalently be viewed as a hom αᵐᵒᵖ →* βᵐᵒᵖ. This is the action of the
(fully faithful) ᵐᵒᵖ-functor on morphisms.
@[simp]
theorem
monoid_hom.op_apply_apply
{α : Type u_1}
{β : Type u_2}
[mul_one_class α]
[mul_one_class β]
(f : α →* β)
(ᾰ : αᵐᵒᵖ) :
⇑(⇑monoid_hom.op f) ᾰ = (mul_opposite.op ∘ ⇑f ∘ mul_opposite.unop) ᾰ
@[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) ᾰ = (mul_opposite.unop ∘ ⇑f ∘ mul_opposite.op) ᾰ
@[simp]
The 'unopposite' of a monoid hom αᵐᵒᵖ →* βᵐᵒᵖ. Inverse to monoid_hom.op.
Equations
A hom α →+ β can equivalently be viewed as a hom αᵐᵒᵖ →+ βᵐᵒᵖ. This is the action of the
(fully faithful) ᵐᵒᵖ-functor on morphisms.
@[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) ᾰ = (mul_opposite.op ∘ ⇑f ∘ mul_opposite.unop) ᾰ
@[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) ᾰ = (mul_opposite.unop ∘ ⇑f ∘ mul_opposite.op) ᾰ
@[simp]
The 'unopposite' of an additive monoid hom αᵐᵒᵖ →+ βᵐᵒᵖ. Inverse to add_monoid_hom.op.
Equations
A iso α ≃+ β can equivalently be viewed as an iso αᵐᵒᵖ ≃+ βᵐᵒᵖ.
Equations
- add_equiv.op = {to_fun := λ (f : α ≃+ β), mul_opposite.op_add_equiv.symm.trans (f.trans mul_opposite.op_add_equiv), inv_fun := λ (f : αᵐᵒᵖ ≃+ βᵐᵒᵖ), mul_opposite.op_add_equiv.trans (f.trans mul_opposite.op_add_equiv.symm), left_inv := _, right_inv := _}
@[simp]
@[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) ᾰ
@[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) ᾰ
A iso α ≃* β can equivalently be viewed as an iso αᵐᵒᵖ ≃+ βᵐᵒᵖ.
Equations
- mul_equiv.op = {to_fun := λ (f : α ≃* β), {to_fun := mul_opposite.op ∘ ⇑f ∘ mul_opposite.unop, inv_fun := mul_opposite.op ∘ ⇑(f.symm) ∘ mul_opposite.unop, left_inv := _, right_inv := _, map_mul' := _}, inv_fun := λ (f : αᵐᵒᵖ ≃* βᵐᵒᵖ), {to_fun := mul_opposite.unop ∘ ⇑f ∘ mul_opposite.op, inv_fun := mul_opposite.unop ∘ ⇑(f.symm) ∘ mul_opposite.op, left_inv := _, right_inv := _, map_mul' := _}, left_inv := _, right_inv := _}
@[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) ᾰ
@[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) ᾰ
@[ext]
theorem
add_monoid_hom.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'.