Algebraic and Topological Structures - Metamath Proof Explorer

Contents of this page    On this page we present an algebraic hierarchy (showing the relationships between the main algebraic objects formalized in set.mm) and a topological hierarchy (showing the relationships between the main topological objects formalized in set.mm). For these figures to make sense, we first describe extensible structure builders (since they are widely used) and notes on the figures (especially the notation used in the figures).

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.

• Bold arrows represent inclusion relationships. That is, if PreHil has a bold arrow pointing to LVec, then PreHil is a subset of LVec. In set.mm, this is written as: |- ( W e. PreHil -> W e. LVec ). (See phllvec.)
• Blue arrows with names represent way to derive one object from another. For example:
  means that one can derive a topological space (in Top) from a topological base (in TopBases) using topGen. In set.mm, this is written as:

  |- ( B e. TopBases -> ( topGen ` B ) e. Top )

  (See ~tgcl.)

There are often two ways to extract a component from a structure, either by directly using the component (TopSet, UnifSet), or by restricting it to the base class (TopOpen, UnifSt). Both are listed in the figure, with the direct component in italics, since it is usually less practical.

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.