# Algebra structures on the multiplicative opposite #

## Main definitions #

• MulOpposite.instAlgebra: the algebra on Aᵐᵒᵖ
• AlgHom.op/AlgHom.unop: simultaneously convert the domain and codomain of a morphism to the opposite algebra.
• AlgHom.opComm: swap which side of a morphism lies in the opposite algebra.
• AlgEquiv.op/AlgEquiv.unop: simultaneously convert the source and target of an isomorphism to the opposite algebra.
• AlgEquiv.opOp: any algebra is isomorphic to the opposite of its opposite.
• AlgEquiv.toOpposite: in a commutative algebra, the opposite algebra is isomorphic to the original algebra.
• AlgEquiv.opComm: swap which side of an isomorphism lies in the opposite algebra.
instance MulOpposite.instAlgebra {R : Type u_1} {A : Type u_3} [] [] [Algebra R A] :
Equations
• MulOpposite.instAlgebra = Algebra.mk (().toOpposite )
@[simp]
theorem MulOpposite.algebraMap_apply {R : Type u_1} {A : Type u_3} [] [] [Algebra R A] (c : R) :
() c = MulOpposite.op (() c)
@[simp]
theorem AlgEquiv.opOp_apply (R : Type u_1) (A : Type u_3) [] [] [Algebra R A] :
∀ (a : A), () a =
@[simp]
theorem AlgEquiv.opOp_symm_apply (R : Type u_1) (A : Type u_3) [] [] [Algebra R A] :
∀ (a : ), ().symm a = a.unop.unop
def AlgEquiv.opOp (R : Type u_1) (A : Type u_3) [] [] [Algebra R A] :

An algebra is isomorphic to the opposite of its opposite.

Equations
• = let __spread.0 := ; { toEquiv := __spread.0.toEquiv, map_mul' := , map_add' := , commutes' := }
Instances For
@[simp]
theorem AlgEquiv.toRingEquiv_opOp (R : Type u_1) (A : Type u_3) [] [] [Algebra R A] :
() =
@[simp]
theorem AlgHom.fromOpposite_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), Commute (f x) (f y)) :
(f.fromOpposite hf) = f MulOpposite.unop
def AlgHom.fromOpposite {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), Commute (f x) (f y)) :

An algebra homomorphism f : A →ₐ[R] B such that f x commutes with f y for all x, y defines an algebra homomorphism from Aᵐᵒᵖ.

Equations
• f.fromOpposite hf = let __src := f.fromOpposite hf; { toFun := f MulOpposite.unop, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
Instances For
@[simp]
theorem AlgHom.toLinearMap_fromOpposite {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), Commute (f x) (f y)) :
(f.fromOpposite hf).toLinearMap = f.toLinearMap ∘ₗ .symm
@[simp]
theorem AlgHom.toRingHom_fromOpposite {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), Commute (f x) (f y)) :
(f.fromOpposite hf) = (f).fromOpposite hf
@[simp]
theorem AlgHom.toOpposite_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), Commute (f x) (f y)) :
(f.toOpposite hf) = MulOpposite.op f
def AlgHom.toOpposite {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), Commute (f x) (f y)) :

An algebra homomorphism f : A →ₐ[R] B such that f x commutes with f y for all x, y defines an algebra homomorphism to Bᵐᵒᵖ.

Equations
• f.toOpposite hf = let __src := f.toOpposite hf; { toFun := MulOpposite.op f, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
Instances For
@[simp]
theorem AlgHom.toLinearMap_toOpposite {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), Commute (f x) (f y)) :
(f.toOpposite hf).toLinearMap = ∘ₗ f.toLinearMap
@[simp]
theorem AlgHom.toRingHom_toOpposite {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), Commute (f x) (f y)) :
(f.toOpposite hf) = (f).toOpposite hf
@[simp]
theorem AlgHom.op_symm_apply_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] (f : Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ) :
∀ (a : A), (AlgHom.op.symm f) a = (f ()).unop
@[simp]
theorem AlgHom.op_apply_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
∀ (a : Aᵐᵒᵖ), (AlgHom.op f) a = MulOpposite.op (f a.unop)
def AlgHom.op {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] :

An algebra hom A →ₐ[R] B can equivalently be viewed as an algebra hom Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ. This is the action of the (fully faithful) ᵐᵒᵖ-functor on morphisms.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AlgHom.toRingHom_op {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :
(AlgHom.op f).toRingHom = RingHom.op f.toRingHom
@[reducible, inline]
abbrev AlgHom.unop {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] :

The 'unopposite' of an algebra hom Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ. Inverse to RingHom.op.

Equations
• AlgHom.unop = AlgHom.op.symm
Instances For
theorem AlgHom.toRingHom_unop {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] (f : Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ) :
(AlgHom.unop f).toRingHom = RingHom.unop f.toRingHom
@[simp]
theorem AlgHom.opComm_symm_apply_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] :
∀ (a : Aᵐᵒᵖ →ₐ[R] B) (a_1 : A), (AlgHom.opComm.symm a) a_1 = MulOpposite.op (a ())
@[simp]
theorem AlgHom.opComm_apply_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] :
∀ (a : A →ₐ[R] Bᵐᵒᵖ) (a_1 : Aᵐᵒᵖ), (AlgHom.opComm a) a_1 = (a a_1.unop).unop
def AlgHom.opComm {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] :

Swap the ᵐᵒᵖ on an algebra hom to the opposite side.

Equations
• AlgHom.opComm = AlgHom.op.trans (AlgEquiv.refl.arrowCongr ().symm)
Instances For
@[simp]
theorem AlgEquiv.op_symm_apply_symm_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] (f : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) :
∀ (a : B), (AlgEquiv.op.symm f).symm a = ((f).symm ()).unop
@[simp]
theorem AlgEquiv.op_apply_symm_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) :
∀ (a : Bᵐᵒᵖ), (AlgEquiv.op f).symm a = MulOpposite.op ((f).symm a.unop)
@[simp]
theorem AlgEquiv.op_apply_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) :
∀ (a : Aᵐᵒᵖ), (AlgEquiv.op f) a = MulOpposite.op (f a.unop)
@[simp]
theorem AlgEquiv.op_symm_apply_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] (f : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) :
∀ (a : A), (AlgEquiv.op.symm f) a = (f ()).unop
def AlgEquiv.op {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] :

An algebra iso A ≃ₐ[R] B can equivalently be viewed as an algebra iso Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ. This is the action of the (fully faithful) ᵐᵒᵖ-functor on morphisms.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AlgEquiv.toAlgHom_op {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) :
(AlgEquiv.op f) = AlgHom.op f
theorem AlgEquiv.toRingEquiv_op {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) :
(AlgEquiv.op f).toRingEquiv = RingEquiv.op f.toRingEquiv
@[reducible, inline]
abbrev AlgEquiv.unop {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] :

The 'unopposite' of an algebra iso Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ. Inverse to AlgEquiv.op.

Equations
• AlgEquiv.unop = AlgEquiv.op.symm
Instances For
theorem AlgEquiv.toAlgHom_unop {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] (f : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) :
(AlgEquiv.unop f) = AlgHom.unop f
theorem AlgEquiv.toRingEquiv_unop {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] (f : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) :
(AlgEquiv.unop f).toRingEquiv = RingEquiv.unop f.toRingEquiv
@[simp]
theorem AlgEquiv.opComm_apply_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] :
∀ (a : A ≃ₐ[R] Bᵐᵒᵖ) (a_1 : Aᵐᵒᵖ), (AlgEquiv.opComm a) a_1 = (a a_1.unop).unop
@[simp]
theorem AlgEquiv.opComm_symm_apply_symm_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] :
∀ (a : Aᵐᵒᵖ ≃ₐ[R] B) (a_1 : Bᵐᵒᵖ), (AlgEquiv.opComm.symm a).symm a_1 = (((AlgEquiv.refl.trans (a.trans ()))).symm ()).unop
@[simp]
theorem AlgEquiv.opComm_symm_apply_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] :
∀ (a : Aᵐᵒᵖ ≃ₐ[R] B) (a_1 : A), (AlgEquiv.opComm.symm a) a_1 = MulOpposite.op (a ())
@[simp]
theorem AlgEquiv.opComm_apply_symm_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] :
∀ (a : A ≃ₐ[R] Bᵐᵒᵖ) (a_1 : B), (AlgEquiv.opComm a).symm a_1 = (AlgEquiv.refl).symm ((((AlgEquiv.op a).trans ().symm)).symm a_1)
def AlgEquiv.opComm {R : Type u_1} {A : Type u_3} {B : Type u_4} [] [] [] [Algebra R A] [Algebra R B] :

Swap the ᵐᵒᵖ on an algebra isomorphism to the opposite side.

Equations
• AlgEquiv.opComm = AlgEquiv.op.trans (AlgEquiv.refl.equivCongr ().symm)
Instances For
@[simp]
theorem AlgEquiv.toOpposite_apply (R : Type u_1) (A : Type u_3) [] [] [Algebra R A] :
∀ (a : A), () a =
@[simp]
theorem AlgEquiv.toOpposite_symm_apply (R : Type u_1) (A : Type u_3) [] [] [Algebra R A] :
∀ (a : Aᵐᵒᵖ), ().symm a = a.unop
def AlgEquiv.toOpposite (R : Type u_1) (A : Type u_3) [] [] [Algebra R A] :

A commutative algebra is isomorphic to its opposite.

Equations
• = let __spread.0 := ; { toEquiv := __spread.0.toEquiv, map_mul' := , map_add' := , commutes' := }
Instances For
@[simp]
theorem AlgEquiv.toRingEquiv_toOpposite (R : Type u_1) (A : Type u_3) [] [] [Algebra R A] :
@[simp]
theorem AlgEquiv.toLinearEquiv_toOpposite (R : Type u_1) (A : Type u_3) [] [] [Algebra R A] :
().toLinearEquiv =