Documentation

Mathlib.Algebra.Ring.Opposite

Ring structures on the multiplicative opposite #

source
instance MulOpposite.instDistrib {R : Type u_1} [Distrib R] :
Distrib Rᵐᵒᵖ
Equations
    source
    instance MulOpposite.instNonUnitalNonAssocSemiring {R : Type u_1} [NonUnitalNonAssocSemiring R] :
    NonUnitalNonAssocSemiring Rᵐᵒᵖ
    Equations
      source
      instance MulOpposite.instNonUnitalSemiring {R : Type u_1} [NonUnitalSemiring R] :
      NonUnitalSemiring Rᵐᵒᵖ
      Equations
        source
        instance MulOpposite.instNonAssocSemiring {R : Type u_1} [NonAssocSemiring R] :
        NonAssocSemiring Rᵐᵒᵖ
        Equations
          source
          instance MulOpposite.instSemiring {R : Type u_1} [Semiring R] :
          Semiring Rᵐᵒᵖ
          Equations
            source
            instance MulOpposite.instNonUnitalCommSemiring {R : Type u_1} [NonUnitalCommSemiring R] :
            NonUnitalCommSemiring Rᵐᵒᵖ
            Equations
              source
              instance MulOpposite.instCommSemiring {R : Type u_1} [CommSemiring R] :
              CommSemiring Rᵐᵒᵖ
              Equations
                source
                instance MulOpposite.instNonUnitalNonAssocRing {R : Type u_1} [NonUnitalNonAssocRing R] :
                NonUnitalNonAssocRing Rᵐᵒᵖ
                Equations
                  source
                  instance MulOpposite.instNonUnitalRing {R : Type u_1} [NonUnitalRing R] :
                  NonUnitalRing Rᵐᵒᵖ
                  Equations
                    source
                    instance MulOpposite.instNonAssocRing {R : Type u_1} [NonAssocRing R] :
                    NonAssocRing Rᵐᵒᵖ
                    Equations
                      source
                      instance MulOpposite.instRing {R : Type u_1} [Ring R] :
                      Ring Rᵐᵒᵖ
                      Equations
                        source
                        instance MulOpposite.instNonUnitalCommRing {R : Type u_1} [NonUnitalCommRing R] :
                        NonUnitalCommRing Rᵐᵒᵖ
                        Equations
                          source
                          instance MulOpposite.instCommRing {R : Type u_1} [CommRing R] :
                          CommRing Rᵐᵒᵖ
                          Equations
                            source
                            instance MulOpposite.instIsDomain {R : Type u_1} [Ring R] [IsDomain R] :
                            IsDomain Rᵐᵒᵖ
                            source
                            instance AddOpposite.instDistrib {R : Type u_1} [Distrib R] :
                            Distrib Rᵃᵒᵖ
                            Equations
                              source
                              instance AddOpposite.instNonUnitalNonAssocSemiring {R : Type u_1} [NonUnitalNonAssocSemiring R] :
                              NonUnitalNonAssocSemiring Rᵃᵒᵖ
                              Equations
                                source
                                instance AddOpposite.instNonUnitalSemiring {R : Type u_1} [NonUnitalSemiring R] :
                                NonUnitalSemiring Rᵃᵒᵖ
                                Equations
                                  source
                                  instance AddOpposite.instNonAssocSemiring {R : Type u_1} [NonAssocSemiring R] :
                                  NonAssocSemiring Rᵃᵒᵖ
                                  Equations
                                    source
                                    instance AddOpposite.instSemiring {R : Type u_1} [Semiring R] :
                                    Semiring Rᵃᵒᵖ
                                    Equations
                                      source
                                      instance AddOpposite.instNonUnitalCommSemiring {R : Type u_1} [NonUnitalCommSemiring R] :
                                      NonUnitalCommSemiring Rᵃᵒᵖ
                                      Equations
                                        source
                                        instance AddOpposite.instCommSemiring {R : Type u_1} [CommSemiring R] :
                                        CommSemiring Rᵃᵒᵖ
                                        Equations
                                          source
                                          instance AddOpposite.instNonUnitalNonAssocRing {R : Type u_1} [NonUnitalNonAssocRing R] :
                                          NonUnitalNonAssocRing Rᵃᵒᵖ
                                          Equations
                                            source
                                            instance AddOpposite.instNonUnitalRing {R : Type u_1} [NonUnitalRing R] :
                                            NonUnitalRing Rᵃᵒᵖ
                                            Equations
                                              source
                                              instance AddOpposite.instNonAssocRing {R : Type u_1} [NonAssocRing R] :
                                              NonAssocRing Rᵃᵒᵖ
                                              Equations
                                                source
                                                instance AddOpposite.instRing {R : Type u_1} [Ring R] :
                                                Ring Rᵃᵒᵖ
                                                Equations
                                                  source
                                                  instance AddOpposite.instNonUnitalCommRing {R : Type u_1} [NonUnitalCommRing R] :
                                                  NonUnitalCommRing Rᵃᵒᵖ
                                                  Equations
                                                    source
                                                    instance AddOpposite.instCommRing {R : Type u_1} [CommRing R] :
                                                    CommRing Rᵃᵒᵖ
                                                    Equations
                                                      source
                                                      instance AddOpposite.instIsDomain {R : Type u_1} [Ring R] [IsDomain R] :
                                                      IsDomain Rᵃᵒᵖ
                                                      source
                                                      def NonUnitalRingHom.toOpposite {R : Type u_2} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) :
                                                      R →ₙ+* Sᵐᵒᵖ

                                                      A non-unital ring homomorphism f : R →ₙ+* S such that f x commutes with f y for all x, y defines a non-unital ring homomorphism to Sᵐᵒᵖ.

                                                      Equations
                                                        Instances For
                                                          source
                                                          @[simp]
                                                          theorem NonUnitalRingHom.toOpposite_apply {R : Type u_2} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) :
                                                          ⇑(f.toOpposite hf) = MulOpposite.op ∘ ⇑f
                                                          source
                                                          def NonUnitalRingHom.fromOpposite {R : Type u_2} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) :
                                                          Rᵐᵒᵖ →ₙ+* S

                                                          A non-unital ring homomorphism f : R →ₙ* S such that f x commutes with f y for all x, y defines a non-unital ring homomorphism from Rᵐᵒᵖ.

                                                          Equations
                                                            Instances For
                                                              source
                                                              @[simp]
                                                              theorem NonUnitalRingHom.fromOpposite_apply {R : Type u_2} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) :
                                                              ⇑(f.fromOpposite hf) = ⇑f ∘ MulOpposite.unop
                                                              source
                                                              def NonUnitalRingHom.op {R : Type u_2} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] :
                                                              (R →ₙ+* S) ≃ (Rᵐᵒᵖ →ₙ+* Sᵐᵒᵖ)

                                                              A non-unital ring hom R →ₙ+* S can equivalently be viewed as a non-unital ring hom Rᵐᵒᵖ →+* Sᵐᵒᵖ. This is the action of the (fully faithful) ᵐᵒᵖ-functor on morphisms.

                                                              Equations
                                                                Instances For
                                                                  source
                                                                  @[simp]
                                                                  theorem NonUnitalRingHom.op_symm_apply_apply {R : Type u_2} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : Rᵐᵒᵖ →ₙ+* Sᵐᵒᵖ) (a✝ : R) :
                                                                  (op.symm f) a✝ = (↑(AddMonoidHom.mulUnop f.toAddMonoidHom)).toFun a✝
                                                                  source
                                                                  @[simp]
                                                                  theorem NonUnitalRingHom.op_apply_apply {R : Type u_2} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (a✝ : Rᵐᵒᵖ) :
                                                                  (op f) a✝ = (↑(AddMonoidHom.mulOp f.toAddMonoidHom)).toFun a✝
                                                                  source
                                                                  def NonUnitalRingHom.unop {R : Type u_2} {S : Type u_3} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] :
                                                                  (Rᵐᵒᵖ →ₙ+* Sᵐᵒᵖ) ≃ (R →ₙ+* S)

                                                                  The 'unopposite' of a non-unital ring hom Rᵐᵒᵖ →ₙ+* Sᵐᵒᵖ. Inverse to NonUnitalRingHom.op.

                                                                  Equations
                                                                    Instances For
                                                                      source
                                                                      def RingHom.toOpposite {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] (f : R →+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) :
                                                                      R →+* Sᵐᵒᵖ

                                                                      A ring homomorphism f : R →+* S such that f x commutes with f y for all x, y defines a ring homomorphism to Sᵐᵒᵖ.

                                                                      Equations
                                                                        Instances For
                                                                          source
                                                                          @[simp]
                                                                          theorem RingHom.toOpposite_apply {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] (f : R →+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) :
                                                                          ⇑(f.toOpposite hf) = MulOpposite.op ∘ ⇑f
                                                                          source
                                                                          def RingHom.fromOpposite {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] (f : R →+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) :
                                                                          Rᵐᵒᵖ →+* S

                                                                          A ring homomorphism f : R →+* S such that f x commutes with f y for all x, y defines a ring homomorphism from Rᵐᵒᵖ.

                                                                          Equations
                                                                            Instances For
                                                                              source
                                                                              @[simp]
                                                                              theorem RingHom.fromOpposite_apply {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] (f : R →+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) :
                                                                              ⇑(f.fromOpposite hf) = ⇑f ∘ MulOpposite.unop
                                                                              source
                                                                              def RingHom.op {R : Type u_2} {S : Type u_3} [NonAssocSemiring R] [NonAssocSemiring S] :
                                                                              (R →+* S) ≃ (Rᵐᵒᵖ →+* Sᵐᵒᵖ)

                                                                              A ring hom R →+* S can equivalently be viewed as a ring hom Rᵐᵒᵖ →+* Sᵐᵒᵖ. This is the action of the (fully faithful) ᵐᵒᵖ-functor on morphisms.

                                                                              Equations
                                                                                Instances For
                                                                                  source
                                                                                  @[simp]
                                                                                  theorem RingHom.op_symm_apply_apply {R : Type u_2} {S : Type u_3} [NonAssocSemiring R] [NonAssocSemiring S] (f : Rᵐᵒᵖ →+* Sᵐᵒᵖ) (a✝ : R) :
                                                                                  (op.symm f) a✝ = MulOpposite.unop (f (MulOpposite.op a✝))
                                                                                  source
                                                                                  @[simp]
                                                                                  theorem RingHom.op_apply_apply {R : Type u_2} {S : Type u_3} [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (a✝ : Rᵐᵒᵖ) :
                                                                                  (op f) a✝ = MulOpposite.op (f (MulOpposite.unop a✝))
                                                                                  source
                                                                                  def RingHom.unop {R : Type u_2} {S : Type u_3} [NonAssocSemiring R] [NonAssocSemiring S] :
                                                                                  (Rᵐᵒᵖ →+* Sᵐᵒᵖ) ≃ (R →+* S)

                                                                                  The 'unopposite' of a ring hom Rᵐᵒᵖ →+* Sᵐᵒᵖ. Inverse to RingHom.op.

                                                                                  Equations
                                                                                    Instances For