Part I Realizations and their obstructions
On this page · Permalink · Source line 1
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.
1 Views and coherent realizations
On this page · Permalink · Source line 2
1.1 The data of a view system
On this page · Permalink · Source line 3
Fix a small category \({\mathcal V}\), or work in fixed universes so that the products below exist in the chosen ambient universe. A view is an object of \({\mathcal 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.
Definition 1.1: View system
A view system consists of sets \(F_v\) and maps
satisfying \((1_v)^*={\operatorname{id}}\) and \((g\circ f)^*=f^*g^*\). Equivalently, it is a functor \(F:{\mathcal V}^{\mathrm{op}}\to{\mathbf{Set}}\).
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.
Definition 1.2: Strict Komorebi realization
The ambient realization set is
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\).
The raw product contains all families, including inconsistent ones. Equation (1.1) cuts out the exact families. No nonemptiness hypothesis is built into the definition.
Theorem 1.3: Joint determination and the universal property
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.
Proof
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
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\).
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,
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.
To prove uniqueness, let \(b:T\to\Gamma(F)\) be another such function. At every \(t\) and \(v\),
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.
Thus the strict construction is precisely the ordinary limit of the view diagram, with the usual limit interpretation in the sequential case [1]. This identifies its mathematical content and its universal property. It does not supply a universal view diagram for every possible mathematical question.
1.2 Maps of realizations
On this page · Permalink · Source line 53
Let \(\alpha:F\to G\) consist of maps \(\alpha_v:F_v\to G_v\) with
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.
Proposition 1.4: Functorial transport
These induced maps preserve identities and composition:
Proof
Evaluate each side at an arbitrary view and apply the corresponding identity for the coordinate maps. Theorem 1.3 then identifies the maps on the whole realization set.
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.
1.3 A global view and a useful warning
On this page · Permalink · Source line 73
Proposition 1.5: Terminal evaluation
If \(t\) is terminal in \({\mathcal V}\), evaluation induces an equivalence \(\Gamma(F)\simeq F_t\).
Proof
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\).
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.
The category of elements \(\int_{\mathcal 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.
2 Partial data, gluing, and correspondence fibers
On this page · Permalink · Source line 85
2.1 Prescribed views
On this page · Permalink · Source line 86
For \(U\subseteq{\operatorname{Ob}}{\mathcal 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
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.
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
Identities imply that this condition also covers every object.
Theorem 2.1: Strict gluing
Under (2.2), restriction induces an equivalence
Every fixed matching family has a unique global glue.
Proof
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
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
In particular the value is independent of the selected index.
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
Thus \(x\in\Gamma(F)\). Object coverage alone would not supply the common patch used in this step.
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.
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.
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.
Example 2.2: An object cover with no glue
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.
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.
2.2 Correspondences must also be coherent
On this page · Permalink · Source line 137
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
Naturality and coherence provide its restrictions. A global bridge is an element of
Theorem 2.3: Fiber and section compatibility
There is a coordinate preserving equivalence
Under a transition cover, matching local bridge sections glue to a unique global bridge with both prescribed projections unchanged.
Proof
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
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.
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.
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.
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.
These are ordinary fibers. They do not retain comparison isomorphisms or automorphisms. Section 14 constructs the appropriate groupoid version when this information matters.
2.3 Locally inhabited does not mean globally inhabited
On this page · Permalink · Source line 170
Example 2.4: The loop with no coherent choice
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.
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.
How to read the result
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.