Algebra structures on the multiplicative opposite #
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ᵐᵒᵖ
.
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ᵐᵒᵖ
.
An algebra hom A →ₐ[R] B
can equivalently be viewed as an algebra hom αᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ
.
This is the action of the (fully faithful) ᵐᵒᵖ
-functor on morphisms.
Equations
- alg_hom.op = {to_fun := λ (f : A →ₐ[R] B), {to_fun := (⇑ring_hom.op f.to_ring_hom).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}, inv_fun := λ (f : Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ), {to_fun := (⇑ring_hom.unop f.to_ring_hom).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}, left_inv := _, right_inv := _}
The 'unopposite' of an algebra hom αᵐᵒᵖ →+* Bᵐᵒᵖ
. Inverse to ring_hom.op
.
Equations
An algebra iso A ≃ₐ[R] B
can equivalently be viewed as an algebra iso αᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ
.
This is the action of the (fully faithful) ᵐᵒᵖ
-functor on morphisms.
Equations
- alg_equiv.alg_equiv.op = {to_fun := λ (f : A ≃ₐ[R] B), {to_fun := (⇑ring_equiv.op f.to_ring_equiv).to_fun, inv_fun := (⇑ring_equiv.op f.to_ring_equiv).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}, inv_fun := λ (f : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ), {to_fun := (⇑ring_equiv.unop f.to_ring_equiv).to_fun, inv_fun := (⇑ring_equiv.unop f.to_ring_equiv).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}, left_inv := _, right_inv := _}
The 'unopposite' of an algebra iso Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ
. Inverse to alg_equiv.op
.
Equations
The double opposite is isomorphic as an algebra to the original type.
Equations
- mul_opposite.op_op_alg_equiv = alg_equiv.of_linear_equiv ((mul_opposite.op_linear_equiv R).trans (mul_opposite.op_linear_equiv R)).symm mul_opposite.op_op_alg_equiv._proof_7 mul_opposite.op_op_alg_equiv._proof_8