Przemebra/praca-magisterska/wykonanie.tex

\chapter{Wykonanie} \label{chap:wykonanie}
W rozdziale zostały opisane twierdzenia sformalizowane w trakcie tworzenia pracy magisterskiej. Do części struktur przytoczony jest kod źródłowy je definiujący; kod źródłowy opisujący twierdzenia (ciekawszy niż definicja struktur) nie jest przytaczany ze względu na rozmiar, w tekście znajdują się odnośniki do modułów Agdowych zawierających implementację.
Kod źródłowy znajduje się na serwerze \href{http://student.agh.edu.pl/~wkarpiel/praca-magisterska/przemebra.git}{student.agh.edu.pl}, jest dostępny po HTTP\footnote{Starsza wersja, ''\href{https://git-scm.com/book/en/v2/Git-on-the-Server-The-Protocols}{Dumb HTTP}``}
\begin{verbatim}
git clone http://student.agh.edu.pl/~wkarpiel/praca-magisterska/przemebra.git
\end{verbatim}
Ze względu na wygodę czytelnika przeglądalna kopia repozytorium znajduje się też na \href{https://notabug.org/WojciechKarpiel/Przemebra/}{serwerach poza-uczelnianych}.

\section{Pod-struktury} \label{sec:pod-struktury}
W matematyce konstruktywistycznej podzbiory modeluje się jako predykaty na zbiorze \cite[strona 7]{algebra}.
Standardowa biblioteka Agdy oferuje opis półgrup, monoidów i grup, ale nie oferuje pod-struktur (podzbiorów, podgrup itp.).
Zbiór jest modelowany przez standardową bibliotekę jako typ. W teorii typów {\PerMartinLofDopelniacz} nie istnieje pojęcie pod-typu. Podzbiór modeluję predykatem na typie. Predykaty są częscią biblioteki standardowej Agdy \footnote{moduł biblioteki standardowej \inlinecode{Relation.Unary}}.
Pozwalam, aby przeciwdziedzina predykatu należała do dowolnego wszechświata, a zatem w ogólności nie można nawet stwierdzić rozstrzygalności predykatu (to zwiększa ogólność rozwiązania). Definicje pod-struktur znajdując się w module \inlinecode{Substructures}.
\subsection{Podmonoidy}
Monoid \(A, \approx, \cdot , \epsilon\) wraz z predykatem nad $A$ -- $I$ musi spełniać następujące warunki:
\begin{itemize}
\item działanie musi być zamknięte względem predykatu: \( \forall x,y \in I: (x \cdot y) \in I\),
\item predykat musi szanować relację równoważności: \( \forall x, y \in A : x \approx y \land x \in I \implies y \in I\),
\item element neutralny musi należeć do podzbioru: \( \epsilon \in I\).
\end{itemize}
\input{agda-tex/SubMonoid}

\subsection{Podgrupy}
Podgrupa musi być podmonoidem, a oprócz tego predykat musi być zamknięty ze względu na operację odwracania: \(\forall x \in I : x ^{-1} \in I \). Podgrupa grupy abelowej musi być podgrupą, przemienność działania nie wymusza dodatkowego warunku.
\input{agda-tex/SubGroup}

\subsubsection{Podgrupa normalna} \label{subsec:normal-subgroup}
\(H = (A,\approx,\cdot, \epsilon, ^{-1}, I) \) jest podgrupą normalną grupy \((A,\approx,\cdot, \epsilon, ^{-1}, I)\) jeśli:
\[ \forall a, x \in A : x \in I \implies (a \cdot x \cdot a^{-1}) \in I\]
Normalność podgrupy jest słabszą wersją przemienności. Każda podgrupa przemienna jest normalna (ten lemat jest zaimplementowany obok definicji podgrupy normalnej, w module \inlinecode{Substructures}).
Implementacja pozwala nałożyć dodatkowy warunek na \inlinecode{A} (\inlinecode{normalInWhat}), co będzie wykorzystane w twierdzeniu \ref{thm:II-1-2}.
\input{agda-tex/IsNormalIn}

\section{Jądro homomorfizmu}
Jądro jest zdefiniowane w module \inlinecode{Kern} jako predykat:
\input{agda-tex/Kern.tex}
\begin{theorem} \label{thm:kern-subgroup}
  Jeśli $f$ jest homomorfizmem (\ref{subsec:homomorfizmy}) z $G = (A,\approx, \cdot, ^{-1})$ do $H$  to \((A,\approx, \cdot, ^{-1}, \ker(f) ) \) jest podgrupą $G$.
\end{theorem}
\input{agda-tex/Kern-induces-subgroup}
Kolejne twierdzenie na temat homomorfizmów to \ref{thm:II-1-1}.

\section{Grupa ilorazowa} \label{sec:grupa-ilorazowa}
Każda podgrupa normalna $H$ grupy $G$ jest jądrem homomorfizmu % wyznacznonemu w następujący sposób \cite[strona 38]{algebra}:
powiązanego z grupą ilorazową \(G/H\) \cite[strona 38]{algebra}:

\subsection{Relacja ilorazowa} \label{subsec:relacja-ilorazowa}
Jeśli \( H = (A,\approx,\cdot, \epsilon, ^{-1}, I) \) jest podgrupą $G$ to definiuje się relację ilorazową G względem H ($\approx_I$) jako:
\[ \forall a,b \in A : a \approx_I b \iff a \cdot b^{-1} \in I \]
\input{agda-tex/QuotientRelation}
Taka relacja jest relacją równoważności (\ref{subsec:equivalence-relation}), co jest zaimplemntowane jako część dowodu \ref{thm:quotient-group-is--a-group}.

\begin{theorem} \label{thm:quotient-group-is--a-group}
Struktura $G/H = (A, \approx_I, \cdot, \epsilon , ^{-1})$ (G z podmienioną relacją równoważności) jest grupą.
\end{theorem}
Dowód twierdzenia jest w module \inlinecode{QuotientRelation}

\subsection{Izomorfizm}
%twierdzenie II.1.1,
Twierdzenie zawarte w \cite[strona 38]{algebra}:
\begin{theorem} \label{thm:II-1-1}
Niech $G = (A_G, \approx, \cdot, \epsilon_G , ^{-1_G})$ i $L = (A_L, \approx, \cdot, \epsilon_L , ^{-1_L})$ będą grupami. Niech $N = (A_G, \approx, \cdot, \epsilon_G , ^{-1_G}, I)$ będzie normalną podgrupą $G$. Niech $f$ będzie homomorfizmem z $G$ do $L$ oraz niech \(\forall x \in I : f(x) \approx_L \epsilon_L\). Wtedy $f$ jest homomorfizmem z $G/H$ do $L$. Jeżeli $f$ jest surjekcją i $kef(f) = I$ to $f$ jest izomorfizmem z $G/H$ do $L$.
\end{theorem}
Dowód twierdzenia jest w module \inlinecode{II-1-1}.


\subsection{Dodatkowe własności} \label{subsec:II-1-2}
Twierdzenie zawarte w \cite[strona 39]{algebra}:
\begin{theorem} \label{thm:II-1-2}
  Niech $H =(A, \approx, \cdot, \epsilon, ^{-1}, I_H)$ będzie podgrupą grupy $G = (A, \approx, \cdot, \epsilon, ^{-1}) $. Niech $K=(A, \approx, \cdot, \epsilon, ^{-1},I_K)$ będzie normalną podgrupą grupy $G$. Wtedy: \begin{enumerate}
  \item \( HK = (A, \approx, \cdot, \epsilon, ^{-1}, \{h \cdot k : h \in I_H, k \in I_K \}) \) jest podgrupą $G$,
  \item  \(H \cap K = (A, \approx, \cdot, \epsilon, ^{-1}  , I_H \cap I_K)\) jest normalną podgrupą w $H$.
    % tu był trzeci punkt ale on chyba był błędny
  \end{enumerate}
\end{theorem}
Dowód twierdzenia jest w module \inlinecode{II-1-2}

\section{Warstwy}
Niech $H =(A, \approx, \cdot, \epsilon, ^{-1}, I_H)$ będzie podgrupą grupy $G$, oraz niech $a \in A$ wtedy: \begin{itemize}
\item \(aH  = \{ a \cdot h | h \in I_H  \}  \quad \text{ -- lewostronna warstwa $G$ względem $H$ wyznaczona przez $a$}\),
\item \(Ha  = \{ h \cdot a | h \in I_H  \}  \quad \text{ -- prawostronna warstwa $G$ względem $H$ wyznaczona przez $a$}\),
\item jeśli \(aH = Ha\) wtedy mówi się o warstwie obustronnej.
\end{itemize}

\begin{theorem} \label{thm:cosets-norm-eq}
  Niech $H =(A, \approx, \cdot, \epsilon, ^{-1}, I_H)$ będzie normalną (\ref{subsec:normal-subgroup}) podgrupą grupy $G = (A, \approx, \cdot, \epsilon, ^{-1}) $. Wtedy
  \[ \forall a \in A : aH = Ha \]
\end{theorem}
Założenie twierdzenia zapisane w Agdzie jest poniżej. Pełny dowód znaduje się w module \inlinecode{Coset}.
\input{agda-tex/CosetLRnorm}

\section{Ideały}
Niech \( R = \left(A,\approx,+,\cdot,0,1,- \right)\) będzie pierścieniem (\ref{subsubsection:ring-field}).
Podgrupa addytywna \(I = \left(A,\approx,+,0,-,I_I \right)\) pierścienia $R$ jest ideałem jeśli:
\[ \forall x \in I_I, r \in R : r \cdot x \in I_I \land x \cdot r \in I_I \]
\input{agda-tex/IdealProp}

W module \inlinecode{Ideal} znajduje się pełna definicja struktury:
\input{agda-tex/IsIdeal}
\subsection{Homomorfizm wyznacza ideał}
\begin{theorem} \label{thm:hom-induces-ideal}
  Niech $f$ będzie homomorfizmem między pierścieniami \(R_1 = \left(A_1,\approx_1, +_1, \cdot_1, 0_1, 1_1, -_1 \right)\) i \(R_2\). Wtedy
  \[ I = \left(A_1,\approx_1, +_1, \cdot_1, 0_1, 1_1, -_1, \ker(f)) \right) \]
  jest ideałem pierścienia $R_1$.
\end{theorem}
Założenie twierdzenia zapisana w Agdzie jest poniżej. Pełny dowód znajduje się w module \inlinecode{Ideal}.
\input{agda-tex/IdealKern}

\subsection{Struktura ilorazowa pierścienia względem ideału jest pierścieniem}
Jeśli \( I = (A,\approx,+,\cdot,0,1,-, I_I)\) jest ideałem pierścienia $R$,
$R_+ = (A,\approx,+,0,-)$ jest addytywną grupą pierścienia $R$,
\(I_+ = (A,\approx,+,0,-,I_I) \) jest podgrupą addytywną ideału.
to przez $R/I$ oznacza się strukturę \(R/I = (A,\approx_I,+,0,-,I_I) \),
gdzie $\approx_I$ jest relacją ilorazową $R_+$ względem $I_+$ (\ref{subsec:relacja-ilorazowa}).

Twierdzenie zawarte w \cite[strona 43]{algebra}:
\begin{theorem} \label{thm:quotient-ring-is-a-ring}
Niech \(I\) będzie ideałem pierścienia $R$. $R/I$ jest pierścieniem.
\end{theorem}
Dowód twierdzenia znajduje się w module \inlinecode{Ideal}.

\subsection{Ideały a homomorfizmy}
Poniżej znajduje się uogólnienie twierdzenia \ref{thm:II-1-1} z grup na pierścienie \cite[twierdzenie 2.1, strona 44]{algebra}
\begin{theorem} \label{thm:II-2-1}  % DOZRO: to jest połowa twierdzenia
  Niech \( R = (A_{R},\approx_{R},+_{R},\cdot_{R},0_{R},1_{R},-_{R})\) oraz \(S = (A_{S},\approx_{S},+_{S},\cdot_{S},0_{S},1_{S},-_{S})\) będą pierścieniami.
  Niech \( I = (A_{R},\approx_{R},+_{R},\cdot_{R},0_{R},1_{R},-_{R}, I_I) \) będzie ideałem pierścienia $R$.
  Niech $f$ będzie homomorfizmem z $R$ do $S$ oraz niech \(\forall x \in I_I : f(x) \approx_{S} 0_{S} \).
  Wtedy f jest homomorfizmem z $R/I$ to $S$.
\end{theorem}
Dowód twierdzenia znajdue się w module \inlinecode{II-2-1}

\section{Idempotentny pierścień} \label{sec:impotent-ring}
Pierścień \(R = \left(A,\approx,+,\cdot,0,1,-\right) \) jest idempotentny jeśli:
\begin {itemize}
\item      nie ma nilpotentnych elementów: \( \forall a \in A : a \cdot a \approx 0 \implies a \approx 0 \),
\item      każdy jego element idempotentny to 0 lub 1: \(\forall a \in A : a \cdot a \approx a \implies a \approx 0 \lor a \approx 1  \).
\end{itemize}
Lemat zawarty w \cite[strona 141]{algebra}:
\begin{theorem} \label{thm:impotent-lemma}
  Niech $a$ i $b$ będą elementami idempotentnego pierścienia \(R = \left(A,\approx,+,\cdot,0,1,-\right) \), takimi że:
  \( \left( a + b \approx 1 \land a \cdot b \approx 0 \right) \).
  Wtedy zachodzi:
  \[ \left( a \approx 0 \land b \approx 1 \right) \lor \left( a \approx 1 \land b \approx 0 \right)\]
\end{theorem}

Dowód twierdzenia znajduje się w module \inlinecode{Lemma-VI-1-7}.

\section{Wielomiany} \label{sec:wielomiany}
Twierdzenia teorii ciał dotyczą w większości wielomianów nad pierścieniami. W dalszej części rozdziału będzą rozważane wielomiany jednej zmiennej.
Wielomian zmiennej $X \in A$ nad pierścieniem $R = (A,\approx, +, \cdot, 0, 1, -)$ to skończona suma
\[ R[X] \equiv \sum^{n}_{i=0} r_i \cdot X^i \]
gdzie $r \in A$ oraz $n \in \nat$.

Jeśli wielomian $R[X]$ da się zapisać jako $\sum^{n}_{i=0} r_i \cdot X^i$ oraz $r_n \not\approx 0$ wtedy wielomian $R[X]$ ma stopień $n$.
\subsection{Wielomian unormowany}
Jeśli wielomian $R[X]$ nad pierścieniem $R = (A, \approx, +, \cdot, 0, 1,-)$ jest stopnia $n$ i $r_n \approx 1$ to wtedy wielomian $R[X]$ jest unormowany. Unormowane wielomiany jednej zmiennej nad pierścieniem $R$ tworzą monoid, w którym działaniem jest mnożenie wielomianów (bo $1 \cdot 1 \approx 1$ przy mnożeniu wartości przy najwyższych współczynnikach), a elementem neutralnym jest wielomian stały: $C[X] = 1$.
\subsection{Ograniczenia implementacyjne} \label{subsec:ograniczenia-implementacyjne}
Od implementacji wielomianu wymaga się przede wszystkim możliwości określenia stopnia wielomianu, w tym stopnia dodanych lub wymnożonych wielomianów. To może być zrealizowane przez zawarcie stopnia w typie wielomianu, lub dobrze\footnote{``dobrze'' jest nie precyzyjnie zdefiniowane, bo ciężko jest liczbowo opisać reprezentację z którą łatwo się pracuje} normalizującą się funkcję obliczającą stopień. Kolejne wymaganie to możliwość określenia czy wielomian jest unormowany.
Poniższe implementacje zakładają, że równoważność elementów pierścienia jest rozstrzygalna (zob. przypis do (\ref{sec:niekonstruktywnost})), tzn. istnieje funkcja ($\sumtype{}{}$ to oznaczenie typu wspólnotowego (\ref{subsec:wspolnoty})):
\[ d : (x : A) \rightarrow (y : A) \rightarrow  \sumtype{(x \approx y)}{(x \not\approx y)}  \]
Jest to konieczne dla m.in obliczania stopnia wielomianu (aby sprawdzić czy wiodący element wielomianu jest różny od zera).
\subsection{Implementacja biblioteki standardowej}
Biblioteka standardowa (moduł \inlinecode{Algebra.Solver.Ring}) definiuje wielomian jako algebraiczną strukturę danych: 
\input{agda-tex/StdPoly}
\inlinecode{Op} to dodawanie lub mnożenie. Implementacja jest ogólna, pozwala na wielomiany wielu zmiennych (konstruktor \inlinecode{var} wybiera zmienną). Wielomian jednej zmiennej może być znormalizowany do postaci normalnej Hornera. Ta implementacja nie ma zaszytego w typie stopnia wielomianu, natomiast łatwo można napisać funkcję. Ta funkcja w przypadku obliczanie stopnia sumy wielomianów musiała by orzec, że stopień sumy jest co najwyżej\footnote{Bo może też spaść, np dla $P(x) = 2x^2$, $Q(x) = -2x^2$} równy większemu ze stopni składników. Obliczanie maksimum źle się normalizuje (wymaga wprowadzania i rozpatrywania przypadków gdy $x \le y$ i $x > y$).
Stąd ta reprezentacja jest kiepsko używalna w praktyce. 
Możliwą zmianą byłoby wprowadzenie do konstruktorów nowego argumentu, który gwarantuje że elementem wiodącym nie będzie zero, lecz to nie rozwiązuje problemu z normalizacją.
\subsection{Wektor współczynników}
W mojej implementacji (moduł \inlinecode{UnivariatePolynomial}) wielomian jest reprezentowany jako wektor współczynników.
Wymaga się, żeby pierwszym elementem wektora nie było zero, dzięki temu stopień wielomianu da się odczytać z typu.
Natomiast to sprawia że typy funkcji dodającej i mnożączej\footnote{Pomnożenie przez siebie dwóch elementów pierścienia może dawać 0. Na przykład  w pierścieniu liczb całkowitych modulo 4 zachodzi:  $2 \cdot 2 = 0$} wielomiany wyglądają w taki sposób  (nie przytaczam kodu źródłowego ze względu na jego objętość):
\[ \cdot : (w_1 : Wielomian \; n) \rightarrow (w_2 : Wielomian \; m) \rightarrow \deppair{q : \nat}{ \left( (q \le n + m ) \times Wielomian \; q \right)}\]
Ta definicja również jest niewygodna w użyciu, a stopień kiepsko się normalizuje, nie udało mi się udowodnić że: $R[X] \cdot 1 \approx R[X]$

\subsection{Inne możliowści i dalsza praca} \label{subsec:dalsza-praca}
UniMath \cite{UniMath} używa wielomianów zbudowanych podobnie jak te z biblioteki standardowej Agdy (postać normalna Hornera; \inlinecode{Ring\_polynom.v}):
\begin{verbatim}
 Inductive Pol : Type :=
  | Pc : C -> Pol
  | Pinj : positive -> Pol -> Pol
  | PX : Pol -> positive -> Pol -> Pol.
\end{verbatim}
Unimath definiuje uproszczoną wersję dla wielomianów jednej zmiennej, jednakże również nie próbuje wyznaczać stopni wielomianów. Nie znalazłem artykułów naukowych na temat komputerowej reprezentacji wielomianów pozwalającej wnioskować na temat stopnia wielomianu, wydaje się że jest to problem otwarty.