\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*{prime ideal theorem} \hypertarget{contents}{}\section*{{Contents}}\label{contents} \noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak \noindent\hyperlink{a_ladder_of_prime_ideal_theorems}{A ladder of prime ideal theorems}\dotfill \pageref*{a_ladder_of_prime_ideal_theorems} \linebreak \noindent\hyperlink{boolean_pit_and_the_ultrafilter_principle}{Boolean PIT and the ultrafilter principle}\dotfill \pageref*{boolean_pit_and_the_ultrafilter_principle} \linebreak \noindent\hyperlink{bpit_implies_prime_ideal_theorem_for_distributive_lattices}{BPIT implies prime ideal theorem for distributive lattices}\dotfill \pageref*{bpit_implies_prime_ideal_theorem_for_distributive_lattices} \linebreak \noindent\hyperlink{banaschewskis_lemma}{Banaschewski's lemma}\dotfill \pageref*{banaschewskis_lemma} \linebreak \noindent\hyperlink{prime_elements_in_quantales_of_ideals}{Prime elements in quantales of ideals}\dotfill \pageref*{prime_elements_in_quantales_of_ideals} \linebreak \noindent\hyperlink{generalized_prime_ideal_theorems}{Generalized prime ideal theorems}\dotfill \pageref*{generalized_prime_ideal_theorems} \linebreak \noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak \hypertarget{idea}{}\subsection*{{Idea}}\label{idea} A \textbf{prime ideal theorem} is a theorem stating that every [[proper ideal]] is contained in some [[prime ideal]]. A prime ideal theorem is typically equivalent to the [[ultrafilter principle]] (UF), a weak form of the [[axiom of choice]] (AC). We say `a' prime ideal theorem (PIT) instead of `the' prime ideal theorem, since we have not said what the ideals are in. We list some representative examples of prime ideal theorems, all of which are equivalent to (UF) in ZF or even in BZ (bounded Zermelo set theory): \begin{itemize}% \item The PIT for (commutative) [[rings]]. \item The PIT for (bounded) [[distributive lattices]]. \item The PIT for [[Boolean algebras]]. \item The PIT for [[rigs]], which subsumes all of the above. In fact one can generalize quite a bit further, as we indicate below when we discuss prime element theorems. \end{itemize} The usual way to prove a prime ideal theorem is with the help of [[Zorn's Lemma]], unless one is specifically trying to use something weaker like UF (as we do in this article). In fact [[Zorn's lemma]] can be used to prove a [[maximal ideal theorem]], which is stronger: in all the usual examples maximal ideals are prime so that a [[prime ideal theorem]] becomes a corollary. There are stronger forms of prime ideal theorems which assert the existence of a prime ideal that does not intersect a given multiplicatively closed subset $\mathfrak{m}$. However, these can often be reduced to an ordinary PIT, by first localizing or inverting the elements in $\mathfrak{m}$, and then applying a PIT to the localization. \hypertarget{a_ladder_of_prime_ideal_theorems}{}\subsection*{{A ladder of prime ideal theorems}}\label{a_ladder_of_prime_ideal_theorems} Prime ideal theorems may be arranged as a sequence of results and techniques that gradually increase in sophistication; we sketch one possible development here, filling in details in the remainder of the article. A first easy wave of results concerns the equivalence between the Boolean PIT (or BPIT) and UF. While these are easy, the BPIT is a theoretical underpinning of fundamental techniques such as the [[compactness theorem]] for [[first-order logic]], which leads to the next rung on the ladder. The next step derives the PIT for distributive lattices as a simple application of the compactness theorem. In effect we write down a simple [[propositional theory]] where a [[model]] is tantamount to a prime ideal in a given distributive lattice. Part of the work involves checking finite satisfiability of the theory, where we may invoke a simple [[Stone duality]] between finite distributive lattices and finite posets to get the job done. With the PIT for distributive lattices in hand, we prove a key result due to Banaschewski, which may be summarized roughly as saying that a (nontrivial) compact [[frame]] admits a prime element. This is an early result in [[Stone Spaces]], related to the spatiality of compact regular [[locales]]. Banaschewski's lemma is a key of entry into prime ideal theorems of general type. The general idea is that ideals in a monoid (now in suitably nice monoidal categories) tend to form compact [[quantales]], whose prime elements correspond to prime ideals. One then invokes a simple construction which associates to each compact quantale a quotient compact frame, in such a way that the existence of a prime element in the quantale is reduced to existence of a prime element in the compact frame \emph{\`a{} la} Banaschewski's lemma. As promised, this gives prime ideal theorems of fairly general type (call them collectively ``GPIT''). As suggested earlier, any one of these prime ideal theorems implies the BPIT as a special case, and so we come full circle: \begin{displaymath} UF \Rightarrow BPIT \Rightarrow PIT(DistLat) \Rightarrow Banaschewski \Rightarrow GPIT \Rightarrow BPIT \Rightarrow UF. \end{displaymath} We now turn to details. \hypertarget{boolean_pit_and_the_ultrafilter_principle}{}\subsubsection*{{Boolean PIT and the ultrafilter principle}}\label{boolean_pit_and_the_ultrafilter_principle} The Boolean prime ideal theorem or BPIT is equivalent to the [[ultrafilter principle]] UF. The reasoning may be summarized as follows: the ultrafilter principle implies the [[Tychonoff theorem]] for compact Hausdorff spaces; see this \href{/nlab/show/Tychonoff+theorem#TyCH}{Remark} and the argument immediately preceding it. The Tychonoff theorem for compact Hausdorff spaces in turn implies that every Boolean ring $B$ has a maximal (and therefore prime) ideal; see \href{/nlab/show/Tychonoff+theorem#nonempty}{here}. Consequently, for any ideal $I$ of a Boolean algebra $B$, the quotient Boolean ring $B/I$ has a prime ideal $P$, and the pullback $q^{-1}(P) \subseteq B$ of the quotient map $q: B \to B/I$ produces a prime ideal in $B$ which contains a given ideal $I$, thus proving the BPIT from UF. (In passing, one may note that prime ideals in Boolean algebras (or Boolean rings) $B$ are the same as maximal ideals. For, the corresponding Boolean quotient ring is an [[integral domain]] only if it is the [[field]] $\mathbb{Z}/(2)$, since [[idempotent element|idempotency]] of elements yields $e(1-e) = 0$ and then $e = 0$ or $e = 1$ assuming no [[zero divisors]].) Finally, maximal ideals are complementary to ultrafilters (see \href{/nlab/show/Boolean+algebra#aremax}{here}). So UF, which says that every [[filter]] in $B = P X$ is contained in an ultrafilter, translates into a special case of the BPIT: every ideal of $P X$ (consisting of negations of elements of a corresponding filter) is contained in a prime/maximal ideal. This brings us full circle: BPIT implies UF implies Tychonoff(CH) implies BPIT. \hypertarget{bpit_implies_prime_ideal_theorem_for_distributive_lattices}{}\subsubsection*{{BPIT implies prime ideal theorem for distributive lattices}}\label{bpit_implies_prime_ideal_theorem_for_distributive_lattices} Now let us prove that the Tychonoff theorem for CH spaces implies the PIT for distributive lattices $D$: that any proper ideal $I$ of $D$ is contained in a prime ideal of $D$. By passing to the quotient lattice $D/I$, it suffices to show that $D/I$ has a prime ideal $P$, since the inverse image $\phi^{-1}(P)$ of a prime ideal $P$ along the quotient map $\phi: D \to D/I$ is again prime. \begin{theorem} \label{}\hypertarget{}{} (UF) Any nontrivial distributive lattice $D$ has a prime ideal $P$. \end{theorem} To prove this, we write down a propositional theory of ``a prime ideal $P$ of $D$'' (and consider its [[Lindenbaum algebra]]). Form a free Boolean algebra $Bool(U D)$ freely generated by the underlying set $U D$ of $D$. So each $x \in U D$ corresponds to a generator $P_x \in Bool(U D)$, which we will think of as standing for a proposition $P_x =$ ``$x \in P$''. The conditions that enforce ``$P$ is a prime ideal of $D$'' are the axioms of our theory: \begin{itemize}% \item ($P$ is closed under finite joins) $P_0$, $P_a \wedge P_b \Rightarrow P_{a \vee b}$. \item ($P$ is downward closed) For each $b \in U D$, $P_a \Rightarrow P_{a \wedge b}$. \item ($P$ is proper) $\neg P_1$. \item (primality condition) $P_{a \wedge b} \Rightarrow (P_a \vee P_b)$. \end{itemize} These axioms (certain elements of $Bool(U D)$) then generate a [[filter]] $\mathcal{F}$. As soon as we know $\mathcal{F}$ is proper (``finite satisfiability of the theory''), the BPIT ensures that $F$ is contained in an ultrafilter $\mathcal{U}$, corresponding to a [[model]] or a Boolean ring homomorphism $Bool(U D)/\mathcal{F} \to \mathbf{2}$ out of the Lindenbaum algebra. For that model, the collection $\{a \in D: P_a \in \mathcal{U}\}$ then forms a prime ideal $P$ of $D$, as desired. So: \begin{proof} (The filter $\mathcal{F}$ is proper.) To see that the filter generated by finitely many axioms does not contain $0 \in Bool(U D)$, consider the sublattice of $D$ generated by the finitely many elements $a$ named in atomic subformulas of such axioms. A finitely generated distributive lattice is finite (indeed, by [[Stone duality]], the free distributive lattice on a finite number $n$ or elements is isomorphic to the poset of downward-closed subsets of the poset $\mathbf{2}^n$). So all we need to do is show that any nontrivial finite distributive lattice $L$ has a prime ideal. This also follows from Stone duality: a distributive lattice homomorphism $L \to \mathbf{2}$ corresponds to a point of the Stone dual $S$, and if $L$ is nontrivial then $S$ must be inhabited by a point $x$, so lattice homomorphisms $L \to \mathbf{2}$ exist and the kernel of such is a maximal and therefore prime ideal. \end{proof} \hypertarget{banaschewskis_lemma}{}\subsubsection*{{Banaschewski's lemma}}\label{banaschewskis_lemma} During the 1980's, \hyperlink{Ban}{Banaschewski} discovered the following result (a breakthrough in the study of prime ideal theorems, according to \href{http://www.researchgate.net/publication/242573716_Prime_Ideal_Theorems_and_systems_of_finite_character}{Marcel Ern\'e{}}). We state and prove the lemma for now, and show how it is used in later sections. \begin{theorem} \label{}\hypertarget{}{} \textbf{(Banaschewski's lemma)} Every nontrivial distributive complete lattice $L$ whose top element $1$ is [[compact element|compact]], e.g., a compact [[frame]], has a prime element. \end{theorem} \begin{remark} \label{}\hypertarget{}{} Here ``nontrivial'' means $0 \neq 1$: distinct top and bottom elements. This is needed because prime ideals are required to be proper (see [[too simple to be simple]]). An element $p$ is \emph{prime} if the principal ideal it generates is prime, i.e., if $a \wedge b \leq p$ implies $a \leq p$ or $b \leq p$. In a distributive lattice, this is the same as saying $p = a \wedge b$ implies $p = a$ or $p = b$ (meet-irreducibility). \end{remark} \begin{proof} First we observe that a coproduct of nontrivial bounded distributive lattices $\{X_i\}_{i \in I}$ (in the category of bounded distributive lattices) is also nontrivial. Again this is a kind of finite satisfiability result: if such a coproduct were trivial, i.e., if $0 = 1$ were satisfied in the coproduct (constructed syntactically as the free distributive lattice $F = F(\sum_i X_i)$ modulo equations that identify finite meets and joins in each $X_i$ with formal meets and joins in $F$), then $0 = 1$ would be derivable from finitely many equations involving finitely many elements $x_i$ in the $X_i$, and hence $0 = 1$ would be derivable in a finite coproduct of finite bounded nontrivial distributive lattices generated by these elements. This cannot happen, by considering their [[Stone duality]] with finite [[posets]] and products thereof: finite products of [[inhabited set|inhabited]] finite posets are also inhabited. With that in hand, consider the [[coproduct]] $M = \sum_{a \in L \setminus \{1\}} \uparrow a$ of all the nontrivial principal filters of $L$, taken in the category of bounded distributive lattices; let $i_a: \uparrow a \to M$ denote the coproduct inclusion. $M$ has a prime ideal $P$ by the PIT for distributive lattices; the pullback $P_a \coloneqq i_a^{-1}(P)$ is a prime ideal of $\uparrow a$. Of course $P_a \subseteq L \setminus \{1\}$ by properness of prime ideals. Put $S = L \setminus \{1\}$. This is a [[dcpo]] by completeness of $L$ and compactness of $1$; since proper ideals $I \subseteq S$ are directed subsets, we see that $S$ admits a sup $\sigma(a) \coloneqq \bigvee P_a$ for each $a \in S$. We have $a \leq \sigma(a)$ for all $a \in S$. By the [[Zorn's lemma|Bourbaki-Witt fixed point theorem]], the inflationary operator $\sigma: S \to S$ has a fixed point, say $c: c = \sigma(c)$. For that $c$, note that $P_c \subseteq \uparrow c$ is just $\{c\}$. So $\{c\}$ is a prime ideal in $\uparrow c$. By meet-irreducibility, this means $c$ is a prime element in $L$. \end{proof} \begin{remark} \label{}\hypertarget{}{} When the statement is about compact frames, it can be rephrased as saying that every nontrivial compact locale has at least one point; compare [[Stone Spaces]], Lemma 1.9. \end{remark} \hypertarget{prime_elements_in_quantales_of_ideals}{}\subsubsection*{{Prime elements in quantales of ideals}}\label{prime_elements_in_quantales_of_ideals} To show how Banaschewski's lemma is applied, we consider for example the prime ideal theorem for (possibly noncommutative) rings. We follow the common convention that rings have units. Let $R$ be a ring, and let $Idl(R)$ be the sup-lattice of two-sided ideals of $R$. Under multiplication of ideals $A \cdot B$, we obtain a [[quantale]] structure on $Idl(R)$ whose multiplicative unit is the top element $R$. In general we will call a quantale \emph{affine} (or [[semicartesian monoidal category|semicartesian]]) if its unit is the top element. The top element $1$ of $Idl(R)$ is also a \emph{[[compact element]]}. In general, and generalizing a definition from the theory of [[frames]]/[[locales]], we will say that a quantale is \emph{compact} if its top element is a compact element. Finally, in a quantale $Q$, we say an element $p \in Q$ is \emph{prime} if for all $a, b \in Q$ we have $a b \leq p$ implies $a \leq p$ or $b \leq p$. Prime elements in $Idl(R)$ are precisely prime ideals of $R$. \begin{theorem} \label{quantale}\hypertarget{quantale}{} (ZF + UF) Every nontrivial compact affine quantale has a prime element. \end{theorem} The strategy (following \hyperlink{Pas}{Paseka}) is to reduce the claim to an application of Banaschewski's lemma. We begin by introducing an equivalence relation on $Q$: say $a \equiv b$ if $(\forall_c)\; 1 = a \vee c \Leftrightarrow 1 = b \vee c$. \begin{lemma} \label{}\hypertarget{}{} The relation $\equiv$ is a quantale congruence. \end{lemma} \begin{proof} First we show that $\equiv$ respects the quantale multiplication $\cdot$. Suppose $a \equiv b$ and $x \equiv y$. So for any $c$, if $1 \leq a x \vee c$, it follows that $1 \leq a \vee c$ and $1 \leq x \vee c$, whence $1 \leq b \vee c$ and $1 \leq y \vee c$. Then \begin{displaymath} 1 \leq b \vee c = (b \cdot 1) \vee c = b(y \vee c) \vee c = b y \vee b c \vee c = b y \vee c \end{displaymath} and similarly $1 = b y \vee c$ implies $1 = a x \vee c$. So $a x \equiv b y$. Now we show that $\equiv$ respects joins, i.e., if $x_i \equiv y_i$ for all $i \in I$, then $\bigvee_i x_i \equiv \bigvee_i y_i$. Suppose $1 = c \vee \bigvee_i x_i$. Since $Q$ is compact, there is a finite set of the $x_i$, say $x_1, \ldots, x_n$, such that $1 = c \vee x_1 \vee \ldots \vee x_n$. From $x_n \equiv y_n$ and $1 = (c \vee x_1 \vee \ldots \vee x_{n-1}) \vee x_n$, we derive \begin{displaymath} 1 = (c \vee x_1 \vee \ldots \vee x_{n-1}) \vee y_n = (y_n \vee c) \vee x_1 \vee \ldots \vee x_{n-1} \end{displaymath} and we proceed by induction to show $1 = c \vee y_1 \vee \ldots \vee y_n$, which implies $1 \leq c \vee \bigvee_{i \in I} y_i$. Similarly, $1 = c \vee \bigvee_i y_i$ implies $1 = c \vee \bigvee_i x_i$, and so we are done. \end{proof} \begin{prop} \label{quot}\hypertarget{quot}{} The quantale $\tilde{Q}$ formed as the quotient $Q/\equiv$ is a nontrivial compact frame. \end{prop} \begin{proof} Clearly $1 \leq x x \vee c$ implies $1 \leq x x \vee c \leq x \vee c$. But also if $1 \leq x \vee c$, then \begin{displaymath} 1 \leq x \vee c = x \cdot 1 \vee c = x\cdot (x \vee c) \vee c = x x \vee x c \vee c = x x \vee c \end{displaymath} and thus $x x \equiv x$ for all $x$. Being an idempotent affine quantale, $\tilde{Q}$ is a frame. We have $\neg (0 \equiv 1)$ since ($0 \vee c = 1$ iff $1 \vee c = 1$) fails for $c = 0$, under the assumption $Q$ is nontrivial. So $\tilde{Q}$ is nontrivial. The same proof shows that for \emph{any} $i \in Q$, we have $\neg (i \equiv 1)$ if $\neg (i = 1)$. To show $\tilde{Q}$ is compact, suppose $\{x_i\}_{i \in I}$ is a family in $Q$ such that $\bigvee_i x_i \equiv 1$, in other words such that $c \vee \bigvee_i x_i = 1$ for all $c \in Q$. Setting $c = 0$ and applying compactness of $Q$, there is a finite subfamily $F$ such that $\bigvee_{i \in F} x_i = 1$, and then $\bigvee_{i \in F} x_i \equiv 1$ which proves compactness of $\tilde{Q}$. \end{proof} The quantale quotient map $Q \to \tilde{Q}$ preserves arbitrary sups and thus has a right adjoint $\pi: \tilde{Q} \to Q$, by the poset form of the [[adjoint functor theorem]]. If we denote the $\equiv$-class of an element $a \in Q$ by $[a]$, then for $c \in \tilde{Q}$ the element $\pi(c)$ is given by the explicit formula \begin{displaymath} \pi(c) = \bigvee \{y \in Q: [y] \leq c\}. \end{displaymath} \begin{lemma} \label{inverse}\hypertarget{inverse}{} Given a regular epi $[-]: Q \to \tilde{Q}$ in the category of quantales, with right adjoint $\pi: \tilde{Q} \to Q$, if $c$ is prime in $\tilde{Q}$, then $\pi(c)$ is prime in $Q$. \end{lemma} \begin{proof} For elements $a, b \in Q$ we have \begin{displaymath} \itexarray{ a b \leq \pi(c) & iff & [a b] \leq c & since \; [-] \dashv \pi \\ & iff & [a] \cdot [b] \leq c & since \; [-]\; is\; \mathrm{a}\; quantale\; map \\ & iff & ([a] \leq c) \vee ([b] \leq c) & since \; c \; is\; prime \\ & iff & (a \leq \pi(c)) \vee (b \leq \pi(c)) & since \; [-] \dashv \pi } \end{displaymath} which completes the proof. \end{proof} The proof of Theorem \ref{quantale} is immediate: \begin{proof} Given that $Q$ is a nontrivial compact affine quantale, $\tilde{Q}$ is a nontrivial compact frame by Proposition \ref{quot}. Then $\tilde{Q}$ has a prime element $c$ by Banaschewski's lemma, whence $Q$ has a prime element by Lemma \ref{inverse}. \end{proof} \begin{cor} \label{}\hypertarget{}{} \textbf{(PIT for rings)} Every unital ring $R$ has a prime ideal under ZF + (UF). \end{cor} \begin{remark} \label{}\hypertarget{}{} See also \hyperlink{BH}{Banaschewski-Harting}. We remark that the nucleus $k$ on $Idl(R)$ formed by the composition $k = \pi \circ [-]: Idl(R) \to Idl(R)$ has the following properties: \begin{itemize}% \item $k(I \cap J) = k(I J) = k(I) \cap k(J)$, \item $k(J) = 1$ implies $J = 1$. \end{itemize} These properties are all that is needed to verify that the fixed points of $k$ (corresponding to the quotient $\widetilde{Idl(R)}$) forms a compact frame to which we can apply Banaschewski's lemma. For example, the nucleus obtained by taking the Jacobson [[radical]] of an ideal has these properties, as do other radicals considered in noncommutative ring theory (Levitski radical, Brown-McCoy radical). \end{remark} In fact the same methods show that we can strengthen Theorem \ref{quantale} to get what we really mean by a PIT: \begin{cor} \label{pit}\hypertarget{pit}{} Let $Q$ be a nontrivial compact affine quantale, and let $i \in Q$ be any \emph{proper} element, i.e., assume $\neg (i = 1)$. Then there exists a prime element $p \in Q$ such that $i \leq p$. \end{cor} \begin{proof} Let $k = \pi \circ [-]: Q \to Q$ be the \href{/nlab/show/quantale#quantale_congruences_and_nuclei}{nucleus} corresponding to the congruence $\equiv$ (i.e., the regular epi $[-]: Q \to \tilde{Q}$). Since $i \neq 1$, we also have $k(i) \neq 1$ (i.e., $\neg (i \equiv 1)$), as shown in the proof of Proposition \ref{quot}. So $\tilde{Q} = Fix(k)$ and the upwards-closed set $k(i) \downarrow Fix(k)$ are both nontrivial compact affine frames, and there is a prime element $p$ of $k(i) \downarrow Fix(k)$. We have a regular epi of quantales $r$ defined as the composite \begin{displaymath} Q \stackrel{[-]}{\to} Fix(k) \stackrel{k(i) \vee -}{\to} k(i) \downarrow Fix(k) \end{displaymath} (here using the fact that $k(i) \vee -$ preserves finite meets, since $Fix(k)$ is a distributive lattice). The right adjoint of $r$ is the inclusion $\rho: k(i) \downarrow Fix(k) \hookrightarrow Q$, and it follows from Lemma \ref{inverse} that $p = \rho(p)$ is a prime of $Q$ such that $k(i) \leq p$. Since $i \leq k(i)$, we conclude $i \leq p$. \end{proof} \hypertarget{generalized_prime_ideal_theorems}{}\subsubsection*{{Generalized prime ideal theorems}}\label{generalized_prime_ideal_theorems} Now we consider more general settings in which we can speak of (two-sided) ideals and prime ideals, and to which we can apply Theorem \ref{quantale}. For example, let $\mathbf{C}$ be a [[complete category|complete]], [[cocomplete category|cocomplete]] [[biclosed monoidal category]] (e.g., a [[cosmos]]). If $A$ is a [[monoid]] object in $\mathbf{C}$, then we can speak of [[ideal in a monoid|ideals]] in $A$, and typically $Idl(A)$ will inherit good properties from $\mathbf{C}$. If for example $\mathbf{C}$ is regular and well-powered, then $Idl(A)$ forms a quantale under multiplication of ideals, as discussed \href{/nlab/show/ideal+in+a+monoid#ideals_forming_a_quantale}{here}. If we further assume that the monoidal unit $I$ of $\mathbf{C}$ is [[compact object|compact]] (i.e., finitely presented), then the top element of $Idl(A)$ generated by the monoid unit $e: I \to A$ will be a compact element. Then, defining a prime ideal in $A$ as usual to be a prime element in $Idl(A)$, we deduce existence of prime ideals from Theorem \ref{quantale}. Here is a sample result along these lines: \begin{theorem} \label{gpit}\hypertarget{gpit}{} Let $T$ be a [[commutative theory|commutative Lawvere theory]]. Then the category of algebras $Set^T$ is a well-powered regular cosmos in which the monoidal unit is compact. Consequently, for every monoid $A$ of $Set^T$ and every proper ideal $I \hookrightarrow A$, there is a prime ideal $P$ containing $I$ (by applying Corollary \ref{pit} to $Idl(A)$). \end{theorem} \begin{cor} \label{}\hypertarget{}{} \textbf{(PIT for rigs)} Every proper ideal in a [[rig]] is contained in a prime ideal. \end{cor} \begin{proof} Take $T$ to be the theory of [[commutative monoids]], and apply Theorem \ref{gpit}. \end{proof} \hypertarget{references}{}\subsection*{{References}}\label{references} \begin{itemize}% \item [[Bernhard Banaschewski]] and Roswitha Harting, \emph{Lattice Aspects of Radical Ideals and Choice Principles}, Proc. London Math. Soc. s3-50 (3) (1985), 385-404. (\href{http://plms.oxfordjournals.org/content/s3-50/3/385.extract}{web}) \end{itemize} \begin{itemize}% \item Bernhard Banaschewski, \emph{Prime Elements from Prime Ideals}, Order 2 (1985), 211-213. (\href{http://link.springer.com/article/10.1007%2FBF00334858}{Springer link}) \end{itemize} \begin{itemize}% \item Jan Paseka, \emph{A note on the prime ideal theorem}, Acta Universitatis Carolinae, Mathematica et Physica, Vol. 30 (1989), No. 2, 131-136. (\href{http://dml.cz/bitstream/handle/10338.dmlcz/701805/ActaCarolinae_030-1989-2_20.pdf}{pdf}) \end{itemize} \end{document}