Group isomorphism between a group and its opposite

def MulOpposite.opAddEquiv {α : Type u_1} [Add α] : α ≃+ αᵐᵒᵖ

The function MulOpposite.op is an additive equivalence.

@[simp]

theorem MulOpposite.opAddEquiv_symm_apply {α : Type u_1} [Add α] : ⇑opAddEquiv.symm = unop

@[simp]

theorem MulOpposite.opAddEquiv_apply {α : Type u_1} [Add α] : ⇑opAddEquiv = op

@[simp]

theorem MulOpposite.opAddEquiv_toEquiv {α : Type u_1} [Add α] : ↑opAddEquiv = opEquiv

def AddOpposite.opMulEquiv {α : Type u_1} [Mul α] : α ≃* αᵃᵒᵖ

The function AddOpposite.op is a multiplicative equivalence.

@[simp]

theorem AddOpposite.opMulEquiv_apply {α : Type u_1} [Mul α] : ⇑opMulEquiv = op

@[simp]

theorem AddOpposite.opMulEquiv_symm_apply {α : Type u_1} [Mul α] : ⇑opMulEquiv.symm = unop

@[simp]

theorem AddOpposite.opMulEquiv_toEquiv {α : Type u_1} [Mul α] : ↑opMulEquiv = opEquiv

def MulEquiv.inv' (G : Type u_2) [DivisionMonoid G] : G ≃* Gᵐᵒᵖ

Inversion on a group is a MulEquiv to the opposite group. When G is commutative, there is MulEquiv.inv.

def AddEquiv.neg' (G : Type u_2) [SubtractionMonoid G] : G ≃+ Gᵃᵒᵖ

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

@[simp]

theorem MulEquiv.inv'_symm_apply (G : Type u_2) [DivisionMonoid G] : ⇑(inv' G).symm = Inv.inv ∘ MulOpposite.unop

@[simp]

theorem AddEquiv.neg'_symm_apply (G : Type u_2) [SubtractionMonoid G] : ⇑(neg' G).symm = Neg.neg ∘ AddOpposite.unop

@[simp]

theorem MulEquiv.inv'_apply (G : Type u_2) [DivisionMonoid G] : ⇑(inv' G) = MulOpposite.op ∘ Inv.inv

@[simp]

theorem AddEquiv.neg'_apply (G : Type u_2) [SubtractionMonoid G] : ⇑(neg' G) = AddOpposite.op ∘ Neg.neg

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ᵐᵒᵖ.

def AddHom.toOpposite {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : M →ₙ+ N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) : 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 to Sᵃᵒᵖ.

@[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

@[simp]

theorem AddHom.toOpposite_apply {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : M →ₙ+ N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) : ⇑(f.toOpposite hf) = AddOpposite.op ∘ ⇑f

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ᵐᵒᵖ.

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

@[simp]

theorem AddHom.fromOpposite_apply {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : M →ₙ+ N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) : ⇑(f.fromOpposite hf) = ⇑f ∘ AddOpposite.unop

@[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

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ᵐᵒᵖ.

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ᵃᵒᵖ.

@[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

@[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

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ᵐᵒᵖ.

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ᵃᵒᵖ.

@[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

@[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

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.

def AddHom.op {M : Type u_2} {N : Type u_3} [Add M] [Add N] : (M →ₙ+ N) ≃ (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.

@[simp]

theorem MulHom.op_apply_apply {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] (f : M →ₙ* N) (a✝ : Mᵐᵒᵖ) : (op f) a✝ = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a✝

@[simp]

theorem AddHom.op_apply_apply {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : M →ₙ+ N) (a✝ : Mᵃᵒᵖ) : (op f) a✝ = (AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) a✝

@[simp]

theorem MulHom.op_symm_apply_apply {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] (f : Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ) (a✝ : M) : (op.symm f) a✝ = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a✝

@[simp]

theorem AddHom.op_symm_apply_apply {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : Mᵃᵒᵖ →ₙ+ Nᵃᵒᵖ) (a✝ : M) : (op.symm f) a✝ = (AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op) a✝

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.

def AddHom.unop {M : Type u_2} {N : Type u_3} [Add M] [Add N] : (Mᵃᵒᵖ →ₙ+ Nᵃᵒᵖ) ≃ (M →ₙ+ N)

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

def AddHom.mulOp {M : Type u_2} {N : Type u_3} [Add M] [Add N] : (M →ₙ+ N) ≃ (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.

@[simp]

theorem AddHom.mulOp_symm_apply_apply {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : Mᵐᵒᵖ →ₙ+ Nᵐᵒᵖ) (a✝ : M) : (mulOp.symm f) a✝ = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a✝

@[simp]

theorem AddHom.mulOp_apply_apply {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : M →ₙ+ N) (a✝ : Mᵐᵒᵖ) : (mulOp f) a✝ = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a✝

def AddHom.mulUnop {α : Type u_2} {β : Type u_3} [Add α] [Add β] : (αᵐᵒᵖ →ₙ+ βᵐᵒᵖ) ≃ (α →ₙ+ β)

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

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.

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.

@[simp]

theorem AddMonoidHom.op_apply_apply {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (a✝ : Mᵃᵒᵖ) : (op f) a✝ = (AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) a✝

@[simp]

theorem AddMonoidHom.op_symm_apply_apply {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) (a✝ : M) : (op.symm f) a✝ = (AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op) a✝

@[simp]

theorem MonoidHom.op_apply_apply {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass N] (f : M →* N) (a✝ : Mᵐᵒᵖ) : (op f) a✝ = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a✝

@[simp]

theorem MonoidHom.op_symm_apply_apply {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass N] (f : Mᵐᵒᵖ →* Nᵐᵒᵖ) (a✝ : M) : (op.symm f) a✝ = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a✝

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.

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.

def MulEquiv.opOp (M : Type u_2) [Mul M] : M ≃* Mᵐᵒᵖᵐᵒᵖ

A monoid is isomorphic to the opposite of its opposite.

def AddEquiv.opOp (M : Type u_2) [Add M] : M ≃+ Mᵃᵒᵖᵃᵒᵖ

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

@[simp]

theorem MulEquiv.opOp_apply (M : Type u_2) [Mul M] (a✝ : M) : (opOp M) a✝ = MulOpposite.op (MulOpposite.op a✝)

@[simp]

theorem AddEquiv.opOp_apply (M : Type u_2) [Add M] (a✝ : M) : (opOp M) a✝ = AddOpposite.op (AddOpposite.op a✝)

@[simp]

theorem MulEquiv.opOp_symm_apply (M : Type u_2) [Mul M] (a✝ : Mᵐᵒᵖᵐᵒᵖ) : (opOp M).symm a✝ = MulOpposite.unop (MulOpposite.unop a✝)

@[simp]

theorem AddEquiv.opOp_symm_apply (M : Type u_2) [Add M] (a✝ : Mᵃᵒᵖᵃᵒᵖ) : (opOp M).symm a✝ = AddOpposite.unop (AddOpposite.unop a✝)

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.

@[simp]

theorem AddMonoidHom.mulOp_apply_apply {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (a✝ : Mᵐᵒᵖ) : (mulOp f) a✝ = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a✝

@[simp]

theorem AddMonoidHom.mulOp_symm_apply_apply {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : Mᵐᵒᵖ →+ Nᵐᵒᵖ) (a✝ : M) : (mulOp.symm f) a✝ = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a✝

def AddMonoidHom.mulUnop {α : Type u_2} {β : Type u_3} [AddZeroClass α] [AddZeroClass β] : (αᵐᵒᵖ →+ βᵐᵒᵖ) ≃ (α →+ β)

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

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

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

@[simp]

theorem AddEquiv.mulOp_symm_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : αᵐᵒᵖ ≃+ βᵐᵒᵖ) : mulOp.symm f = MulOpposite.opAddEquiv.trans (f.trans MulOpposite.opAddEquiv.symm)

@[simp]

theorem AddEquiv.mulOp_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : α ≃+ β) : mulOp f = MulOpposite.opAddEquiv.symm.trans (f.trans MulOpposite.opAddEquiv)

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

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

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

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

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

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

@[simp]

theorem MulEquiv.op_apply_symm_apply {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] (f : α ≃* β) (a✝ : βᵐᵒᵖ) : (op f).symm a✝ = (MulOpposite.op ∘ ⇑f.symm ∘ MulOpposite.unop) a✝

@[simp]

theorem MulEquiv.op_apply_apply {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] (f : α ≃* β) (a✝ : αᵐᵒᵖ) : (op f) a✝ = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a✝

@[simp]

theorem MulEquiv.op_symm_apply_symm_apply {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] (f : αᵐᵒᵖ ≃* βᵐᵒᵖ) (a✝ : β) : (op.symm f).symm a✝ = (MulOpposite.unop ∘ ⇑f.symm ∘ MulOpposite.op) a✝

@[simp]

theorem MulEquiv.op_symm_apply_apply {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] (f : αᵐᵒᵖ ≃* βᵐᵒᵖ) (a✝ : α) : (op.symm f) a✝ = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a✝

@[simp]

theorem AddEquiv.op_apply_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : α ≃+ β) (a✝ : αᵃᵒᵖ) : (op f) a✝ = (AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) a✝

@[simp]

theorem AddEquiv.op_symm_apply_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) (a✝ : α) : (op.symm f) a✝ = (AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op) a✝

@[simp]

theorem AddEquiv.op_apply_symm_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : α ≃+ β) (a✝ : βᵃᵒᵖ) : (op f).symm a✝ = (AddOpposite.op ∘ ⇑f.symm ∘ AddOpposite.unop) a✝

@[simp]

theorem AddEquiv.op_symm_apply_symm_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) (a✝ : β) : (op.symm f).symm a✝ = (AddOpposite.unop ∘ ⇑f.symm ∘ AddOpposite.op) a✝

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

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

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

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

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

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