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 == {sg:s-GroupStructure| s-group-axioms(sg)}

Definitions occuring in Statement : s-group-axioms: s-group-axioms(sg), s-group-structure: s-GroupStructure, set: {x:A| B[x]}
Definitions occuring in definition : set: {x:A| B[x]} , s-group-structure: s-GroupStructure, s-group-axioms: s-group-axioms(sg)
FDL editor aliases : s-group

Latex:
s-Group == \{sg:s-GroupStructure| s-group-axioms(sg)\} Date html generated: 2017_10_02-PM-03_24_43 Last ObjectModification: 2017_06_23-AM-11_20_47 Theory : constructive!algebra Home Index