Algebra structures on the multiplicative opposite #
Main definitions #
MulOpposite.instAlgebra: the algebra onAᵐᵒᵖ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}
[CommSemiring R]
[Semiring A]
[Algebra R A]
:
Equations
- MulOpposite.instAlgebra = { toSMul := MulOpposite.instSMul, algebraMap := (algebraMap R A).toOpposite ⋯, commutes' := ⋯, smul_def' := ⋯ }
@[simp]
theorem
MulOpposite.algebraMap_apply
{R : Type u_1}
{A : Type u_3}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(c : R)
:
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' := ⋯ }
@[simp]
theorem
AlgEquiv.opOp_symm_apply
(R : Type u_1)
(A : Type u_3)
[CommSemiring R]
[Semiring A]
[Algebra R A]
(a✝ : Aᵐᵒᵖᵐᵒᵖ)
:
@[simp]
theorem
AlgEquiv.opOp_apply
(R : Type u_1)
(A : Type u_3)
[CommSemiring R]
[Semiring A]
[Algebra R A]
(a✝ : A)
:
@[simp]
theorem
AlgEquiv.toRingEquiv_opOp
(R : Type u_1)
(A : Type u_3)
[CommSemiring R]
[Semiring A]
[Algebra R A]
:
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))
:
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' := ⋯ }
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))
:
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' := ⋯ }
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]
:
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.
@[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]
:
The 'unopposite' of an algebra hom Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ. Inverse to RingHom.op.
Equations
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]
:
Swap the ᵐᵒᵖ on an algebra hom to the opposite side.
Equations
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]
:
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.
@[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]
:
The 'unopposite' of an algebra iso Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ. Inverse to AlgEquiv.op.
Equations
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]
:
Swap the ᵐᵒᵖ on an algebra isomorphism to the opposite side.
Equations
def
AlgEquiv.toOpposite
(R : Type u_1)
(A : Type u_3)
[CommSemiring R]
[CommSemiring A]
[Algebra 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' := ⋯ }
@[simp]
theorem
AlgEquiv.toOpposite_symm_apply
(R : Type u_1)
(A : Type u_3)
[CommSemiring R]
[CommSemiring A]
[Algebra R A]
(a✝ : Aᵐᵒᵖ)
:
@[simp]
theorem
AlgEquiv.toOpposite_apply
(R : Type u_1)
(A : Type u_3)
[CommSemiring R]
[CommSemiring A]
[Algebra R A]
(a✝ : A)
:
@[simp]
theorem
AlgEquiv.toRingEquiv_toOpposite
(R : Type u_1)
(A : Type u_3)
[CommSemiring R]
[CommSemiring A]
[Algebra R A]
:
@[simp]
theorem
AlgEquiv.toLinearEquiv_toOpposite
(R : Type u_1)
(A : Type u_3)
[CommSemiring R]
[CommSemiring A]
[Algebra R A]
: