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