Documentation

Mathlib.Algebra.Ring.Opposite

Ring structures on the multiplicative opposite #

source
šŸ”ø coverage
@[implicit_reducible]
instance MulOpposite.instDistrib {R : Type u_1} [Distrib R] :
Distrib Rįµįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance MulOpposite.instNatCast {R : Type u_1} [NatCast R] :
NatCast Rįµįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance AddOpposite.instNatCast {R : Type u_1} [NatCast R] :
NatCast Rįµƒįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance MulOpposite.instIntCast {R : Type u_1} [IntCast R] :
IntCast Rįµįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance AddOpposite.instIntCast {R : Type u_1} [IntCast R] :
IntCast Rįµƒįµ’įµ–
source
šŸ“ coverage
@[simp]
theorem MulOpposite.op_natCast {R : Type u_1} [NatCast R] (n : ā„•) :
op ā†‘n = ā†‘n
source
šŸ“ coverage
@[simp]
theorem AddOpposite.op_natCast {R : Type u_1} [NatCast R] (n : ā„•) :
op ā†‘n = ā†‘n
source
šŸ“ coverage
@[simp]
theorem MulOpposite.op_ofNat {R : Type u_1} [NatCast R] (n : ā„•) [n.AtLeastTwo] :
op (OfNat.ofNat n) = OfNat.ofNat n
source
šŸ“ coverage
@[simp]
theorem AddOpposite.op_ofNat {R : Type u_1} [NatCast R] (n : ā„•) [n.AtLeastTwo] :
op (OfNat.ofNat n) = OfNat.ofNat n
source
šŸ“ coverage
@[simp]
theorem MulOpposite.op_intCast {R : Type u_1} [IntCast R] (n : ā„¤) :
op ā†‘n = ā†‘n
source
šŸ“ coverage
@[simp]
theorem AddOpposite.op_intCast {R : Type u_1} [IntCast R] (n : ā„¤) :
op ā†‘n = ā†‘n
source
šŸ“ coverage
@[simp]
theorem MulOpposite.unop_natCast {R : Type u_1} [NatCast R] (n : ā„•) :
unop ā†‘n = ā†‘n
source
šŸ“ coverage
@[simp]
theorem AddOpposite.unop_natCast {R : Type u_1} [NatCast R] (n : ā„•) :
unop ā†‘n = ā†‘n
source
šŸ“ coverage
@[simp]
theorem MulOpposite.unop_ofNat {R : Type u_1} [NatCast R] (n : ā„•) [n.AtLeastTwo] :
unop (OfNat.ofNat n) = OfNat.ofNat n
source
šŸ“ coverage
@[simp]
theorem AddOpposite.unop_ofNat {R : Type u_1} [NatCast R] (n : ā„•) [n.AtLeastTwo] :
unop (OfNat.ofNat n) = OfNat.ofNat n
source
šŸ“ coverage
@[simp]
theorem MulOpposite.unop_intCast {R : Type u_1} [IntCast R] (n : ā„¤) :
unop ā†‘n = ā†‘n
source
šŸ“ coverage
@[simp]
theorem AddOpposite.unop_intCast {R : Type u_1} [IntCast R] (n : ā„¤) :
unop ā†‘n = ā†‘n
source
šŸ”ø coverage
@[implicit_reducible]
instance MulOpposite.instAddMonoidWithOne {R : Type u_1} [AddMonoidWithOne R] :
AddMonoidWithOne Rįµįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance MulOpposite.instAddCommMonoidWithOne {R : Type u_1} [AddCommMonoidWithOne R] :
AddCommMonoidWithOne Rįµįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance MulOpposite.instAddGroupWithOne {R : Type u_1} [AddGroupWithOne R] :
AddGroupWithOne Rįµįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance MulOpposite.instAddCommGroupWithOne {R : Type u_1} [AddCommGroupWithOne R] :
AddCommGroupWithOne Rįµįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance MulOpposite.instNonUnitalNonAssocSemiring {R : Type u_1} [NonUnitalNonAssocSemiring R] :
NonUnitalNonAssocSemiring Rįµįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance MulOpposite.instNonUnitalSemiring {R : Type u_1} [NonUnitalSemiring R] :
NonUnitalSemiring Rįµįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance MulOpposite.instNonAssocSemiring {R : Type u_1} [NonAssocSemiring R] :
NonAssocSemiring Rįµįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance MulOpposite.instSemiring {R : Type u_1} [Semiring R] :
Semiring Rįµįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance MulOpposite.instNonUnitalCommSemiring {R : Type u_1} [NonUnitalCommSemiring R] :
NonUnitalCommSemiring Rįµįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance MulOpposite.instCommSemiring {R : Type u_1} [CommSemiring R] :
CommSemiring Rįµįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance MulOpposite.instNonUnitalNonAssocRing {R : Type u_1} [NonUnitalNonAssocRing R] :
NonUnitalNonAssocRing Rįµįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance MulOpposite.instNonUnitalRing {R : Type u_1} [NonUnitalRing R] :
NonUnitalRing Rįµįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance MulOpposite.instNonAssocRing {R : Type u_1} [NonAssocRing R] :
NonAssocRing Rįµįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance MulOpposite.instRing {R : Type u_1} [Ring R] :
Ring Rįµįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance MulOpposite.instNonUnitalCommRing {R : Type u_1} [NonUnitalCommRing R] :
NonUnitalCommRing Rįµįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance MulOpposite.instCommRing {R : Type u_1} [CommRing R] :
CommRing Rįµįµ’įµ–
source
šŸ“ coverage
instance MulOpposite.instIsDomain {R : Type u_1} [Ring R] [IsDomain R] :
IsDomain Rįµįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance AddOpposite.instDistrib {R : Type u_1} [Distrib R] :
Distrib Rįµƒįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance AddOpposite.instAddCommMonoidWithOne {R : Type u_1} [AddCommMonoidWithOne R] :
AddCommMonoidWithOne Rįµƒįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance AddOpposite.instAddCommGroupWithOne {R : Type u_1} [AddCommGroupWithOne R] :
AddCommGroupWithOne Rįµƒįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance AddOpposite.instNonUnitalNonAssocSemiring {R : Type u_1} [NonUnitalNonAssocSemiring R] :
NonUnitalNonAssocSemiring Rįµƒįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance AddOpposite.instNonUnitalSemiring {R : Type u_1} [NonUnitalSemiring R] :
NonUnitalSemiring Rįµƒįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance AddOpposite.instNonAssocSemiring {R : Type u_1} [NonAssocSemiring R] :
NonAssocSemiring Rįµƒįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance AddOpposite.instSemiring {R : Type u_1} [Semiring R] :
Semiring Rįµƒįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance AddOpposite.instNonUnitalCommSemiring {R : Type u_1} [NonUnitalCommSemiring R] :
NonUnitalCommSemiring Rįµƒįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance AddOpposite.instCommSemiring {R : Type u_1} [CommSemiring R] :
CommSemiring Rįµƒįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance AddOpposite.instNonUnitalNonAssocRing {R : Type u_1} [NonUnitalNonAssocRing R] :
NonUnitalNonAssocRing Rįµƒįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance AddOpposite.instNonUnitalRing {R : Type u_1} [NonUnitalRing R] :
NonUnitalRing Rįµƒįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance AddOpposite.instNonAssocRing {R : Type u_1} [NonAssocRing R] :
NonAssocRing Rįµƒįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance AddOpposite.instRing {R : Type u_1} [Ring R] :
Ring Rįµƒįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance AddOpposite.instNonUnitalCommRing {R : Type u_1} [NonUnitalCommRing R] :
NonUnitalCommRing Rįµƒįµ’įµ–
source
šŸ”ø coverage
@[implicit_reducible]
instance AddOpposite.instCommRing {R : Type u_1} [CommRing R] :
CommRing Rįµƒįµ’įµ–
source
šŸ“ coverage
instance AddOpposite.instIsDomain {R : Type u_1} [Ring R] [IsDomain R] :
IsDomain Rįµƒįµ’įµ–
source
šŸ”ø coverage
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
    šŸ“ coverage
    @[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
    šŸ”ø coverage
    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
      šŸ“ coverage
      @[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
      šŸ”ø coverage
      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
        šŸ“ coverage
        @[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
        šŸ“ coverage
        @[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
        šŸ”ø coverage
        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
          šŸ”ø coverage
          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
            šŸ“ coverage
            @[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
            šŸ”ø coverage
            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
              šŸ“ coverage
              @[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
              šŸ”ø coverage
              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
                šŸ“ coverage
                @[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
                šŸ“ coverage
                @[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
                šŸ”ø coverage
                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