Group structures on the multiplicative and additive opposites #

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

Equations

f.toOpposite hf = { toFun := AddOpposite.op ∘ ⇑f, map_add' := ⋯ }

source

@[simp]

theorem MulHom.toOpposite_apply {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] (f : M →ₙ* N) (hf : ∀ (x y : M), Commute (f x) (f y)) :

⇑(f.toOpposite hf) = MulOpposite.op ∘ ⇑f

source

@[simp]

theorem AddHom.toOpposite_apply {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : AddHom M N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) :

⇑(f.toOpposite hf) = AddOpposite.op ∘ ⇑f

source

def MulHom.toOpposite {M : Type u_2} {N : Type u_3} [Mul M] [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

f.toOpposite hf = { toFun := MulOpposite.op ∘ ⇑f, map_mul' := ⋯ }

source

def AddHom.fromOpposite {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : AddHom M N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) :

AddHom Mᵃᵒᵖ N

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

Equations

f.fromOpposite hf = { toFun := ⇑f ∘ AddOpposite.unop, map_add' := ⋯ }

source

@[simp]

theorem AddHom.fromOpposite_apply {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : AddHom M N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) :

⇑(f.fromOpposite hf) = ⇑f ∘ AddOpposite.unop

source

@[simp]

theorem MulHom.fromOpposite_apply {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] (f : M →ₙ* N) (hf : ∀ (x y : M), Commute (f x) (f y)) :

⇑(f.fromOpposite hf) = ⇑f ∘ MulOpposite.unop

source

def MulHom.fromOpposite {M : Type u_2} {N : Type u_3} [Mul M] [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

f.fromOpposite hf = { toFun := ⇑f ∘ MulOpposite.unop, map_mul' := ⋯ }

source

def AddMonoidHom.toOpposite {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (hf : ∀ (x y : M), AddCommute (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

f.toOpposite hf = { toFun := AddOpposite.op ∘ ⇑f, map_zero' := ⋯, map_add' := ⋯ }

source

@[simp]

theorem AddMonoidHom.toOpposite_apply {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) :

⇑(f.toOpposite hf) = AddOpposite.op ∘ ⇑f

source

@[simp]

theorem MonoidHom.toOpposite_apply {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass N] (f : M →* N) (hf : ∀ (x y : M), Commute (f x) (f y)) :

⇑(f.toOpposite hf) = MulOpposite.op ∘ ⇑f

source

def MonoidHom.toOpposite {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass 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

f.toOpposite hf = { toFun := MulOpposite.op ∘ ⇑f, map_one' := ⋯, map_mul' := ⋯ }

source

def AddMonoidHom.fromOpposite {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (hf : ∀ (x y : M), AddCommute (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

f.fromOpposite hf = { toFun := ⇑f ∘ AddOpposite.unop, map_zero' := ⋯, map_add' := ⋯ }

source

@[simp]

theorem MonoidHom.fromOpposite_apply {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass N] (f : M →* N) (hf : ∀ (x y : M), Commute (f x) (f y)) :

⇑(f.fromOpposite hf) = ⇑f ∘ MulOpposite.unop

source

@[simp]

theorem AddMonoidHom.fromOpposite_apply {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) :

⇑(f.fromOpposite hf) = ⇑f ∘ AddOpposite.unop

source

def MonoidHom.fromOpposite {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass 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

f.fromOpposite hf = { toFun := ⇑f ∘ MulOpposite.unop, map_one' := ⋯, map_mul' := ⋯ }

source

def AddUnits.opEquiv {M : Type u_2} [AddMonoid M] :

AddUnits Mᵃᵒᵖ ≃+ (AddUnits M)ᵃᵒᵖ

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

Equations

One or more equations did not get rendered due to their size.

source

def Units.opEquiv {M : Type u_2} [Monoid M] :

Mᵐᵒᵖˣ ≃* Mˣᵐᵒᵖ

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

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem AddUnits.coe_unop_opEquiv {M : Type u_2} [AddMonoid M] (u : AddUnits Mᵃᵒᵖ) :

↑(AddOpposite.unop (AddUnits.opEquiv u)) = AddOpposite.unop ↑u

source

@[simp]

theorem Units.coe_unop_opEquiv {M : Type u_2} [Monoid M] (u : Mᵐᵒᵖˣ) :

↑(MulOpposite.unop (Units.opEquiv u)) = MulOpposite.unop ↑u

source

@[simp]

theorem AddUnits.coe_opEquiv_symm {M : Type u_2} [AddMonoid M] (u : (AddUnits M)ᵃᵒᵖ) :

↑(AddUnits.opEquiv.symm u) = AddOpposite.op ↑(AddOpposite.unop u)

source

@[simp]

theorem Units.coe_opEquiv_symm {M : Type u_2} [Monoid M] (u : Mˣᵐᵒᵖ) :

↑(Units.opEquiv.symm u) = MulOpposite.op ↑(MulOpposite.unop u)

source

theorem IsAddUnit.op {M : Type u_2} [AddMonoid M] {m : M} (h : IsAddUnit m) :

IsAddUnit (AddOpposite.op m)

source

theorem IsUnit.op {M : Type u_2} [Monoid M] {m : M} (h : IsUnit m) :

IsUnit (MulOpposite.op m)

source

theorem IsAddUnit.unop {M : Type u_2} [AddMonoid M] {m : Mᵃᵒᵖ} (h : IsAddUnit m) :

IsAddUnit (AddOpposite.unop m)

source

theorem IsUnit.unop {M : Type u_2} [Monoid M] {m : Mᵐᵒᵖ} (h : IsUnit m) :

IsUnit (MulOpposite.unop m)

source

@[simp]

theorem isAddUnit_op {M : Type u_2} [AddMonoid M] {m : M} :

IsAddUnit (AddOpposite.op m) ↔ IsAddUnit m

source

@[simp]

theorem isUnit_op {M : Type u_2} [Monoid M] {m : M} :

IsUnit (MulOpposite.op m) ↔ IsUnit m

source

@[simp]

theorem isAddUnit_unop {M : Type u_2} [AddMonoid M] {m : Mᵃᵒᵖ} :

IsAddUnit (AddOpposite.unop m) ↔ IsAddUnit m

source

@[simp]

theorem isUnit_unop {M : Type u_2} [Monoid M] {m : Mᵐᵒᵖ} :

IsUnit (MulOpposite.unop m) ↔ IsUnit m

source

def AddHom.op {M : Type u_2} {N : Type u_3} [Add M] [Add N] :

AddHom M N ≃ AddHom Mᵃᵒᵖ Nᵃᵒᵖ

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

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem AddHom.op_apply_apply {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : AddHom M N) :

∀ (a : Mᵃᵒᵖ), (AddHom.op f) a = (AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) a

source

@[simp]

theorem MulHom.op_symm_apply_apply {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] (f : Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ) :

∀ (a : M), (MulHom.op.symm f) a = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a

source

@[simp]

theorem MulHom.op_apply_apply {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] (f : M →ₙ* N) :

∀ (a : Mᵐᵒᵖ), (MulHom.op f) a = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a

source

@[simp]

theorem AddHom.op_symm_apply_apply {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : AddHom Mᵃᵒᵖ Nᵃᵒᵖ) :

∀ (a : M), (AddHom.op.symm f) a = (AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op) a

source

def MulHom.op {M : Type u_2} {N : Type u_3} [Mul M] [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

One or more equations did not get rendered due to their size.

source

def AddHom.unop {M : Type u_2} {N : Type u_3} [Add M] [Add N] :

AddHom Mᵃᵒᵖ Nᵃᵒᵖ ≃ AddHom M N

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

Equations

AddHom.unop = AddHom.op.symm

source

def MulHom.unop {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] :

(Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ) ≃ (M →ₙ* N)

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

Equations

MulHom.unop = MulHom.op.symm

source

@[simp]

theorem AddHom.mulOp_apply_apply {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : AddHom M N) :

∀ (a : Mᵐᵒᵖ), (AddHom.mulOp f) a = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a

source

@[simp]

theorem AddHom.mulOp_symm_apply_apply {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : AddHom Mᵐᵒᵖ Nᵐᵒᵖ) :

∀ (a : M), (AddHom.mulOp.symm f) a = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a

source

def AddHom.mulOp {M : Type u_2} {N : Type u_3} [Add M] [Add N] :

AddHom M N ≃ AddHom Mᵐᵒᵖ Nᵐᵒᵖ

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

Equations

One or more equations did not get rendered due to their size.

source

def AddHom.mulUnop {α : Type u_2} {β : Type u_3} [Add α] [Add β] :

AddHom αᵐᵒᵖ βᵐᵒᵖ ≃ AddHom α β

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

Equations

AddHom.mulUnop = AddHom.mulOp.symm

source

def AddMonoidHom.op {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass 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

One or more equations did not get rendered due to their size.

source

@[simp]

theorem AddMonoidHom.op_symm_apply_apply {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) :

∀ (a : M), (AddMonoidHom.op.symm f) a = (AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op) a

source

@[simp]

theorem MonoidHom.op_apply_apply {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass N] (f : M →* N) :

∀ (a : Mᵐᵒᵖ), (MonoidHom.op f) a = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a

source

@[simp]

theorem AddMonoidHom.op_apply_apply {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :

∀ (a : Mᵃᵒᵖ), (AddMonoidHom.op f) a = (AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) a

source

@[simp]

theorem MonoidHom.op_symm_apply_apply {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass N] (f : Mᵐᵒᵖ →* Nᵐᵒᵖ) :

∀ (a : M), (MonoidHom.op.symm f) a = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a

source

def MonoidHom.op {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass 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

One or more equations did not get rendered due to their size.

source

def AddMonoidHom.unop {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] :

(Mᵃᵒᵖ →+ Nᵃᵒᵖ) ≃ (M →+ N)

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

Equations

AddMonoidHom.unop = AddMonoidHom.op.symm

source

def MonoidHom.unop {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass N] :

(Mᵐᵒᵖ →* Nᵐᵒᵖ) ≃ (M →* N)

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

Equations

MonoidHom.unop = MonoidHom.op.symm

source

def AddEquiv.opOp (M : Type u_2) [Add M] :

M ≃+ Mᵃᵒᵖᵃᵒᵖ

A additive monoid is isomorphic to the opposite of its opposite.

Equations

AddEquiv.opOp M = { toEquiv := AddOpposite.opEquiv.trans AddOpposite.opEquiv, map_add' := ⋯ }

source

@[simp]

theorem MulEquiv.opOp_apply (M : Type u_2) [Mul M] :

∀ (a : M), (MulEquiv.opOp M) a = MulOpposite.op (MulOpposite.op a)

source

@[simp]

theorem MulEquiv.opOp_symm_apply (M : Type u_2) [Mul M] :

∀ (a : Mᵐᵒᵖᵐᵒᵖ), (MulEquiv.opOp M).symm a = MulOpposite.unop (MulOpposite.unop a)

source

@[simp]

theorem AddEquiv.opOp_apply (M : Type u_2) [Add M] :

∀ (a : M), (AddEquiv.opOp M) a = AddOpposite.op (AddOpposite.op a)

source

@[simp]

theorem AddEquiv.opOp_symm_apply (M : Type u_2) [Add M] :

∀ (a : Mᵃᵒᵖᵃᵒᵖ), (AddEquiv.opOp M).symm a = AddOpposite.unop (AddOpposite.unop a)

source

def MulEquiv.opOp (M : Type u_2) [Mul M] :

M ≃* Mᵐᵒᵖᵐᵒᵖ

A monoid is isomorphic to the opposite of its opposite.

Equations

MulEquiv.opOp M = { toEquiv := MulOpposite.opEquiv.trans MulOpposite.opEquiv, map_mul' := ⋯ }

source

@[simp]

theorem AddMonoidHom.mulOp_symm_apply_apply {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : Mᵐᵒᵖ →+ Nᵐᵒᵖ) :

∀ (a : M), (AddMonoidHom.mulOp.symm f) a = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a

source

@[simp]

theorem AddMonoidHom.mulOp_apply_apply {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :

∀ (a : Mᵐᵒᵖ), (AddMonoidHom.mulOp f) a = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a

source

def AddMonoidHom.mulOp {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass 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

One or more equations did not get rendered due to their size.

source

def AddMonoidHom.mulUnop {α : Type u_2} {β : Type u_3} [AddZeroClass α] [AddZeroClass β] :

(αᵐᵒᵖ →+ βᵐᵒᵖ) ≃ (α →+ β)

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

Equations

AddMonoidHom.mulUnop = AddMonoidHom.mulOp.symm

source

@[simp]

theorem AddEquiv.mulOp_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : α ≃+ β) :

AddEquiv.mulOp f = MulOpposite.opAddEquiv.symm.trans (f.trans MulOpposite.opAddEquiv)

source

@[simp]

theorem AddEquiv.mulOp_symm_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : αᵐᵒᵖ ≃+ βᵐᵒᵖ) :

AddEquiv.mulOp.symm f = MulOpposite.opAddEquiv.trans (f.trans MulOpposite.opAddEquiv.symm)

source

def AddEquiv.mulOp {α : Type u_2} {β : Type u_3} [Add α] [Add β] :

α ≃+ β ≃ (αᵐᵒᵖ ≃+ βᵐᵒᵖ)

An iso α ≃+ β can equivalently be viewed as an iso αᵐᵒᵖ ≃+ βᵐᵒᵖ.

Equations

One or more equations did not get rendered due to their size.

source

def AddEquiv.mulUnop {α : Type u_2} {β : Type u_3} [Add α] [Add β] :

αᵐᵒᵖ ≃+ βᵐᵒᵖ ≃ (α ≃+ β)

The 'unopposite' of an iso αᵐᵒᵖ ≃+ βᵐᵒᵖ. Inverse to AddEquiv.mul_op.

Equations

AddEquiv.mulUnop = AddEquiv.mulOp.symm

source

def AddEquiv.op {α : Type u_2} {β : Type u_3} [Add α] [Add β] :

α ≃+ β ≃ (αᵃᵒᵖ ≃+ βᵃᵒᵖ)

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

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem MulEquiv.op_symm_apply_symm_apply {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] (f : αᵐᵒᵖ ≃* βᵐᵒᵖ) :

∀ (a : β), (MulEquiv.op.symm f).symm a = (MulOpposite.unop ∘ ⇑f.symm ∘ MulOpposite.op) a

source

@[simp]

theorem AddEquiv.op_apply_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : α ≃+ β) :

∀ (a : αᵃᵒᵖ), (AddEquiv.op f) a = (AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) a

source

@[simp]

theorem MulEquiv.op_apply_symm_apply {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] (f : α ≃* β) :

∀ (a : βᵐᵒᵖ), (MulEquiv.op f).symm a = (MulOpposite.op ∘ ⇑f.symm ∘ MulOpposite.unop) a

source

@[simp]

theorem AddEquiv.op_symm_apply_symm_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) :

∀ (a : β), (AddEquiv.op.symm f).symm a = (AddOpposite.unop ∘ ⇑f.symm ∘ AddOpposite.op) a

source

@[simp]

theorem AddEquiv.op_apply_symm_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : α ≃+ β) :

∀ (a : βᵃᵒᵖ), (AddEquiv.op f).symm a = (AddOpposite.op ∘ ⇑f.symm ∘ AddOpposite.unop) a

source

@[simp]

theorem MulEquiv.op_symm_apply_apply {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] (f : αᵐᵒᵖ ≃* βᵐᵒᵖ) :

∀ (a : α), (MulEquiv.op.symm f) a = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a

source

@[simp]

theorem MulEquiv.op_apply_apply {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] (f : α ≃* β) :

∀ (a : αᵐᵒᵖ), (MulEquiv.op f) a = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a

source

@[simp]

theorem AddEquiv.op_symm_apply_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) :

∀ (a : α), (AddEquiv.op.symm f) a = (AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op) a

source

def MulEquiv.op {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] :

α ≃* β ≃ (αᵐᵒᵖ ≃* βᵐᵒᵖ)

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

Equations

One or more equations did not get rendered due to their size.

source

def AddEquiv.unop {α : Type u_2} {β : Type u_3} [Add α] [Add β] :

αᵃᵒᵖ ≃+ βᵃᵒᵖ ≃ (α ≃+ β)

The 'unopposite' of an iso αᵃᵒᵖ ≃+ βᵃᵒᵖ. Inverse to AddEquiv.op.

Equations

AddEquiv.unop = AddEquiv.op.symm

source

def MulEquiv.unop {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] :

αᵐᵒᵖ ≃* βᵐᵒᵖ ≃ (α ≃* β)

The 'unopposite' of an iso αᵐᵒᵖ ≃* βᵐᵒᵖ. Inverse to MulEquiv.op.

Equations

MulEquiv.unop = MulEquiv.op.symm

source

theorem AddMonoidHom.mul_op_ext_iff {α : Type u_2} {β : Type u_3} [AddZeroClass α] [AddZeroClass β] {f : αᵐᵒᵖ →+ β} {g : αᵐᵒᵖ →+ β} :

f = g ↔ f.comp MulOpposite.opAddEquiv.toAddMonoidHom = g.comp MulOpposite.opAddEquiv.toAddMonoidHom

source

theorem AddMonoidHom.mul_op_ext {α : Type u_2} {β : Type u_3} [AddZeroClass α] [AddZeroClass β] (f : αᵐᵒᵖ →+ β) (g : αᵐᵒᵖ →+ β) (h : f.comp MulOpposite.opAddEquiv.toAddMonoidHom = g.comp MulOpposite.opAddEquiv.toAddMonoidHom) :

f = g

This ext lemma changes 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.addHom_ext'.

Documentation

Mathlib.Algebra.Group.Opposite

Group structures on the multiplicative and additive opposites #

Additive structures on `αᵐᵒᵖ` #

Multiplicative structures on `αᵐᵒᵖ` #

Multiplicative structures on `αᵃᵒᵖ` #

Group structures on the multiplicative and additive opposites #

Additive structures on αᵐᵒᵖ #

Multiplicative structures on αᵐᵒᵖ #

Multiplicative structures on αᵃᵒᵖ #

Additive structures on `αᵐᵒᵖ` #

Multiplicative structures on `αᵐᵒᵖ` #

Multiplicative structures on `αᵃᵒᵖ` #