Nuprl Definition : s-group
This is a "fully constructive" version of the normal
algebraic concept of a group.
The difference is that the "points" (i.e. the elements) of the group
come from a SeparationSpace -- a type with a separation relation x # x'.
Then the negation ⌜¬x # x'⌝ -- which we write ⌜x ≡ x'⌝ -- is an equivalence
relation on the elements.
We could then form a quotient type ⌜x,x':Point//x ≡ x'⌝ and use the
normal defintion of a group with elements from the quotient type.
But, in general, we may not be able to define the needed operations on the
quotient.
Instead, we state the "equations" (associativity, inverse, and identity) using
the equivalence realtion x ≡ x' instead of equality.
In addition, we add as axioms that the group operations
are "strongly extensional"⋅
s-Group ==
SeparationSpace
"id":Point
"inv":Point ⟶ Point
"op":{f:Point ⟶ Point ⟶ Point|
(∀x,y,z:Point. f x (f y z) ≡ f (f x y) z)
∧ (∀x:Point. f x self."id" ≡ x)
∧ (∀x:Point. f x (self."inv" x) ≡ self."id")}
"opsep":∀x,x',y,y':Point. (self."op" x y # self."op" x' y ⇒ (x # x' ∨ y # y'))
"invsep":∀x,y:Point. (self."inv" x # self."inv" y ⇒ x # y)
Definitions occuring in Statement :
ss-eq: x ≡ y,
ss-sep: x # y,
ss-point: Point,
separation-space: SeparationSpace,
all: ∀x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
token: "$token",
record-select: r.x,
record+: record+
Definitions occuring in definition :
ss-sep: x # y,
token: "$token",
record-select: r.x,
apply: f a,
implies: P ⇒ Q,
ss-point: Point,
all: ∀x:A. B[x],
or: P ∨ Q,
ss-eq: x ≡ y,
and: P ∧ Q,
function: x:A ⟶ B[x],
set: {x:A| B[x]} ,
separation-space: SeparationSpace,
record+: record+
FDL editor aliases :
s-group
Latex:
s-Group ==
SeparationSpace
"id":Point
"inv":Point {}\mrightarrow{} Point
"op":\{f:Point {}\mrightarrow{} Point {}\mrightarrow{} Point|
(\mforall{}x,y,z:Point. f x (f y z) \mequiv{} f (f x y) z)
\mwedge{} (\mforall{}x:Point. f x self."id" \mequiv{} x)
\mwedge{} (\mforall{}x:Point. f x (self."inv" x) \mequiv{} self."id")\}
"opsep":\mforall{}x,x',y,y':Point. (self."op" x y \# self."op" x' y {}\mRightarrow{} (x \# x' \mvee{} y \# y'))
"invsep":\mforall{}x,y:Point. (self."inv" x \# self."inv" y {}\mRightarrow{} x \# y)
Date html generated:
2016_11_08-AM-09_11_20
Last ObjectModification:
2016_11_02-PM-05_05_31
Theory : inner!product!spaces
Home
Index