Metamath Proof Explorer Algebraic and Topological Structures |
||
Mirrors > Home > MPE Home > Algebraic and Topological Structures |
Extensible structure builders An "extensible structure" is a function (set of ordered pairs) on a finite (and not necessarily sequential) subset of the natural numbers, used to define a specific group, ring, poset, etc. The function's argument is the index of a structure component (such as 1 for the base set of a group), and its value is the component (such as the base set). A group will have at least two components (base set and operation), although it can be further specialized by adding other components such as a multiplicative operation for rings (and still remain a group per our definition). Thus, every ring is also a group. This allows theorems from more general structures (groups) to be reused for more specialized structures (rings) without having to reprove them.
Notes
In the following figures, set.mm's tokens are written in fixed width
, followed by the mathematical name in italics.
Extensible structures are represented as rectangles, and classes of objects as circles. The same background
color is used for classes of the same family.
|- ( B e. TopBases -> ( topGen ` B ) e. Top )(See ~tgcl.)
Dotted line arrows show how some additional relations and the theorems that provide them.
Algebraic hierarchy The following picture attempts to show the relationships between the main algebraic objects formalized in set.mm:
Figure 2. Algebraic hierarchy in set.mm. |
There is currently no structure in set.mm representing a magma, but this does not seem to be an issue.
The ordered algebraic structures are currently required to be totally ordered sets, while it is usual to require them only to be partially ordered sets. This might need to be changed.
Topological hierarchy The following picture attempts to show the relationships between the main topological objects formalized in set.mm:
Figure 3. Topological hierarchy in set.mm. |
Algebraic-topological hierarchy The following picture attempts to show the relationships between the main structures formalized in set.mm with both algebraic and topological properties:
Figure 4. Algebraic-topological hierarchy in set.mm. |
This page was last updated on 7-Dec-2018.
Copyright terms: Public domain |
W3C HTML validation [external] |