Magma

Magmaā€…ā€ŠAā€…ā€ŠāŠ—\textbf{Magma} \; A \; \otimes

Functionā€…ā€Š(AƗA)ā€…ā€ŠAā€…ā€ŠāŠ—\textbf{Function} \; (A \times A) \; A \; \otimes


pred Magma(A: set univ, op: univ->univ->univ) {
  op in (A->A)-> one A
}
AutoInverseā€…ā€ŠAā€…ā€Šfā€…ā€ŠI\textbf{AutoInverse} \; A \; f \; I

Unitalā€…ā€ŠAā€…ā€Šfā€…ā€ŠI\textbf{Unital} \; A \; f\; I

āˆ€(xāˆˆA::f(x,x)=I)\forall(x \in A ::f(x,x) = I)


pred AutoInverse(A: set univ, f: univ->univ->univ, I: univ) {
  Unital[A,f,I]
  all x: A | f[x,x] = I
}
Idempotentā€…ā€ŠAā€…ā€ŠāŠ—\textbf{Idempotent} \; A \; \otimes

Magmaā€…ā€ŠAā€…ā€ŠāŠ—\textbf{Magma} \; A \; \otimes

āˆ€(aāˆˆA::aāŠ—a=a)\forall(a \in A :: a \otimes a = a)


pred Idempotent(A: set univ, op: univ->univ->univ) {
  Magma[A,op]
  all a: A | op[a,a] = a
}
Inverseā€…ā€ŠAā€…ā€Šfā€…ā€ŠIā€…ā€Šyā€…ā€Šx\textbf{Inverse} \; A \; f \; I \; y \; x

LeftInverseā€…ā€ŠAā€…ā€Šfā€…ā€ŠIā€…ā€Šyā€…ā€Šx\textbf{LeftInverse} \; A \; f \; I \; y \; x

RightInverseā€…ā€ŠAā€…ā€Šfā€…ā€ŠIā€…ā€Šyā€…ā€Šx\textbf{RightInverse} \; A \; f \; I \; y \; x


pred Inverse(A: set univ, f: univ->univ->univ, I,y,x: univ) {
  LeftInverse[A,f,I,y,x]
  RightInverse[A,f,I,y,x]
}
LeftInverseā€…ā€ŠAā€…ā€Šfā€…ā€ŠIā€…ā€Šyā€…ā€Šx\textbf{LeftInverse} \; A \; f \; I \; y \; x

Unitalā€…ā€ŠAā€…ā€Šfā€…ā€ŠI\textbf{Unital} \; A \; f \; I

f(L,x)=If(L,x) = I


pred LeftInverse(A: set univ, f: univ->univ->univ, I,L,x: univ) {
  Unital[A,f,I]
  f[L,x] = I
}
LeftUnitā€…ā€ŠAā€…ā€ŠāŠ—ā€…ā€ŠI\textbf{LeftUnit} \; A \; \otimes \; I

Magmaā€…ā€ŠAā€…ā€ŠāŠ—\textbf{Magma} \; A \; \otimes

IāˆˆAI \in A

āˆ€(xāˆˆA::IāŠ—x=x)\forall(x \in A :: I \otimes x = x )


pred LeftUnit(A: set univ, op: univ->univ->univ, I: univ) {
  Magma[A,op]
  I in A
  all x: A | op[I,x] = x
}
LeftZeroā€…ā€ŠAā€…ā€Šfā€…ā€ŠZ\textbf{LeftZero} \; A \; f \; Z

Magmaā€…ā€ŠAā€…ā€ŠāŠ—\textbf{Magma} \; A \; \otimes

IāˆˆAI \in A

āˆ€(xāˆˆA::f(Z,x)=Z)\forall(x \in A :: f(Z,x) = Z)


pred LeftZero(A: set univ, f: univ->univ->univ, Z: univ) {
  Magma[A,f]
  Z in A
  all x: A | f[Z,x] = Z
}
RightInverseā€…ā€ŠAā€…ā€Šfā€…ā€ŠIā€…ā€Šyā€…ā€Šx\textbf{RightInverse} \; A \; f \; I \; y \; x

Unitalā€…ā€ŠAā€…ā€Šfā€…ā€ŠI\textbf{Unital} \; A \; f \; I

f(x,R)=If(x,R) = I


pred RightInverse(A: set univ, f: univ->univ->univ, I,R,x: univ) {
  Unital[A,f,I]
  f[x,R] = I
}
RightUnitā€…ā€ŠAā€…ā€ŠāŠ—ā€…ā€ŠI\textbf{RightUnit} \; A \; \otimes \; I

Magmaā€…ā€ŠAā€…ā€ŠāŠ—\textbf{Magma} \; A \; \otimes

IāˆˆAI \in A

āˆ€(xāˆˆA::x=xāŠ—I)\forall(x \in A :: x = x \otimes I )


pred RightUnit(A: set univ, op: univ->univ->univ, I: univ) {
  Magma[A,op]
  I in A
  all x: A | x = op[x,I]
}
RightZeroā€…ā€ŠAā€…ā€Šfā€…ā€ŠZ\textbf{RightZero} \; A \; f \; Z

Magmaā€…ā€ŠAā€…ā€ŠāŠ—\textbf{Magma} \; A \; \otimes

IāˆˆAI \in A

āˆ€(xāˆˆA::f(x,Z)=Z)\forall(x \in A :: f(x,Z) = Z)


pred RightZero(A: set univ, f: univ->univ->univ, Z: univ) {
  Magma[A,f]
  Z in A
  all x: A | f[x,Z] = Z
}
Symmetricā€…ā€ŠAā€…ā€ŠāŠ—\textbf{Symmetric} \; A \; \otimes

Magmaā€…ā€ŠAā€…ā€ŠāŠ—\textbf{Magma} \; A \; \otimes

āˆ€(x,yāˆˆA::xāŠ—y=yāŠ—x)\forall(x,y \in A :: x \otimes y = y \otimes x)


pred Symmetric(A: set univ, op: univ->univ->univ) {
  Magma[A,op]
  all x,y: A | op[x,y] = op[y,x]
}
Unitalā€…ā€ŠAā€…ā€ŠāŠ—ā€…ā€ŠI\textbf{Unital} \; A \; \otimes \; I

LeftUnitā€…ā€ŠAā€…ā€ŠāŠ—ā€…ā€ŠI\textbf{LeftUnit} \; A \; \otimes \; I

RightUnitā€…ā€ŠAā€…ā€ŠāŠ—ā€…ā€ŠI\textbf{RightUnit} \; A \; \otimes \; I


pred Unital(A: set univ, op: univ->univ->univ, I: univ) {
  LeftUnit[A,op,I]
  RightUnit[A,op,I]
}
Zeroā€…ā€ŠAā€…ā€Šfā€…ā€ŠZ\textbf{Zero} \; A \; f \; Z

LeftZeroā€…ā€ŠAā€…ā€Šfā€…ā€ŠZ\textbf{LeftZero} \; A \; f \; Z

RightZeroā€…ā€ŠAā€…ā€Šfā€…ā€ŠZ\textbf{RightZero} \; A \; f \; Z


pred Zero(A: set univ, f: univ->univ->univ, Z: univ) {
  LeftZero[A,f,Z]
  RightZero[A,f,Z]
}

Last updated