Realization Calculus: twin edition

Download original file

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

1 \partnote{Symmetry and effective descent}{A set of solutions forgets the witnesses relating equivalent solutions. The next layer retains those witnesses, their composition, and their automorphisms. Gluing then has to respect the overlap identifications themselves.}
2 \section{Nonabelian coherence and relative trivialization}\label{sec:gauge}
3 \subsection{Coherent transition labels}
4 Fix groups \(G_v\) and restriction homomorphisms \(f^*:G_w\to G_v\), with the same identity and composition laws as before. The groups need not be abelian and the homomorphisms need not be bijective.
5 
6 \begin{definition}[Cocycle]
7 A cocycle is a family \(c_f\in G_v\) for every \(f:v\to w\), satisfying
8 \[
9  c_{1_v}=1,\qquad c_{g\circ f}=c_f f^*(c_g).
10 \]
11 It determines a twisted view system with maps
12 \[
13  T_c(f)(x)=c_f f^*(x).
14 \]
15 A section of the twisted system satisfies \(x_v=c_f f^*(x_w)\).
16 \end{definition}
17 The cocycle law says that the transition rules compose coherently. It does not assert that the twisted system has a section. The coherent transition system and a global trivialization of that system are different objects.
18 
19 For a family \(a=(a_v)\in\prod_vG_v\), define
20 \begin{equation}\label{eq:gauge}
21  (a\cdot c)_f=a_vc_f[f^*(a_w)]^{-1}.
22 \end{equation}
23 
24 \begin{proposition}[Gauge action and its groupoid]\label{KS30}
25 Equation~\eqref{eq:gauge} defines an action on cocycles. A gauge carrying \(c\) to \(d\) induces an equivalence of twisted section sets by \(x_v\mapsto a_vx_v\). The cocycles and actual gauges form a groupoid: an arrow \(a:c\to d\) followed by \(b:d\to e\) has label \(ba\).
26 \end{proposition}
27 \begin{proof}
28 First, $T_c$ really is a view system. For $f:v\to w$, $g:w\to z$, and $x\in G_z$, the homomorphism and cocycle laws give
29 \[
30  T_c(f)T_c(g)(x)=c_ff^*(c_gg^*x)
31  =c_ff^*(c_g)f^*g^*x=c_{g\circ f}(g\circ f)^*x.
32 \]
33 The identity equation follows from $c_{1_v}=1$. No rearrangement of factors is involved.
34 
35 Put $d=a\cdot c$. Its identity label is $a_v1a_v^{-1}=1$. For a composite, expand all factors in their original order:
36 \[
37 \begin{aligned}
38  d_f f^*(d_g)
39  &=a_vc_f[f^*(a_w)]^{-1}
40    f^*(a_wc_g[g^*(a_z)]^{-1})\\
41  &=a_vc_f[f^*(a_w)]^{-1}f^*(a_w)f^*(c_g)
42        [f^*g^*(a_z)]^{-1}\\
43  &=a_vc_{g\circ f}[(g\circ f)^*(a_z)]^{-1}
44  =d_{g\circ f}.
45 \end{aligned}
46 \]
47 Thus the gauge formula preserves the cocycle condition. For two gauges $a,b$, substitution gives
48 \[
49  (a\cdot(b\cdot c))_f
50  =a_vb_vc_f[f^*(b_w)]^{-1}[f^*(a_w)]^{-1}
51  =((ab)\cdot c)_f.
52 \]
53 The reversed order in the two inverse factors is exactly the formula for the inverse of a product. The identity gauge acts trivially.
54 
55 If $d=a\cdot c$ and $x$ is a section of $T_c$, put $y_v=a_vx_v$. Then
56 \[
57  d_ff^*(y_w)
58  =a_vc_f[f^*(a_w)]^{-1}f^*(a_w)f^*(x_w)
59  =a_vx_v=y_v.
60 \]
61 The inverse map is multiplication by $a_v^{-1}$ at each view, proving an equivalence of the actual section sets.
62 
63 For the groupoid, an arrow $a:c\to d$ means the equation $a\cdot c=d$. If $b:d\to e$, then $(ba)\cdot c=b\cdot(a\cdot c)=e$, giving composition. The identity label is $1$ and the inverse label is $a^{-1}$. Associativity and the two inverse identities now follow from the corresponding multiplication laws in the product group. The label $ba$ is therefore forced by the order of application, not an arbitrary notational convention.
64 \end{proof}
65 \source{KS30}
66 The action groupoid \(Z^1(\V;G)//\prod_vG_v\) retains comparison witnesses. Its orbit set \(Z^1(\V;G)/\prod_vG_v\) retains only isomorphism classes. There is no reason for the orbit set to be a group in this nonabelian setting.
67 
68 \subsection{Automorphisms and ambiguity are not the same question}
69 The stabilizer of a cocycle is the group of families with
70 \[
71  a_v=c_f f^*(a_w)c_f^{-1}.
72 \]
73 If one gauge \(a:c\to d\) is known, all gauges from \(c\) to \(d\) are uniquely of the form \(ah\), with \(h\in\Stab(c)\). Indeed \(a^{-1}b\) stabilizes \(c\) for every other gauge \(b\). This is the ordinary Hom torsor principle in a groupoid.
74 
75 That symmetry group must not be confused with the set of global trivializations of one fixed cocycle. The latter will be parametrized by ordinary coherent group elements, after one trivialization has been selected.
76 
77 \subsection{The relative obstruction without commutativity}
78 Prescribe a coherent partial section \(s\) of \(T_c\) on \(U\). The based gauge group is
79 \[
80  \mathcal G_U=\{a\in\prod_vG_v:a_u=1\text{ for }u\in U\}.
81 \]
82 Choose a raw family \(q\) equal to \(s\) on \(U\). Identity elements can be used elsewhere. Normalize the labels by
83 \[
84  c^q_f=q_v^{-1}c_f f^*(q_w).
85 \]
86 Its labels on arrows internal to \(U\) are one. Define the pointed orbit obstruction
87 \[
88  \mathfrak o_U(c,s)=[c^q]\in Z^1(\V;G)/\mathcal G_U,
89 \]
90 whose neutral point is the class of the trivial cocycle.
91 
92 \begin{theorem}[Nonabelian relative extension]\label{KS31}
93 The obstruction is independent of the raw lift. It is neutral exactly when \(s\) extends to a global section of \(T_c\).
94 \end{theorem}
95 \begin{proof}
96 The normalized label $c^q$ is the gauge transform of $c$ by $q^{-1}$, so Proposition~\ref{KS30} makes it a cocycle. If $f:v\to w$ is internal to $U$, the partial-section equation says $q_v=c_ff^*(q_w)$, and therefore $c_f^q=1$ on that arrow.
97 
98 If $t$ is another raw lift, define $a_v=t_v^{-1}q_v$. On $U$ both lifts equal $s$, so $a_v=1$ and $a\in\mathcal G_U$. Its action is
99 \[
100 \begin{aligned}
101  (a\cdot c^q)_f
102  &=t_v^{-1}q_v\,q_v^{-1}c_ff^*(q_w)
103        [f^*(t_w^{-1}q_w)]^{-1}\\
104  &=t_v^{-1}c_ff^*(q_w)
105        [f^*(q_w)]^{-1}f^*(t_w)
106  =t_v^{-1}c_ff^*(t_w)=c_f^t.
107 \end{aligned}
108 \]
109 Thus changing the raw lift leaves the based orbit unchanged.
110 
111 Suppose the orbit is neutral. Equality of orbit classes means there exists an actual based gauge $b$ with $b\cdot c^q=1$. At an arrow $f:v\to w$, this equation is
112 \[
113  b_vq_v^{-1}c_ff^*(q_w)[f^*(b_w)]^{-1}=1.
114 \]
115 Multiply on the left by $q_vb_v^{-1}$. Homomorphic preservation of products then gives
116 \[
117  c_ff^*(q_wb_w^{-1})=q_vb_v^{-1}.
118 \]
119 Therefore $x_v=q_vb_v^{-1}$ is a twisted coherent family. On $U$, $b_v=1$ and $q_v=s_v$, so it extends the prescribed section.
120 
121 Conversely, suppose $x$ is a global twisted section extending $s$. Put $b_v=x_v^{-1}q_v$. This is based, and direct substitution gives
122 \[
123  (b\cdot c^q)_f
124  =x_v^{-1}c_ff^*(x_w)=1,
125 \]
126 where the last equality is precisely the section equation for $x$. Hence the obstruction is neutral. These arguments establish the result using group cancellation only. In particular they do not assume an additive quotient, a norm on labels, or a decision procedure for finding $b$.
127 \end{proof}
128 \source{KS31}
129 The orbit is defined from actual cocycles and an actual group action. It is not a Boolean test defined to be neutral precisely when an extension exists. Deciding orbit membership in arbitrary groups remains a separate problem.
130 
131 Let
132 \[
133  H_U=\{h:f^*(h_w)=h_v\text{ for every }f,\ h|_U=1\}.
134 \]
135 
136 \begin{theorem}[The nonabelian extension torsor]\label{KS32}
137 Given one extension \(x_0\), the map \(h\mapsto x_0h\) is an equivalence from \(H_U\) to the extension set. The extension is unique if and only if the obstruction is neutral and \(H_U\) is trivial.
138 \end{theorem}
139 \begin{proof}
140 Take \(h\in H_U\). Its pointwise product with the chosen extension \(x_0\) agrees with the prescribed data on \(U\), because \(h|_U=1\). For an arrow \(f:v\to w\), the coefficient homomorphism preserves multiplication and the two coherence equations give
141 \[
142  c_f f^*((x_0)_wh_w)
143  =c_f f^*((x_0)_w)f^*(h_w)
144  =(x_0)_vh_v.
145 \]
146 Thus \(x_0h\) is another twisted extension.
147 
148 Conversely, if \(x\) is a twisted extension of the same prescribed data, define \(h_v=(x_0)_v^{-1}x_v\). On \(U\) its value is one. For every arrow,
149 \[
150  \begin{aligned}
151  h_v
152  &=[c_f f^*((x_0)_w)]^{-1}[c_f f^*(x_w)]\\
153  &=f^*((x_0)_w)^{-1}c_f^{-1}c_f f^*(x_w)\\
154  &=f^*((x_0)_w^{-1}x_w)=f^*(h_w).
155  \end{aligned}
156 \]
157 The cancellation uses inverse multiplication in its actual order. No commuting factors have been moved past one another. Hence \(h\in H_U\). Pointwise group cancellation shows that \(h\mapsto x_0h\) and \(x\mapsto x_0^{-1}x\) are inverse maps.
158 
159 The extension set is nonempty precisely when the earlier orbit obstruction is neutral. Once it is nonempty, the displayed bijection makes it a singleton precisely when \(H_U\) has only its identity element. Both conditions are needed for unique existence. Changing the chosen extension changes the parametrization, not the extension set or the criterion.
160 \end{proof}
161 \source{KS32}
162 The additive theory is recovered by applying a multiplicative type tag to an additive view system and choosing the trivial cocycle. The normalized label then becomes \(f^*q_w-q_v\). The source proves agreement of the actual extension sets and vanishing criteria. It does not identify the whole nonabelian orbit set with every element of the larger additive arrow residual quotient.
163 
164 \subsection{A small noncommutative model}
165 \begin{example}[A \(C_2\) loop with \(S_3\) coefficients]\label{KS33}
166 Take one view with a loop \(\sigma\) satisfying \(\sigma^2=1\), and constant coefficients in a group \(H\). A cocycle is determined by an element \(p\in H\) whose square is the identity. Gauge equivalence is conjugacy, and its automorphisms form the centralizer of \(p\).
167 
168 For \(H=S_3\), these elements are the identity and the three transpositions. There are exactly two orbit classes. The identity cocycle has automorphism group \(S_3\), which is noncommutative. A nonidentity involution gives a coherent cocycle whose regular twisted section equation \(x=px\) has no solution.
169 \end{example}
170 \begin{proof}
171 The only nontrivial cocycle relation is \(p^2=1\). At a single view the gauge action is \(p\mapsto apa^{-1}\). All three transpositions are conjugate and none is conjugate to the identity. The stabilizer is therefore the centralizer. Finally \(x=px\) implies \(p=1\) after multiplication by \(x^{-1}\).
172 \end{proof}
173 \source{KS33}
174 The example makes an important boundary visible. A cocycle can exist and glue as an object even when it admits no global trivializing section. Stackhood will concern the former gluing problem, not a claim that every cocycle becomes trivial.
175 
176 \plate{06_groupoid}{The orbit set sees two classes in the \(C_2\)-to-\(S_3\) example. The groupoid also retains the arrows between conjugate transpositions and all automorphisms. Collapsing the arrows loses information that matters in descent.}{fig:groupoid}
177 
178 \chap{Effective gluing of objects and their identifications}\label{sec:descent}
179 \subsection{Why pairwise agreement is not the right datum}
180 For objects with symmetry, local descriptions need not be literally equal on overlaps. They may instead come with specified isomorphisms. Those isomorphisms must satisfy their own composition law. It is not enough to know that some isomorphism exists for each pair.
181 
182 Let \(U_i\) be full patches in \(\V\). Assume the composition cover condition
183 \begin{equation}\label{eq:compositioncover}
184  \forall(v\xrightarrow f w\xrightarrow g z),\quad
185  \exists i:\ v,w,z\in U_i.
186 \end{equation}
187 By inserting identity arrows, this implies coverage of objects and arrows.
188 
189 A descent datum consists of local cocycles \(c_i\) and overlap gauges \(a_{ij}(v)\) with
190 \begin{align}
191  c_j(f)&=a_{ij}(v)c_i(f)[f^*a_{ij}(w)]^{-1},\label{eq:localgauge}\\
192  a_{ik}(v)&=a_{jk}(v)a_{ij}(v).\label{eq:triple}
193 \end{align}
194 The triple equation implies \(a_{ii}=1\) and \(a_{ji}=a_{ij}^{-1}\). A morphism of descent data is a family of local gauges \(r_i\) satisfying
195 \[
196  r_j(v)a_{ij}(v)=a'_{ij}(v)r_i(v).
197 \]
198 These objects and arrows form a groupoid.
199 
200 \begin{theorem}[Effective cocycle descent]\label{KS34}
201 Under \eqref{eq:compositioncover}, restriction is an equivalence between the global cocycle gauge groupoid and the groupoid of descent data. The overlap gauges supplied in the datum are realized, not discarded.
202 \end{theorem}
203 \begin{proof}
204 \emph{Step 1: normalize the supplied identifications.} The triple-overlap equation with all indices equal gives $a_{ii}=a_{ii}a_{ii}$, hence $a_{ii}=1$. With indices $i,j,i$ it gives $a_{ji}a_{ij}=1$, hence $a_{ji}=a_{ij}^{-1}$. Composition coverage implies object coverage by inserting identity arrows. Choose a containing patch $\kappa(v)$ for each view and put
205 \[
206  b_i(v)=a_{\kappa(v),i}(v)\quad(v\in U_i).
207 \]
208 At a point of $U_i\cap U_j$, the triple law, now on patches $\kappa(v),i,j$, gives
209 \[
210  b_j(v)=a_{ij}(v)b_i(v).                                    \tag{*}
211 \]
212 The two endpoints of an arrow may have different reference patches. No common reference patch is being assumed.
213 
214 \emph{Step 2: obtain literal matching labels.} Define
215 \[
216  \widetilde c_i(f)=b_i(v)^{-1}c_i(f)f^*(b_i(w))
217  \quad(f:v\to w\text{ in }U_i).
218 \]
219 This is a gauge transform and hence a cocycle on $U_i$. If the arrow lies also in $U_j$, substitute the original overlap equation and (*) at its two endpoints:
220 \[
221 \begin{aligned}
222  \widetilde c_j(f)
223  &=b_i(v)^{-1}a_{ij}(v)^{-1}
224    a_{ij}(v)c_i(f)[f^*a_{ij}(w)]^{-1}
225    f^*(a_{ij}(w)b_i(w))\\
226  &=b_i(v)^{-1}c_i(f)f^*(b_i(w))
227  =\widetilde c_i(f).
228 \end{aligned}
229 \]
230 Every cancellation is between neighboring inverse factors. Commutativity is not required.
231 
232 \emph{Step 3: construct the global cocycle.} Every arrow is contained in a patch, again by inserting an identity in a composable pair. Define $c_f$ to be $\widetilde c_i(f)$ in any such patch. Step 2 proves independence. For an identity arrow, choose a patch through its view to obtain $c_{1_v}=1$. For $f:v\to w$ and $g:w\to z$, composition coverage supplies a patch containing all three vertices. Fullness places $f$, $g$, and $g\circ f$ in that same patch. Its cocycle law therefore proves
233 \[
234  c_{g\circ f}=\widetilde c_i(g\circ f)
235  =\widetilde c_i(f)f^*(\widetilde c_i(g))=c_ff^*(c_g).
236 \]
237 This is the exact point where composition coverage, rather than arrow coverage alone, is used.
238 
239 Undoing the normalization proves
240 \[
241  b_i(v)c_f[f^*(b_i(w))]^{-1}=c_i(f).
242 \]
243 Together with (*), these gauges constitute an isomorphism from the restriction of $c$ to the supplied descent datum. They implement its original overlaps, proving essential surjectivity of restriction.
244 
245 \emph{Step 4: retain every morphism.} Let $c,d$ be global cocycles. Their canonical restrictions have identity overlap gauges. A morphism between those restrictions is consequently a family $r_i$ satisfying $r_j(v)=r_i(v)$ on each overlap. Assemble $r_v$ from any containing patch. For an arrow choose a patch containing both endpoints. Its gauge equation proves
246 \[
247  d_f=r_vc_f[f^*(r_w)]^{-1}.
248 \]
249 Thus $r$ is a global gauge. Its restriction is the original family. Conversely, assembling the restrictions of a global gauge preserves every coordinate and returns that gauge. Restriction is therefore bijective on each Hom set, not merely injective on isomorphism classes. This is full faithfulness.
250 
251 \emph{Step 5: obtain an equivalence.} For each descent object choose the global cocycle and isomorphism constructed above. For an arrow between descent objects, conjugate it by these two chosen isomorphisms and use the unique preimage under the Hom bijection of Step 4. This defines the arrow map of a quasi-inverse. Uniqueness of the preimage verifies its identity and composition laws, and the chosen isomorphisms provide the comparison to the identity functor. Hence the restriction functor is an equivalence of groupoids. Different patch choices can alter the representative but not this conclusion.
252 \end{proof}
253 \source{KS34}
254 
255 \subsection{The correct uniqueness statement}
256 Suppose \((c,b_i)\) and \((c',b'_i)\) realize the same descent datum. The only possible compatible comparison is
257 \[
258  g_v=b'_i(v)^{-1}b_i(v),
259 \]
260 using any patch through \(v\). The overlap identities make it independent of the patch, and \(b'_ig=b_i\). It is therefore the unique global comparison respecting the fixed local identifications.
261 
262 This is not a statement that the underlying cocycle has no automorphisms. Those automorphisms can reappear when the local identifications are forgotten. Nor does the construction choose one representative independently of every reference patch. It proves that the choices are related by the appropriate unique comparison.
263 
264 \subsection{A failed triple}
265 Let \(t\ne1\) be an involution and ask for frames \(b_0,b_1,b_2\) satisfying
266 \[
267  b_1=tb_0,\qquad b_2=tb_1,\qquad b_2=tb_0.
268 \]
269 The first two give \(b_2=b_0\), while the third forces \(t=1\). Each displayed transition is individually invertible, but they cannot be the overlap identifications of a global frame. The defect lies in the triple relation.
270 
271 \plate{07_cover}{Object coverage, arrow coverage, and composition coverage are distinct. The proper two-view patches on a three-view chain see every arrow but no patch sees the relation \(0\to1\to2\). The four proper three-view patches on a four-view chain do cover every composable pair.}{fig:cover}
272 
273 \chap{A genuine stack on the composition site}\label{sec:stack}
274 The preceding theorem can be placed in a standard site, rather than called stack-like. We use the usual effective-descent meaning of a stack~\cite{stacks-stack,mathlib-stack}. The base of this site is the inclusion poset of full patches
275 \[
276  \mathcal P(\V)=(\operatorname{Set}(\Ob\V),\subseteq).
277 \]
278 This patch category is different from the original category of views.
279 
280 \subsection{The topology is defined without assuming effectivity}
281 For a composable pair \(q=(v\xrightarrow f w\xrightarrow g z)\), let its support be \(|q|=\{v,w,z\}\). A sieve \(\mathcal R\) on \(W\) is covering when
282 \begin{equation}\label{eq:site}
283  |q|\subseteq W\quad\Longrightarrow\quad
284  (|q|\hookrightarrow W)\in\mathcal R
285  \quad\text{for every composable }q.
286 \end{equation}
287 This condition depends only on the view category, not on the coefficient groups or on a promised global realization.
288 
289 \begin{proposition}[The composition topology]\label{KS35}
290 Condition~\eqref{eq:site} defines a Grothendieck topology \(J_{\mathrm{comp}}\). The sieve generated by a family of inclusions \(U_i\subseteq W\) is covering exactly when the family covers every composition support in \(W\).
291 \end{proposition}
292 \begin{proof}
293 In the inclusion poset, identify a sieve on $W$ with a downward-closed collection of subsets of $W$. Pullback along $Z\subseteq W$ consists of those subsets of $Z$ that were already members of the original sieve. We verify the three topology axioms using this description.
294 
295 The maximal sieve contains every subset of $W$, hence every composition support. For stability under pullback, let $\mathcal R$ cover $W$ and let $q$ be a composable pair whose support lies in $Z\subseteq W$. The same pair lies in the full patch $W$, so $|q|\in\mathcal R$. Since $|q|\subseteq Z$, it belongs to the pulled-back sieve on $Z$. Thus that sieve covers $Z$.
296 
297 For transitivity, suppose $\mathcal R$ covers $W$, and that for every $U\in\mathcal R$ the pullback of a sieve $\mathcal T$ to $U$ covers $U$. Fix a composable pair $q$ in $W$. Its support $S=|q|$ belongs to $\mathcal R$. Since patches are full, $q$ is also a composable pair in $S$. The covering condition for the pullback of $\mathcal T$ to $S$ therefore puts the identity inclusion $S\subseteq S$ in that pullback. By the definition of pullback, this says $S\in\mathcal T$. It holds for every $q$, so $\mathcal T$ covers $W$.
298 
299 Finally, the sieve generated by $U_i\subseteq W$ consists exactly of the subpatches $Z$ contained in at least one $U_i$. One inclusion follows because a sieve contains all restrictions of its generators. The reverse inclusion follows because this collection is itself downward closed and contains all generators, hence is the smallest such sieve. Consequently a support belongs to the generated sieve exactly when some $U_i$ contains all its endpoints. This proves the family characterization. When $W$ is empty, there are no composable pairs to test, so even the empty sieve is covering.
300 \end{proof}
301 \source{KS35}
302 Intersections of a covering family with a subpatch remain covering. Replacing each member by a covering family again gives a cover. Identities imply coverage of single views and arrows. The empty patch admits the empty cover.
303 
304 \subsection{The actual patch pseudofunctor}
305 On a patch \(W\), use
306 \[
307  \mathfrak K_G(W)=Z^1(\V|_W;G|_W)//\prod_{v\in W}G_v.
308 \]
309 Restriction keeps the existing cocycle values and gauge values on the smaller patch. It first gives a strict category valued functor on the opposite patch poset. Its standard pseudofunctor form has identity comparison isomorphisms, with the required coherence laws.
310 
311 \begin{theorem}[Stackhood on the composition site]\label{KS36}
312 The patch pseudofunctor \(\mathfrak K_G\) is a stack for \(J_{\mathrm{comp}}\). It satisfies the standard condition of descent for morphisms and effective descent for objects on every covering sieve.
313 \end{theorem}
314 \begin{proof}
315 We use the equivalence-of-descent-categories formulation of stackhood for the already constructed patch pseudofunctor. Its restriction maps act on actual cocycle labels and gauge values. Their identity and composition laws have been proved, so the descent condition is applied to a specified pseudofunctor, not assumed as part of its definition.
316 
317 \emph{From standard descent data to overlap labels.} For a covering family $(U_i\subseteq W)$, standard descent data provide local objects and comparison gauges on common subpatches, natural under further restriction. At a view $v\in U_i\cap U_j$, restrict the comparison to the singleton patch $\{v\}$ and call its value $a_{ij}(v)$. To verify the gauge equation along $f:v\to w$ in an overlap, use the comparison on $U_i\cap U_j$, which is a full patch containing the arrow. Naturality identifies its two endpoint values with the singleton values. Its own gauge equation then becomes \eqref{eq:localgauge}. Evaluating the standard triple-comparison identity at a singleton gives \eqref{eq:triple}. Thus these labels form the concrete descent datum of Theorem~\ref{KS34}.
318 
319 \emph{From the concrete realization back to standard data.} By Theorem~\ref{KS34} there is a global cocycle $c$ and local gauges $b_i$ implementing these overlaps. On any common subpatch $Z\subseteq U_i\cap U_j$, the required equation between gauge arrows is an equality of their values at every $v\in Z$. At such a view it is $b_j(v)=a_{ij}(v)b_i(v)$, already proved by the construction. Equality of coordinate functions proves equality of the arrows on $Z$. Thus every standard common-subpatch equation holds, not only the equations on singleton tests. This gives an isomorphism from the standard restriction of $c$ to the original standard descent object.
320 
321 \emph{Morphisms.} A standard morphism between restrictions of global objects has local gauge components. Its comparison equations at singleton patches show that these components agree on overlaps. The Hom gluing map from Theorem~\ref{KS34} yields a unique global gauge. Conversely, a global gauge restricts to those components and satisfies all common-subpatch equations. Restriction and gluing are inverse on every Hom set. Standard restriction is therefore fully faithful as well as essentially surjective, hence an equivalence.
322 
323 \emph{Every covering sieve.} Let $\mathcal R$ be an arbitrary covering sieve on $W$. Index a family by all its member inclusions $U\subseteq W$. Each composition support belongs to this family by the covering definition, so it is a composition cover. Its generated sieve is exactly $\mathcal R$: one inclusion uses that $\mathcal R$ is downward closed, and the other uses each member as its own generator. The family argument therefore proves the descent equivalence on the original sieve. Applying it to every covering sieve proves both descent of morphisms and effectiveness of objects. These are the required standard stack conditions \cite{stacks-stack,mathlib-stack}.
324 \end{proof}
325 \source{KS36}
326 The principal source declaration is \code{GroupViewSystem.patch_isStack}. Its target is mathlib's \code{Pseudofunctor.IsStack}, not a project predicate that repeats the conclusion as an assumption.
327 
328 \subsection{The cover is nontrivial, but specific}
329 On a four-view chain, take the four patches obtained by deleting one vertex. All patches are proper, yet every composable pair has at most three endpoints and lies in one of them. The theorem genuinely glues pieces smaller than the whole object.
330 
331 On the three-view chain, the analogous proper patches cover each object and each arrow but miss the support of \(0\to1\to2\). They do not form a cover in this topology. Consequently the theorem is neither vacuous nor an unrestricted gluing principle.
332 
333 \begin{scopebox}
334 \textbf{Exact scope.} This is an ordinary stack of strict group valued cocycle realizations on a specified combinatorial site. It is not an infinity-stack, a universal heterogeneous atlas, or an arithmetic existence theorem. The stack theorem glues coherent cocycles with their overlap isomorphisms. It does not assert that every resulting cocycle has a global trivialization.
335 \end{scopebox}
336 
337 \chap{Equivalent presentations and identified boundaries}\label{sec:relative}
338 \subsection{Transporting the same question}
339 Let \(H:\V\to\W\) be part of a category equivalence, with inverse \(L\) and counit \(\varepsilon:HL\Rightarrow\id_\W\). Pull a view system \(F\) on \(\W\) back along \(H\). Sampling a global section gives \((H^*x)_v=x_{Hv}\).
340 
341 \begin{proposition}[Equivalence of section spaces]\label{KS37}
342 Pullback induces \(\Gamma(F)\simeq\Gamma(H^*F)\). If \(U\subseteq\Ob\W\) is closed under isomorphism and \(U'=H^{-1}U\), it also induces
343 \[
344  \Ext_U^F(s)\simeq\Ext_{U'}^{H^*F}(H^*s).
345 \]
346 Existence and uniqueness of the prescribed extension are preserved and reflected.
347 \end{proposition}
348 \begin{proof}
349 Write the unit of the equivalence as $\eta:I_\V\Rightarrow LH$, and take the unit and counit with their triangle identities. Set $t_w=\varepsilon_w^{-1}:w\to HLw$. Given $y\in\Gamma(H^*F)$, define
350 \[
351  (Ry)_w=F(t_w)y_{Lw}.
352 \]
353 For an arrow $f:w\to w'$, naturality of the inverse counit states
354 \[
355  HL(f)\,t_w=t_{w'}f.
356 \]
357 Contravariance of $F$ and coherence of $y$ therefore give
358 \[
359 \begin{aligned}
360  F(f)(Ry)_{w'}
361  &=F(f)F(t_{w'})y_{Lw'}\\
362  &=F(t_w)F(HL(f))y_{Lw'}
363  =F(t_w)y_{Lw}=(Ry)_w.
364 \end{aligned}
365 \]
366 Thus recovery gives an actual coherent section.
367 
368 If $x\in\Gamma(F)$, coherence along $t_w$ gives
369 \[
370  (RH^*x)_w=F(t_w)x_{HLw}=x_w.
371 \]
372 For the other composite, the triangle identity says $t_{Hv}=H(\eta_v)$. Coherence of $y$ along $\eta_v:v\to LHv$ yields
373 \[
374  (H^*Ry)_v=F(t_{Hv})y_{LHv}=F(H\eta_v)y_{LHv}=y_v.
375 \]
376 These coordinate equations prove both inverse identities.
377 
378 For the relative claim, pullback clearly sends an extension of $s$ to an extension of $H^*s$ on $U'=H^{-1}U$. Conversely suppose $y$ extends $H^*s$. If $w\in U$, the isomorphism $w\cong HLw$ and isomorphism closure imply $HLw\in U$. Hence $Lw\in U'$ and $y_{Lw}=s_{HLw}$. Both endpoints of $t_w$ lie in $U$, so partial coherence gives
379 \[
380  (Ry)_w=F(t_w)s_{HLw}=s_w.
381 \]
382 Recovery therefore preserves the required boundary. The two inverse identities remain valid on the subsets of extensions. Bijections preserve nonemptiness and identify any two elements exactly when their images are equal, proving preservation and reflection of existence and uniqueness.
383 \end{proof}
384 \source{KS37}
385 The coefficients really are pulled back. This does not compare unrelated coefficient systems simply because their diagrams look alike. Isomorphism closure is a sufficient general hypothesis for the relative statement. The theorem does not assert that every unsaturated domain fails.
386 
387 For group coefficients, the invisible coherent groups \(H_U\) are transported by a multiplicative equivalence, and the parameterizations \(x_0h\) commute with pullback. Thus feasibility and ambiguity are both retained. This is more than a comparison of the number of extensions. It is not an assertion that every possible based gauge orbit set is presentation independent.
388 
389 \subsection{Why a boundary must retain its identification}
390 Let \(R:\mathcal C\to\mathcal D\) be a functor between groupoids, and fix \(b\in\mathcal D\). A realization over \(b\) should include a chosen isomorphism to \(b\), rather than require literal equality of representatives.
391 
392 \begin{definition}[Marked realization groupoid]
393 The objects of \(\mathcal E_b(R)\) are pairs \((x,\phi)\), with \(x\in\mathcal C\) and \(\phi:Rx\xrightarrow{\sim}b\). An arrow \((x,\phi)\to(y,\psi)\) is an arrow \(a:x\to y\) with \(\psi R(a)=\phi\).
394 \end{definition}
395 Composition and inverses preserve this equation, so this is a groupoid. It is the explicit groupoid homotopy fiber construction, without invoking a higher categorical interface.
396 
397 \begin{proposition}[Existence and invisible automorphisms]\label{KS38}
398 The groupoid \(\mathcal E_b(R)\) is nonempty exactly when \(b\) is in the essential image of \(R\). An automorphism of \((x,\phi)\) is an automorphism \(a\) of \(x\) satisfying \(R(a)=1_{Rx}\).
399 \end{proposition}
400 \begin{proof}
401 The first assertion is the object definition. For the second, the boundary equation is \(\phi R(a)=\phi\). Cancel the isomorphism \(\phi\). Conversely \(R(a)=1\) makes the equation hold.
402 \end{proof}
403 \source{KS38}
404 This retains precisely the symmetries invisible at the identified boundary. It avoids freezing arbitrary representative coordinates and then mistaking the result for an invariant realization problem.
405 
406 \plate{08_marked}{The chosen boundary identification is part of a realization. A comparison must commute with it. Under an equivalent presentation, the comparison square may commute through an isomorphism rather than a literal equality, and the marked realization groupoid is still transported correctly.}{fig:marked}
407 
408 \subsection{Weakly commuting squares are enough}
409 Suppose \(E:\mathcal C\to\mathcal C'\) and \(K:\mathcal D\to\mathcal D'\) are equivalences, with functors \(R,R'\) and a natural isomorphism
410 \[
411  \sigma:KR\xRightarrow{\sim}R'E.
412 \]
413 The square is not required to commute literally.
414 
415 \begin{theorem}[Invariance of the marked realization problem]\label{KS39}
416 The map
417 \[
418  (x,\phi)\longmapsto(Ex,K(\phi)\sigma_x^{-1}),\qquad a\longmapsto E(a)
419 \]
420 defines an equivalence \(\mathcal E_b(R)\simeq\mathcal E_{Kb}(R')\).
421 \end{theorem}
422 \begin{proof}
423 For an object $(x,\phi)$ put $\beta_x=K(\phi)\sigma_x^{-1}:R'Ex\to Kb$. This is an isomorphism of the required type. If $a:(x,\phi)\to(y,\psi)$, naturality of $\sigma$ says
424 \[
425  R'E(a)\sigma_x=\sigma_yKR(a),
426  \qquad \sigma_y^{-1}R'E(a)=KR(a)\sigma_x^{-1}.
427 \]
428 Consequently
429 \[
430  \beta_yR'E(a)
431  =K(\psi)KR(a)\sigma_x^{-1}
432  =K(\psi R(a))\sigma_x^{-1}
433  =K(\phi)\sigma_x^{-1}=\beta_x.
434 \]
435 So $E(a)$ is a marked arrow. Identity and composition are preserved because the underlying arrow map is that of the functor $E$.
436 
437 To prove full faithfulness, start with a marked arrow $u:Ex\to Ey$ between the transported objects. Full faithfulness of $E$ gives a unique $a:x\to y$ with $E(a)=u$. Its marked equation, rewritten by the naturality identity above, is
438 \[
439  K(\psi R(a))\sigma_x^{-1}=K(\phi)\sigma_x^{-1}.
440 \]
441 Cancel the isomorphism on the right and use faithfulness of $K$ to obtain $\psi R(a)=\phi$. Thus the lifted arrow is marked. Uniqueness of the underlying lift also proves uniqueness as a marked arrow, giving a bijection on every Hom set.
442 
443 For essential surjectivity, let $(y,\psi)$ be a target realization. Choose $x$ and an isomorphism $i:Ex\to y$, using essential surjectivity of $E$. Fullness of $K$ lifts the well-typed composite
444 \[
445  KRx\xrightarrow{\sigma_x}R'Ex
446  \xrightarrow{R'(i)}R'y\xrightarrow{\psi}Kb
447 \]
448 to an arrow $\phi:Rx\to b$. Since $\mathcal D$ is a groupoid, $\phi$ is automatically an isomorphism. Its image satisfies $K(\phi)=\psi R'(i)\sigma_x$, hence $\beta_x=\psi R'(i)$. This is precisely the condition for $i$ to be an arrow from the transported realization to $(y,\psi)$. It is an isomorphism because all categories involved are groupoids.
449 
450 We have verified full faithfulness and essential surjectivity of the specified transport functor. Choosing these preimages and lifting arrows through the Hom bijections constructs a quasi-inverse, as in Theorem~\ref{KS34}, proving the claimed equivalence. No literal equality $KR=R'E$ was used.
451 \end{proof}
452 \source{KS39}
453 Apply this to the actual restriction functors between cocycle patch groupoids and the equivalences induced by an equivalent view presentation. The full realization problem, including comparison witnesses and automorphisms, is transported.
454 
455 Replacing \(b\) by an isomorphic boundary \(b'\) also gives an equivalence, by composing the identification with \(b\to b'\). For \(R=\id\), the marked realization groupoid has center \((b,1_b)\), and between \((x,\phi)\) and \((y,\psi)\) there is exactly one compatible arrow \(\psi^{-1}\phi\). This is a useful example of contractible realization data, not a claim that the original groupoid has no symmetries.
456 

Back to source controls

Back to Realization Calculus: twin edition