Documentation

Mathlib.Algebra.Ring.Opposite

Ring structures on the multiplicative opposite #

Equations
Equations
Equations
  • MulOpposite.instMulZeroOneClass = let __spread.0 := MulOpposite.instMulOneClass; let __spread.1 := MulOpposite.instMulZeroClass; MulZeroOneClass.mk
Equations
  • MulOpposite.instSemigroupWithZero = let __spread.0 := MulOpposite.instSemigroup; let __spread.1 := MulOpposite.instMulZeroClass; SemigroupWithZero.mk
Equations
  • MulOpposite.instMonoidWithZero = let __spread.0 := MulOpposite.instMonoid; let __spread.1 := MulOpposite.instMulZeroOneClass; MonoidWithZero.mk
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • MulOpposite.instNonUnitalSemiring = let __spread.0 := MulOpposite.instNonUnitalNonAssocSemiring; let __spread.1 := MulOpposite.instSemigroupWithZero; NonUnitalSemiring.mk
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • MulOpposite.instNonUnitalCommSemiring = let __spread.0 := MulOpposite.instNonUnitalSemiring; let __spread.1 := MulOpposite.instCommSemigroup; NonUnitalCommSemiring.mk
Equations
  • MulOpposite.instCommSemiring = let __spread.0 := MulOpposite.instSemiring; let __spread.1 := MulOpposite.instCommMonoid; CommSemiring.mk
Equations
  • MulOpposite.instNonUnitalNonAssocRing = let __spread.0 := MulOpposite.instAddCommGroup; let __spread.1 := MulOpposite.instNonUnitalNonAssocSemiring; NonUnitalNonAssocRing.mk
Equations
  • MulOpposite.instNonUnitalRing = let __spread.0 := MulOpposite.instNonUnitalNonAssocRing; let __spread.1 := MulOpposite.instNonUnitalSemiring; NonUnitalRing.mk
Equations
  • One or more equations did not get rendered due to their size.
instance MulOpposite.instRing {α : Type u_1} [Ring α] :
Equations
  • MulOpposite.instRing = let __spread.0 := MulOpposite.instSemiring; let __spread.1 := MulOpposite.instAddCommGroupWithOne; Ring.mk SubNegMonoid.zsmul
Equations
  • MulOpposite.instNonUnitalCommRing = let __spread.0 := MulOpposite.instNonUnitalRing; let __spread.1 := MulOpposite.instNonUnitalCommSemiring; NonUnitalCommRing.mk
Equations
  • MulOpposite.instCommRing = let __spread.0 := MulOpposite.instRing; let __spread.1 := MulOpposite.instCommMonoid; CommRing.mk
Equations
  • =
instance MulOpposite.instIsDomain {α : Type u_1} [Ring α] [IsDomain α] :
Equations
  • =
Equations
  • One or more equations did not get rendered due to their size.
Equations
Equations
Equations
  • AddOpposite.instMulZeroOneClass = let __spread.0 := AddOpposite.instMulOneClass; let __spread.1 := AddOpposite.instMulZeroClass; MulZeroOneClass.mk
Equations
  • AddOpposite.instSemigroupWithZero = let __spread.0 := AddOpposite.instSemigroup; let __spread.1 := AddOpposite.instMulZeroClass; SemigroupWithZero.mk
Equations
  • AddOpposite.instMonoidWithZero = let __spread.0 := AddOpposite.instMonoid; let __spread.1 := AddOpposite.instMulZeroOneClass; MonoidWithZero.mk
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • AddOpposite.instNonUnitalSemiring = let __spread.0 := AddOpposite.instNonUnitalNonAssocSemiring; let __spread.1 := AddOpposite.instSemigroupWithZero; NonUnitalSemiring.mk
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • AddOpposite.instNonUnitalCommSemiring = let __spread.0 := AddOpposite.instNonUnitalSemiring; let __spread.1 := AddOpposite.instCommSemigroup; NonUnitalCommSemiring.mk
Equations
  • AddOpposite.instCommSemiring = let __spread.0 := AddOpposite.instSemiring; let __spread.1 := AddOpposite.instCommMonoid; CommSemiring.mk
Equations
  • AddOpposite.instNonUnitalNonAssocRing = let __spread.0 := AddOpposite.instAddCommGroup; let __spread.1 := AddOpposite.instNonUnitalNonAssocSemiring; NonUnitalNonAssocRing.mk
Equations
  • AddOpposite.instNonUnitalRing = let __spread.0 := AddOpposite.instNonUnitalNonAssocRing; let __spread.1 := AddOpposite.instNonUnitalSemiring; NonUnitalRing.mk
Equations
  • One or more equations did not get rendered due to their size.
instance AddOpposite.instRing {α : Type u_1} [Ring α] :
Equations
  • AddOpposite.instRing = let __spread.0 := AddOpposite.instSemiring; let __spread.1 := AddOpposite.instAddCommGroupWithOne; Ring.mk SubNegMonoid.zsmul
Equations
  • AddOpposite.instNonUnitalCommRing = let __spread.0 := AddOpposite.instNonUnitalRing; let __spread.1 := AddOpposite.instNonUnitalCommSemiring; NonUnitalCommRing.mk
Equations
  • AddOpposite.instCommRing = let __spread.0 := AddOpposite.instRing; let __spread.1 := AddOpposite.instCommMonoid; CommRing.mk
Equations
  • =
instance AddOpposite.instIsDomain {α : Type u_1} [Ring α] [IsDomain α] :
Equations
  • =
Equations
  • One or more equations did not get rendered due to their size.
@[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
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)) :

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
  • f.toOpposite hf = let __src := MulOpposite.opAddEquiv.toAddMonoidHom.comp f; let __src := f.toOpposite hf; { toFun := MulOpposite.op f, map_mul' := , map_zero' := , map_add' := }
Instances For
    @[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
    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)) :

    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
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem NonUnitalRingHom.op_symm_apply_apply {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : αᵐᵒᵖ →ₙ+* βᵐᵒᵖ) :
      ∀ (a : α), (NonUnitalRingHom.op.symm f) a = ((AddMonoidHom.mulUnop f.toAddMonoidHom)).toFun a
      @[simp]
      theorem NonUnitalRingHom.op_apply_apply {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) :
      ∀ (a : αᵐᵒᵖ), (NonUnitalRingHom.op f) a = ((AddMonoidHom.mulOp f.toAddMonoidHom)).toFun a

      A non-unital ring hom α →ₙ+* β can equivalently be viewed as a non-unital ring hom αᵐᵒᵖ →+* βᵐᵒᵖ. 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

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

        Equations
        • NonUnitalRingHom.unop = NonUnitalRingHom.op.symm
        Instances For
          @[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
          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)) :

          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
          • One or more equations did not get rendered due to their size.
          Instances For
            @[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
            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)) :

            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
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem RingHom.op_apply_apply {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [NonAssocSemiring β] (f : α →+* β) :
              ∀ (a : αᵐᵒᵖ), (RingHom.op f) a = MulOpposite.op (f (MulOpposite.unop a))
              @[simp]
              theorem RingHom.op_symm_apply_apply {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [NonAssocSemiring β] (f : αᵐᵒᵖ →+* βᵐᵒᵖ) :
              ∀ (a : α), (RingHom.op.symm f) a = MulOpposite.unop (f (MulOpposite.op a))
              def RingHom.op {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [NonAssocSemiring β] :

              A ring hom α →+* β can equivalently be viewed as a ring hom αᵐᵒᵖ →+* βᵐᵒᵖ. 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
                def RingHom.unop {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [NonAssocSemiring β] :

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

                Equations
                • RingHom.unop = RingHom.op.symm
                Instances For