forked from UniMath/SymmetryBook
-
Notifications
You must be signed in to change notification settings - Fork 0
/
galois.tex
201 lines (179 loc) · 8.5 KB
/
galois.tex
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
\chapter{Galois theory}%
\label{chap:galois-theory}%
%% VERY PRELIMINARY
The goal of Galois theory is to study how the roots of a given polynomial can
be distinguished from one another. Take for example $X^2+1$ as a polynomial
with real coefficients. It has two distincts roots in $\mathbb C$, namely $i$
and $-i$. However, an observer, who is limited to the realm of $\mathbb R$,
can not distinguish between the two. Morally speaking, from the point of view
of this observer, the two roots $i$ and $-i$ are pretty much the same. Formally
speaking, for any polynomial $Q: \mathbb R[X,Y]$, the equation $Q(i,-i) = 0$ is
satisfied if and only if $Q(-i,i) = 0$ also. This property is easily understood
by noticing that there is a automorphism of fields $\sigma: \mathbb C \to
\mathbb C$ such that $\sigma(i) = -i$ and $\sigma(-i) = i$ which also fixes
$\mathbb R$. The goal of this chapter is to provide the rigourous framework in
which this statement holds.
{\color{red} TODO: complete/rewrite the introduction}
\section{Covering spaces and field extensions}
\label{sec:cover-spac-fields}
\def\fieldstype{\mathbf{Fields}}%
\def\Gal{\mathrm{Gal}}%
\def\fieldshom{\hom_{\fieldstype}}%
\def\isHom{\mathrm{isHom}}%
\def\iso{\mathrm{Iso}}%
\newcommand\restr[1]{{{#1}^\ast}}%
\newcommand\fieldsext[1]{#1\backslash\fieldstype}%
Recall that a field extension is simply a morphism of fields $i: k\to K$ from a
field $k$ to a field $K$. Given a fixed field $k$, the type of fields
extensions of $k$ is defined as
\begin{displaymath}
\fieldsext k \defequi \sum_{K:\fieldstype}\fieldshom(k,K)
\end{displaymath}
\begin{definition}
The Galois group of an extension $(K,i)$ of a field $K$, denoted $\Gal(K,i)$
or $\Gal(K/k)$ when $i$ is clear from context, is the group
$\Aut_{\fieldsext k}{(K,i)}$.
\label{def:galois-group}
\end{definition}
\begin{remark}
\label{rem:sip-univalence}
The Structure Identity Principle holds for fields, which means that for
$K,L:\fieldstype$, one has
\begin{displaymath}
(K = L) \weq \iso(K,L)
\end{displaymath}
where $\iso(K,L)$ denotes the type of these equivalences that are
homomorphisms of fields. Indeed, if one uses $K$ and $L$ also for the carrier
types of the fields, one gets:
\begin{displaymath}
\begin{split}
(K = L) \weq \sum_{p:K=_\UU L} (\trp p (+_K) = +_L)
\times (\trp p (\cdot_K) = \cdot_L)
\\ \times (\trp p (0_K) = 0_L)
\times (\trp p (1_K) = 1_L)
\end{split}
\end{displaymath}
Any $p : K =_\UU L$ is the image under univalence of an equivalence $\phi: K \weq L$, and then:
\begin{align*}
\trp p (+_K) &= (x,y) \mapsto \phi( \inv\phi(x) +_K \inv \phi(y)) \\
\trp p (\cdot_K) &= (x,y) \mapsto \phi( \inv\phi(x) \cdot_K \inv \phi(y)) \\
\trp p (0_K) &=\phi( 0_K ) \\
\trp p (1_K) &=\phi( 1_K )
\end{align*}
It follows that:
\begin{displaymath}
\begin{split}
(K=L) \weq \sum_{\phi: K \weq L} (\phi(x +_K y) = \phi (x) +_L \phi (y)) \\
\times (\phi(x\cdot_K y) = \phi (x) \cdot_L \phi (y)) \\
\times (\phi(0_K) = 0_L)
\times (\phi(1_K) = 1_L)
\end{split}
\end{displaymath}
The type on the right hand side is the same as $\iso(K,L)$ by definition.
In particular, given an extension $(K,i)$ of $K$:
\begin{align*}
\US \Gal(K,i) \weq \sum_{p:K=K} \trp p i = i \weq \sum_{\sigma:\iso(K,K)} \sigma \circ i = i
\end{align*}
This is how the Galois group of the extension $(K,i)$ is defined in ordinary mathematics.
\end{remark}
Given an extension $(K,i)$ of field $k$, there is a map of interest:
\begin{displaymath}
\restr i: \fieldsext K \to \fieldsext k,\quad (L,j) \mapsto (L,ji)
\end{displaymath}
\begin{lemma}
The map $\restr i$ is a set-bundle.
\label{lem:field-ext-restriction-set-bundle}
\end{lemma}
\begin{proof}
Given a field extension $(K',i')$ in $\fieldsext k$, one wants to prove that
the fiber over $(K',i')$ is a set. Suppose $(L,j)$ and $(L',j')$ are
extensions of $K$, together with paths $p:(K',i') = (L,ji)$ and $p': (K',i')
= (L',j'i)$. Recall that $p$ and $p'$ are respectively given by equivalences
$\pi: K' = L$ and $\pi': K' = L'$ such that $\pi i' = ji$ and $\pi' i' =
j'i$.
%
A path from $( (L,j), p)$ to $( (L',j'), p')$ in the fiber over $(K',i')$ is
given a path $q: (L,j) = (L',j')$ in $\fieldsext K$ such that $\trp q p =
p'$. However, such a path $q$ is the data of an equivalence $\varphi : L =
L'$ such that $\varphi j = j'$, and then the condition $\trp q p = p'$
translates as $\varphi \pi = \pi'$. So it shows that $\varphi$ is necessarily
equal to $\pi'\inv\pi$, hence is unique.
\end{proof}
The fiber of this map at a given extension $(L,j)$ of $k$ is:
\begin{align*}
\inv{(\restr i)}(L,j) &\weq \sum_{L':\fieldstype}\sum_{j':K \to L'}(L,j) = (L',j'i) \\
&\weq \sum_{L':\fieldstype}\sum_{j':K\to L'}\sum_{p:L = L'} pj=j'i \\
&\weq \sum_{j':K\to L} j=j'i \\
&\weq \hom_k(K,L)
\end{align*}
where the last type denotes the type of homomorphisms of $k$-algebra (the structure of $K$ and $L$ being given by $i$ and $j$ respectively).
In particular, the map $t: \USym \Gal(K,i) \to \inv{(\restr i)}(K,i)$ mapping $g$ to
$\trp g (\id_K)$ identifies with the inclusion of the $k$-automorphisms of $K$
into the $k$-endomorphisms of $K$.
{\color{red} TODO: write a section on polynomials in chapter 12}
%
\begin{definition}
Given an extension $i:k\to K$, an element $\alpha:K$ is algebraic if $\alpha$ is merely
a root of a polynomial with coefficients in $k$. That is if the following
proposition holds:
\begin{displaymath}
\Trunc{\sum_{n:\mathbb N}\sum_{a:\bn n + 1 \to k}i(a(0))+i(a(1))\alpha+\cdots+i(a(n))\alpha^n=0}%
\end{displaymath}
\label{defn:algebraic-element}
\end{definition}
\begin{definition}
A field extension $(K,i)$ is said to be algebraic when each $a:K$ is algebraic.
\label{defn:algebraic-extension}
\end{definition}
\begin{remark}
Note that when the extension $(K,i)$ is algebraic, then $t$ is an
equivalence. However, the converse is false, as shown by the non-algebraic
extension $\mathbb Q \hookrightarrow \mathbb R$. We will prove that every
$\mathbb Q$-endomorphism of $\mathbb R$ is the identity function. Indeed, any
$\mathbb Q$-endormorphism $\varphi : \mathbb R \to \mathbb R$ is linear and
sends squares to squares, hence is non-decreasing. Let us now take an irrational
number $\alpha:\mathbb R$. For any rational $p,q:\mathbb Q$ such that $p <
\alpha < q$, then $p = \varphi(p) < \varphi(\alpha) < \varphi(q) = q$. Hence
$\varphi(\alpha)$ is in any rational interval that $\alpha$ is. One deduces
$\varphi(\alpha) = \alpha$.
%
\label{rem:algebraic-endomorphisms-are-automorphisms}
\end{remark}
\begin{definition}
A field extension $i:k\to K$ is said finite when $K$ as a
$k$-vector space, the structure of which is given by $i$, is of finite dimension.
In that case, the dimension is called the degree of $i$, denoted $[(K,i)]$ or $[K:k]$ when $i$ is clear from context.
\label{defn:degree-field-extension}
\end{definition}
\section{Intermediate extensions and subgroups}
%
Given two extensions $i: k \to K$ and $j: K \to L$, the map $\restr i$ can be seen as a pointed map
\begin{displaymath}
\restr i: \B\Gal(L,j) \to \B\Gal(L,ji),\quad x\mapsto x\circ i.
\end{displaymath}
Then, through \cref{lem:field-ext-restriction-set-bundle}, $\restr i$ presents
$\Gal(L,j)$ as a subgroup of $\Gal(L,ji)$. One goal of Galois theory is to
characterize those extensions $i':k \to L$ for which all subgroups of
$\Gal(L,i')$ arise in this way.
Given any extension $i:k \to L$, there is an obivous $\Gal(L,i)$-set $X$ given by
\begin{displaymath}
(L',i') \mapsto L'.
\end{displaymath}
For a pointed connected set-bundle $g:B \to \B \Gal(L,i)$, one can consider the
type of fixed points of the $\mkgroup B$-set $Xf$:
\begin{displaymath}
K \defequi (Xg)^{\mkgroup B} \jdeq \prod_{x:B}X(g(x))
\end{displaymath}
It is a set, which can be equipped with a field structure, defined pointwise.
Morevover, if one denotes $b$ for the distinguished point of $B$, and $(L'',j'')$ for $g(b)$, then, because $g$ is pointed, one has a path $p:L=L''$ such that $pi'=j''$. There are
fields extensions $i':k \to K$ and $j':K \to L$ given by:
\begin{displaymath}
i'(a) \defequi x\mapsto \snd(g(x))(a),\quad
j'(f) \defequi \inv p f(b)
\end{displaymath}
In particular, for all $a:k$, $j'i'(a) = \inv p \snd(g(b))(a) = \inv p j''(a) = i'(a)$.
Galois theory is interested in the settings when these two contructions are inverse from each other.
\section{separable/normal/etc.}
\label{sec:cover-spac-fields-1}
\section{fundamental theorem}
\label{sec:fundamental-theorem}