Group structures on the multiplicative opposite #
Equations
- mul_opposite.add_comm_semigroup α = {add := add_semigroup.add (mul_opposite.add_semigroup α), add_assoc := _, add_comm := _}
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 := _}
Equations
Equations
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 := _}
Equations
- mul_opposite.semigroup α = {mul := has_mul.mul (mul_opposite.has_mul α), mul_assoc := _}
Equations
- mul_opposite.left_cancel_semigroup α = {mul := semigroup.mul (mul_opposite.semigroup α), mul_assoc := _, mul_left_cancel := _}
Equations
- mul_opposite.right_cancel_semigroup α = {mul := semigroup.mul (mul_opposite.semigroup α), mul_assoc := _, mul_right_cancel := _}
Equations
- mul_opposite.comm_semigroup α = {mul := semigroup.mul (mul_opposite.semigroup α), mul_assoc := _, mul_comm := _}
Equations
- mul_opposite.mul_one_class α = {one := 1, mul := has_mul.mul (mul_opposite.has_mul α), one_mul := _, mul_one := _}
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' := _}
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' := _}
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' := _}
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 := _}
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 := _}
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 := _}
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' := _}
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 := _}
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 := _}
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' := _}
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' := _}
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' := _}
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' := _}
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' := _}
A hom α →* β
can equivalently be viewed as a hom αᵐᵒᵖ →* βᵐᵒᵖ
. This is the action of the
(fully faithful) ᵐᵒᵖ
-functor on morphisms.
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.
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 := _}
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 := _}
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'
.