# Differences

This shows you the differences between two versions of the page.

equations [2010/08/18 12:34]
jipsen
equations [2017/10/02 10:57] (current)
jipsen
Line 3: Line 3:
Here we list equations, with the shorter term on the right (if possible). Here we list equations, with the shorter term on the right (if possible).
-|trivial equations:  | $x = y$ $\quad f(x) = y$ $\quad x*y = z$  | $\Rightarrow$ one-element algebras  || +|1  |trivial equations:  | $x = y$ $\quad f(x) = y$ $\quad x*y = z$  | $\Rightarrow$ one-element algebras  ||
-|identity operation:  | $f(x) = x$  ||| +|2  |identity operation:  | $f(x) = x$  |||
-|self-inverse operation:  | $f(f(x)) = x$  ||| +|3  |involutive operation:  | $f(f(x)) = x$  |||
-|inverse operations:  | $f(g(x)) = x$  ||| +|4  |inverse operations:  | $f(g(x)) = x$  |||
-|order-$n$ operation:  | $f^n(x) = x$  ||| +|5  |inside absorption:  | $f(g(x)) = f(x)$  |||
-|$f$-idempotent  | $f(f(x)) = f(x)$  ||| +|6  |outside absorption:  | $f(g(x)) = g(x)$  |||
-|constant operations:  | $f(x) = 1$ $\quad f(x) = f(y)$ $\quad x*y = 1$  | $x*y = f(z)$  | $x*y = z*w$  | +|7  |order-$n$ operation:  | $f^n(x) = x$  |||
-|left projection:  | $x*y = x$  | right projection:  | $x*y = y$  | +|8  |$f$-idempotent  | $f(f(x)) = f(x)$  |||
-|idempotent:  | $x*x = x$  ||| +|9  |constant operations:  | $f(x) = 1$ $\quad f(x) = f(y)$ $\quad x*y = 1$  | $x*y = f(z)$  | $x*y = z*w$  |
-|$n$-potent:  | $x^{n+1} = x^n$  ||| +|10  |left projection:  | $x*y = x$  | right projection:  | $x*y = y$  |
-|left identity:  | $1*x = x$  | right identity:  | $x*1 = x$  | +|11  |idempotent:  | $x*x = x$  |||
-|left zero:  | $0*x = 0$  | right zero:  | $x*0 = 0$  | +|12  |$n$-potent:  | $x^{n+1} = x^n$  |||
-|left $f$-projection:  | $x*y = f(x)$  | right $f$-projection:  | $x*y = f(y)$  | +|13  |left identity:  | $1*x = x$  | right identity:  | $x*1 = x$  |
-|square constant:  | $x*x = 1$  ||| +|14  |left zero:  | $0*x = 0$  | right zero:  | $x*0 = 0$  |
-|square definition:  | $x*x = f(x)$  ||| +|15  |left $f$-projection:  | $x*y = f(x)$  | right $f$-projection:  | $x*y = f(y)$  |
-|left constant multiple:  | $1*x = f(x)$  | right constant multiple:  | $x*1 = f(x)$  | +|16  |square constant:  | $x*x = 1$  |||
-|commutative:  | $x*y = y*x$  ||| +|17  |square definition:  | $x*x = f(x)$  |||
-|left inverse:  | $f(x)*x = 1$  | right inverse:  | $x*f(x) = 1$  | +|18  |left constant multiple:  | $1*x = f(x)$  | right constant multiple:  | $x*1 = f(x)$  |
-|left $f$-identity:  | $f(x)*x = x$  | right $f$-identity:  | $x*f(x) = x$  | +|19  |commutative:  | $x*y = y*x$  |||
-|interassociative:  | $x*(y+z) = (x+y)*z$  ||| +|20  |left inverse:  | $f(x)*x = 1$  | right inverse:  | $x*f(x) = 1$  |
-|associative:  | $x*(y*z) = (x*y)*z$  ||| +|21  |left $f$-identity:  | $f(x)*x = x$  | right $f$-identity:  | $x*f(x) = x$  |
-|left commutativity:  | $x*(y*z) = y*(x*z)$  | right commutativity:  | $(x*y)*z = (x*z)*y$  | +|22  |interassociative:  | $x*(y+z) = (x+y)*z$  |||
-|left idempotent:  | $x*(x*y) = x*y$  | right idempotent:  | $(x*y)*y = x*y$  | +|23  |associative:  | $x*(y*z) = (x*y)*z$  |||
-|left rectangular:  | $(x*y)*x = x$  | right rectangular:  | $x*(y*x) = x$  | +|24  |left commutativity:  | $x*(y*z) = y*(x*z)$  | right commutativity:  | $(x*y)*z = (x*z)*y$  |
-|left distributive:  | $x*(y+z) = (x*y)+(x*z)$  | right distributive:  | $(x+y)*z = (x*z)+(y*z)$  | +|25  |left idempotent:  | $x*(x*y) = x*y$  | right idempotent:  | $(x*y)*y = x*y$  |
-|$f$-commutative:  | $f(x)*f(y) = f(y)*f(x)$  ||| +|26  |left rectangular:  | $(x*y)*x = x$  | right rectangular:  | $x*(y*x) = x$  |
-|$f$-involutive:  | $f(x*y) = f(y)*f(x)$  ||| +|27  |left absorption:  | $(x*y)+x = x$  | right absorption:  | $x+(y*x) = x$  |
-|$f$-interdistributive:  | $f(x*y) = f(x)+f(y)$  ||| +|28  |left absorption1:  | $(x*y)+y = y$  | right absorption1:  | $y+(x*y) = y$  |
-|$f$-distributive:  | $f(x*y) = f(x)*f(y)$  | also $f$-linear  || +|29  |left subtraction:  | $x*(x+y) = y$  | right subtraction:  | $(y+x)*x = y$  |
-|left $f$-constant multiple:  | $f(1*x) = 1*f(x)$  | right $f$-constant multiple:  | $f(x*1) = f(x)*1$  | +|30  |left distributive:  | $x*(y+z) = (x*y)+(x*z)$  | right distributive:  | $(x+y)*z = (x*z)+(y*z)$  |
-|left twisted:  | $f(x*y)*x = x*f(y)$  | right twisted:  | $x*f(y*x) = f(y)*x$  | +|31  |left self-distributive:  | $x*(y*z) = (x*y)*(x*z)$  | right distributive:  | $(x*y)*z = (x*z)*(y*z)$  |
-|left locality:  | $f(f(x)*y) = f(x*y)$  | right locality:  | $f(x*f(y)) = f(x*y)$  | +|32  |$f$-commutative:  | $f(x)*f(y) = f(y)*f(x)$  |||
-|left $f$-distributive:  | $f(f(x)*y) = f(x)*f(y)$  | right $f$-distributive:  | $f(x*f(y)) = f(x)*f(y)$  | +|33  |$f$-involutive:  | $f(x*y) = f(y)*f(x)$  |||
-|left $f$-absorbtive:  | $f(x)*f(x*y) = f(x*y)$  | right $f$-absorbtive:  | $f(x*y)*f(y)) = f(x*y)$  | +|34  |$f$-interdistributive:  | $f(x*y) = f(x)+f(y)$  |||
-|entropic:  | $(x*y)*(z*w) = (x*z)*(y*w)$  ||| +|35  |$f$-distributive:  | $f(x*y) = f(x)*f(y)$  | also $f$-linear  ||
-|paramedial:  | $(x*y)*(z*w) = (w*y)*(z*x)$  ||| +|36  |left $f$-constant multiple:  | $f(1*x) = 1*f(x)$  | right $f$-constant multiple:  | $f(x*1) = f(x)*1$  |
+|37  |left twisted:  | $f(x*y)*x = x*f(y)$  | right twisted:  | $x*f(y*x) = f(y)*x$  |
+|38  |left locality:  | $f(f(x)*y) = f(x*y)$  | right locality:  | $f(x*f(y)) = f(x*y)$  |
+|39  |left $f$-distributive:  | $f(f(x)*y) = f(x)*f(y)$  | right $f$-distributive:  | $f(x*f(y)) = f(x)*f(y)$  |
+|40  |left $f$-absorbtive:  | $f(x)*f(x*y) = f(x*y)$  | right $f$-absorbtive:  | $f(x*y)*f(y)) = f(x*y)$  |
+|41  |flexible:  | $(x*y)*x = x*(y*x)$  |||
+|42  |entropic:  | $(x*y)*(z*w) = (x*z)*(y*w)$  |||
+|43  |paramedial:  | $(x*y)*(z*w) = (w*y)*(z*x)$  ||
+|44  |Moufang1:  | $((x*y)*x)*z = x*(y*(x*z))$  | Moufang2:  | $((x*y)*z)*y = x*(y*(z*y))$  |
+|45  |Moufang3:  | $(x*y)*(z*x) = (x*(y*z))*x$  | Moufang4:  | $(x*y)*(z*x) = x*((y*z)*x)$  |
+Here are the identities in the syntax of the Lean Theorem Prover
+
+<code>
+section identities
+
+variables {α: Type u} {β: Type v}
+variables f g: α → α → α
+variables h k: α → α
+variable  c: α
+local notation a⬝b  := f a b
+local notation a+b := g a b
+local notation a⁻¹ := h a
+local notation 1   := c
+local notation 0   := c
+
+def involutive              := ∀x,     h(h x) = x
+def inverse_operations      := ∀x,     h(k x) = x
+def left_absorption         := ∀x,     h(k x) = k x
+def right_absorption        := ∀x,     h(k x) = h x
+def unary_idempotent        := ∀x,     h(h x) = h x
+def idempotent              := ∀x,     x⬝x = x
+def left_identity           := ∀x,     1⬝x = x
+def right_identity          := ∀x,     x⬝1 = x
+def left_zero               := ∀x,     0⬝x = 0
+def right_zero              := ∀x,     x⬝0 = 0
+def left_inverse            := ∀x,     x⁻¹⬝x = 1
+def right_inverse           := ∀x,     x⬝x⁻¹ = 1
+def left_const_mult         := ∀x,     c⬝x = h x
+def right_const_mult        := ∀x,     x⬝c = h x
+def square_constant         := ∀x,     x⬝x = c
+def square_unary            := ∀x,     x⬝x = h x
+def left_unary_identity     := ∀x,     (h x)⬝x = x
+def right_unary_identity    := ∀x,     x⬝(h x) = x
+def left_unary_const_mult   := ∀x,     h(c⬝x) = c⬝(h x)
+def right_unary_const_mult  := ∀x,     h(x⬝c) = (h x)⬝c
+def commutative             := ∀x y,   x⬝y = y⬝x
+def left_unary_projection   := ∀x y,   x⬝y = h x
+def right_unary_projection  := ∀x y,   x⬝y = h y
+def left_idempotent         := ∀x y,   x⬝(x⬝y) = x⬝y
+def right_idempotent        := ∀x y,   (x⬝y)⬝y = x⬝y
+def left_rectangular        := ∀x y,   (x⬝y)⬝x = x
+def right_rectangular       := ∀x y,   x⬝(y⬝x) = x
+def left_absorption1        := ∀x y,   (x⬝y)+y = y
+def right_absorption1       := ∀x y,   y+(x⬝y) = y
+def left_absorption2        := ∀x y,   (x⬝y)+x = x
+def right_absorption2       := ∀x y,   x+(y⬝x) = x
+def left_subtraction        := ∀x y,   x⬝(x+y) = y
+def right_subtraction       := ∀x y,   (y+x)⬝x = y
+def unary_commutative       := ∀x y,   (h x)⬝(h y) = (h y)⬝(h x)
+def unary_involutive        := ∀x y,   h(x⬝y) = (h y)⬝(h x)
+def interdistributive       := ∀x y,   h(x⬝y) = (h x)+(h y)
+def unary_distributive      := ∀x y,   h(x⬝y) = (h x)⬝(h y)
+def left_twisted            := ∀x y,   (h(x⬝y))⬝x = x⬝(h y)
+def right_twisted           := ∀x y,   x⬝(h(y⬝x)) = (h y)⬝x
+def left_locality           := ∀x y,   h((h x)⬝y) = h(x⬝y)
+def right_locality          := ∀x y,   h(x⬝(h y)) = h(x⬝y)
+def left_unary_distributive := ∀x y,   h((h x)⬝y) = (h x)⬝(h y)
+def right_unary_distributive:= ∀x y,   h(x⬝(h y)) = (h x)⬝(h y)
+def left_absorbtive         := ∀x y,   (h x)⬝(h(x⬝y)) = h(x⬝y)
+def right_absorbtive        := ∀x y,   (h(x⬝y))⬝(h y) = h(x⬝y)
+def flexible                := ∀x y,   (x⬝y)⬝x = x⬝(y⬝x)
+def associative             := ∀x y z, x⬝(y⬝z) = (x⬝y)⬝z
+def left_commutative        := ∀x y z, x⬝(y⬝z) = y⬝(x⬝z)
+def right_commutative       := ∀x y z, (x⬝y)⬝z = (x⬝z)⬝y
+def interassociative1       := ∀x y z, x⬝(y+z) = (x⬝y)+z
+def interassociative2       := ∀x y z, x⬝(y+z) = (x+y)⬝z
+def left_distributive       := ∀x y z, x⬝(y+z) = (x⬝y)+(x⬝z)
+def right_distributive      := ∀x y z, (x+y)⬝z = (x⬝z)+(y⬝z)
+def left_self_distributive  := ∀x y z, x⬝(y⬝z) = (x⬝y)⬝(x⬝z)
+def right_self_distributive := ∀x y z, (x⬝y)⬝z = (x⬝z)⬝(y⬝z)
+def Moufang1                := ∀x y z, ((x⬝y)⬝x)⬝z = x⬝(y⬝(x⬝z))
+def Moufang2                := ∀x y z, ((x⬝y)⬝z)⬝y = x⬝(y⬝(z⬝y))
+def Moufang3                := ∀x y z, (x⬝y)⬝(z⬝x) = (x⬝(y⬝z))⬝x
+def Moufang4                := ∀x y z, (x⬝y)⬝(z⬝x) = x⬝((y⬝z)⬝x)
+def entropic                := ∀x y z w, (x⬝y)⬝(z⬝w) = (x⬝z)⬝(y⬝w)
+def paramedial              := ∀x y z w, (x⬝y)⬝(z⬝w) = (w⬝y)⬝(z⬝x)
+
+
+end identities
+</code>