Group structures on the multiplicative and additive opposites #
Additive structures on αᵐᵒᵖ #
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
Multiplicative structures on αᵐᵒᵖ #
We also generate additive structures on αᵃᵒᵖ using to_additive
@[protected, instance]
Equations
- add_opposite.add_semigroup α = {add := has_add.add (add_opposite.has_add α), add_assoc := _}
@[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
- add_opposite.left_cancel_add_semigroup α = {add := add_semigroup.add (add_opposite.add_semigroup α), add_assoc := _, add_left_cancel := _}
@[protected, instance]
Equations
- mul_opposite.right_cancel_semigroup α = {mul := semigroup.mul (mul_opposite.semigroup α), mul_assoc := _, mul_right_cancel := _}
@[protected, instance]
Equations
- add_opposite.right_cancel_add_semigroup α = {add := add_semigroup.add (add_opposite.add_semigroup α), add_assoc := _, add_right_cancel := _}
@[protected, instance]
Equations
- mul_opposite.comm_semigroup α = {mul := semigroup.mul (mul_opposite.semigroup α), mul_assoc := _, mul_comm := _}
@[protected, instance]
Equations
- add_opposite.add_comm_semigroup α = {add := add_semigroup.add (add_opposite.add_semigroup α), add_assoc := _, add_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
- add_opposite.add_zero_class α = {zero := 0, add := has_add.add (add_opposite.has_add α), zero_add := _, add_zero := _}
@[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
- add_opposite.add_monoid α = {add := add_semigroup.add (add_opposite.add_semigroup α), add_assoc := _, zero := add_zero_class.zero (add_opposite.add_zero_class α), zero_add := _, add_zero := _, nsmul := λ (n : ℕ) (x : αᵃᵒᵖ), add_opposite.op (n • add_opposite.unop x), nsmul_zero' := _, nsmul_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
- add_opposite.left_cancel_add_monoid α = {add := add_left_cancel_semigroup.add (add_opposite.left_cancel_add_semigroup α), add_assoc := _, add_left_cancel := _, zero := add_monoid.zero (add_opposite.add_monoid α), zero_add := _, add_zero := _, nsmul := add_monoid.nsmul (add_opposite.add_monoid α), nsmul_zero' := _, nsmul_succ' := _}
@[protected, instance]
Equations
- add_opposite.right_cancel_add_monoid α = {add := add_right_cancel_semigroup.add (add_opposite.right_cancel_add_semigroup α), add_assoc := _, add_right_cancel := _, zero := add_monoid.zero (add_opposite.add_monoid α), zero_add := _, add_zero := _, nsmul := add_monoid.nsmul (add_opposite.add_monoid α), nsmul_zero' := _, nsmul_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
- add_opposite.cancel_add_monoid α = {add := add_right_cancel_monoid.add (add_opposite.right_cancel_add_monoid α), add_assoc := _, add_left_cancel := _, zero := add_right_cancel_monoid.zero (add_opposite.right_cancel_add_monoid α), zero_add := _, add_zero := _, nsmul := add_right_cancel_monoid.nsmul (add_opposite.right_cancel_add_monoid α), nsmul_zero' := _, nsmul_succ' := _, add_right_cancel := _}
@[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
- add_opposite.add_comm_monoid α = {add := add_monoid.add (add_opposite.add_monoid α), add_assoc := _, zero := add_monoid.zero (add_opposite.add_monoid α), zero_add := _, add_zero := _, nsmul := add_monoid.nsmul (add_opposite.add_monoid α), nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
@[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
- add_opposite.cancel_add_comm_monoid α = {add := add_cancel_monoid.add (add_opposite.cancel_add_monoid α), add_assoc := _, add_left_cancel := _, zero := add_cancel_monoid.zero (add_opposite.cancel_add_monoid α), zero_add := _, add_zero := _, nsmul := add_cancel_monoid.nsmul (add_opposite.cancel_add_monoid α), nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
@[protected, instance]
Equations
- add_opposite.sub_neg_add_monoid α = {add := add_monoid.add (add_opposite.add_monoid α), add_assoc := _, zero := add_monoid.zero (add_opposite.add_monoid α), zero_add := _, add_zero := _, nsmul := add_monoid.nsmul (add_opposite.add_monoid α), nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg (add_opposite.has_neg α), sub := λ (a b : αᵃᵒᵖ), add_monoid.add a (-b), sub_eq_add_neg := _, zsmul := λ (n : ℤ) (x : αᵃᵒᵖ), add_opposite.op (n • add_opposite.unop x), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _}
@[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
- add_opposite.add_group α = {add := sub_neg_monoid.add (add_opposite.sub_neg_add_monoid α), add_assoc := _, zero := sub_neg_monoid.zero (add_opposite.sub_neg_add_monoid α), zero_add := _, add_zero := _, nsmul := sub_neg_monoid.nsmul (add_opposite.sub_neg_add_monoid α), nsmul_zero' := _, nsmul_succ' := _, neg := sub_neg_monoid.neg (add_opposite.sub_neg_add_monoid α), sub := sub_neg_monoid.sub (add_opposite.sub_neg_add_monoid α), sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul (add_opposite.sub_neg_add_monoid α), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _}
@[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 := _}
@[protected, instance]
Equations
- add_opposite.add_comm_group α = {add := add_group.add (add_opposite.add_group α), add_assoc := _, zero := add_group.zero (add_opposite.add_group α), zero_add := _, add_zero := _, nsmul := add_group.nsmul (add_opposite.add_group α), nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg (add_opposite.add_group α), sub := add_group.sub (add_opposite.add_group α), sub_eq_add_neg := _, zsmul := add_group.zsmul (add_opposite.add_group α), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
@[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
@[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
@[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
@[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
@[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
@[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
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
@[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
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
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)
theorem
commute.op
{α : Type u}
[has_mul α]
{x y : α}
(h : commute x y) :
commute (mul_opposite.op x) (mul_opposite.op y)
@[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
@[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]
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
@[simp]
The function mul_opposite.op 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]
Multiplicative structures on αᵃᵒᵖ #
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
- add_opposite.has_pow α = {pow := λ (a : αᵃᵒᵖ) (b : β), add_opposite.op (add_opposite.unop a ^ b)}
@[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
@[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
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
@[simp]
The function add_opposite.op is a multiplicative equivalence.
Equations
- add_opposite.op_mul_equiv = {to_fun := add_opposite.op_equiv.to_fun, inv_fun := add_opposite.op_equiv.inv_fun, left_inv := _, right_inv := _, map_mul' := _}
@[simp]
@[simp]
theorem
add_equiv.neg'_symm_apply
(G : Type u_1)
[add_group G] :
⇑((add_equiv.neg' G).symm) = ⇑((equiv.trans (equiv.neg G) add_opposite.op_equiv).symm)
@[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)
Negation on an additive group is an add_equiv to the opposite group. When G
is commutative, there is add_equiv.inv.
Equations
- add_equiv.neg' G = {to_fun := (equiv.trans (equiv.neg G) add_opposite.op_equiv).to_fun, inv_fun := (equiv.trans (equiv.neg G) add_opposite.op_equiv).inv_fun, left_inv := _, right_inv := _, map_add' := _}
@[simp]
@[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
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
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
- f.to_opposite hf = {to_fun := add_opposite.op ∘ ⇑f, map_zero' := _, map_add' := _}
@[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
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
- f.to_opposite hf = {to_fun := mul_opposite.op ∘ ⇑f, map_one' := _, map_mul' := _}
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
- f.from_opposite hf = {to_fun := ⇑f ∘ add_opposite.unop, map_zero' := _, map_add' := _}
@[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
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
- f.from_opposite hf = {to_fun := ⇑f ∘ mul_opposite.unop, map_one' := _, map_mul' := _}
@[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
The additive units of the additive opposites are equivalent to the additive opposites of the additive units.
Equations
- add_units.op_equiv = {to_fun := λ (u : add_units Mᵃᵒᵖ), add_opposite.op {val := add_opposite.unop ↑u, neg := add_opposite.unop (↑-u), val_neg := _, neg_val := _}, inv_fun := add_opposite.rec (λ (u : add_units M), {val := add_opposite.op ↑u, neg := add_opposite.op (↑-u), val_neg := _, neg_val := _}), left_inv := _, right_inv := _, map_add' := _}
The units of the opposites are equivalent to the opposites of the units.
Equations
- units.op_equiv = {to_fun := λ (u : Mᵐᵒᵖˣ), mul_opposite.op {val := mul_opposite.unop ↑u, inv := mul_opposite.unop ↑u⁻¹, val_inv := _, inv_val := _}, inv_fun := mul_opposite.rec (λ (u : Mˣ), {val := mul_opposite.op ↑u, inv := mul_opposite.op ↑u⁻¹, val_inv := _, inv_val := _}), left_inv := _, right_inv := _, map_mul' := _}
@[simp]
@[simp]
@[simp]
@[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)
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.
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.
@[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) ᾰ
@[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) ᾰ
@[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) ᾰ
@[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) ᾰ
@[simp]
The 'unopposite' of an additive monoid homomorphism Mᵃᵒᵖ →+ Nᵃᵒᵖ. Inverse to
add_monoid_hom.op.
Equations
@[simp]
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.
@[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) ᾰ
@[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) ᾰ
@[simp]
The 'unopposite' of an additive monoid hom αᵐᵒᵖ →+ βᵐᵒᵖ. Inverse to
add_monoid_hom.mul_op.
Equations
@[simp]
A iso α ≃+ β can equivalently be viewed as an iso αᵐᵒᵖ ≃+ βᵐᵒᵖ.
Equations
- add_equiv.mul_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]
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 : αᵃᵒᵖ ≃+ βᵃᵒᵖ)
(ᾰ : β) :
⇑((⇑(add_equiv.op.symm) f).symm) ᾰ = (add_opposite.unop ∘ ⇑(f.symm) ∘ add_opposite.op) ᾰ
@[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
- add_equiv.op = {to_fun := λ (f : α ≃+ β), {to_fun := add_opposite.op ∘ ⇑f ∘ add_opposite.unop, inv_fun := add_opposite.op ∘ ⇑(f.symm) ∘ add_opposite.unop, left_inv := _, right_inv := _, map_add' := _}, inv_fun := λ (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ), {to_fun := add_opposite.unop ∘ ⇑f ∘ add_opposite.op, inv_fun := add_opposite.unop ∘ ⇑(f.symm) ∘ add_opposite.op, left_inv := _, right_inv := _, map_add' := _}, left_inv := _, right_inv := _}
@[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) ᾰ
@[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) ᾰ
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) ᾰ
@[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) ᾰ
@[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'.