\documentclass[12pt,titlepage]{article} \usepackage{amsmath} \usepackage{mathrsfs} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsthm} \usepackage{mathtools} \usepackage{graphicx} \usepackage{color} \usepackage{ucs} \usepackage[utf8x]{inputenc} \usepackage{xparse} \usepackage{hyperref} %----Macros---------- % % Unresolved issues: % % \righttoleftarrow % \lefttorightarrow % % \color{} with HTML colorspec % \bgcolor % \array with options (without options, it's equivalent to the matrix environment) % Of the standard HTML named colors, white, black, red, green, blue and yellow % are predefined in the color package. Here are the rest. \definecolor{aqua}{rgb}{0, 1.0, 1.0} \definecolor{fuschia}{rgb}{1.0, 0, 1.0} \definecolor{gray}{rgb}{0.502, 0.502, 0.502} \definecolor{lime}{rgb}{0, 1.0, 0} \definecolor{maroon}{rgb}{0.502, 0, 0} \definecolor{navy}{rgb}{0, 0, 0.502} \definecolor{olive}{rgb}{0.502, 0.502, 0} \definecolor{purple}{rgb}{0.502, 0, 0.502} \definecolor{silver}{rgb}{0.753, 0.753, 0.753} \definecolor{teal}{rgb}{0, 0.502, 0.502} % Because of conflicts, \space and \mathop are converted to % \itexspace and \operatorname during preprocessing. % itex: \space{ht}{dp}{wd} % % Height and baseline depth measurements are in units of tenths of an ex while % the width is measured in tenths of an em. \makeatletter \newdimen\itex@wd% \newdimen\itex@dp% \newdimen\itex@thd% \def\itexspace#1#2#3{\itex@wd=#3em% \itex@wd=0.1\itex@wd% \itex@dp=#2ex% \itex@dp=0.1\itex@dp% \itex@thd=#1ex% \itex@thd=0.1\itex@thd% \advance\itex@thd\the\itex@dp% \makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}} \makeatother % \tensor and \multiscript \makeatletter \newif\if@sup \newtoks\@sups \def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}% \def\reset@sup{\@supfalse\@sups={}}% \def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else% \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}% \else \append@sup#2 \@suptrue \fi% \expandafter\mk@scripts\fi} \def\tensor#1#2{\reset@sup#1\mk@scripts#2_/} \def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2% \reset@sup\mk@scripts#3_/} \makeatother % \slash \makeatletter \newbox\slashbox \setbox\slashbox=\hbox{$/$} \def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$} \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa \copy\slashbox \kern-\@tempdima \box\@tempboxa} \def\slash{\protect\itex@pslash} \makeatother % math-mode versions of \rlap, etc % from Alexander Perlis, "A complement to \smash, \llap, and lap" % http://math.arizona.edu/~aprl/publications/mathclap/ \def\clap#1{\hbox to 0pt{\hss#1\hss}} \def\mathllap{\mathpalette\mathllapinternal} \def\mathrlap{\mathpalette\mathrlapinternal} \def\mathclap{\mathpalette\mathclapinternal} \def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}} \def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}} \def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}} % Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2} \let\oldroot\root \def\root#1#2{\oldroot #1 \of{#2}} \renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}} % Manually declare the txfonts symbolsC font \DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n} \SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n} \DeclareFontSubstitution{U}{txsyc}{m}{n} % Manually declare the stmaryrd font \DeclareSymbolFont{stmry}{U}{stmry}{m}{n} \SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n} % Manually declare the MnSymbolE font \DeclareFontFamily{OMX}{MnSymbolE}{} \DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n} \SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n} \DeclareFontShape{OMX}{MnSymbolE}{m}{n}{ <-6> MnSymbolE5 <6-7> MnSymbolE6 <7-8> MnSymbolE7 <8-9> MnSymbolE8 <9-10> MnSymbolE9 <10-12> MnSymbolE10 <12-> MnSymbolE12}{} % Declare specific arrows from txfonts without loading the full package \makeatletter \def\re@DeclareMathSymbol#1#2#3#4{% \let#1=\undefined \DeclareMathSymbol{#1}{#2}{#3}{#4}} \re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46} \re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12} \re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64} \re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6} \re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77} \re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77} \makeatother % \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE \makeatletter \def\Decl@Mn@Delim#1#2#3#4{% \if\relax\noexpand#1% \let#1\undefined \fi \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}} \def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}} \def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}} \Decl@Mn@Open{\llangle}{mnomx}{'164} \Decl@Mn@Close{\rrangle}{mnomx}{'171} \Decl@Mn@Open{\lmoustache}{mnomx}{'245} \Decl@Mn@Close{\rmoustache}{mnomx}{'244} \makeatother % Widecheck \makeatletter \DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}} \def\@widecheck#1#2{% \setbox\z@\hbox{\m@th$#1#2$}% \setbox\tw@\hbox{\m@th$#1% \widehat{% \vrule\@width\z@\@height\ht\z@ \vrule\@height\z@\@width\wd\z@}$}% \dp\tw@-\ht\z@ \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@ \setbox\tw@\hbox{% \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box \tw@}}}% {\ooalign{\box\tw@ \cr \box\z@}}} \makeatother % \mathraisebox{voffset}[height][depth]{something} \makeatletter \NewDocumentCommand\mathraisebox{moom}{% \IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{% \IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}% }{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}% \mathpalette\@temp{#4}} \makeatletter % udots (taken from yhmath) \makeatletter \def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.} \mkern2mu\raise4\p@\hbox{.}\mkern1mu \raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}} \makeatother %% Fix array \newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}} %% \itexnum is a noop \newcommand{\itexnum}[1]{#1} %% Renaming existing commands \newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}} \newcommand{\widevec}{\overrightarrow} \newcommand{\darr}{\downarrow} \newcommand{\nearr}{\nearrow} \newcommand{\nwarr}{\nwarrow} \newcommand{\searr}{\searrow} \newcommand{\swarr}{\swarrow} \newcommand{\curvearrowbotright}{\curvearrowright} \newcommand{\uparr}{\uparrow} \newcommand{\downuparrow}{\updownarrow} \newcommand{\duparr}{\updownarrow} \newcommand{\updarr}{\updownarrow} \newcommand{\gt}{>} \newcommand{\lt}{<} \newcommand{\map}{\mapsto} \newcommand{\embedsin}{\hookrightarrow} \newcommand{\Alpha}{A} \newcommand{\Beta}{B} \newcommand{\Zeta}{Z} \newcommand{\Eta}{H} \newcommand{\Iota}{I} \newcommand{\Kappa}{K} \newcommand{\Mu}{M} \newcommand{\Nu}{N} \newcommand{\Rho}{P} \newcommand{\Tau}{T} \newcommand{\Upsi}{\Upsilon} \newcommand{\omicron}{o} \newcommand{\lang}{\langle} \newcommand{\rang}{\rangle} \newcommand{\Union}{\bigcup} \newcommand{\Intersection}{\bigcap} \newcommand{\Oplus}{\bigoplus} \newcommand{\Otimes}{\bigotimes} \newcommand{\Wedge}{\bigwedge} \newcommand{\Vee}{\bigvee} \newcommand{\coproduct}{\coprod} \newcommand{\product}{\prod} \newcommand{\closure}{\overline} \newcommand{\integral}{\int} \newcommand{\doubleintegral}{\iint} \newcommand{\tripleintegral}{\iiint} \newcommand{\quadrupleintegral}{\iiiint} \newcommand{\conint}{\oint} \newcommand{\contourintegral}{\oint} \newcommand{\infinity}{\infty} \newcommand{\bottom}{\bot} \newcommand{\minusb}{\boxminus} \newcommand{\plusb}{\boxplus} \newcommand{\timesb}{\boxtimes} \newcommand{\intersection}{\cap} \newcommand{\union}{\cup} \newcommand{\Del}{\nabla} \newcommand{\odash}{\circleddash} \newcommand{\negspace}{\!} \newcommand{\widebar}{\overline} \newcommand{\textsize}{\normalsize} \renewcommand{\scriptsize}{\scriptstyle} \newcommand{\scriptscriptsize}{\scriptscriptstyle} \newcommand{\mathfr}{\mathfrak} \newcommand{\statusline}[2]{#2} \newcommand{\tooltip}[2]{#2} \newcommand{\toggle}[2]{#2} % Theorem Environments \theoremstyle{plain} \newtheorem{theorem}{Theorem} \newtheorem{lemma}{Lemma} \newtheorem{prop}{Proposition} \newtheorem{cor}{Corollary} \newtheorem*{utheorem}{Theorem} \newtheorem*{ulemma}{Lemma} \newtheorem*{uprop}{Proposition} \newtheorem*{ucor}{Corollary} \theoremstyle{definition} \newtheorem{defn}{Definition} \newtheorem{example}{Example} \newtheorem*{udefn}{Definition} \newtheorem*{uexample}{Example} \theoremstyle{remark} \newtheorem{remark}{Remark} \newtheorem{note}{Note} \newtheorem*{uremark}{Remark} \newtheorem*{unote}{Note} %------------------------------------------------------------------- \begin{document} %------------------------------------------------------------------- \section*{principal ideal domain} \hypertarget{context}{}\subsubsection*{{Context}}\label{context} \hypertarget{algebra}{}\paragraph*{{Algebra}}\label{algebra} [[!include higher algebra - contents]] \hypertarget{contents}{}\section*{{Contents}}\label{contents} \noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak \noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak \noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak \noindent\hyperlink{StructureTheoryOfModules}{Structure theory of modules}\dotfill \pageref*{StructureTheoryOfModules} \linebreak \noindent\hyperlink{free_and_projective_modules}{Free and projective modules}\dotfill \pageref*{free_and_projective_modules} \linebreak \noindent\hyperlink{SmithNormalForm}{Normal forms}\dotfill \pageref*{SmithNormalForm} \linebreak \noindent\hyperlink{torsionfree_modules}{Torsion-free modules}\dotfill \pageref*{torsionfree_modules} \linebreak \noindent\hyperlink{structure_theory_of_finitely_generated_modules}{Structure theory of finitely generated modules}\dotfill \pageref*{structure_theory_of_finitely_generated_modules} \linebreak \noindent\hyperlink{in_constructive_mathematics}{In constructive mathematics}\dotfill \pageref*{in_constructive_mathematics} \linebreak \noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak \hypertarget{definition}{}\subsection*{{Definition}}\label{definition} A [[ring]] $R$ is a \textbf{principal ideal domain} if \begin{enumerate}% \item it is an [[integral domain]] (hence in particular a [[commutative ring]]) \item every [[ideal]] in $R$ is a [[principal ideal]]. \end{enumerate} Often \emph{pid} is used as an abbreviation of ``principal ideal domain''. \hypertarget{examples}{}\subsection*{{Examples}}\label{examples} \begin{itemize}% \item any [[field]] \item the ring $\mathbb{Z}$ of [[integers]] \item a [[polynomial ring]] with [[coefficients]] in a field (in fact, for any commutative ring $R$, the ring $R[x]$ is a pid if and \emph{only if} $R$ is a field) \item a [[valuation ring|discrete valuation ring]] (for example, a ring of formal power series over a field) \item any [[Euclidean domain]] \item in the ring of [[entire function|entire]] [[holomorphic functions]] on $\mathbb{C}$ every finitely generated ideal is principal (\hyperlink{Helmer40}{Helmer 40}), but the ring is only a [[Bézout domain]]. \end{itemize} That both the [[integers]] and the [[polynomial rings]] $\mathbb{F}_q[x]$ over [[finite fields]] are principal integral domains with [[finite group|finite]] [[group of units]] is one aspect of the close similarity between the two that is the topic of the [[function field analogy]]. That also the [[holomorphic functions]] on the [[complex plane]] form a [[Bézout domain]] may then be viewed as part of the further similarity that relates the previous two to topics such as [[geometric Langlands duality]]. See at \emph{[[function field analogy -- table]]} for more on this. \hypertarget{properties}{}\subsection*{{Properties}}\label{properties} \begin{lemma} \label{}\hypertarget{}{} In a pid $R$, an element $x$ is irreducible iff $(x)$ is a maximal ideal. \end{lemma} \begin{proof} Suppose $x$ is irreducible and $a \notin (x)$. Then the ideal generated by $a, x$ is principal, say $(b)$. Then $x = b y$ and since $x$ is irreducible, one of $b, y$ is a unit; if $y$ is a unit then $(x) = (b) = (a, x)$ and thus $a \in (x)$, contradiction. So then $b$ must be a unit, i.e., $(b)$ is the improper ideal. Thus $(x)$ has no proper extension: $(x)$ is maximal. For any ring $R$, if $(x)$ is maximal and $x = a b$ for a non-unit $a$, then the inclusion $(x) \subseteq (a)$ is an equality by maximality, so $a = x v$ for some $v$. Then $x = x v b$. In an integral domain we conclude $1 = v b$; thus $b$ is a unit. \end{proof} \begin{prop} \label{noeth}\hypertarget{noeth}{} A pid is a [[Noetherian ring]]. \end{prop} \begin{proof} The union of an ascending chain of ideals $I_1 \subseteq I_2 \subseteq \ldots$ is an ideal $I$; if $I = (x)$, then $x$ belongs to one of the $I_n$, whereupon $I = I_n$. \end{proof} \begin{prop} \label{}\hypertarget{}{} A PID is a [[unique factorization domain]]. \end{prop} \begin{proof} Working in classical logic, Proposition \ref{noeth} says that the reverse inclusion relation on the set of nonzero ideals is [[well-founded relation|well-founded]]. Let $A$ be the subset of ideals $(a)$ that are products of finitely many (maybe zero!) maximal principal ideals. For any proper ideal $(x) \neq (0)$, if every $(t)$ properly containing $(x)$ can be factored into maximals, then so can $(x)$. (Spelling this out: either $(x)$ is maximal/irreducible, or factors as $(s)(t)$ where both $s$ and $t$ are non-units; $(s)$ and $(t)$ factor into maximals by hypothesis, and therefore so does $(x)$.) Thus $A$ is an inductive set, so by well-foundedness it contains every ideal $(x) \neq (0)$, i.e., $x$ can be factored into irreducibles. For uniqueness of the factorization, we first remark that if $p$ is irreducible and $p|a b$, then $p|a$ or $p|b$. (For $R/(p)$ is a [[field]] and thus \emph{a fortiori} an [[integral domain]], so that if $a b \equiv 0 \; mod p$, then $a \equiv 0 \; mod p$ or $b \equiv 0 \; mod p$.) Thus if $p_1 p_2 \ldots p_m = q_1 q_2 \ldots q_n$ are two factorizations into irreducibles of the same element, then $p_1$ divides one of the irreducibles $q_i$, in which case $(p_1) = (q_i)$ and each is a unit times the other, meaning we can cancel $p_1$ on both sides and argue by induction. \end{proof} \hypertarget{StructureTheoryOfModules}{}\subsection*{{Structure theory of modules}}\label{StructureTheoryOfModules} \hypertarget{free_and_projective_modules}{}\subsubsection*{{Free and projective modules}}\label{free_and_projective_modules} \begin{theorem} \label{free}\hypertarget{free}{} If $R$ is a pid, then any [[submodule]] $M$ of a [[free module]] $F$ over $R$ is also free. (For the converse statement, see \href{http://ncatlab.org/nlab/show/free+module#submod}{here}.) \end{theorem} \begin{proof} By freeness of $F$, there exists an isomorphism $F \cong \sum_{j \in J} R_j$, a [[coproduct]] of copies $R_j$ of $R$ (as a module over the ring $R$) indexed over a set $J$, which we assume [[well-ordering|well-ordered]] using the [[axiom of choice]]. Define submodules of $F$: \begin{displaymath} F_{\leq j} \coloneqq \sum_{i \leq j} R_i, \qquad F_{\lt j} \coloneqq \sum_{i \lt j} R_i\,. \end{displaymath} Any element of $M \cap F_{\leq j}$ can be written uniquely as $(x, r)$ where $x \in F_{\lt j}$ and $r \in R_j$. Define a [[homomorphism]] \begin{displaymath} p_j \colon M \cap F_{\leq j} \to R \end{displaymath} by $p_j((x, r)) = r$. The [[kernel]] of $p_j$ is $M \cap F_{\lt j}$, and we have an [[exact sequence]] \begin{displaymath} 0 \to M \cap F_{\lt j} \to M \cap F_{\leq j} \to \im p_j \to 0 \end{displaymath} where $\im p_j$ is a submodule (i.e., an [[ideal]]) of $R$, hence generated by a single element $r_j$. Let $K \subseteq J$ consist of those $j$ such that $r_j \neq 0$, and for $k \in K$, choose $m_k$ such that $p_k(m_k) = r_k$. We claim that $\{m_k: k \in K\}$ forms a [[basis]] for $M$. First we prove [[linear independence]] of $\{m_k\}$. Suppose $\sum_{i=1}^{n} a_i m_{k_i} = 0$, with $k_1 \lt k_2 \lt \ldots \lt k_n$. Applying $p_{k_n}$, we get $a_n p_{k_n}(m_{k_n}) = a_n r_{k_n} = 0$. Since $r_{k_n} \neq 0$, we have $a_n = 0$ (since we are working over a domain). The assertion now follows by [[induction]]. Now we prove that the $m_k$ generate $M$. Assume otherwise, and let $j \in J$ be the least $j$ such that some $m \in M \cap F_{\leq j}$ cannot be written as a linear combination of the $m_k$, for $k \in K$. If $j \notin K$, then $m \in M \cap F_{\lt j}$, so that $m \in M \cap F_{\leq i}$ for some $i \lt j$, but this contradicts minimality of $j$. Therefore $j \in K$. Now, we have $p_j(m) = r \cdot r_j$ for some $r$; put $m' = m - r m_j$. Clearly \begin{displaymath} p_j(m') = p_j(m) - r \cdot p_j(m_j) = 0 \end{displaymath} and so $m' \in M \cap F_{\lt j}$. Thus $m' \in M \cap F_{\leq i}$ for some $i \lt j$. At the same time, $m'$ cannot be written as a linear combination of the $m_k$; again, this contradicts minimality of $j$. Thus the $m_k$ generate $M$, as claimed. \end{proof} Since the [[integers]] $\mathbb{Z}$ for a pid, and [[abelian groups]] are the same as $\mathbb{Z}$-[[modules]], we have \begin{cor} \label{}\hypertarget{}{} \textbf{(Dedekind)} A [[subgroup]] of a [[free abelian group]] is also free abelian. \end{cor} \begin{remark} \label{}\hypertarget{}{} The analog of this statement for possibly non-abelian [[groups]] is the \emph{[[Nielsen-Schreier theorem]]}. \end{remark} Also, since [[projective modules]] are [[retracts]] of free modules, we have \begin{cor} \label{}\hypertarget{}{} Projective modules over a pid are free. In particular, submodules of projective modules are projective. \end{cor} \hypertarget{SmithNormalForm}{}\subsubsection*{{Normal forms}}\label{SmithNormalForm} \begin{prop} \label{MatricesOverPrincipalIdealDomainsHaveSmithNormalForm}\hypertarget{MatricesOverPrincipalIdealDomainsHaveSmithNormalForm}{} \textbf{([[matrices]] over [[principal ideal domains]] [[matrix equivalence|equivalent]] to [[Smith normal form]])} For $R$ a [[commutative ring]] which is a [[principal ideal domain]], every [[matrix]] $A \in Mat_{n \times m}(R)$ with entries in $R$ is [[matrix equivalence|matrix equivalent]] to a [[diagonal matrix]] filled up with zeros: There exist [[invertible matrices]] $P \in Mat_{n \times n}(R)$ and $Q \in Mat_{m \times m}(R)$ such that the [[matrix product|product matrix]] $P A Q$ is a [[diagonal matrix]] filled up with zeros: \begin{displaymath} P A Q \;=\; \end{displaymath} such that, moreover, each $a_i$ [[divisor|divides]] $a_{i+1}$. \end{prop} For [[matrices]] with coefficients in the pid of [[integers]] see also \begin{itemize}% \item \emph{[[Hermite normal form]]}. \end{itemize} \hypertarget{torsionfree_modules}{}\subsubsection*{{Torsion-free modules}}\label{torsionfree_modules} \begin{prop} \label{torsionfree}\hypertarget{torsionfree}{} A finitely generated [[torsion subgroup|torsionfree]] module $M$ over a pid $R$ is free. \end{prop} \begin{proof} Let $S$ be a finite set of generators of $M$, and let $T \subseteq S$ be a maximal subset of linearly independent elements. (Unless $M = 0$, then $T$ has at least one element, because $M$ is torsionfree.) We claim that $M$ can be embedded as a submodule of the free module $F$ generated by $T$ (which in turn is the span of $T$ as a submodule $F \subseteq M$). By Theorem \ref{free}, it follows that $M$ is free. Let $x_1, \ldots, x_n$ be the elements of $T$. It follows from maximality of $T$ that for any $m \in S - T$, there is a linear relation \begin{displaymath} r_m m + r_1 x_1 + \ldots + r_n x_n = 0 \end{displaymath} with $r_m \neq 0$. For each $m$ in the complement $S - T$, pick such an $r_m$, and form $r = \prod_{m \in S - T} r_m$. Then the image of the scalar multiplication $\lambda_r \colon M \to M$ factors through $F \subseteq M$, and $M \to \lambda_r(M)$ is monic because $M$ is torsionfree. This completes the proof. \end{proof} \begin{prop} \label{flat}\hypertarget{flat}{} Let $R$ be a pid. Then an $R$-module $M$ is torsionfree if and only if it is [[flat module|flat]]. \end{prop} \begin{proof} Suppose $M$ is flat. Let $K$ be the field of fractions of $R$; since $R$ is a domain, we have a monic $R$-module map $R \to K$. By flatness, we have an induced monomorphism $M \cong R \otimes_R M \to K \otimes_R M$. For any nonzero $r \in R$, the naturality square \begin{displaymath} \itexarray{ M & \to & K \otimes_R M \\ \mathllap{\lambda_r} \downarrow & & \downarrow \mathrlap{1 \otimes \lambda_r} \\ M & \to & K \otimes_R M } \end{displaymath} commutes, and since the map $1 \otimes \lambda_r$ is multiplication by a non-zero scalar on a vector space, it follows that this map and therefore also $\lambda_r$ is monic, i.e., $M$ is torsionfree. In the other direction, suppose $M$ is torsionfree. Any module is the filtered colimit over the system of finitely generated submodules and inclusions between them; in this case all the finitely generated submodules of $M$ are torsion-free and hence free, by Proposition \ref{torsionfree}. Thus $M$ is a filtered colimit of free modules; it is therefore flat by a standard result proved \href{http://ncatlab.org/nlab/show/flat+module#filtfree}{here}. \end{proof} \hypertarget{structure_theory_of_finitely_generated_modules}{}\subsubsection*{{Structure theory of finitely generated modules}}\label{structure_theory_of_finitely_generated_modules} \emph{[[structure theorem for finitely generated modules over a principal ideal domain]]} \hypertarget{in_constructive_mathematics}{}\subsection*{{In constructive mathematics}}\label{in_constructive_mathematics} In [[constructive mathematics]], many important rings may fail to be principal ideal domains in the na\"i{}ve sense; the notion of \emph{[[Bézout domain]]}, in which only the finitely generated ideals are required to be principal, is better behaved. For instance, the ring of integers is a principal ideal domain if and only if the [[excluded middle|law of excluded middle]] holds: In one direction, the usual proofs rely on being able to [[decidable proposition|decide]] whether any particular integer belongs to the ideal or not. For the converse, let $\varphi$ be an arbitrary proposition. Consider the ideal $\{ x \in \mathbb{Z} | (x = 0) \vee \varphi \}$. By assumption, it is generated by some number $n$. Since the integers are [[decidable equality|discrete]], it holds that $n = 0$ or $n \neq 0$. In the first case $\neg\varphi$ holds, in the second $\varphi$. However, this ideal cannot be proved to be finitely generated either. If an ideal is generated by $n_1, \ldots, n_k$, then we may form their [[gcd]] one step at a time, which we can do algorithmically. Therefore, $\mathbb{Z}$ remains a B\'e{}zout domain. On the other hand, we could try to modify the concept of principal ideal domain to recover a concept that is identical to the usual one in [[classical mathematics]] but also includes $\mathbb{Z}$. For instance, we could demand that every [[decidable subset|decidable]] ideal is principal, or (potentially more strongly) that any ideal generated by a decidable subset is principal. While these seem to work at first, they are too weak to prove that every PID is a B\'e{}zout domain, so we should try to think of something better. \hypertarget{references}{}\subsection*{{References}}\label{references} \begin{itemize}% \item O. Helmer, \emph{Divisibility properties of integral functions}, Duke Math. J. 6 (1940), 345-356. \item Wikipedia, \emph{\href{http://en.wikipedia.org/wiki/Principal_ideal_domain}{Principal ideal domain}} \item Eric Wofsey, \emph{Principal Ideal Domains}, (written for Mathcamp 2009) \href{http://www.math.harvard.edu/~waffle/pids.pdf}{pdf} \end{itemize} [[!redirects principal ideal domain]] [[!redirects principal ideal domains]] [[!redirects pid]] [[!redirects pids]] [[!redirects PID]] [[!redirects PIDs]] \end{document}