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.MulOpposite.instAlgebra {R : Type u_5} {A : Type u_6} [CommSemiring R] [Semiring A] [Algebra R A] :

Algebra R Aᵐᵒᵖ

source

@[simp]

theorem MulOpposite.algebraMap_apply {R : Type u_6} {A : Type u_5} [CommSemiring R] [Semiring A] [Algebra R A] (c : R) :

↑(algebraMap R Aᵐᵒᵖ) c = MulOpposite.op (↑(algebraMap R A) c)

source

@[simp]

theorem AlgEquiv.opOp_apply (R : Type u_1) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] :

∀ (a : A), ↑(AlgEquiv.opOp R A) a = MulOpposite.op (MulOpposite.op a)

source

@[simp]

theorem AlgEquiv.opOp_symm_apply (R : Type u_1) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] :

∀ (a : Aᵐᵒᵖᵐᵒᵖ), ↑(AlgEquiv.symm (AlgEquiv.opOp R A)) a = MulOpposite.unop (MulOpposite.unop a)

source

def AlgEquiv.opOp (R : Type u_1) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] :

A ≃ₐ[R] Aᵐᵒᵖᵐᵒᵖ

An algebra is isomorphic to the opposite of its opposite.

Instances For

source

@[simp]

theorem AlgEquiv.toRingEquiv_opOp (R : Type u_1) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] :

↑(AlgEquiv.opOp R A) = RingEquiv.opOp A

source

@[simp]

theorem AlgHom.fromOpposite_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), Commute (↑f x) (↑f y)) :

↑(AlgHom.fromOpposite f hf) = ↑f ∘ MulOpposite.unop

source

def AlgHom.fromOpposite {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), Commute (↑f x) (↑f y)) :

Aᵐᵒᵖ →ₐ[R] B

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

Instances For

source

@[simp]

theorem AlgHom.toLinearMap_fromOpposite {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), Commute (↑f x) (↑f y)) :

AlgHom.toLinearMap (AlgHom.fromOpposite f hf) = LinearMap.comp (AlgHom.toLinearMap f) ↑(LinearEquiv.symm (MulOpposite.opLinearEquiv R))

source

@[simp]

theorem AlgHom.toRingHom_fromOpposite {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), Commute (↑f x) (↑f y)) :

↑(AlgHom.fromOpposite f hf) = RingHom.fromOpposite (↑f) hf

source

@[simp]

theorem AlgHom.toOpposite_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), Commute (↑f x) (↑f y)) :

↑(AlgHom.toOpposite f hf) = MulOpposite.op ∘ ↑f

source

def AlgHom.toOpposite {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), Commute (↑f x) (↑f y)) :

A →ₐ[R] Bᵐᵒᵖ

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

Instances For

source

@[simp]

theorem AlgHom.toLinearMap_toOpposite {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), Commute (↑f x) (↑f y)) :

AlgHom.toLinearMap (AlgHom.toOpposite f hf) = LinearMap.comp (↑(MulOpposite.opLinearEquiv R)) (AlgHom.toLinearMap f)

source

@[simp]

theorem AlgHom.toRingHom_toOpposite {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), Commute (↑f x) (↑f y)) :

↑(AlgHom.toOpposite f hf) = RingHom.toOpposite (↑f) hf

source

@[simp]

theorem AlgHom.op_symm_apply_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ) :

∀ (a : A), ↑(↑AlgHom.op.symm f) a = MulOpposite.unop (↑f (MulOpposite.op a))

source

@[simp]

theorem AlgHom.op_apply_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :

∀ (a : Aᵐᵒᵖ), ↑(↑AlgHom.op f) a = MulOpposite.op (↑f (MulOpposite.unop a))

source

def AlgHom.op {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :

(A →ₐ[R] B) ≃ (Aᵐᵒᵖ →ₐ[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.

Instances For

source

theorem AlgHom.toRingHom_op {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) :

↑(↑AlgHom.op f) = ↑RingHom.op ↑f

source

@[inline, reducible]

abbrev AlgHom.unop {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :

(Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ) ≃ (A →ₐ[R] B)

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

Instances For

source

theorem AlgHom.toRingHom_unop {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ) :

↑(↑AlgHom.unop f) = ↑RingHom.unop ↑f

source

@[simp]

theorem AlgHom.opComm_symm_apply_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :

∀ (a : Aᵐᵒᵖ →ₐ[R] B) (a_1 : A), ↑(↑AlgHom.opComm.symm a) a_1 = MulOpposite.op (↑a (MulOpposite.op a_1))

source

@[simp]

theorem AlgHom.opComm_apply_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :

∀ (a : A →ₐ[R] Bᵐᵒᵖ) (a_1 : Aᵐᵒᵖ), ↑(↑AlgHom.opComm a) a_1 = MulOpposite.unop (↑a (MulOpposite.unop a_1))

source

def AlgHom.opComm {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :

(A →ₐ[R] Bᵐᵒᵖ) ≃ (Aᵐᵒᵖ →ₐ[R] B)

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

Instances For

source

@[simp]

theorem AlgEquiv.op_symm_apply_symm_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) :

∀ (a : B), ↑(AlgEquiv.symm (↑AlgEquiv.op.symm f)) a = MulOpposite.unop (↑(AddEquiv.symm ↑↑f) (MulOpposite.op a))

source

@[simp]

theorem AlgEquiv.op_symm_apply_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) :

∀ (a : A), ↑(↑AlgEquiv.op.symm f) a = MulOpposite.unop (↑f (MulOpposite.op a))

source

@[simp]

theorem AlgEquiv.op_apply_symm_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) :

∀ (a : Bᵐᵒᵖ), ↑(AlgEquiv.symm (↑AlgEquiv.op f)) a = MulOpposite.op (↑(AddEquiv.symm ↑↑f) (MulOpposite.unop a))

source

@[simp]

theorem AlgEquiv.op_apply_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) :

∀ (a : Aᵐᵒᵖ), ↑(↑AlgEquiv.op f) a = MulOpposite.op (↑f (MulOpposite.unop a))

source

def AlgEquiv.op {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :

(A ≃ₐ[R] B) ≃ Aᵐᵒᵖ ≃ₐ[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.

Instances For

source

theorem AlgEquiv.toAlgHom_op {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) :

↑(↑AlgEquiv.op f) = ↑AlgHom.op ↑f

source

theorem AlgEquiv.toRingEquiv_op {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) :

AlgEquiv.toRingEquiv (↑AlgEquiv.op f) = ↑RingEquiv.op (AlgEquiv.toRingEquiv f)

source

@[inline, reducible]

abbrev AlgEquiv.unop {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :

(Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) ≃ A ≃ₐ[R] B

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

Instances For

source

theorem AlgEquiv.toAlgHom_unop {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) :

↑(↑AlgEquiv.unop f) = ↑AlgHom.unop ↑f

source

theorem AlgEquiv.toRingEquiv_unop {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) :

AlgEquiv.toRingEquiv (↑AlgEquiv.unop f) = ↑RingEquiv.unop (AlgEquiv.toRingEquiv f)

source

@[simp]

theorem AlgEquiv.opComm_symm_apply_symm_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :

∀ (a : Aᵐᵒᵖ ≃ₐ[R] B) (a_1 : Bᵐᵒᵖ), ↑(AlgEquiv.symm (↑AlgEquiv.opComm.symm a)) a_1 = MulOpposite.unop (↑(AddEquiv.symm ↑↑(AlgEquiv.trans AlgEquiv.refl (AlgEquiv.trans a (AlgEquiv.opOp R B)))) (MulOpposite.op a_1))

source

@[simp]

theorem AlgEquiv.opComm_apply_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :

∀ (a : A ≃ₐ[R] Bᵐᵒᵖ) (a_1 : Aᵐᵒᵖ), ↑(↑AlgEquiv.opComm a) a_1 = MulOpposite.unop (↑a (MulOpposite.unop a_1))

source

@[simp]

theorem AlgEquiv.opComm_symm_apply_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :

∀ (a : Aᵐᵒᵖ ≃ₐ[R] B) (a_1 : A), ↑(↑AlgEquiv.opComm.symm a) a_1 = MulOpposite.op (↑a (MulOpposite.op a_1))

source

@[simp]

theorem AlgEquiv.opComm_apply_symm_apply {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :

∀ (a : A ≃ₐ[R] Bᵐᵒᵖ) (a_1 : B), ↑(AlgEquiv.symm (↑AlgEquiv.opComm a)) a_1 = ↑(MulEquiv.symm ↑↑AlgEquiv.refl) (↑(MulEquiv.symm ↑↑(AlgEquiv.trans (↑AlgEquiv.op a) (AlgEquiv.symm (AlgEquiv.opOp R B)))) a_1)

source

def AlgEquiv.opComm {R : Type u_1} {A : Type u_3} {B : Type u_4} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] :

(A ≃ₐ[R] Bᵐᵒᵖ) ≃ Aᵐᵒᵖ ≃ₐ[R] B

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

Instances For

source

@[simp]

theorem AlgEquiv.toOpposite_apply (R : Type u_1) (A : Type u_3) [CommSemiring R] [CommSemiring A] [Algebra R A] :

∀ (a : A), ↑(AlgEquiv.toOpposite R A) a = MulOpposite.op a

source

@[simp]

theorem AlgEquiv.toOpposite_symm_apply (R : Type u_1) (A : Type u_3) [CommSemiring R] [CommSemiring A] [Algebra R A] :

∀ (a : Aᵐᵒᵖ), ↑(AlgEquiv.symm (AlgEquiv.toOpposite R A)) a = MulOpposite.unop a

source

def AlgEquiv.toOpposite (R : Type u_1) (A : Type u_3) [CommSemiring R] [CommSemiring A] [Algebra R A] :

A ≃ₐ[R] Aᵐᵒᵖ

A commutative algebra is isomorphic to its opposite.

Instances For

source

@[simp]

theorem AlgEquiv.toRingEquiv_toOpposite (R : Type u_1) (A : Type u_3) [CommSemiring R] [CommSemiring A] [Algebra R A] :

↑(AlgEquiv.toOpposite R A) = RingEquiv.toOpposite A

source

@[simp]

theorem AlgEquiv.toLinearEquiv_toOpposite (R : Type u_1) (A : Type u_3) [CommSemiring R] [CommSemiring A] [Algebra R A] :

AlgEquiv.toLinearEquiv (AlgEquiv.toOpposite R A) = MulOpposite.opLinearEquiv R