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.

source

instance MulOpposite.instAlgebra {R : Type u_1} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] :

Algebra R Aᵐᵒᵖ

Equations

MulOpposite.instAlgebra = { toSMul := MulOpposite.instSMul, algebraMap := (algebraMap R A).toOpposite ⋯, commutes' := ⋯, smul_def' := ⋯ }

source

@[simp]

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

(algebraMap R Aᵐᵒᵖ) c = op ((algebraMap R A) c)

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.

Equations

AlgEquiv.opOp R A = { toEquiv := (RingEquiv.opOp A).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

Instances For

source

@[simp]

theorem AlgEquiv.opOp_symm_apply (R : Type u_1) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] (a✝ : Aᵐᵒᵖ ᵐᵒᵖ) :

(opOp R A).symm a✝ = MulOpposite.unop (MulOpposite.unop a✝)

source

@[simp]

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

(opOp R A) a✝ = MulOpposite.op (MulOpposite.op a✝)

source

@[simp]

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

↑(opOp R A) = RingEquiv.opOp A

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

Equations

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

Instances For

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)) :

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

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)) :

(f.fromOpposite hf).toLinearMap = f.toLinearMap ∘ₗ ↑(MulOpposite.opLinearEquiv R).symm

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)) :

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

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

Equations

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

Instances For

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)) :

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

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)) :

(f.toOpposite hf).toLinearMap = ↑(MulOpposite.opLinearEquiv R) ∘ₗ f.toLinearMap

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)) :

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

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.

Equations

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

Instances For

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

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).toRingHom = RingHom.op f.toRingHom

source

@[reducible, inline]

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 RingHom.op.

Equations

AlgHom.unop = AlgHom.op.symm

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ᵐᵒᵖ) :

(unop f).toRingHom = RingHom.unop f.toRingHom

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.

Equations

AlgHom.opComm = AlgHom.op.trans (AlgEquiv.refl.arrowCongr (AlgEquiv.opOp R B).symm)

Instances For

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✝¹ : A) :

(opComm.symm a✝) a✝¹ = MulOpposite.op (a✝ (MulOpposite.op a✝¹))

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✝¹ : Aᵐᵒᵖ) :

(opComm a✝) a✝¹ = MulOpposite.unop (a✝ (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.

Equations

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

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) :

(op.symm f).symm a✝ = MulOpposite.unop ((↑↑f).symm (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ᵐᵒᵖ) :

(op f).symm a✝ = MulOpposite.op ((↑↑f).symm (MulOpposite.unop 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) :

(op.symm f) a✝ = MulOpposite.unop (f (MulOpposite.op 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ᵐᵒᵖ) :

(op f) a✝ = MulOpposite.op (f (MulOpposite.unop a✝))

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) :

↑(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) :

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

source

@[reducible, inline]

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.

Equations

AlgEquiv.unop = AlgEquiv.op.symm

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ᵐᵒᵖ) :

↑(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ᵐᵒᵖ) :

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

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.

Equations

AlgEquiv.opComm = AlgEquiv.op.trans (AlgEquiv.refl.equivCongr (AlgEquiv.opOp R B).symm)

Instances For

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✝¹ : A) :

(opComm.symm a✝) a✝¹ = MulOpposite.op (a✝ (MulOpposite.op a✝¹))

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✝¹ : Bᵐᵒᵖ) :

(opComm.symm a✝).symm a✝¹ = MulOpposite.unop ((↑↑(refl.trans (a✝.trans (opOp R B)))).symm (MulOpposite.op a✝¹))

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✝¹ : Aᵐᵒᵖ) :

(opComm a✝) a✝¹ = MulOpposite.unop (a✝ (MulOpposite.unop a✝¹))

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✝¹ : B) :

(opComm a✝).symm a✝¹ = (↑↑refl).symm ((↑↑((op a✝).trans (opOp R B).symm)).symm a✝¹)

source

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

Aᵐᵒᵖ ≃ₐ[R] Module.End A A

The canonical algebra isomorphism from Aᵐᵒᵖ to Module.End A A induced by the right multiplication.

Equations

AlgEquiv.moduleEndSelf R = { toEquiv := (RingEquiv.moduleEndSelf A).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

Instances For

source

@[simp]

theorem AlgEquiv.moduleEndSelf_symm_apply (R : Type u_1) {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (f : Module.End A A) :

(moduleEndSelf R).symm f = MulOpposite.op (f 1)

source

@[simp]

theorem AlgEquiv.moduleEndSelf_apply_apply (R : Type u_1) {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (s : Aᵐᵒᵖ) (a✝ : A) :

((moduleEndSelf R) s) a✝ = a✝ * MulOpposite.unop s

source

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

A ≃ₐ[R] Module.End Aᵐᵒᵖ A

The canonical algebra isomorphism from A to Module.End Aᵐᵒᵖ A induced by the left multiplication.

Equations

AlgEquiv.moduleEndSelfOp R = { toEquiv := (RingEquiv.moduleEndSelfOp A).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

Instances For

source

@[simp]

theorem AlgEquiv.moduleEndSelfOp_symm_apply (R : Type u_1) {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (f : Module.End Aᵐᵒᵖ A) :

(moduleEndSelfOp R).symm f = f 1

source

@[simp]

theorem AlgEquiv.moduleEndSelfOp_apply_apply (R : Type u_1) {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (s a✝ : A) :

((moduleEndSelfOp R) s) a✝ = s * 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.

Equations

AlgEquiv.toOpposite R A = { toEquiv := (RingEquiv.toOpposite A).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

Instances For

source

@[simp]

theorem AlgEquiv.toOpposite_symm_apply (R : Type u_1) (A : Type u_3) [CommSemiring R] [CommSemiring A] [Algebra R A] (a✝ : Aᵐᵒᵖ) :

(toOpposite R A).symm a✝ = MulOpposite.unop a✝

source

@[simp]

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

(toOpposite R A) a✝ = MulOpposite.op a✝

source

@[simp]

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

↑(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] :

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

Documentation

Mathlib.Algebra.Algebra.Opposite

Algebra structures on the multiplicative opposite #

Main definitions #