diff options
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | latex/naproche.sty | 3 | ||||
| -rw-r--r-- | latex/stdlib.tex | 3 | ||||
| -rw-r--r-- | library/algebra/group.tex | 83 | ||||
| -rw-r--r-- | library/algebra/monoid.tex | 19 | ||||
| -rw-r--r-- | library/everything.tex | 3 | ||||
| -rw-r--r-- | library/nat.tex | 45 | ||||
| -rw-r--r-- | library/numbers.tex | 140 | ||||
| -rw-r--r-- | library/order/order.tex | 1 | ||||
| -rw-r--r-- | library/topology/order-topology.tex | 7 |
10 files changed, 302 insertions, 3 deletions
@@ -41,3 +41,4 @@ premseldump/ haddocks/ stack.yaml.lock zf*.svg +Anmerkungen.txt diff --git a/latex/naproche.sty b/latex/naproche.sty index 9764693..cb65fe7 100644 --- a/latex/naproche.sty +++ b/latex/naproche.sty @@ -127,6 +127,9 @@ \newcommand{\Univ}[1]{\fun{Univ}(#1)} \newcommand{\upward}[2]{#2^{\uparrow #1}} \newcommand{\LeftOrb}[2]{#2\cdot #1} +\newcommand{\integers}{\mathcal{Z}} +\newcommand{\zero}{0} +\newcommand{\one}{1} \newcommand\restrl[2]{{% we make the whole thing an ordinary symbol diff --git a/latex/stdlib.tex b/latex/stdlib.tex index 3673801..dba42a2 100644 --- a/latex/stdlib.tex +++ b/latex/stdlib.tex @@ -36,6 +36,8 @@ \input{../library/cardinal.tex} \input{../library/algebra/magma.tex} \input{../library/algebra/semigroup.tex} + \input{../library/algebra/monoid.tex} + \input{../library/algebra/group.tex} %\input{../library/algebra/quasigroup.tex} %\input{../library/algebra/loop.tex} \input{../library/order/order.tex} @@ -43,4 +45,5 @@ \input{../library/topology/topological-space.tex} \input{../library/topology/basis.tex} \input{../library/topology/disconnection.tex} + \input{../library/numbers.tex} \end{document} diff --git a/library/algebra/group.tex b/library/algebra/group.tex index 48934bd..a79bd2f 100644 --- a/library/algebra/group.tex +++ b/library/algebra/group.tex @@ -1 +1,82 @@ -\section{Groups} +\import{algebra/monoid.tex} +\section{Group} + +\begin{struct}\label{group} + A group $G$ is a monoid such that + \begin{enumerate} + \item\label{group_inverse} for all $g \in \carrier[G]$ there exist $h \in \carrier[G]$ such that $\mul[G](g, h) =\neutral[G]$. + \end{enumerate} +\end{struct} + +\begin{corollary}\label{group_implies_monoid} + Let $G$ be a group. Then $G$ is a monoid. +\end{corollary} + +\begin{abbreviation}\label{cfourdot} + $g \cdot h = \mul(g,h)$. +\end{abbreviation} + +\begin{lemma}\label{neutral_is_idempotent} + Let $G$ be a group. $\neutral[G]$ is a idempotent element of $G$. +\end{lemma} + +\begin{lemma}\label{group_divison_right} + Let $G$ be a group. Let $a,b,c \in G$. + Then $a \cdot c = b \cdot c$ iff $a = b$. +\end{lemma} +\begin{proof} + Take $a,b,c \in G$ such that $a \cdot c = b \cdot c$. + There exist $c' \in G$ such that $c \cdot c' = \neutral[G]$. + Therefore $a \cdot c = b \cdot c$ iff $(a \cdot c) \cdot c' = (b \cdot c) \cdot c'$. + \begin{align*} + (a \cdot c) \cdot c' + &= a \cdot (c \cdot c') + \explanation{by \cref{semigroup_assoc,group_implies_monoid,monoid_implies_semigroup}}\\ + &= a \cdot \neutral[G] + \explanation{by \cref{group_inverse}}\\ + &= a + \explanation{by \cref{group_implies_monoid,monoid_right}} + \end{align*} + \begin{align*} + (b \cdot c) \cdot c' + &= b \cdot (c \cdot c') + \explanation{by \cref{semigroup_assoc,group_implies_monoid,monoid_implies_semigroup}}\\ + &= b \cdot \neutral[G] + \explanation{by \cref{group_inverse}}\\ + &= b + \explanation{by \cref{group_implies_monoid,monoid_right}} + \end{align*} + $(a \cdot c) \cdot c' = (b \cdot c) \cdot c'$ iff $a \cdot c = b \cdot c$ by assumption. + $a = b$ iff $a \cdot c = b \cdot c$ by assumption. +\end{proof} + + +\begin{proposition}\label{leftinverse_eq_rightinverse} + Let $G$ be a group and assume $a \in G$. + Then there exist $b\in G$ + such that $a \cdot b = \neutral[G]$ and $b \cdot a = \neutral[G]$. +\end{proposition} +\begin{proof} + There exist $b \in G$ such that $a \cdot b = \neutral[G]$. + There exist $c \in G$ such that $b \cdot c = \neutral[G]$. + $a \cdot b = \neutral[G]$. + $(a \cdot b) \cdot c = (\neutral[G]) \cdot c$. + $(a \cdot b) \cdot c = a \cdot (b \cdot c)$. + $a \cdot \neutral[G] = \neutral[G] \cdot c$. + $c = c \cdot \neutral[G]$. + $c = \neutral[G] \cdot c$. + $a \cdot \neutral[G] = c \cdot \neutral[G]$. + $a \cdot \neutral[G] = c$ by \cref{monoid_right,group_divison_right}. + $a = c$ by \cref{monoid_right,group_divison_right,neutral_is_idempotent}. + $b \cdot a = b \cdot c$. + $b \cdot a = \neutral[G]$. +\end{proof} + +\begin{definition}\label{group_abelian} + $G$ is an abelian group iff $G$ is a group and for all $g,h \in G$ $\mul[G](g,h) = \mul[G](h,g)$. +\end{definition} + + +\begin{definition}\label{group_automorphism} + Let $f$ be a function. $f$ is a group-automorphism iff $G$ is a group and $\dom{f}=G$ and $\ran{f}=G$. +\end{definition} diff --git a/library/algebra/monoid.tex b/library/algebra/monoid.tex new file mode 100644 index 0000000..06fcb50 --- /dev/null +++ b/library/algebra/monoid.tex @@ -0,0 +1,19 @@ +\import{algebra/semigroup.tex} +\section{Monoid} + +\begin{struct}\label{monoid} + A monoid $A$ is a semigroup equipped with + \begin{enumerate} + \item $\neutral$ + \end{enumerate} + such that + \begin{enumerate} + \item\label{monoid_type} $\neutral[A]\in \carrier[A]$. + \item\label{monoid_right} for all $a\in \carrier[A]$ we have $\mul[A](a,\neutral[A]) = a$. + \item\label{monoid_left} for all $a\in \carrier[A]$ we have $\mul[A](\neutral[A], a) = a$. + \end{enumerate} +\end{struct} + +\begin{corollary}\label{monoid_implies_semigroup} + Let $A$ be a monoid. Then $A$ is a semigroup. +\end{corollary}
\ No newline at end of file diff --git a/library/everything.tex b/library/everything.tex index 9b85f83..61bccb2 100644 --- a/library/everything.tex +++ b/library/everything.tex @@ -20,12 +20,15 @@ \import{cardinal.tex} \import{algebra/magma.tex} \import{algebra/semigroup.tex} +\import{algebra/monoid.tex} +\import{algebra/group.tex} \import{order/order.tex} %\import{order/semilattice.tex} \import{topology/topological-space.tex} \import{topology/basis.tex} \import{topology/disconnection.tex} \import{topology/separation.tex} +\import{numbers.tex} \begin{proposition}\label{trivial} $x = x$. diff --git a/library/nat.tex b/library/nat.tex index 529ba54..ac9a141 100644 --- a/library/nat.tex +++ b/library/nat.tex @@ -1,5 +1,5 @@ \import{set/suc.tex} - +\import{set.tex} \section{Natural numbers} @@ -17,5 +17,46 @@ \end{axiom} \begin{abbreviation}\label{naturalnumber} - $n$ is a natural number iff $n\in\naturals$. + $n$ is a natural number iff $n\in \naturals$. +\end{abbreviation} + +\begin{lemma}\label{emptyset_in_naturals} + $\emptyset\in\naturals$. +\end{lemma} + +\begin{signature}\label{addition_is_set} + $x+y$ is a set. +\end{signature} + +\begin{axiom}\label{addition_on_naturals} + $x+y$ is a natural number iff $x$ is a natural number and $y$ is a natural number. +\end{axiom} + +\begin{abbreviation}\label{zero_is_emptyset} + $\zero = \emptyset$. \end{abbreviation} + +\begin{axiom}\label{addition_axiom_1} + For all $x \in \naturals$ $x + \zero = \zero + x = x$. +\end{axiom} + +\begin{axiom}\label{addition_axiom_2} + For all $x, y \in \naturals$ $x + \suc{y} = \suc{x} + y = \suc{x+y}$. +\end{axiom} + +\begin{lemma}\label{naturals_is_equal_to_two_times_naturals} + $\{x+y \mid x \in \naturals, y \in \naturals \} = \naturals$. +\end{lemma} + + + + + + + + + + + + + diff --git a/library/numbers.tex b/library/numbers.tex new file mode 100644 index 0000000..93623fa --- /dev/null +++ b/library/numbers.tex @@ -0,0 +1,140 @@ +\import{nat.tex} +\import{order/order.tex} +\import{relation.tex} + +\section{The real numbers} + +\begin{signature} + $\reals$ is a set. +\end{signature} + +\begin{signature} + $x + y$ is a set. +\end{signature} + +\begin{signature} + $x \times y$ is a set. +\end{signature} + +\begin{axiom}\label{one_in_reals} + $1 \in \reals$. +\end{axiom} + +\begin{axiom}\label{reals_axiom_order} + $\lt[\reals]$ is an order on $\reals$. + %$\reals$ is an ordered set. +\end{axiom} + +\begin{axiom}\label{reals_axiom_strictorder} + $\lt[\reals]$ is a strict order. +\end{axiom} + +\begin{axiom}\label{reals_axiom_dense} + For all $x,y \in \reals$ if $(x,y)\in \lt[\reals]$ then + there exist $z \in \reals$ such that $(x,z) \in \lt[\reals]$ and $(z,y) \in \lt[\reals]$. + + %For all $X,Y \subseteq \reals$ if for all $x,y$ $x\in X$ and $y \in Y$ such that $x \lt[\reals] y$ + %then there exist a $z \in \reals$ such that if $x \neq z$ and $y \neq z$ $x \lt[\reals] z$ and $z \lt[\reals] y$. +\end{axiom} + +\begin{axiom}\label{reals_axiom_order_def} + $(x,y) \in \lt[\reals]$ iff there exist $z \in \reals$ such that $(\zero, z) \in \lt[\reals]$ and $x + z = y$. +\end{axiom} + +\begin{lemma}\label{reals_one_bigger_than_zero} + $(\zero,1) \in \lt[\reals]$. +\end{lemma} + + +\begin{axiom}\label{reals_axiom_assoc} + For all $x,y,z \in \reals$ $(x + y) + z = x + (y + z)$ and $(x \times y) \times z = x \times (y \times z)$. +\end{axiom} + +\begin{axiom}\label{reals_axiom_kommu} + For all $x,y \in \reals$ $x + y = y + x$ and $x \times y = y \times x$. +\end{axiom} + +\begin{axiom}\label{reals_axiom_zero_in_reals} + $\zero \in \reals$. +\end{axiom} + +%\begin{axiom}\label{reals_axiom_one_in_reals} +% $\one \in \reals$. +%\end{axiom} + +\begin{axiom}\label{reals_axiom_zero} + %There exist $\zero \in \reals$ such that + For all $x \in \reals$ $x + \zero = x$. +\end{axiom} + +\begin{axiom}\label{reals_axiom_one} + %There exist $1 \in \reals$ such that + For all $x \in \reals$ $1 \neq \zero$ and $x \times 1 = x$. +\end{axiom} + +\begin{axiom}\label{reals_axiom_add_invers} + For all $x \in \reals$ there exist $y \in \reals$ such that $x + y = \zero$. +\end{axiom} + +%TODO: Implementing Notion for negativ number such as -x. + +%\begin{abbreviation}\label{reals_notion_minus} +% $y = -x$ iff $x + y = \zero$. +%\end{abbreviation} %This abbrevation result in a killed process. + +\begin{axiom}\label{reals_axiom_mul_invers} + For all $x \in \reals$ there exist $y \in \reals$ such that $x \neq \zero$ and $x \times y = 1$. +\end{axiom} + +\begin{axiom}\label{reals_axiom_disstro1} + For all $x,y,z \in \reals$ $x \times (y + z) = (x \times y) + (x \times z)$. +\end{axiom} + +\begin{proposition}\label{reals_disstro2} + For all $x,y,z \in \reals$ $(y + z) \times x = (y \times x) + (z \times x)$. +\end{proposition} + +\begin{proposition}\label{reals_reducion_on_addition} + For all $x,y,z \in \reals$ if $x + y = x + z$ then $y = z$. +\end{proposition} + +\begin{signature} + $\invers$ is a set. +\begin{signature} + +%TODO: +%x \rless y in einer signatur hinzufügen und dann axiom x+z = y und dann \rlt in def per iff +%\inv{} für inverse benutzen. Per Signatur einfüheren und dann axiomatisch absicher +%\cdot für multiklikation verwenden. +%< für die relation benutzen. + +%\begin{signature} +% $y^{\rightarrow}$ is a function. +%\end{signature} + +%\begin{axiom}\label{notion_multi_invers} +% If $y \in \reals$ then $\invers{y} \in \reals$ and $y \times y^{\rightarrow} = 1$. +%\end{axiom} + +%\begin{abbreviation}\label{notion_fraction} +% $\frac{x}{y} = x \times y^{\rightarrow}$. +%\end{abbreviation} + +\begin{lemma}\label{order_reals_lemma1} + For all $x,y,z \in \reals$ such that $(\zero,x) \in \lt[\reals]$ + if $(y,z) \in \lt[\reals]$ + then $((y \times x), (z \times x)) \in \lt[\reals]$. +\end{lemma} + +\begin{lemma}\label{order_reals_lemma2} + For all $x,y,z \in \reals$ such that $(\zero,x) \in \lt[\reals]$ + if $(y,z) \in \lt[\reals]$ + then $((x \times y), (x \times z)) \in \lt[\reals]$. +\end{lemma} + + +\begin{lemma}\label{order_reals_lemma3} + For all $x,y,z \in \reals$ such that $(x,\zero) \in \lt[\reals]$ + if $(y,z) \in \lt[\reals]$ + then $((x \times z), (x \times y)) \in \lt[\reals]$. +\end{lemma} diff --git a/library/order/order.tex b/library/order/order.tex index 339bad8..1b7692f 100644 --- a/library/order/order.tex +++ b/library/order/order.tex @@ -1,6 +1,7 @@ \import{relation.tex} \import{relation/properties.tex} \import{order/quasiorder.tex} +\section{Order} % also called "(partial) ordering" or "partial order" to contrast with connex (i.e. "total") orders. \begin{abbreviation}\label{order} diff --git a/library/topology/order-topology.tex b/library/topology/order-topology.tex new file mode 100644 index 0000000..afa8755 --- /dev/null +++ b/library/topology/order-topology.tex @@ -0,0 +1,7 @@ +\import{topology/topological-space.tex} + +\section{Order Topology} + +\begin{definition} + A +\end{definition} |