|
| 1 | +/- |
| 2 | +Copyright (c) 2023 Eric Wieser. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Eric Wieser |
| 5 | +-/ |
| 6 | +import Mathlib.Algebra.Algebra.Equiv |
| 7 | +import Mathlib.Algebra.Module.Opposites |
| 8 | +import Mathlib.Algebra.Ring.Opposite |
| 9 | + |
| 10 | +/-! |
| 11 | +# Algebra structures on the multiplicative opposite |
| 12 | +
|
| 13 | +## Main definitions |
| 14 | +
|
| 15 | +* `MulOpposite.instAlgebra`: the algebra on `Aᵐᵒᵖ` |
| 16 | +* `AlgHom.op`/`AlgHom.unop`: simultaneously convert the domain and codomain of a morphism to the |
| 17 | + opposite algebra. |
| 18 | +* `AlgEquiv.op`/`AlgEquiv.unop`: simultaneously convert the source and target of an isomorphism to |
| 19 | + the opposite algebra. |
| 20 | +* `AlgEquiv.toOpposite`: in a commutative algebra, the opposite algebra is isomorphic to the |
| 21 | + original algebra. |
| 22 | +-/ |
| 23 | + |
| 24 | + |
| 25 | +variable {R S A B : Type*} |
| 26 | + |
| 27 | +open MulOpposite |
| 28 | + |
| 29 | +section Semiring |
| 30 | + |
| 31 | +variable [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] |
| 32 | +variable [Algebra R S] [Algebra R A] [Algebra R B] [Algebra S A] [SMulCommClass R S A] |
| 33 | +variable [IsScalarTower R S A] |
| 34 | + |
| 35 | +namespace MulOpposite |
| 36 | + |
| 37 | +variable {R A : Type _} [CommSemiring R] [Semiring A] [Algebra R A] |
| 38 | + |
| 39 | +instance MulOpposite.instAlgebra : Algebra R Aᵐᵒᵖ where |
| 40 | + toRingHom := (algebraMap R A).toOpposite fun x y => Algebra.commutes _ _ |
| 41 | + smul_def' c x := unop_injective <| by |
| 42 | + simp only [unop_smul, RingHom.toOpposite_apply, Function.comp_apply, unop_mul, op_mul, |
| 43 | + Algebra.smul_def, Algebra.commutes, op_unop, unop_op] |
| 44 | + commutes' r := MulOpposite.rec' fun x => by |
| 45 | + simp only [RingHom.toOpposite_apply, Function.comp_apply, ← op_mul, Algebra.commutes] |
| 46 | + |
| 47 | +@[simp] |
| 48 | +theorem algebraMap_apply (c : R) : algebraMap R Aᵐᵒᵖ c = op (algebraMap R A c) := |
| 49 | + rfl |
| 50 | +#align mul_opposite.algebra_map_apply MulOpposite.algebraMap_apply |
| 51 | + |
| 52 | +end MulOpposite |
| 53 | + |
| 54 | +namespace AlgHom |
| 55 | + |
| 56 | +/-- |
| 57 | +An algebra homomorphism `f : A →ₐ[R] B` such that `f x` commutes with `f y` for all `x, y` defines |
| 58 | +an algebra homomorphism from `Aᵐᵒᵖ`. -/ |
| 59 | +@[simps (config := { fullyApplied := false })] |
| 60 | +def fromOpposite (f : A →ₐ[R] B) (hf : ∀ x y, Commute (f x) (f y)) : Aᵐᵒᵖ →ₐ[R] B := |
| 61 | + { f.toRingHom.fromOpposite hf with |
| 62 | + toFun := f ∘ unop |
| 63 | + commutes' := fun r => f.commutes r } |
| 64 | + |
| 65 | +@[simp] |
| 66 | +theorem toLinearMap_fromOpposite (f : A →ₐ[R] B) (hf : ∀ x y, Commute (f x) (f y)) : |
| 67 | + (f.fromOpposite hf : Aᵐᵒᵖ →ₗ[R] B) = f ∘ₗ (opLinearEquiv R).symm.toLinearMap := |
| 68 | + rfl |
| 69 | + |
| 70 | +@[simp] |
| 71 | +theorem toRingHom_fromOpposite (f : A →ₐ[R] B) (hf : ∀ x y, Commute (f x) (f y)) : |
| 72 | + (f.fromOpposite hf : Aᵐᵒᵖ →+* B) = (f : A →+* B).fromOpposite hf := |
| 73 | + rfl |
| 74 | + |
| 75 | +/-- |
| 76 | +An algebra homomorphism `f : A →ₐ[R] B` such that `f x` commutes with `f y` for all `x, y` defines |
| 77 | +an algebra homomorphism to `Bᵐᵒᵖ`. -/ |
| 78 | +@[simps (config := { fullyApplied := false })] |
| 79 | +def toOpposite (f : A →ₐ[R] B) (hf : ∀ x y, Commute (f x) (f y)) : A →ₐ[R] Bᵐᵒᵖ := |
| 80 | + { f.toRingHom.toOpposite hf with |
| 81 | + toFun := op ∘ f |
| 82 | + commutes' := fun r => unop_injective <| f.commutes r } |
| 83 | + |
| 84 | +@[simp] |
| 85 | +theorem toLinearMap_toOpposite (f : A →ₐ[R] B) (hf : ∀ x y, Commute (f x) (f y)) : |
| 86 | + (f.toOpposite hf : A →ₗ[R] Bᵐᵒᵖ) = (opLinearEquiv R : B ≃ₗ[R] Bᵐᵒᵖ) ∘ₗ f.toLinearMap := |
| 87 | + rfl |
| 88 | + |
| 89 | +@[simp] |
| 90 | +theorem toRingHom_toOpposite (f : A →ₐ[R] B) (hf : ∀ x y, Commute (f x) (f y)) : |
| 91 | + (f.toOpposite hf : A →+* Bᵐᵒᵖ) = (f : A →+* B).toOpposite hf := |
| 92 | + rfl |
| 93 | + |
| 94 | +/-- An algebra hom `A →ₐ[R] B` can equivalently be viewed as an algebra hom `Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ`. |
| 95 | +This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms. -/ |
| 96 | +@[simps!] |
| 97 | +protected def op : (A →ₐ[R] B) ≃ (Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ) where |
| 98 | + toFun f := { RingHom.op f.toRingHom with commutes' := fun r => unop_injective <| f.commutes r } |
| 99 | + invFun f := { RingHom.unop f.toRingHom with commutes' := fun r => op_injective <| f.commutes r } |
| 100 | + left_inv _f := AlgHom.ext fun _a => rfl |
| 101 | + right_inv _f := AlgHom.ext fun _a => rfl |
| 102 | + |
| 103 | +theorem toRingHom_op (f : A →ₐ[R] B) : f.op.toRingHom = RingHom.op f.toRingHom := |
| 104 | + rfl |
| 105 | + |
| 106 | +/-- The 'unopposite' of an algebra hom `Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ`. Inverse to `ring_hom.op`. -/ |
| 107 | +abbrev unop : (Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ) ≃ (A →ₐ[R] B) := AlgHom.op.symm |
| 108 | + |
| 109 | +theorem toRingHom_unop (f : Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ) : f.unop.toRingHom = RingHom.unop f.toRingHom := |
| 110 | + rfl |
| 111 | + |
| 112 | +end AlgHom |
| 113 | + |
| 114 | +namespace AlgEquiv |
| 115 | + |
| 116 | +/-- An algebra iso `A ≃ₐ[R] B` can equivalently be viewed as an algebra iso `Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ`. |
| 117 | +This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms. -/ |
| 118 | +@[simps!] |
| 119 | +def op : (A ≃ₐ[R] B) ≃ Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ where |
| 120 | + toFun f := |
| 121 | + { RingEquiv.op f.toRingEquiv with |
| 122 | + commutes' := fun r => MulOpposite.unop_injective <| f.commutes r } |
| 123 | + invFun f := |
| 124 | + { RingEquiv.unop f.toRingEquiv with |
| 125 | + commutes' := fun r => MulOpposite.op_injective <| f.commutes r } |
| 126 | + left_inv _f := AlgEquiv.ext fun _a => rfl |
| 127 | + right_inv _f := AlgEquiv.ext fun _a => rfl |
| 128 | + |
| 129 | +theorem toAlgHom_op (f : A ≃ₐ[R] B) : |
| 130 | + (AlgEquiv.op f).toAlgHom = AlgHom.op f.toAlgHom := |
| 131 | + rfl |
| 132 | + |
| 133 | +theorem toRingEquiv_op (f : A ≃ₐ[R] B) : |
| 134 | + (AlgEquiv.op f).toRingEquiv = RingEquiv.op f.toRingEquiv := |
| 135 | + rfl |
| 136 | + |
| 137 | +/-- The 'unopposite' of an algebra iso `Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ`. Inverse to `alg_equiv.op`. -/ |
| 138 | +abbrev unop : (Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) ≃ A ≃ₐ[R] B := AlgEquiv.op.symm |
| 139 | + |
| 140 | +theorem toAlgHom_unop (f : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) : f.unop.toAlgHom = AlgHom.unop f.toAlgHom := |
| 141 | + rfl |
| 142 | + |
| 143 | +theorem toRingEquiv_unop (f : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ) : |
| 144 | + (AlgEquiv.unop f).toRingEquiv = RingEquiv.unop f.toRingEquiv := |
| 145 | + rfl |
| 146 | + |
| 147 | +end AlgEquiv |
| 148 | + |
| 149 | +end Semiring |
| 150 | + |
| 151 | +section CommSemiring |
| 152 | +variable (R A) [CommSemiring R] [CommSemiring A] [Algebra R A] |
| 153 | + |
| 154 | +namespace AlgEquiv |
| 155 | + |
| 156 | +/-- A commutative algebra is isomorphic to its opposite. -/ |
| 157 | +@[simps!] |
| 158 | +def toOpposite : A ≃ₐ[R] Aᵐᵒᵖ where |
| 159 | + __ := RingEquiv.toOpposite A |
| 160 | + commutes' _r := rfl |
| 161 | + |
| 162 | +@[simp] lemma toRingEquiv_toOpposite : (toOpposite R A : A ≃+* Aᵐᵒᵖ) = RingEquiv.toOpposite A := rfl |
| 163 | +@[simp] lemma toLinearEquiv_toOpposite : toLinearEquiv (toOpposite R A) = opLinearEquiv R := rfl |
| 164 | + |
| 165 | +end AlgEquiv |
| 166 | + |
| 167 | +end CommSemiring |
0 commit comments