HepLean Documentation

Mathlib.Algebra.Ring.Opposite

Ring structures on the multiplicative opposite #

source
instance MulOpposite.instDistrib {α : Type u_1} [Distrib α] :
Distrib αᵐᵒᵖ
Equations
source
instance MulOpposite.instNonUnitalNonAssocSemiring {α : Type u_1} [NonUnitalNonAssocSemiring α] :
NonUnitalNonAssocSemiring αᵐᵒᵖ
Equations
source
instance MulOpposite.instNonUnitalSemiring {α : Type u_1} [NonUnitalSemiring α] :
NonUnitalSemiring αᵐᵒᵖ
Equations
source
instance MulOpposite.instNonAssocSemiring {α : Type u_1} [NonAssocSemiring α] :
NonAssocSemiring αᵐᵒᵖ
Equations
source
instance MulOpposite.instSemiring {α : Type u_1} [Semiring α] :
Semiring αᵐᵒᵖ
Equations
  • MulOpposite.instSemiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ Monoid.npow ⋯ ⋯
source
instance MulOpposite.instNonUnitalCommSemiring {α : Type u_1} [NonUnitalCommSemiring α] :
NonUnitalCommSemiring αᵐᵒᵖ
Equations
source
instance MulOpposite.instCommSemiring {α : Type u_1} [CommSemiring α] :
CommSemiring αᵐᵒᵖ
Equations
source
instance MulOpposite.instNonUnitalNonAssocRing {α : Type u_1} [NonUnitalNonAssocRing α] :
NonUnitalNonAssocRing αᵐᵒᵖ
Equations
source
instance MulOpposite.instNonUnitalRing {α : Type u_1} [NonUnitalRing α] :
NonUnitalRing αᵐᵒᵖ
Equations
source
instance MulOpposite.instNonAssocRing {α : Type u_1} [NonAssocRing α] :
NonAssocRing αᵐᵒᵖ
Equations
source
instance MulOpposite.instRing {α : Type u_1} [Ring α] :
Ring αᵐᵒᵖ
Equations
  • MulOpposite.instRing = Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
source
instance MulOpposite.instNonUnitalCommRing {α : Type u_1} [NonUnitalCommRing α] :
NonUnitalCommRing αᵐᵒᵖ
Equations
source
instance MulOpposite.instCommRing {α : Type u_1} [CommRing α] :
CommRing αᵐᵒᵖ
Equations
source
instance MulOpposite.instIsDomain {α : Type u_1} [Ring α] [IsDomain α] :
IsDomain αᵐᵒᵖ
Equations
  • ⋯ = ⋯
source
instance MulOpposite.instGroupWithZero {α : Type u_1} [GroupWithZero α] :
GroupWithZero αᵐᵒᵖ
Equations
  • MulOpposite.instGroupWithZero = GroupWithZero.mk ⋯ DivInvMonoid.zpow ⋯ ⋯ ⋯ ⋯ ⋯
source
instance AddOpposite.instDistrib {α : Type u_1} [Distrib α] :
Distrib αᵃᵒᵖ
Equations
source
instance AddOpposite.instNonUnitalNonAssocSemiring {α : Type u_1} [NonUnitalNonAssocSemiring α] :
NonUnitalNonAssocSemiring αᵃᵒᵖ
Equations
source
instance AddOpposite.instNonUnitalSemiring {α : Type u_1} [NonUnitalSemiring α] :
NonUnitalSemiring αᵃᵒᵖ
Equations
source
instance AddOpposite.instNonAssocSemiring {α : Type u_1} [NonAssocSemiring α] :
NonAssocSemiring αᵃᵒᵖ
Equations
source
instance AddOpposite.instSemiring {α : Type u_1} [Semiring α] :
Semiring αᵃᵒᵖ
Equations
  • AddOpposite.instSemiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ Monoid.npow ⋯ ⋯
source
instance AddOpposite.instNonUnitalCommSemiring {α : Type u_1} [NonUnitalCommSemiring α] :
NonUnitalCommSemiring αᵃᵒᵖ
Equations
source
instance AddOpposite.instCommSemiring {α : Type u_1} [CommSemiring α] :
CommSemiring αᵃᵒᵖ
Equations
source
instance AddOpposite.instNonUnitalNonAssocRing {α : Type u_1} [NonUnitalNonAssocRing α] :
NonUnitalNonAssocRing αᵃᵒᵖ
Equations
source
instance AddOpposite.instNonUnitalRing {α : Type u_1} [NonUnitalRing α] :
NonUnitalRing αᵃᵒᵖ
Equations
source
instance AddOpposite.instNonAssocRing {α : Type u_1} [NonAssocRing α] :
NonAssocRing αᵃᵒᵖ
Equations
source
instance AddOpposite.instRing {α : Type u_1} [Ring α] :
Ring αᵃᵒᵖ
Equations
  • AddOpposite.instRing = Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
source
instance AddOpposite.instNonUnitalCommRing {α : Type u_1} [NonUnitalCommRing α] :
NonUnitalCommRing αᵃᵒᵖ
Equations
source
instance AddOpposite.instCommRing {α : Type u_1} [CommRing α] :
CommRing αᵃᵒᵖ
Equations
source
instance AddOpposite.instIsDomain {α : Type u_1} [Ring α] [IsDomain α] :
IsDomain αᵃᵒᵖ
Equations
  • ⋯ = ⋯
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.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
  • f.toOpposite hf = { toFun := MulOpposite.op ∘ ⇑f, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
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.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
    • f.fromOpposite hf = { toFun := ⇑f ∘ MulOpposite.unop, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
    Instances For
      source
      @[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
      source
      @[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
      source
      def NonUnitalRingHom.op {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] :
      (α →ₙ+* β) ≃ (αᵐᵒᵖ →ₙ+* βᵐᵒᵖ)

      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
        source
        def NonUnitalRingHom.unop {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] :
        (αᵐᵒᵖ →ₙ+* βᵐᵒᵖ) ≃ (α →ₙ+* β)

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

        Equations
        • NonUnitalRingHom.unop = NonUnitalRingHom.op.symm
        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.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
          • f.toOpposite hf = { toFun := MulOpposite.op ∘ ⇑f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
          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.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
            • f.fromOpposite hf = { toFun := ⇑f ∘ MulOpposite.unop, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
            Instances For
              source
              @[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))
              source
              @[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))
              source
              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
                source
                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