Documentation

Mathlib.Algebra.Ring.Opposite

Ring structures on the multiplicative opposite #

source
@[instance_reducible]
instance MulOpposite.instDistrib {R : Type u_1} [Distrib R] :
Distrib Rᵐᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instNatCast {R : Type u_1} [NatCast R] :
NatCast Rᵐᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instNatCast {R : Type u_1} [NatCast R] :
NatCast Rᵃᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instIntCast {R : Type u_1} [IntCast R] :
IntCast Rᵐᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instIntCast {R : Type u_1} [IntCast R] :
IntCast Rᵃᵒᵖ
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_reducible]
instance MulOpposite.instAddMonoidWithOne {R : Type u_1} [AddMonoidWithOne R] :
AddMonoidWithOne Rᵐᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instAddCommMonoidWithOne {R : Type u_1} [AddCommMonoidWithOne R] :
AddCommMonoidWithOne Rᵐᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instAddGroupWithOne {R : Type u_1} [AddGroupWithOne R] :
AddGroupWithOne Rᵐᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instAddCommGroupWithOne {R : Type u_1} [AddCommGroupWithOne R] :
AddCommGroupWithOne Rᵐᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instNonUnitalNonAssocSemiring {R : Type u_1} [NonUnitalNonAssocSemiring R] :
NonUnitalNonAssocSemiring Rᵐᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instNonUnitalSemiring {R : Type u_1} [NonUnitalSemiring R] :
NonUnitalSemiring Rᵐᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instNonAssocSemiring {R : Type u_1} [NonAssocSemiring R] :
NonAssocSemiring Rᵐᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instSemiring {R : Type u_1} [Semiring R] :
Semiring Rᵐᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instNonUnitalCommSemiring {R : Type u_1} [NonUnitalCommSemiring R] :
NonUnitalCommSemiring Rᵐᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instCommSemiring {R : Type u_1} [CommSemiring R] :
CommSemiring Rᵐᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instNonUnitalNonAssocRing {R : Type u_1} [NonUnitalNonAssocRing R] :
NonUnitalNonAssocRing Rᵐᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instNonUnitalRing {R : Type u_1} [NonUnitalRing R] :
NonUnitalRing Rᵐᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instNonAssocRing {R : Type u_1} [NonAssocRing R] :
NonAssocRing Rᵐᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instRing {R : Type u_1} [Ring R] :
Ring Rᵐᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instNonUnitalCommRing {R : Type u_1} [NonUnitalCommRing R] :
NonUnitalCommRing Rᵐᵒᵖ
source
@[instance_reducible]
instance MulOpposite.instCommRing {R : Type u_1} [CommRing R] :
CommRing Rᵐᵒᵖ
source
instance MulOpposite.instIsDomain {R : Type u_1} [Ring R] [IsDomain R] :
IsDomain Rᵐᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instDistrib {R : Type u_1} [Distrib R] :
Distrib Rᵃᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instAddCommMonoidWithOne {R : Type u_1} [AddCommMonoidWithOne R] :
AddCommMonoidWithOne Rᵃᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instAddCommGroupWithOne {R : Type u_1} [AddCommGroupWithOne R] :
AddCommGroupWithOne Rᵃᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instNonUnitalNonAssocSemiring {R : Type u_1} [NonUnitalNonAssocSemiring R] :
NonUnitalNonAssocSemiring Rᵃᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instNonUnitalSemiring {R : Type u_1} [NonUnitalSemiring R] :
NonUnitalSemiring Rᵃᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instNonAssocSemiring {R : Type u_1} [NonAssocSemiring R] :
NonAssocSemiring Rᵃᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instSemiring {R : Type u_1} [Semiring R] :
Semiring Rᵃᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instNonUnitalCommSemiring {R : Type u_1} [NonUnitalCommSemiring R] :
NonUnitalCommSemiring Rᵃᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instCommSemiring {R : Type u_1} [CommSemiring R] :
CommSemiring Rᵃᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instNonUnitalNonAssocRing {R : Type u_1} [NonUnitalNonAssocRing R] :
NonUnitalNonAssocRing Rᵃᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instNonUnitalRing {R : Type u_1} [NonUnitalRing R] :
NonUnitalRing Rᵃᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instNonAssocRing {R : Type u_1} [NonAssocRing R] :
NonAssocRing Rᵃᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instRing {R : Type u_1} [Ring R] :
Ring Rᵃᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instNonUnitalCommRing {R : Type u_1} [NonUnitalCommRing R] :
NonUnitalCommRing Rᵃᵒᵖ
source
@[instance_reducible]
instance AddOpposite.instCommRing {R : Type u_1} [CommRing R] :
CommRing Rᵃᵒᵖ
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ᵐᵒᵖ.

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ᵐᵒᵖ.

    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.

      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.

        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ᵐᵒᵖ.

          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ᵐᵒᵖ.

            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.

              Instances For
                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
                @[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
                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.

                Instances For