add more algebra content

algebra/field.math

@@ -20,10 +20,12 @@ when:
 . 'x [in]: F'
 means: 'y [in]: F'
 specifies:
-. 'x * y = F.1'
-. 'y * x = F.1'
+. 'x * y = 1'
+. 'y * x = 1'
 Documented:
 . called: "multiplicative inverse of x? in F?"
+Aliases:
+. '1 :=> F.1'
 ------------------------------------------
 Id: "594614bc-fde5-4b06-8697-f8cc921c1fc0"
 

algebra/group.math

@@ -49,19 +49,65 @@ Documented:
 Id: "404e418f-9ab4-4080-9dfd-ff8054f3f555"
 
 
+[\subgroup:of{G := (X, *, e)}]
+Describes: H := (Y, *_0, u)
+when: 'G is \group'
+extends: 'Y is \set'
+satisfies:
+. 'Y [subset] X'
+. 'Y is \non.empty.set'
+. forAll: x, y
+  where: 'x, y [in]: Y'
+  then: 'x *_0 y := x * y'
+. forAll: x
+  where: 'x [in]: Y'
+  then: 'x.inv [in]: Y'
+. forAll: x, y
+  where: 'x, y [in]: Y'
+  then: 'x *_0 y [in]: Y'
+Documented:
+. called: "subgroup of $G?$"
+------------------------------------------
+Id: "c12a4601-5513-42b6-97e3-19e64896b14f"
+
+
+[H := (X, *, e) \subgroup/ G]
+States:
+when:
+. 'G is \group'
+. 'X is \set'
+that: 'H is \subgroup:of{G}'
+Documented:
+. written: "H? \leq G?"
+------------------------------------------
+Id: "8b8b2238-a9bb-44e4-a4aa-b7857fbd9d51"
+
+
+Theorem:
+given: G, H
+where: 'G is \group'
+if: 'H \subgroup/ G'
+then: 'H is \group'
+------------------------------------------
+Id: "6fe2d452-6b58-442e-920b-f273fac1b3b9"
+
+
+
 [\group.inverse:of{x}:in{G}]
 Defines: y
 when:
 . 'G is \group'
 . 'x [in]: G'
 means: 'y [in]: G'
 specifies:
-. 'x * y = G.e'
-. 'y * x = G.e'
+. 'x * y = e'
+. 'y * x = e'
 Justified:
 . by: "\[group]::(existence.of.inverses)"
 Documented:
 . written: "x?^{-1}"
+Aliases:
+. 'e :=> G.e'
 ------------------------------------------
 Id: "2293a62b-71a4-431e-82a1-c7613a52267f"
 
@@ -90,9 +136,8 @@ Documented:
 Id: "1aaf732a-1987-4ee2-860e-98adf261b5f6"
 
 
-[G1 \group.direct.product/ G2]
+[G1 := (X1, *_1, e1) \group.direct.product/ G2 := (X2, *_2, e2)]
 Defines: H := (Y, +, u)
-using: G1 := (X1, *_1, e1), G2 := (X2, *_2, e2)
 when: 'G1, G2 is \group'
 specifies:
 . 'Y := X1 \set.times/ X2'
@@ -191,9 +236,8 @@ Documented:
 Id: "ad529afe-2429-4264-b7f1-bacdf017cdcc"
 
 
-[\finite.group.order.of{x}:in{G}]
+[\finite.group.order.of{x}:in{G := (X, *, e)}]
 Defines: n
-using: G := (X, *, e)
 when:
 . 'G is \group'
 . 'n is \natural'

algebra/module.math

@@ -3,22 +3,21 @@
 ::
 
 [\left.module:over{R0}]
-Describes: M := (R, G, **)
+Describes: M := (R, G, *)
 when: 'R0 is \ring'
 extends: 'G is \group'
 satisfies:
 . 'R := R0'
-. '"**" is \function:on{R, G}:to{G}'
+. '"*" is \function:on{R, G}:to{G}'
 . [scalar.multiplication]
   forAll: r, s, x, y
   where:
   . 'r, s [in]: R'
   . 'x, y [in]: G'
   then:
-  . 'r ** (x + y) = r ** x + r ** y'
-  . '(r + s) ** x = r ** x + s ** x'
-  . '(r * s) ** x = r ** (s ** x)'
-  . 'R.1 ** x = x'
+  . 'r * (x + y) = r * x + r * y'
+  . '(r + s) * x = r * x + s * x'
+  . '(r * s) * x = r * (s * x)'
 Provides:
 . 'x [in]: M :-> x is \left.module.element:of{M}:over{R0}'
 Documented:
@@ -39,23 +38,56 @@ Documented:
 Id: "16fcb4da-dd89-4c0f-a6a9-2cbbde4db34d"
 
 
+[\left.module]
+Describes: M := (R, G, *)
+extends: 'M is \left.module:over{R}'
+Documented:
+. called: "left module"
+------------------------------------------
+Id: "b31db455-e075-4e67-823e-65d76087290a"
+
+
+[\unital.left.module:over{R}]
+Describes: M
+when: 'R is \ring.with.identity'
+extends: 'M is \left.module:over{R}'
+satisfies:
+. forAll: x
+  where: 'x [in]: M'
+  then: 'R.1 * x = x'
+Provides:
+. 'M.1 :=> R.1'
+Documented:
+. called: "unital left module over $R?$"
+------------------------------------------
+Id: "a3ee62a8-9a0b-46a8-89e1-95fd1bebb379"
+
+
+[\unital.left.module]
+Describes: M := (R, G, *)
+extends: 'M is \unital.left.module:over{R}'
+Documented:
+. called: "unital left module"
+------------------------------------------
+Id: "9e4db744-9571-4952-8f91-4ccb0873d788"
+
+
 [\right.module:over{R0}]
-Describes: M := (R, G, **)
+Describes: M := (R, G, *)
 when: 'R0 is \ring'
 extends: 'G is \group'
 satisfies:
 . 'R := R0'
-. '"**" is \function:on{G, R}:to{G}'
+. '"*" is \function:on{G, R}:to{G}'
 . [scalar.multiplication]
   forAll: r, s, x, y
   where:
   . 'r, s [in]: R'
   . 'x, y [in]: G'
   then:
-  . '(x + y) ** r = x ** r + y ** r'
-  . 'x ** (r + s) = x ** r + x ** s'
-  . 'x ** (r * s) = (x ** r) ** s'
-  . 'x ** R.1 = x'
+  . '(x + y) * r = x * r + y * r'
+  . 'x * (r + s) = x * r + x * s'
+  . 'x * (r * s) = (x * r) * s'
 Provides:
 . 'x [in]: M :-> x is \right.module.element:of{M}:over{R0}'
 Documented:
@@ -76,12 +108,46 @@ Documented:
 Id: "6cf2b484-f3e4-426a-9429-14443fa6c1d4"
 
 
+[\right.module]
+Describes: M := (R, G, *)
+extends: 'M is \right.module:over{R}'
+Documented:
+. called: "right module"
+------------------------------------------
+Id: "d8a4d363-63ff-4bc4-b0d1-60336739c587"
+
+
+[\unital.right.module:over{R}]
+Describes: M
+when: 'R is \ring.with.identity'
+extends: 'M is \right.module:over{R}'
+satisfies:
+. forAll: x
+  where: 'x [in]: M'
+  then: 'x * R.1  = x'
+Provides:
+. 'M.1 :=> R.1'
+Documented:
+. called: "unital right module over $R?$"
+------------------------------------------
+Id: "28e4fc1f-2a8a-4261-acfc-39102dcb0bb3"
+
+
+[\unital.right.module]
+Describes: M := (R, G, *)
+extends: 'M is \unital.right.module:over{R}'
+Documented:
+. called: "unital right module"
+------------------------------------------
+Id: "0b048b82-51b6-4d8f-82c9-ffd7259884a7"
+
+
 [\bi.module:over{R0, S0}]
-Describes: M := (R, S, G, **_R, **_S)
+Describes: M := (R, S, G, *_R, *_S)
 when: 'R0, S0 is \ring'
 extends:
-. '(R, G, "**_R") is \left.module:over{R0}'
-. '(R, G, "**_S") is \right.module:over{S0}'
+. '(R, G, "*_R") is \left.module:over{R0}'
+. '(S, G, "*_S") is \right.module:over{S0}'
 Documented:
 . called: "$(R0?, S0?)$ bi-module"
 ------------------------------------------
@@ -102,12 +168,28 @@ Documented:
 Id: "dae7a056-c405-43ac-ab29-3dead7c9e9d9"
 
 
-[\module.over:over{R0}]
-Describes: M := (R, G, **)
-when: 'R is \commutative.ring'
-extends:
-. '(R, R, G, "**", "**") is \bi.module:over{R0, S0}'
+[\bi.module]
+Describes: M := (R, S, G, *_R, *_S)
+extends: 'M is \bi.module:over{R, S}'
 Documented:
-. called: "$R0?$-module"
+. called: "bi-module"
+------------------------------------------
+Id: "224597f1-649e-459d-a7c9-68fd325f2eb4"
+
+
+Theorem:
+given: M := (R, G, *), *_0
+where:
+. 'M is \left.module'
+. '"*_0" is \function:on{M, R}:to{M}'
+if:
+. forAll: m, r
+  where:
+  . 'm [in]: M'
+  . 'r [in]: R'
+  then:
+  . 'm *_0 r := r * m'
+then: '(R, G, "*_0") is \right.module'
 ------------------------------------------
-Id: "515e7510-65e6-4a22-8a7f-59486bd16d6c"
+Id: "df6f95f4-7552-49e0-ad02-ff9a9a123cb1"
+

algebra/ring.math

@@ -109,19 +109,22 @@ Id: "029fa21a-8527-4a08-9035-d5a29d8014f6"
 Describes: R
 extends: 'R is \ring.with.identity'
 satisfies:
-. 'R.0 != R.1'
+. '0 != 1'
 . forAll: x
   where: 'x [in]: R'
-  suchThat: 'x != R.0'
+  suchThat: 'x != 0'
   then:
   . exists: y
     where: 'y [in]: R'
     suchThat:
-    . 'x * y = R.1'
-    . 'y * x = R.1'
+    . 'x * y = 1'
+    . 'y * x = 1'
 Documented:
 . called:
   . "division ring"
   . "skew field"
+Aliases:
+. '0 :=> R.0'
+. '1 :=> R.1'
 ------------------------------------------
 Id: "15c7b3f3-7fbb-4746-b6a9-e5e374fff494"

algebra/vector_space.math

@@ -2,12 +2,12 @@
 # Vector Spaces
 ::
 
-[\vector.space:over{F0}]
+[\vector.space:over{F}]
 Describes: V
-when: 'F0 is \field'
-extends: 'V is \module.over:over{F}'
+when: 'F is \field'
+extends: 'V is \left.module:over{F}'
 Documented:
-. called: "vector space over $F0?$"
+. called: "vector space over $F?$"
 ------------------------------------------
 Id: "20ed885f-67b5-406f-a8f1-50739781633e"
 
@@ -17,7 +17,7 @@ Describes: x
 when:
 . 'F is \field'
 . 'V is \vector.space:over{F}'
-extends: 'x is \module.over:over{V}'
+extends: 'x is \left.module:over{V}'
 Documented:
 . called: "element of vector space $V?$ over $F?$"
 ------------------------------------------