\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*{antisubalgebra}

\hypertarget{antisubalgebras}{}\section*{{Antisubalgebras}}\label{antisubalgebras}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definitions}{Definitions}\dotfill \pageref*{definitions} \linebreak
\noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak
\noindent\hyperlink{quotient_algebras}{Quotient algebras}\dotfill \pageref*{quotient_algebras} \linebreak
\noindent\hyperlink{localic_point_of_view}{Localic point of view}\dotfill \pageref*{localic_point_of_view} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

In [[constructive mathematics]], we often do [[algebra]] by equipping an [[gebra|algebra]] with a [[tight apartness]] (and requiring the algebraic operations to be [[strongly extensional function|strongly extensional]]). In this context, it is convenient to replace [[subalgebras]] with \emph{anti}-subalgebras, which [[classical mathematics|classically]] are simply the [[complements]] of subalgebras.

\hypertarget{definitions}{}\subsection*{{Definitions}}\label{definitions}

Let us work in the context of [[universal algebra]], so an \textbf{algebra} is a [[set]] $X$ equipped with a family of [[functions]] $f_i\colon X^{n_i} \to X$ (where each [[arity]] $n_i$ is a [[cardinal number]]) that satisfy certain equational identities (which are irrelevant here). As usual, a \textbf{subalgebra} of $X$ is a [[subset]] $S$ such that $f_i(p_1,\ldots,p_{n_i}) \in S$ whenever each $p_k \in S$. There is no need, in general, to require that any arity $n_i$ be finite or that there be finitely many $f_i$; however, for a few results, we will need a special case of these that we will call having \textbf{well-behaved constants}:

\begin{itemize}%
\item each arity is either $0$ or at least $1$ (so each operation either is a constant or has at least one operand), and
\item the number of constants is [[Kuratowski-finite]] (so there is an exhaustive list $c_1, c_2, c_3, \ldots c_n$ of constants for some [[natural number]] $n$, where it remains possible that $c_i = c_j$ might be an equational law).

\end{itemize}
The first item is true of all derived operations in the theory as long as it is true of the fundamental operations in the signature; but in this last item, we're counting all derived constants, not just the fundamental ones. For example, the theory of (unital) [[rings]] does \emph{not} have well-behaved constants, because there are infinitely many constants (one for each [[integer]]).

Now we require $S$ to have a [[tight apartness]] $\ne$, which induces a tight apartness on each $X^{n_i}$ (via [[existential quantification]]), and we require the operations $f_i$ to be [[strongly extensional function|strongly extensional]]. An algebra $X$ with these properties is called an \textbf{inequality algebra}. (For much of the theory we don't need the apartness to be tight, but for some purposes it is necessary.)

A [[subset]] $A$ of $X$ is \textbf{[[open subset|open]]} (or $\ne$-open) if, whenever $p \in A$, $q \in A$ or $p \ne q$. An \textbf{antisubalgebra} of $X$ is an open subset $A$ such that $p_j \in A$ for some $j$ whenever $f_i(p_1,\ldots,p_{n_i}) \in A$ for any $i$. By taking the [[contrapositive]], we see that the [[complement]] of $A$ is a subalgebra $S$, but we cannot (in general) start with a subalgebra $S$ and get an antisubalgebra $A$. (Impredicatively, we can take the antisubalgebra generated, as described below, by the $\ne$-complement of $S$, that is the set of those elements of $X$ that $\ne$ every element of $S$, but its complement will generally only be a superset of $S$.)

\hypertarget{examples}{}\subsection*{{Examples}}\label{examples}

Unless otherwise noted, all of the constructions in these examples should be [[predicative mathematics|predicative]].

The [[empty subset]] of any algebra is an antisubalgebra, the \textbf{empty antisubalgebra} or \textbf{improper antisubalgebra}, whose complement is the [[improper subset|improper]] subalgebra (which is all of $X$). An antisubalgebra is \textbf{[[proper subset|proper]]} if it is [[inhabited subset|inhabited]]; the ability to have a positive definition of when an antisubalgebra is proper is a significant motivation for the concept.

If $A$ is an antisubalgebra and $c$ is a constant (given by an operation $X^0 \to X$ or a composite of same with other operations), then $p \ne c$ whenever $p \in A$. If the theory has well-behaved constants, then we can define the \textbf{trivial antisubalgebra} to be the subset of those elements $p$ such that $p \ne c$ for each constant $c$ (the $\ne$-complement of the [[trivial subalgebra]]). In general, we may also take the \textbf{trivial antisubalgebra} to be the [[union]] of all antisubalgebras (but this is not predicative).

Instead of [[subgroups]], use antisubgroups. In this case the definition can be simplified a bit: a subset $A$ of an inequality group $X$ is an \textbf{antisubgroup} if $p \ne 1$ whenever $p \in A$, $p \in A$ or $q \in A$ whenever $p q \in A$, and $p \in A$ whenever $p^{-1} \in A$. We need not assume that $A$ is open; this can be proved from strong extensionality of the group operations on $X$ and the stronger form of the nullary anticlosure condition (``$p \ne 1$ whenever $p \in A$'' is a strengthening of the condition $\neg (1\in A)$ that would be the literal nullary case of the general definition.) An antisubgroup $A$ is \textbf{[[normal subgroup|normal]]} if $p q \in A$ whenever $q p \in A$. The \textbf{[[trivial subgroup|trivial]] antisubgroup} is the $\ne$-complement of $\{1\}$.

Instead of [[ideals]] (of [[rings]]), use antiideals. (Technically, these are antisubalgebras of the ring as a module over itself.) Again we can omit $\ne$-openness by strengthening the nullary condition. In detail, a subset $A$ of $X$ is a \textbf{two-sided antiideal} (or simply an \textbf{antiideal} in the commutative case) if $p \ne 0$ whenever $p \in A$, $p \in A$ or $q \in A$ whenever $p + q \in A$, and $p \in A$ and $q \in A$ whenever $p q \in A$. $A$ is a \textbf{left antiideal} if instead the last condition requires only that $p \in A$, and $A$ is a \textbf{right antiideal} if instead the last condition requires only that $q \in A$. It follows that an antiideal $A$ is proper iff $1 \in A$. $A$ is \textbf{[[prime ideal|prime]]} (or \emph{antiprime}) if it is proper and $p r q \in A$ for some $r$ whenever $p \in A$ and $q \in A$; in the commutative case, we can say that $p q \in A$ whenever $p \in A$ and $q \in a$. $A$ is \textbf{[[maximal ideal|minimal]]} (or \emph{antimaximal}) if it is proper and, for each $p \in A$, for some $q$, for each $r \in A$, $p q + r \ne 1$ and $q p + r \ne 1$ (which is constructively stronger than being prime and [[minimal element|minimal]] among proper ideals); of course, we only need one of these two inequalities in the commutative case. The \textbf{[[trivial ideal|trivial]] antiideal} is the $\ne$-complement of $\{0\}$.

Note that a [[union]] of antisubalgebras is again an antisubalgebra. Given any subset $B$ of $X$, the antisubalgebra \textbf{generated} by $B$ is the union of all antisubalgebras contained in $B$. (This construction is not predicative, although it may still be true predicatively that the generated subalgebra exists in some situations.)

In some cases, we may prefer to anti-generate: given any subset $B$ of $X$, the antisubalgebra \textbf{antigenerated} by $B$ is the union of all antisubalgebras whose elements are all distinct from ($\ne$) each element of $B$, in other words the antisubalgebra generated by the $\ne$-complement of $B$. For example, the trivial antisubgroup of a group is antigenerated by $\{1\}$, and the trivial antiideal of a ring is antigenerated by $\{0\}$. More generally than these examples, we may talk of the \textbf{[[cyclic subgroup|cyclic antisubgroup]]} or \textbf{[[principal ideal|principal antiideal]]} antigenerated by a given element of the group or ring.

\hypertarget{quotient_algebras}{}\subsection*{{Quotient algebras}}\label{quotient_algebras}

To form a [[quotient group]] or a [[quotient ring]], it's enough to have a [[normal subgroup]] or a [[two-sided ideal]]. However, if we want the quotient algebra to inherit an apartness from the original algebra, then we need antisubgroups and antiideals.

In general, instead of [[congruence relations]], use anticongruence relations. An \textbf{anticongruence relation} $K$ on $X$ is an [[apartness relation]] on $X$ that is also an antisubalgebra of $X \times X$. Given this, let $R$ be the [[negation]] of $K$; then $R$ is a congruence relation, giving a quotient algebra $X/R$. Furthermore, $K$ becomes a [[tight relation|tight]] apartness on $X/R$, relative to which the algebra operations on $X/R$ are strongly extensional. We denote the resulting algebra-with-apartness by $X/K$. (This notation should cause no confusion; if an apartness relation on a set $X$ is also an equivalence relation, then $X$ must be the [[empty set]], which has a unique apartness and at most one algebra structure, and the only [[quotient set]] of the empty set is itself.) The quotient map $X \twoheadrightarrow X/K$ is also strongly extensional.

Conversely, any strongly extensional map $f\colon X \to Y$ between algebras with apartness gives rise to an anticongruence $\aker f$ on $X$ (the \textbf{antikernel} of $f$), where $(p, q) \in \aker f$ iff $f(p) \ne f(q)$. The complement of the antikernel is (because the apartness of $Y$ is tight) the [[kernel]] in the usual sense of universal algebra. Thus, the quotient algebra $X/(\aker f)$ is [[naturally isomorphic]] to a [[subalgebra]] $im f$ of $Y$; the maps $X \twoheadrightarrow X/(\aker f) \cong \im f \hookrightarrow Y$ are strongly extensional. Similarly, a sequence $X \overset{f}\to Y \overset{g} \to Z$ is [[exact sequence|exact]] iff $\im f$ is the complement of $\aker g$.

(We would like to say that there is an antisubalgebra $\aim f$ of $Y$ whose complement is $\im f$; then we could, for example, define a stronger notion of exactness requiring that $\aker g$ equal the antiimage of $f$. In principle, $\aim f$ should be the $\ne$-complement of $\im f$. If $X$ is Kuratowski-finite, then this works, but in general, we can prove neither that this is open nor that its complement is all of $\im f$.)

Given a group-with-apartness and a normal antisubgroup $A$, we define an anticongruence $K$, where $(p, q) \in K$ iff $p q^{-1} \in A$. Similarly, given a ring-with-apartness and a two-sided antiideal $A$, we define an anticongruence $K$, where $(p, q) \in K$ iff $p - q \in A$. This allows us to form quotient groups or quotient rings by modding out by normal antisubgroups or two-sided antiideals. Conversely, we can interpret the antikernel as a normal antisubgroup or two-sided antiideal: $p \in \aker f$ iff $f(p) \ne 1$, $p \in \aker f$ iff $f(p) \ne 0$, etc. In general, this works for any [[Omega-group]] structure.

\hypertarget{localic_point_of_view}{}\subsection*{{Localic point of view}}\label{localic_point_of_view}

As noted at [[apartness relation]], an apartness relation on a set $X$ is equivalent to a (strongly) closed [[equivalence relation]] on the corresponding [[discrete locale]], and the $\ne$-open subsets are those whose complementary closed sublocales are stable under this equivalence relation, and the $\ne$-topology itself is the corresponding quotient locale. From this point of view, an algebra structure is strongly extensional if it respects the equivalence relation, hence passes to the quotient; and an antisubalgebra is an $\ne$-open set whose complementary closed sublocale is additionally a localic subalgebra, since the operation $\mathsf{C}$ from open sublocales to closed ones takes arbitrary (not only finite) unions to intersections.

In other words, antisubalgebras of an inequality algebra are equivalent to closed subalgebras of a localic algebra, in the case when the latter is the quotient of a discrete algebra by a closed localic congruence.

\hypertarget{references}{}\subsection*{{References}}\label{references}

According to \hyperlink{TvD}{Troelstra and van Dalen}:

\begin{quote}%
The study of algebraic structures in an intuitionistic setting was undertaken by Heyting (\hyperlink{Heyting1941}{1941})\ldots{} in full generality, equipped with an apartness relation. The notion of an antisubstructure, implicit in Heyting's treatment of ideals in polynomial rings, was formulated explicitly by D.S. Scott (\hyperlink{Scott1979}{1979}) (N.B. the first draft of this paper contains a good deal more than the published version). Ruitenburg (\hyperlink{Ruitenberg1982Thesis}{1982}, \hyperlink{Ruitenberg1982}{1982A}) deals with intuitionistic algebra in the spirit of Heyting and Scott.


\end{quote}
\begin{itemize}%
\item [[Arend Heyting]], \emph{Untersuchungen \"u{}ber intuitionistische Algebra}, 1941


\item [[Dana Scott]], \emph{Identity and existence in intuitionistic logic}, 1979


\item [[Wim Ruitenberg]], \emph{Intuitionistic Algebra}, Ph.D. Thesis, Rijksuniversiteit Utrecht, 1982


\item [[Wim Ruitenberg]], \emph{Primality and invertibility of polynomials}, 1982


\item Surprisingly, antisubalgebras make hardly any appearence in [[Ray Mines]], [[Fred Richman]], [[Wim Ruitenburg]]. \emph{A Course in Constructive Algebra}. Springer, 1987.


\item More can be found in [[Anne Troelstra]] and [[Dirk van Dalen]], \emph{Constructivism in Mathematics} (volume 2).



\end{itemize}
[[!redirects antisubalgebra]] [[!redirects antisubalgebras]] [[!redirects anti-subalgebra]] [[!redirects anti-subalgebras]]

[[!redirects empty antisubalgebra]] [[!redirects empty antisubalgebras]] [[!redirects empty anti-subalgebra]] [[!redirects empty anti-subalgebras]]

[[!redirects improper antisubalgebra]] [[!redirects improper antisubalgebras]] [[!redirects improper anti-subalgebra]] [[!redirects improper anti-subalgebras]]

[[!redirects proper antisubalgebra]] [[!redirects proper antisubalgebras]] [[!redirects proper anti-subalgebra]] [[!redirects proper anti-subalgebras]]

[[!redirects antisubgroup]] [[!redirects antisubgroups]] [[!redirects anti-subgroup]] [[!redirects anti-subgroups]]

[[!redirects normal antisubgroup]] [[!redirects normal antisubgroups]] [[!redirects normal anti-subgroup]] [[!redirects normal anti-subgroups]]

[[!redirects trivial antisubgroup]] [[!redirects trivial antisubgroups]] [[!redirects trivial anti-subgroup]] [[!redirects trivial anti-subgroups]]

[[!redirects antiideal]] [[!redirects antiideals]] [[!redirects anti-ideal]] [[!redirects anti-ideals]]

[[!redirects left antiideal]] [[!redirects left antiideals]] [[!redirects left anti-ideal]] [[!redirects left anti-ideals]]

[[!redirects right antiideal]] [[!redirects right antiideals]] [[!redirects right anti-ideal]] [[!redirects right anti-ideals]]

[[!redirects two-sided antiideal]] [[!redirects two-sided antiideals]] [[!redirects two-sided anti-ideal]] [[!redirects two-sided anti-ideals]]

[[!redirects prime antiideal]] [[!redirects prime antiideals]] [[!redirects prime anti-ideal]] [[!redirects prime anti-ideals]]

[[!redirects minimal antiideal]] [[!redirects minimal antiideals]] [[!redirects minimal anti-ideal]] [[!redirects minimal anti-ideals]]

[[!redirects trivial antiideal]] [[!redirects trivial antiideals]] [[!redirects trivial anti-ideal]] [[!redirects trivial anti-ideals]]

[[!redirects generated antisubalgebra]] [[!redirects generated antisubalgebras]] [[!redirects antisubalgebra generated]] [[!redirects antisubalgebras generated]] [[!redirects generated anti-subalgebra]] [[!redirects generated anti-subalgebras]] [[!redirects anti-subalgebra generated]] [[!redirects anti-subalgebras generated]]

[[!redirects generated antisubgroup]] [[!redirects generated antisubgroups]] [[!redirects antisubgroup generated]] [[!redirects antisubgroups generated]] [[!redirects generated anti-subgroup]] [[!redirects generated anti-subgroups]] [[!redirects anti-subgroup generated]] [[!redirects anti-subgroups generated]]

[[!redirects generated antiideal]] [[!redirects generated antiideals]] [[!redirects antiideal generated]] [[!redirects antiideals generated]] [[!redirects generated anti-ideal]] [[!redirects generated anti-ideals]] [[!redirects anti-ideal generated]] [[!redirects anti-ideals generated]]

[[!redirects antigenerated antisubalgebra]] [[!redirects antigenerated antisubalgebras]] [[!redirects antisubalgebra antigenerated]] [[!redirects antisubalgebras antigenerated]] [[!redirects anti-generated anti-subalgebra]] [[!redirects anti-generated anti-subalgebras]] [[!redirects anti-subalgebra anti-generated]] [[!redirects anti-subalgebras anti-generated]]

[[!redirects antigenerated antisubgroup]] [[!redirects antigenerated antisubgroups]] [[!redirects antisubgroup antigenerated]] [[!redirects antisubgroups antigenerated]] [[!redirects anti-generated anti-subgroup]] [[!redirects anti-generated anti-subgroups]] [[!redirects anti-subgroup anti-generated]] [[!redirects anti-subgroups anti-generated]]

[[!redirects antigenerated antiideal]] [[!redirects antigenerated antiideals]] [[!redirects antiideal antigenerated]] [[!redirects antiideals antigenerated]] [[!redirects anti-generated anti-ideal]] [[!redirects anti-generated anti-ideals]] [[!redirects anti-ideal anti-generated]] [[!redirects anti-ideals anti-generated]]

[[!redirects cyclic antisubgroup]] [[!redirects cyclic antisubgroups]] [[!redirects cyclic anti-subgroup]] [[!redirects cyclic anti-subgroups]]

[[!redirects principal antiideal]] [[!redirects principal antiideals]] [[!redirects principal anti-ideal]] [[!redirects principal anti-ideals]]

[[!redirects anticongruence]] [[!redirects anticongruences]] [[!redirects anti-congruence]] [[!redirects anti-congruences]] [[!redirects anticongruence relation]] [[!redirects anticongruence relations]] [[!redirects anti-congruence relation]] [[!redirects anti-congruence relations]]

[[!redirects antikernel]] [[!redirects antikernels]] [[!redirects anti-kernel]] [[!redirects anti-kernels]]

[[!redirects strongly exact sequence]] [[!redirects strongly exact sequences]]



\end{document}