Documentation

Mathlib.Algebra.Ring.Associator

Associator in a ring #

If R is a non-associative ring, then (x * y) * z - x * (y * z) is called the associator of ring elements x y z : R.

The associator vanishes exactly when R is associative.

We prove variants of this statement also for the AddMonoidHom bundled version of the associator, as well as the bundled version of mulLeft₃ and mulRight₃, the multiplications (x * y) * z and x * (y * z).

source
def associator {R : Type u_1} [NonUnitalNonAssocRing R] (x y z : R) :
R

The associator (x * y) * z - x * (y * z)

Equations
    Instances For
      source
      theorem associator_apply {R : Type u_1} [NonUnitalNonAssocRing R] (x y z : R) :
      associator x y z = x * y * z - x * (y * z)
      source
      theorem associator_eq_zero_iff_associative {R : Type u_1} [NonUnitalNonAssocRing R] :
      associator = 0 ↔ Std.Associative fun (x y : R) => x * y
      source
      theorem associator_cocycle {R : Type u_1} [NonUnitalNonAssocRing R] (a b c d : R) :
      a * associator b c d - associator (a * b) c d + associator a (b * c) d - associator a b (c * d) + associator a b c * d = 0
      source
      @[simp]
      theorem associator_eq_zero {R : Type u_1} [NonUnitalRing R] :
      associator = 0
      source
      def AddMonoidHom.mulLeft₃ {R : Type u_1} [NonUnitalNonAssocSemiring R] :
      R →+ R →+ R →+ R

      The multiplication (x * y) * z of three elements of a (non-associative) (semi)-ring is an AddMonoidHom in each argument. See also LinearMap.mulLeftRight for a related functions realized as a linear map.

      Equations
        Instances For
          source
          @[simp]
          theorem AddMonoidHom.mulLeft₃_apply {R : Type u_1} [NonUnitalNonAssocSemiring R] (x y z : R) :
          ((mulLeft₃ x) y) z = x * y * z
          source
          def AddMonoidHom.mulRight₃ {R : Type u_1} [NonUnitalNonAssocSemiring R] :
          R →+ R →+ R →+ R

          The multiplication x * (y * z) of three elements of a (non-associative) (semi)-ring is an AddMonoidHom in each argument.

          Equations
            Instances For
              source
              @[simp]
              theorem AddMonoidHom.mulRight₃_apply {R : Type u_1} [NonUnitalNonAssocSemiring R] (x y z : R) :
              ((mulRight₃ x) y) z = x * (y * z)
              source
              theorem AddMonoidHom.mulLeft₃_eq_mulRight₃_iff_associative {R : Type u_1} [NonUnitalNonAssocSemiring R] :
              mulLeft₃ = mulRight₃ ↔ Std.Associative fun (x y : R) => x * y

              An a priori non-associative semiring is associative if the AddMonoidHom versions of the multiplications (x * y) * z and x * (y * z) agree.

              source
              theorem AddMonoidHom.mulLeft₃_eq_mulRight₃ {R : Type u_1} [NonUnitalSemiring R] :
              mulLeft₃ = mulRight₃
              source
              def AddMonoidHom.associator {R : Type u_1} [NonUnitalNonAssocRing R] :
              R →+ R →+ R →+ R

              The associator for a non-associative ring is (x * y) * z - x * (y * z). It is an AddMonoidHom in each argument.

              Equations
                Instances For
                  source
                  @[simp]
                  theorem AddMonoidHom.associator_apply {R : Type u_1} [NonUnitalNonAssocRing R] (a b c : R) :
                  ((associator a) b) c = _root_.associator a b c
                  source
                  theorem AddMonoidHom.associator_eq_zero_iff_associative {R : Type u_1} [NonUnitalNonAssocRing R] :
                  associator = 0 ↔ Std.Associative fun (x y : R) => x * y

                  An a priori non-associative ring is associative iff the AddMonoidHom version of the associator vanishes.

                  source
                  @[simp]
                  theorem AddMonoidHom.associator_eq_zero {R : Type u_1} [NonUnitalRing R] :
                  associator = 0