\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*{closure operator} \begin{quote}% For the closure of a subset of a topological space, see at \emph{[[closed subset]]}. \end{quote} \vspace{.5em} \hrule \vspace{.5em} \hypertarget{context}{}\subsubsection*{{Context}}\label{context} \hypertarget{modalities_closure_and_reflection}{}\paragraph*{{Modalities, Closure and Reflection}}\label{modalities_closure_and_reflection} [[!include modalities - contents]] \hypertarget{contents}{}\section*{{Contents}}\label{contents} \noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak \noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak \noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak \noindent\hyperlink{InducedClosureOnSlices}{Induced closure on slices}\dotfill \pageref*{InducedClosureOnSlices} \linebreak \noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak \hypertarget{idea}{}\subsection*{{Idea}}\label{idea} A \emph{closure operator} is a [[monad]] on a [[poset]], typically a [[poset of subobjects]] (of some [[object]]) in some [[category]]. In [[logic]], this is often referred to as a (monadic) \emph{[[modal operator]]}. The elements of the poset that are fixed by the closure operator are called \emph{closed} (or perhaps \emph{[[modal type|modal]]}). Dually, a [[comonad]] on a poset is called a \emph{co-closure operator} and the elements fixed by it are called \emph{co-closed}. More generally, in [[type theory]]/[[category theory]], we may think of any [[idempotent monad]] on a [[category]] as being a closure operator, and of any idempotent [[comonad]] as a co-closure operator. \hypertarget{definition}{}\subsection*{{Definition}}\label{definition} \begin{defn} \label{ClosureOperatorAsMonad}\hypertarget{ClosureOperatorAsMonad}{} For $\mathcal{C}$ a [[category]], a \textbf{closure operator} $\diamond$ on $\mathcal{C}$ is an [[idempotent monad]] on $\mathcal{C}$, hence an [[endofunctor]] $\diamond \colon \mathcal{C} \to \mathcal{C}$ equipped with [[unit of a monad|unit]] and product [[natural transformations]] \begin{itemize}% \item $\eta_{\diamond} \;\colon\; id_{\mathcal{C}} \to \diamond$ \item $\mu_{\diamond} \;\colon\; \diamond \circ \diamond \to \diamond$ \end{itemize} such that the [[monad]]-axioms hold and such that the following equivalent conditions hold (idempotency) \begin{itemize}% \item the product map is an [[isomorphism]]; \item $\eta_{\diamond(-)}$ is an isomorphism. \end{itemize} \end{defn} \begin{defn} \label{ClosureAndClosedObjects}\hypertarget{ClosureAndClosedObjects}{} For $\diamond \colon \mathcal{C} \to \mathcal{C}$ a closure operator, def. \ref{ClosureOperatorAsMonad}, and for $X \in \mathcal{C}$ an object, we say that \begin{itemize}% \item $\diamond X \in \mathcal{C}$ is the \textbf{$\diamond$-closure} of $X$; \item $\eta_{X} \colon X \to \diamond X$ is the \textbf{closing map} or \textbf{map to the closure}; \item $X$ is \textbf{$\diamond$-closed} precisely if $\eta_X$ is an [[isomorphism]]. \end{itemize} We write \begin{displaymath} \mathcal{C}_\diamond \hookrightarrow \mathcal{C} \end{displaymath} for the [[full subcategory]] on the $\diamond$-closed objects. \end{defn} \hypertarget{examples}{}\subsection*{{Examples}}\label{examples} \begin{itemize}% \item A closure operator on a [[power set]] is also called a \emph{[[Moore closure]]}. See there for more. \item One well-known example of a Moore closure is [[topological closure]], which is precisely a Moore closure that preserves finite joins (unions). Similarly, one can view \emph{[[topological interior]]} as a co-closure operator on a power set that preserves finite meets, or dually as a closure operator on the \emph{[[opposite poset|opposite]]} of a power set that preserves finite [[joins]] (given by [[intersections]] of subsets). \item A [[Lawvere-Tierney topology]] is a closure operator on the [[subobject classifier]] $\Omega$ of a [[topos]] $E$, viewed as an internal [[meet-semilattice]]. More precisely, it is a just such a closure operator that preserves internal finite meets. Externally, $\hom(-, \Omega) \colon E^{op} \to Set$ provides an example of a [[universal closure operator]]. \end{itemize} \hypertarget{InducedClosureOnSlices}{}\subsection*{{Induced closure on slices}}\label{InducedClosureOnSlices} We discuss here how a closure operator on a [[topos]] may induce closure operators on each of its [[slice categories]]. Throughout, our [[topos]] is denoted $\mathcal{C}$. Given a [[monad]] $\diamond \colon \mathcal{C} \to \mathcal{C}$ we write $\eta_\diamond \colon id_{\mathcal{C}} \to \diamond$ for its [[unit of a monad|unit]], and write $\mu_\diamond \colon \diamond \circ \diamond \to \diamond$ for its multiplication. As we proceed, we add assumptions on $\diamond$, such as that it preserves certain [[limits]] and/or that it be [[idempotent monad|idempotent]]. For $X \in \mathcal{C}$ any [[object]], we write $\mathcal{C}_{/X}$ for the [[slice topos]] over it. The corresponding [[base change geometric morphism]] ([[dependent sum]] $\dashv$ [[context extension]] $\dashv$ [[dependent product]]) we write \begin{displaymath} \left( \underset{X}{\sum} \dashv X^\ast \dashv \underset{X}{\prod} \right) \;\colon\; \mathcal{C}_{/X} \stackrel{\overset{\sum_X}{\to}}{\stackrel{\overset{X^\ast}{\leftarrow}}{\underset{\prod_X}{\to}}} \mathcal{C} \,. \end{displaymath} We denote an object $p \in \mathcal{C}_{/X}$ in the slice also by the corresponding [[morphism]] \begin{displaymath} p \coloneqq \left( \left(\sum_X p\right) \stackrel{p}{\to} X \right) \coloneqq \sum_X \left( p \to \ast_{X} \right) \end{displaymath} in $\mathcal{C}$, which is the image under [[dependent sum]] of the unique morphism from $p$ to the [[terminal object]] in $\mathcal{C}_{/X}$. Accordingly, a morphism $\phi \colon p_1 \to p_2$ in the slice we also denote by the corresponding triangular [[commuting diagram]] \begin{displaymath} \left( \itexarray{ \sum_X p_1 &&\stackrel{\sum_X \phi}{\to}&& \sum_X p_2 \\ & {}_{\mathllap{p}_1}\searrow && \swarrow_{\mathrlap{p_2}} \\ && X } \right) \end{displaymath} in $\mathcal{C}$. Here we study the following endofunctors on slices induced from a monad on the total topos. \begin{defn} \label{InducedOperatorOnSlice}\hypertarget{InducedOperatorOnSlice}{} For $\diamond \colon \mathcal{C} \to \mathcal{C}$ an [[monad]] on a [[topos]] $\mathcal{C}$, and for $X \in \mathcal{C}$ any [[object]], the \textbf{induced operator} \begin{displaymath} \diamond_{/X} \colon \mathcal{C}_{/X} \to \mathcal{C}_{/X} \end{displaymath} on the [[slice topos]] $\mathcal{C}_{/X}$ is the [[functor]] which sends an object $(E \stackrel{p}{\to} X) \in \mathcal{C}_{/X}$ to $(X \underset{\diamond X}{\times} \diamond E \stackrel{\eta_\diamond(X)^\ast \diamond p}{\to} X)$, hence to the left vertical morphism in the [[pullback]] [[diagram]] \begin{displaymath} \itexarray{ X \underset{\diamond X}{\times} \diamond E &\to& \diamond E \\ \downarrow^{\mathrlap{\eta_\diamond(X)^\ast \diamond p}} && \downarrow^{\mathrlap{\diamond p}} \\ X &\stackrel{\eta_\diamond(X)}{\to}& \diamond X } \,, \end{displaymath} regarded as an object in $\mathcal{C}_{/X}$, and which sends morphisms to the corresponding universal maps between these pullbacks: \begin{displaymath} \diamond_{/X} \;\; \colon \;\; \left( \itexarray{ E_1 &&\stackrel{\phi}{\to}&& E_2 \\ & \searrow && \swarrow \\ && X } \right) \;\; \mapsto \;\; \left( \itexarray{ X \underset{\diamond X}{\times} \diamond E_1 && \stackrel{X \underset{\diamond X}{\times} \diamond \phi}{\to} && X \underset{\diamond X}{\times} \diamond E_2 \\ & \searrow && \swarrow \\ && X } \right) \,. \end{displaymath} \end{defn} We now want to identify conditions under which $\diamond_{/X}$ is itself a monad. First observe that the [[unit of a monad|unit]]-like map is canonically present. \begin{prop} \label{SliceOperatorHasUnit}\hypertarget{SliceOperatorHasUnit}{} In the situation of def. \ref{InducedOperatorOnSlice}, there is a [[natural transformation]] \begin{displaymath} \eta_{\diamond_{/X}} \;\colon\; id_{\mathcal{C}_{/X}} \to \diamond_{/X} \end{displaymath} from the identity on the slice to the induced operator on the slice, whose component over an object $(E \stackrel{p}{\to} X) \in \mathcal{C}_{/X}$ is the universal morphism into the defining [[pullback]] in def. \ref{InducedOperatorOnSlice} induced from the naturality of the $\diamond$-unit $\eta_{\diamond}$: \begin{displaymath} \itexarray{ \eta_{\diamond}(E) \colon & E &\stackrel{\sum_{X} \left(\eta_{\diamond_{/X}}\left(p\right)\right) }{\to}& X \underset{\diamond X}{\times} \diamond E &\to& \diamond E \\ & &{}_{\mathllap{p}}\searrow& \downarrow^{\mathrlap{\eta_\diamond(X)^\ast \diamond p}} && \downarrow^{\diamond \mathrlap{p}} \\ & && X &\stackrel{\eta_\diamond(X)}{\to}& \diamond X } \,, \end{displaymath} \end{prop} \begin{proof} We have to show that for all morphisms \begin{displaymath} \left( \itexarray{ E_1 &&\stackrel{f}{\to}&& E_2 \\ & {}_{\mathllap{p_1}}\searrow && \swarrow_{\mathrlap{p_2}} \\ && X } \right) \end{displaymath} in $\mathcal{C}_{/X}$ the induced diagram \begin{displaymath} \itexarray{ E_1 &\stackrel{\sum_X (\eta_{\diamond_{/X}}(p_1) )}{\to}& X \underset{\diamond X}{\times} \diamond E_1 \\ \downarrow^{\mathrlap{f}} && \downarrow^{\mathrlap{X \underset{\diamond X}{\times} \diamond f }} \\ E_2 &\stackrel{\sum_X (\eta_{\diamond_{/X}}(p_2) )}{\to}& X \underset{\diamond X}{\times} \diamond E_2 } \end{displaymath} in $\mathcal{C}$ commutes. Inspection of the defining pullback diagram shows that both composites in this diagram constitute [[cones]] over the pullback diagram that defines the bottom right object. Therefore by the [[universal property]] of the pullback they have to coincide. \end{proof} Next, to have also a product operation on the induced operator $\diamond_{/X}$ we need that $\diamond$ preserves some pullbacks: \begin{prop} \label{ProductOnSliceOperator}\hypertarget{ProductOnSliceOperator}{} Assume that the monad $\diamond \colon \mathcal{C} \to \mathcal{C}$ preserves [[pullbacks]] over objects in its image. Then for each $X \in \mathcal{C}$ the induced endofunctor $\diamond_{/X}$ of def. \ref{InducedOperatorOnSlice} comes with a [[natural transformation]] \begin{displaymath} \mu_{\diamond_{/X}} \;\colon\; \diamond_{/X} \circ \diamond_{/X} \to \diamond_{/X} \end{displaymath} whose component on an object $(E \stackrel{p}{\to} X) \in \mathcal{C}_{/X}$ is the pullback of the component $\mu_{\diamond} E$ of the product of $\diamond$ itself over the component $\mu_\diamond X$ along the unit components $\eta_{\diamond} X$. \end{prop} \begin{proof} First we produce the component map as claimed, then we show that it is indeed the component of a natural transformation. So for $p \in \mathcal{C}_{/X}$ an object in the slice, consider the defining pullback diagram of $\diamond_{/X} p$ from def. \ref{InducedOperatorOnSlice} \begin{displaymath} \itexarray{ X \underset{\diamond X}{\times} \diamond E &\to& \diamond E \\ \downarrow^{\mathrlap{\eta_\diamond(X)^\ast \diamond p}} && \downarrow^{\mathrlap{\diamond p}} \\ X &\stackrel{\eta_\diamond(X)}{\to}& \diamond X } \,. \end{displaymath} By the assumption that $\diamond$ preserves pullback diagrams of this form, application of $\diamond$ yields the pullback diagram \begin{displaymath} \itexarray{ \diamond( X \underset{\diamond X}{\times} \diamond E ) &\to& \diamond \diamond E \\ \downarrow^{\mathrlap{}} && \downarrow^{\mathrlap{\diamond \diamond p}} \\ \diamond X &\stackrel{\diamond(\eta_\diamond(X))}{\to}& \diamond \diamond X } \,. \end{displaymath} Pasting to this the pullback of its left vertical morphism along $\eta_\diamond(X)$ yields \begin{displaymath} \itexarray{ X \underset{\diamond X}{\times} \diamond(X \underset{\diamond X}{\times} \diamond E) &\to& \diamond( X \underset{\diamond X}{\times} \diamond E ) &\to& \diamond \diamond E \\ \downarrow && \downarrow^{\mathrlap{}} && \downarrow^{\mathrlap{\diamond \diamond p}} \\ X &\stackrel{\eta_\diamond X}{\to}& \diamond X &\stackrel{\diamond(\eta_\diamond(X))}{\to}& \diamond \diamond X } \,, \end{displaymath} where the total rectangle is also a pullback, by the [[pasting law]]. We now build a morphism of [[diagrams]] from the underlying [[cospan]] of this diagram to another cospan, such that the induced map on pullbacks is the component of the natural transformation that we are looking for, To this end, first paste to the above diagram the [[naturality square]] of the monad multiplication map $\mu_\diamond \colon \diamond \circ \diamond \to \diamond$ to obtain \begin{displaymath} \itexarray{ X \underset{\diamond X}{\times} \diamond(X \underset{\diamond X}{\times} \diamond E) &\to& \diamond( X \underset{\diamond X}{\times} \diamond E ) &\to& \diamond \diamond E \\ \downarrow && \downarrow^{\mathrlap{}} && \downarrow^{\mathrlap{\diamond \diamond p}} & \searrow^{\mathrlap{\mu_{\diamond}(E)}} \\ X &\stackrel{\eta_\diamond X}{\to}& \diamond X &\stackrel{\diamond(\eta_\diamond(X))}{\to}& \diamond \diamond X && \diamond E \\ && && & \searrow^{\mathrlap{\mu_\diamond X} } & \downarrow^{\mathrlap{\diamond p}} \\ && && && \diamond X } \,, \end{displaymath} Then fill in the commuting diagram that exhibits the [[unitality]] axiom of $\diamond$ to obtain \begin{displaymath} \itexarray{ X \underset{\diamond X}{\times} \diamond(X \underset{\diamond X}{\times} \diamond E) &\to& \diamond( X \underset{\diamond X}{\times} \diamond E ) &\to& \diamond \diamond E \\ \downarrow && \downarrow^{\mathrlap{}} && \downarrow^{\mathrlap{\diamond \diamond p}} & \searrow^{\mathrlap{\mu_{\diamond}(E)}} \\ X &\stackrel{\eta_\diamond X}{\to}& \diamond X &\stackrel{\diamond(\eta_\diamond(X))}{\to}& \diamond \diamond X && \diamond E \\ && &\searrow^{\mathrlap{id_{\diamond X}}} & & \searrow^{\mathrlap{\mu_\diamond X} } & \downarrow^{\mathrlap{\diamond p}} \\ && && \diamond X &\stackrel{id_{\diamond X}}{\to}& \diamond X } \,. \end{displaymath} Finally paste in an identity square, just as to manifestly exhibit a morphism of diagrams \begin{displaymath} \itexarray{ X \underset{\diamond X}{\times} \diamond(X \underset{\diamond X}{\times} \diamond E) &\to& \diamond( X \underset{\diamond X}{\times} \diamond E ) &\to& \diamond \diamond E \\ \downarrow && \downarrow^{\mathrlap{}} && \downarrow^{\mathrlap{\diamond \diamond p}} & \searrow^{\mathrlap{\mu_{\diamond}(E)}} \\ X &\stackrel{\eta_\diamond X}{\to}& \diamond X &\stackrel{\diamond(\eta_\diamond(X))}{\to}& \diamond \diamond X && \diamond E \\ &\searrow^{\mathrlap{id_X}}& &\searrow^{\mathrlap{id_{\diamond X}}} & & \searrow^{\mathrlap{\mu_\diamond X} } & \downarrow^{\mathrlap{\diamond p}} \\ && X &\stackrel{\eta_\diamond X}{\to}& \diamond X &\stackrel{id_{\diamond X}}{\to}& \diamond X } \,. \end{displaymath} Now observe that the total front [[cospan]] of morphisms is such that the [[limit]] [[cone]] over it is the [[pullback]] that defines $X \underset{\diamond X}{\times} \diamond E$. By functoriality of [[pullbacks]] (by their universal property), this induces a component morphism \begin{displaymath} \mu_{\diamond_{/X}} \;\colon\; X \underset{\diamond X}{\times} \diamond (X \underset{\diamond}{\times} \diamond E) \to X \underset{\diamond X}{\times} \diamond E \end{displaymath} as claimed. Since this is built just from universal constructions, the fact that this morphism is indeed [[natural transformation|natural]] follows as in prop. \ref{SliceOperatorHasUnit}. \end{proof} So far we have constructed from a monad that preserves pullbacks over objects in its image an operator on slices which is equipped with a unit-like and a multiplication-like transformation. We now claim that this yields indeed a monad on the slice. \begin{prop} \label{InducedOperatorOnSliceIsMonad}\hypertarget{InducedOperatorOnSliceIsMonad}{} For $\diamond \colon \mathcal{C} \to \mathcal{C}$ a [[monad]] which preserves [[pullbacks]] over objects in its image, and for $X \in \mathcal{C}$ any object, the natural transformations \begin{enumerate}% \item $\eta_{\diamond_{/X}} \colon id_{\mathcal{C}_{/X}} \to \diamond_{/X}$ of prop. \ref{SliceOperatorHasUnit} \item $\mu_{\diamond_{/X}} \colon \diamond_{/X} \circ \diamond_{/X} \to \diamond_{/X}$ from prop. \ref{ProductOnSliceOperator} \end{enumerate} constitute the unit and product of a [[monad]] structure $(\diamond_{/X}, \mu_{\diamond_{/X}}, \eta_{\diamond_{/X}})$ on the slice operator $\diamond_{/X}$ of def. \ref{InducedOperatorOnSlice}. If moreover $\diamond$ is [[idempotent monad|idemponent]], then so is $\diamond_{/X}$. \end{prop} \begin{proof} By forming cospan morphisms and inducing maps between the corresponding pullbacks, this follows from the monad structure $(\diamond, \mu_{\diamond}, \eta_{\diamond})$ by the same arguments as in the proof of prop. \ref{ProductOnSliceOperator}. \end{proof} \begin{remark} \label{}\hypertarget{}{} If $\diamond$ is an [[idempotent monad]], hence a closure operator, then, by the discussion there, the monad unit exhibits an [[equivalence of categories]] between the objects in the image of $\diamond$ and the $\diamond$-closed objects. Therefore in this case the condition that $\diamond$ preserves pullbacks over objects in its image is equivalently that it preserves pullbacks over $\diamond$-closed objects. In this form we will mostly state this condition in the following. \end{remark} \begin{prop} \label{}\hypertarget{}{} Let $\diamond \colon \mathcal{C} \to \mathcal{C}$ be an [[idempotent monad]] that preserves pullbacks over $\diamond$-closed objects. Then the closed objects $p \in \mathcal{C}_{/X}$, def. \ref{ClosureAndClosedObjects}, of the induced idempotent monad $\diamond_{/X}$ on the slice over any $X \in \mathcal{C}$ are precisely those objects $(E \stackrel{p}{\to} X)$ for which the naturality square of the $\diamond$-unit is a pullback square in $\mathcal{C}$. \end{prop} \begin{proof} By def. \ref{ClosureAndClosedObjects} we need to show that for $p \in \mathcal{C}_{/X}$ the corresponding component of the $\diamond_{/X}$-unit $\eta_{\diamond_{/X}}(p)$ is an [[isomorphism]] precisely if \begin{displaymath} \itexarray{ E &\stackrel{\eta_{\diamond} E}{\to}& \diamond E \\ \downarrow^{\mathrlap{p}} && \downarrow^{\mathrlap{\diamond p}} \\ X &\stackrel{\eta_{\diamond} X}{\to}& \diamond X } \end{displaymath} is a pullback diagram in $\mathcal{C}$. By prop. \ref{InducedOperatorOnSliceIsMonad} and prop. \ref{SliceOperatorHasUnit}, the universal map from this diagram, regarded as a [[cone]] over the underlying [[cospan]], to the limiting cone is precisely $\eta_{\diamond_{/X}}(p)$. Hence the claim follows by the universal property of the pullback. \end{proof} As a special case of def. \ref{ClosureAndClosedObjects} we are therefore now interested in the following. \begin{defn} \label{}\hypertarget{}{} For $\diamond \colon \mathcal{C} \to \mathcal{C}$ an [[idempotent monad]] which preserves pullbacks over $\diamond$-closed objects, write \begin{displaymath} (\mathcal{C}_{/X})_{\diamond_{/X}} \hookrightarrow \mathcal{C}_{/X} \end{displaymath} of the [[full subcategory]] of the [[slice topos]] on the $\diamond_{/X}$-closed objects. \end{defn} \hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts} \begin{itemize}% \item [[universal closure operator]] \item [[modal logic]] \item [[reflective factorization system]], [[stable factorization system]] \end{itemize} [[!redirects closure]] [[!redirects closures]] [[!redirects closure operator]] [[!redirects closure operators]] [[!redirects closure operation]] [[!redirects closure operations]] [[!redirects coclosure operator]] [[!redirects coclosure operators]] [[!redirects coclosure operation]] [[!redirects coclosure operations]] [[!redirects co-closure operator]] [[!redirects co-closure operators]] [[!redirects co-closure operation]] [[!redirects co-closure operations]] \end{document}