Realization Calculus: twin edition

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

1 \partnote{Realizations and their obstructions}{A global object is not added to local data by terminology. It is a family satisfying every prescribed transition equation. The first task is to construct the space of such families and to keep its possible emptiness visible.}
2 \section{Views and coherent realizations}\label{sec:views}
3 \subsection{The data of a view system}
4 Fix a small category \(\V\), or work in fixed universes so that the products below exist in the chosen ambient universe. A \emph{view} is an object of \(\V\). It can encode a resolution level, a coordinate presentation, or a context in which part of an object is visible. These interpretations are mathematical choices, not additional axioms.
5 
6 \begin{definition}[View system]
7 A view system consists of sets \(F_v\) and maps
8 \[
9  f^*:F_w\longrightarrow F_v\qquad(f:v\longrightarrow w)
10 \]
11 satisfying \((1_v)^*=\id\) and \((g\circ f)^*=f^*g^*\). Equivalently, it is a functor \(F:\V^{\mathrm{op}}\to\Set\).
12 \end{definition}
13 The direction matters. An arrow \(v\to w\) induces a restriction from the fiber at \(w\) to the fiber at \(v\). A restriction need not be invertible. A category with several arrows between two views can retain different routes between their descriptions. Replacing it by a preorder can lose those routes and the constraints they impose.
14 
15 \begin{definition}[Strict Komorebi realization]
16 The ambient realization set is
17 \begin{equation}\label{eq:ambient}
18  \mathfrak K(F)=\Gamma(F)=
19  \left\{x\in\prod_{v\in\Ob\V}F_v:
20  f^*(x_w)=x_v\text{ for every }f:v\to w\right\}.
21 \end{equation}
22 A point of \(\mathfrak K(F)\) is a whole coherent family. Its value in view \(v\) is the evaluation \(\operatorname{ev}_v(x)=x_v\).
23 \end{definition}
24 The raw product contains all families, including inconsistent ones. Equation~\eqref{eq:ambient} cuts out the exact families. No nonemptiness hypothesis is built into the definition.
25 
26 \begin{theorem}[Joint determination and the universal property]\label{KS01}
27 The evaluations jointly determine a realization. If a set \(T\) carries maps \(c_v:T\to F_v\) satisfying \(f^*c_w=c_v\), there is a unique map \(c:T\to\Gamma(F)\) satisfying \(\operatorname{ev}_v c=c_v\) for every view.
28 \end{theorem}
29 \begin{proof}
30 We first verify that the evaluation maps themselves form a compatible family. If $x\in\Gamma(F)$ and $f:v\to w$, the defining equation for $x$ gives
31 \[
32  f^*(\operatorname{ev}_w x)=f^*(x_w)=x_v=\operatorname{ev}_v x.
33 \]
34 If $x,y\in\Gamma(F)$ have equal evaluations, then $x_v=y_v$ for every $v$. Equality of functions into a dependent product gives equality of their underlying families. Membership in $\Gamma(F)$ is a property of a family, not a further choice of coordinate. Thus $x=y$.
35 
36 Now fix the compatible maps $c_v:T\to F_v$. For each $t\in T$ define a family by $x(t)_v=c_v(t)$. For every arrow,
37 \[
38  f^*x(t)_w=f^*c_w(t)=c_v(t)=x(t)_v.
39 \]
40 This calculation verifies membership in $\Gamma(F)$, so the rule $c(t)=x(t)$ defines an actual function $c:T\to\Gamma(F)$. Evaluating it gives $\operatorname{ev}_vc(t)=c_v(t)$, as required.
41 
42 To prove uniqueness, let $b:T\to\Gamma(F)$ be another such function. At every $t$ and $v$,
43 \[
44  (b(t))_v=\operatorname{ev}_v b(t)=c_v(t)=\operatorname{ev}_v c(t).
45 \]
46 Joint determination first yields $b(t)=c(t)$, and function extensionality then yields $b=c$. Nothing in this argument assumes that $T$ or $\Gamma(F)$ is inhabited. For example, when $T$ is empty there is the unique empty function. When $T$ is inhabited, existence of the compatible family $(c_v)$ is already substantive data.
47 \end{proof}
48 \source{KS01}
49 Thus the strict construction is precisely the ordinary limit of the view diagram, with the usual limit interpretation in the sequential case~\cite{stacks-limits}. This identifies its mathematical content and its universal property. It does not supply a universal view diagram for every possible mathematical question.
50 
51 \plate{01_views}{The same realization is evaluated in several views. Compatibility is imposed along the arrows, not inferred from the fact that all displayed fibers exist. The ambient family belongs to the simultaneous solution set of the transition equations.}{fig:views}
52 
53 \subsection{Maps of realizations}
54 Let \(\alpha:F\to G\) consist of maps \(\alpha_v:F_v\to G_v\) with
55 \[
56  \alpha_v f_F^*=f_G^*\alpha_w.
57 \]
58 The induced map on realizations is \(\Gamma(\alpha)(x)_v=\alpha_v(x_v)\). The naturality square is exactly what is needed to show that the image family is coherent.
59 
60 \begin{proposition}[Functorial transport]\label{KS02}
61 These induced maps preserve identities and composition:
62 \[
63  \Gamma(\id_F)=\id_{\Gamma(F)},\qquad
64  \Gamma(\beta\alpha)=\Gamma(\beta)\Gamma(\alpha).
65 \]
66 \end{proposition}
67 \begin{proof}
68 Evaluate each side at an arbitrary view and apply the corresponding identity for the coordinate maps. Theorem~\ref{KS01} then identifies the maps on the whole realization set.
69 \end{proof}
70 \source{KS02}
71 An arbitrary collection of fiber maps need not define a map on realizations. Its compatibility equations are part of the theorem, not a convention that can be omitted after a notation has been chosen.
72 
73 \subsection{A global view and a useful warning}
74 \begin{proposition}[Terminal evaluation]\label{KS03}
75 If \(t\) is terminal in \(\V\), evaluation induces an equivalence \(\Gamma(F)\simeq F_t\).
76 \end{proposition}
77 \begin{proof}
78 For \(a\in F_t\), take its restriction along the unique arrow \(v\to t\) at each view. Uniqueness of the arrow to \(t\), together with the functor laws, proves coherence. Evaluation at \(t\) recovers \(a\). Conversely, any coherent family is the restriction of its coordinate at \(t\).
79 \end{proof}
80 \source{KS03}
81 This proposition is both useful and diagnostic. If the supposedly reconstructed global object has already been placed in a terminal fiber, the limit recovers that fiber. The proposition does not prove that arbitrary partial data have a preimage there.
82 
83 The category of elements \(\int_\V F\) and \(\Gamma(F)\) also have different roles. The former organizes individual appearances and their transitions. The latter selects coherent families across all views. The category of elements serves here as explanatory notation, while the Lean formalization directly represents families and their coherence.
84 
85 \chap{Partial data, gluing, and correspondence fibers}\label{sec:glue}
86 \subsection{Prescribed views}
87 For \(U\subseteq\Ob\V\), use the full subcategory on \(U\). A partial section \(s\in\Gamma_U(F)\) satisfies all transition equations whose endpoints lie in \(U\). Define
88 \begin{equation}\label{eq:extension}
89  \Ext_U(s)=\{x\in\Gamma(F):x|_U=s\}.
90 \end{equation}
91 This fiber can be empty, a singleton, or much larger. A partial section is already coherent on its prescribed domain. A raw assignment that fails an internal transition equation is not a partial section of this kind.
92 
93 Let \((U_i)_{i\in I}\) be full patches. A matching family consists of \(s_i\in\Gamma_{U_i}(F)\) with equal values on every overlap. The relevant covering condition is
94 \begin{equation}\label{eq:transitioncover}
95  \text{for every }f:v\to w,\quad
96  \text{some }U_i\text{ contains both }v\text{ and }w.
97 \end{equation}
98 Identities imply that this condition also covers every object.
99 
100 \begin{theorem}[Strict gluing]\label{KS04}
101 Under \eqref{eq:transitioncover}, restriction induces an equivalence
102 \[
103  \Gamma(F)\simeq\Match(F,(U_i)).
104 \]
105 Every fixed matching family has a unique global glue.
106 \end{theorem}
107 \begin{proof}
108 \emph{Step 1: every coordinate can be selected.} Apply the cover condition to the identity arrow of $v$. It gives an index containing $v$. Choose one such index $i(v)$ and put
109 \[
110  x_v=(s_{i(v)})_v.
111 \]
112 The choice is an existence construction. It is not an algorithm selecting patches in a preferred order. If $v\in U_j$, matching on the overlap $U_{i(v)}\cap U_j$ gives
113 \[
114  x_v=(s_j)_v.                                                   \tag{*}
115 \]
116 In particular the value is independent of the selected index.
117 
118 \emph{Step 2: the selected coordinates satisfy every arrow equation.} For $f:v\to w$, choose a single index $j$ with $v,w\in U_j$. Formula (*) applies to both endpoints. Since the patch is full, it contains this actual arrow, even when other arrows have the same endpoints. Coherence of $s_j$ gives
119 \[
120  f^*x_w=f^*(s_j)_w=(s_j)_v=x_v.
121 \]
122 Thus $x\in\Gamma(F)$. Object coverage alone would not supply the common patch used in this step.
123 
124 \emph{Step 3: assembly and restriction are inverse.} Formula (*) proves $x|_{U_j}=s_j$ for every $j$. Conversely, start with $y\in\Gamma(F)$ and assemble its restrictions. The resulting coordinate at $v$ is $y_v$, regardless of which containing patch is chosen. Joint determination gives the original $y$. These two identities are exactly the inverse identities for the displayed equivalence.
125 
126 For uniqueness with a fixed matching family, any other glue has coordinate $(s_{i(v)})_v=x_v$ at every $v$, hence equals $x$. If the view category is empty, its product has one empty family and the same conclusion follows without making any choices.
127 \end{proof}
128 \source{KS04}
129 The proof explains why object coverage alone is insufficient. Coherence is an equation attached to an arrow, so existence of a glue must see that equation somewhere in the local data.
130 
131 \begin{example}[An object cover with no glue]\label{KS05}
132 Take two views \(0\to1\), Boolean fibers, and the identity restriction. The singleton patches cover all objects. A local value false at \(0\) and true at \(1\) agrees on the empty overlap, yet no global section realizes both values. A global family would have to assign the same Boolean to both views.
133 \end{example}
134 \source{KS05}
135 Object coverage does prove uniqueness of a possible glue. It does not prove its existence. This distinction persists when sets are replaced by objects with symmetries.
136 
137 \subsection{Correspondences must also be coherent}
138 Suppose natural maps form a span \(F\xleftarrow{p}M\xrightarrow{q}G\), and fix \(a\in\Gamma(F)\), \(b\in\Gamma(G)\). At each view define the ordinary fiber
139 \[
140  B_{a,b}(v)=\{m\in M_v:p_v(m)=a_v,\ q_v(m)=b_v\}.
141 \]
142 Naturality and coherence provide its restrictions. A global bridge is an element of
143 \[
144  \mathfrak B(a,b)=\{z\in\Gamma(M):\Gamma(p)z=a,\ \Gamma(q)z=b\}.
145 \]
146 
147 \begin{theorem}[Fiber and section compatibility]\label{KS06}
148 There is a coordinate preserving equivalence
149 \[
150  \Gamma(B_{a,b})\simeq\mathfrak B(a,b).
151 \]
152 Under a transition cover, matching local bridge sections glue to a unique global bridge with both prescribed projections unchanged.
153 \end{theorem}
154 \begin{proof}
155 We must first check that the displayed fibers really form a view system. Let $m\in B_{a,b}(w)$ and $f:v\to w$. Naturality of $p$ and coherence of $a$ give
156 \[
157  p_v(f_M^*m)=f_F^*p_w(m)=f_F^*a_w=a_v.
158 \]
159 The same calculation with $q,b$ gives $q_v(f_M^*m)=b_v$. Therefore $f_M^*m$ belongs to $B_{a,b}(v)$. Identity and composition of these restricted maps are inherited from $M$, because equality in a subset is equality of its underlying elements.
160 
161 Given $u\in\Gamma(B_{a,b})$, forget each fiber-membership condition and call the underlying family $z_v\in M_v$. Coherence of $u$ is precisely coherence of $z$, so $z\in\Gamma(M)$. The equations $p_vz_v=a_v$ hold at every coordinate. Joint determination in $\Gamma(F)$ yields $\Gamma(p)z=a$, and the equations for $q$ similarly yield $\Gamma(q)z=b$. Thus $z$ is a global bridge.
162 
163 In the opposite direction, let $z\in\mathfrak B(a,b)$. Evaluate its two global projection equations at $v$. They show that $z_v$ belongs to $B_{a,b}(v)$, and its original coherence shows that these elements form a section of the fiber system. Forgetting and reattaching membership conditions preserves every coordinate, so the two constructions are inverse.
164 
165 Finally apply strict gluing to this specific fiber system. The glued section retains its membership in every $B_{a,b}(v)$, which is why both prescribed projections survive gluing. Uniqueness is for the fixed matching bridge family. Different matching families for the same $(a,b)$ can still yield different global bridges.
166 \end{proof}
167 \source{KS06}
168 These are ordinary fibers. They do not retain comparison isomorphisms or automorphisms. Section~\ref{sec:relative} constructs the appropriate groupoid version when this information matters.
169 
170 \subsection{Locally inhabited does not mean globally inhabited}
171 \begin{example}[The loop with no coherent choice]\label{KS07}
172 Let the view category have one object and automorphism group \(C_2\). Let its nonidentity arrow act on a set with two elements by swapping the elements. The fiber is nonempty and every transport is bijective. Nevertheless a global section would be a fixed point of the swap, and there is none.
173 \end{example}
174 \source{KS07}
175 The problem is not missing local elements or noninvertible transition maps. It is the absence of an element satisfying the loop equation. Inserting a point in each fiber does not certify a coherent selection of those points.
176 
177 \begin{insight}
178 The strict theory already distinguishes three levels: possible local appearances, compatible partial descriptions, and an actual global realization. A correspondence must pass through the same levels. Local nonemptiness of its fibers is not a globalization theorem.
179 \end{insight}

Back to source controls

Back to Realization Calculus: twin edition