forked from metamath/set.mm
-
Notifications
You must be signed in to change notification settings - Fork 0
/
mmtopstr.html
198 lines (169 loc) · 8.04 KB
/
mmtopstr.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"
"http://www.w3.org/TR/html4/loose.dtd">
<HTML LANG="EN-US">
<HEAD>
<!-- improve mobile display -->
<META NAME="viewport" CONTENT="width=device-width, initial-scale=1.0">
<META HTTP-EQUIV="Content-Type"
CONTENT="text/html; charset=iso-8859-1">
<TITLE>Algebraic and Topological Structures - Metamath Proof Explorer</TITLE>
<LINK REL="shortcut icon" HREF="favicon.ico" TYPE="image/x-icon">
<STYLE TYPE="text/css">
<!--
/* Math symbol image will be shifted down 4 pixels to align with normal
text for compatibility with various browsers. The old ALIGN=TOP for
math symbol images did not align in all browsers and should be deleted.
All other images must override this shift with STYLE="margin-bottom:0px".
(2-Oct-2015 nm) */
img { margin-bottom: -4px }
-->
</STYLE>
</HEAD>
<BODY BGCOLOR="#FFFFFF" STYLE="padding: 0px 8px">
<TABLE BORDER=0 CELLSPACING=0 CELLPADDING=0 WIDTH="100%">
<TR>
<TD ALIGN=LEFT VALIGN=TOP><A HREF="mmset.html"><IMG SRC="mm.gif"
BORDER=0
ALT="Metamath Proof Explorer Home"
TITLE="Metamath Proof Explorer Home"
HEIGHT=32 WIDTH=32 ALIGN=TOP STYLE="margin-bottom:0px"></A>
</TD>
<TD ALIGN=CENTER VALIGN=TOP><FONT SIZE="+3"
COLOR="#006633"><B>Metamath Proof Explorer</B></FONT><BR>
<FONT SIZE="+2" COLOR="#006633"><B>Algebraic and Topological Structures</B>
</FONT>
</TD>
<TD NOWRAP ALIGN=RIGHT VALIGN=TOP>
</TD>
</TR>
<TR>
<TD COLSPAN=3 ALIGN=LEFT VALIGN=TOP><FONT SIZE=-2
FACE=sans-serif>
<A HREF="../mm.html">Mirrors</A> >
<A HREF="../index.html">Home</A> >
<A HREF="mmset.html">MPE Home</A> >
Algebraic and Topological Structures
</FONT>
</TD>
</TR>
</TABLE>
<!--
<CENTER><FONT SIZE="+2" COLOR="#006633"><B>ZFC Axioms Without Distinct
Variable Conditions</B></FONT></CENTER>
-->
<HR NOSHADE SIZE=1>
<B><FONT COLOR="#006633">Contents of this
page</FONT></B>
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).
<P><B><FONT COLOR="#006633">Extensible structure
builders</FONT></B>
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.
<P><B><FONT COLOR="#006633">Notes</FONT></B>
In the following figures, set.mm's tokens are written in <CODE>fixed width</CODE>, followed by the mathematical name in <I>italics</I>.
Extensible structures are represented as rectangles, and classes of objects as circles. The same background
color is used for classes of the same family.
<UL>
<LI>Bold arrows represent inclusion relationships.
That is, if <TT>PreHil</TT> has a bold arrow pointing
to <TT>LVec</TT>, then <TT>PreHil</TT> is a subset of <TT>LVec</TT>.
In set.mm, this is written as:
<TT>|- ( W e. PreHil -> W e. LVec )</TT>.
(See <A HREF="phllvec.html">phllvec</A>.)</LI>
<LI>Blue arrows with names represent way to derive one object from another. For example:
<P><CENTER><IMG BORDER=0 STYLE="margin:10px" SRC="_relexample.svg" ALT="Legend/Example"></CENTER>
means that one can derive a topological space (in <TT>Top</TT>)
from a topological base (in <TT>TopBases</TT>) using <TT>topGen</TT>.
In set.mm, this is written as:
<pre>|- ( B e. TopBases -> ( topGen ` B ) e. Top )</pre>
(See <A HREF="tgcl.html">~tgcl</A>.)</LI>
</UL>
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.
<P>Dotted line arrows show how some additional relations and the theorems that provide them.
<P><B><FONT COLOR="#006633">Algebraic hierarchy</FONT></B> The following picture attempts to show the relationships between the main algebraic objects formalized in set.mm:
<!-- Note - To edit or update the figure, please use "https://www.draw.io/". You can load the SVG file directly there. -->
<P> <A NAME="figure2"></A>
<TABLE ALIGN=CENTER><TR><TD>
<IMG BORDER=0 SRC="_alghierarchy.svg"
WIDTH="100%"
ALT="Relationships between algebraic structures. Credit: T. Arnoux
2018. Public domain."
TITLE="Relationships between algebraic structures.
Credit: T. Arnoux 2018. Public domain."
ALIGN=RIGHT STYLE="margin-bottom:0px">
</TD></TR>
<TR><TD ALIGN=CENTER><FONT SIZE="-1"><B>Figure 2.</B> Algebraic hierarchy in set.mm.</FONT>
</TABLE>
<P>There is currently no structure in set.mm representing a magma, but this does not seem to be an issue.
<P>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.
<P><B><FONT COLOR="#006633">Topological
hierarchy</FONT></B> The following picture attempts to show the relationships between the main topological objects formalized in set.mm:
<!-- Note - To edit or update the figure, please use "https://www.draw.io/". You can load the SVG file directly there. -->
<P> <A NAME="figure3"></A>
<TABLE ALIGN=CENTER><TR><TD>
<IMG BORDER=0 SRC="_tophierarchy.svg"
WIDTH="100%"
ALT="Relationships between topological structures. Credit: T. Arnoux
2018. Public domain."
TITLE="Relationships between topological structures.
Credit: T. Arnoux 2018. Public domain."
ALIGN=RIGHT STYLE="margin-bottom:0px">
</TD></TR>
<TR><TD ALIGN=CENTER><FONT SIZE="-1"><B>Figure 3.</B> Topological hierarchy in set.mm.</FONT>
</TABLE>
<P><B><FONT COLOR="#006633">Algebraic-topological
hierarchy</FONT></B> The following picture attempts to show the relationships between the main structures formalized in set.mm with both algebraic and topological properties:
<!-- Note - To edit or update the figure, please use "https://www.draw.io/". You can load the SVG file directly there. -->
<P> <A NAME="figure4"></A>
<TABLE ALIGN=CENTER WIDTH="90%"><TR><TD>
<OBJECT DATA="_algtophierarchy.svg" TYPE="image/svg+xml" WIDTH="100%"
ALT="Relationships between topological structures. Credit: T. Arnoux
2018. Public domain.">
<P>Your browser does not support SVG - please upgrade to a modern browser.</P>
</OBJECT>
</TD></TR>
<TR><TD ALIGN=CENTER><FONT SIZE="-1"><B>Figure 4.</B> Algebraic-topological hierarchy in set.mm.</FONT>
</TABLE>
<HR NOSHADE SIZE=1>
<TABLE BORDER=0 WIDTH="100%"><TR>
<TD ALIGN=left VALIGN=TOP WIDTH="25%"><FONT SIZE=-2 FACE=sans-serif>
</FONT></TD>
<TD NOWRAP ALIGN=CENTER><I>This page was last updated on 7-Dec-2018.</I>
<BR><FONT SIZE=-2 FACE=ARIAL>
Copyright terms:
<A HREF="../copyright.html#pd">Public domain</A>
</FONT></TD>
<TD ALIGN=RIGHT VALIGN=BOTTOM WIDTH="25%">
<FONT FACE="ARIAL" SIZE=-2>
<A
HREF="http://validator.w3.org/check?uri=referer">W3C HTML validation</A>
[external]
</FONT>
</TD>
</TR></TABLE>
<!-- <SCRIPT SRC="http://www.google-analytics.com/urchin.js" TYPE="text/javascript">
</SCRIPT>
<SCRIPT TYPE="text/javascript">
_uacct = "UA-1862729-1";
urchinTracker();
</SCRIPT>
-->
</BODY></HTML>