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.instNatCast {R : Type u_1} [NatCast R] :
    NatCast Rᵐᵒᵖ
    Equations
      source
      instance AddOpposite.instNatCast {R : Type u_1} [NatCast R] :
      NatCast Rᵃᵒᵖ
      Equations
        source
        instance MulOpposite.instIntCast {R : Type u_1} [IntCast R] :
        IntCast Rᵐᵒᵖ
        Equations
          source
          instance AddOpposite.instIntCast {R : Type u_1} [IntCast R] :
          IntCast Rᵃᵒᵖ
          Equations
            source
            @[simp]
            theorem MulOpposite.op_natCast {R : Type u_1} [NatCast R] (n : ℕ) :
            op ↑n = ↑n
            source
            @[simp]
            theorem AddOpposite.op_natCast {R : Type u_1} [NatCast R] (n : ℕ) :
            op ↑n = ↑n
            source
            @[simp]
            theorem MulOpposite.op_ofNat {R : Type u_1} [NatCast R] (n : ℕ) [n.AtLeastTwo] :
            op (OfNat.ofNat n) = OfNat.ofNat n
            source
            @[simp]
            theorem AddOpposite.op_ofNat {R : Type u_1} [NatCast R] (n : ℕ) [n.AtLeastTwo] :
            op (OfNat.ofNat n) = OfNat.ofNat n
            source
            @[simp]
            theorem MulOpposite.op_intCast {R : Type u_1} [IntCast R] (n : ℤ) :
            op ↑n = ↑n
            source
            @[simp]
            theorem AddOpposite.op_intCast {R : Type u_1} [IntCast R] (n : ℤ) :
            op ↑n = ↑n
            source
            @[simp]
            theorem MulOpposite.unop_natCast {R : Type u_1} [NatCast R] (n : ℕ) :
            unop ↑n = ↑n
            source
            @[simp]
            theorem AddOpposite.unop_natCast {R : Type u_1} [NatCast R] (n : ℕ) :
            unop ↑n = ↑n
            source
            @[simp]
            theorem MulOpposite.unop_ofNat {R : Type u_1} [NatCast R] (n : ℕ) [n.AtLeastTwo] :
            unop (OfNat.ofNat n) = OfNat.ofNat n
            source
            @[simp]
            theorem AddOpposite.unop_ofNat {R : Type u_1} [NatCast R] (n : ℕ) [n.AtLeastTwo] :
            unop (OfNat.ofNat n) = OfNat.ofNat n
            source
            @[simp]
            theorem MulOpposite.unop_intCast {R : Type u_1} [IntCast R] (n : ℤ) :
            unop ↑n = ↑n
            source
            @[simp]
            theorem AddOpposite.unop_intCast {R : Type u_1} [IntCast R] (n : ℤ) :
            unop ↑n = ↑n
            source
            instance MulOpposite.instAddMonoidWithOne {R : Type u_1} [AddMonoidWithOne R] :
            AddMonoidWithOne Rᵐᵒᵖ
            Equations
              source
              instance MulOpposite.instAddCommMonoidWithOne {R : Type u_1} [AddCommMonoidWithOne R] :
              AddCommMonoidWithOne Rᵐᵒᵖ
              Equations
                source
                instance MulOpposite.instAddGroupWithOne {R : Type u_1} [AddGroupWithOne R] :
                AddGroupWithOne Rᵐᵒᵖ
                Equations
                  source
                  instance MulOpposite.instAddCommGroupWithOne {R : Type u_1} [AddCommGroupWithOne R] :
                  AddCommGroupWithOne 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.instAddCommMonoidWithOne {R : Type u_1} [AddCommMonoidWithOne R] :
                                              AddCommMonoidWithOne Rᵃᵒᵖ
                                              Equations
                                                source
                                                instance AddOpposite.instAddCommGroupWithOne {R : Type u_1} [AddCommGroupWithOne R] :
                                                AddCommGroupWithOne 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