Documentation

Mathlib.Algebra.Algebra.Opposite

Algebra structures on the multiplicative opposite #

Main definitions #

instance MulOpposite.instAlgebra {R : Type u_1} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] :
Equations
@[simp]
theorem MulOpposite.algebraMap_apply {R : Type u_1} {A : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] (c : R) :
@[simp]
theorem AlgEquiv.opOp_symm_apply (R : Type u_1) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] :
@[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)
def AlgEquiv.opOp (R : Type u_1) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] :

An algebra is isomorphic to the opposite of its opposite.

Equations
Instances For
    @[simp]
    theorem AlgEquiv.toRingEquiv_opOp (R : Type u_1) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] :
    @[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
    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' := }
    Instances For
      @[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
      @[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
      @[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
      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' := }
      Instances For
        @[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
        @[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
        @[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))
        @[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))
        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.
        Instances For
          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
          @[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
          • AlgHom.unop = AlgHom.op.symm
          Instances For
            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).toRingHom = RingHom.unop f.toRingHom
            @[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))
            @[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))
            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
            • AlgHom.opComm = AlgHom.op.trans (AlgEquiv.refl.arrowCongr (AlgEquiv.opOp R B).symm)
            Instances For
              @[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))
              @[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.op.symm f).symm a = MulOpposite.unop ((↑f).symm (MulOpposite.op a))
              @[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.op f).symm a = MulOpposite.op ((↑f).symm (MulOpposite.unop a))
              @[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))
              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.
              Instances For
                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
                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.op f).toRingEquiv = RingEquiv.op f.toRingEquiv
                @[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
                • AlgEquiv.unop = AlgEquiv.op.symm
                Instances For
                  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
                  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.unop f).toRingEquiv = RingEquiv.unop f.toRingEquiv
                  @[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))
                  @[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.opComm.symm a).symm a_1 = MulOpposite.unop ((↑(AlgEquiv.refl.trans (a.trans (AlgEquiv.opOp R B)))).symm (MulOpposite.op a_1))
                  @[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))
                  @[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.opComm a).symm a_1 = (↑AlgEquiv.refl).symm ((↑((AlgEquiv.op a).trans (AlgEquiv.opOp R B).symm)).symm a_1)
                  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
                  • AlgEquiv.opComm = AlgEquiv.op.trans (AlgEquiv.refl.equivCongr (AlgEquiv.opOp R B).symm)
                  Instances For
                    @[simp]
                    theorem AlgEquiv.toOpposite_symm_apply (R : Type u_1) (A : Type u_3) [CommSemiring R] [CommSemiring A] [Algebra R A] :
                    ∀ (a : Aᵐᵒᵖ), (AlgEquiv.toOpposite R A).symm a = MulOpposite.unop a
                    @[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
                    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
                    Instances For