\documentclass[11pt,reqno]{amsart}

\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{lmodern}
\usepackage{microtype}
\usepackage{natbib}

\usepackage[margin=1.15in]{geometry}

\usepackage{xcolor}
\definecolor{LinkBlue}{HTML}{1A4E9A}
\definecolor{CiteBlue}{HTML}{1A4E9A}
\definecolor{UrlBlue}{HTML}{1A4E9A}

\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{mathrsfs}
\usepackage{enumitem}
\setlist[enumerate]{noitemsep,nolistsep,leftmargin=*,labelindent=0pt,listparindent=0pt,itemindent=0pt}
\setlist[itemize]{noitemsep,nolistsep,leftmargin=*,labelindent=0pt,listparindent=0pt,itemindent=0pt}

\usepackage{tikz}
\usepackage{tikz-cd}
\usetikzlibrary{arrows.meta,calc,positioning}

\usepackage[
  colorlinks=true,
  linkcolor=LinkBlue,
  citecolor=CiteBlue,
  urlcolor=UrlBlue
]{hyperref}
\usepackage[nameinlink,noabbrev]{cleveref}

\setlength{\parindent}{0pt}
\setlength{\parskip}{0.55\baselineskip plus 1.5pt minus 1pt}
\setlist{topsep=\parskip,partopsep=0pt,parsep=0pt,itemsep=0pt}
\widowpenalty=10000
\clubpenalty=10000
\displaywidowpenalty=10000
\allowdisplaybreaks[1]
\raggedbottom
\makeatletter
\def\thm@space@setup{\thm@preskip=\parskip \thm@postskip=0pt}
\makeatother

\theoremstyle{plain}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{theoremx}{Theorem}
\renewcommand{\thetheoremx}{\Alph{theoremx}}
\crefname{theoremx}{Theorem}{Theorems}
\Crefname{theoremx}{Theorem}{Theorems}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}

\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{construction}[theorem]{Construction}
\newtheorem{example}[theorem]{Example}
\newtheorem{remark}[theorem]{Remark}

\DeclareMathOperator{\Hom}{Hom}
\DeclareMathOperator{\id}{id}
\DeclareMathOperator{\Ob}{Ob}
\DeclareMathOperator{\Mor}{Mor}
\DeclareMathOperator{\colim}{colim}
\DeclareMathOperator{\supp}{supp}
\DeclareMathOperator{\im}{im}

\newcommand{\Set}{\mathbf{Set}}
\newcommand{\Ab}{\mathbf{Ab}}
\newcommand{\Ch}{\mathbf{Ch}}
\newcommand{\RMod}{R\text{-}\mathbf{Mod}}
\newcommand{\Part}{\operatorname{\mathbf{Part}}}
\newcommand{\PartH}{\Part^{\mathrm{Hel},n}}
\newcommand{\Cc}{C_{\mathrm c}}
\newcommand{\Gz}{G^{(0)}}
\numberwithin{equation}{section}

\title[Laminar Presentations and Finite Chain Models]{A Note on Laminar Presentations and Finite Chain Models for Ample Groupoid Homology}

\author{Luciano Melodia}
\address{Department of Mathematics, Friedrich-Alexander Universität Erlangen-Nürnberg, Cauerstraße 11, 91058 Erlangen}
\email{luciano.melodia@fau.de}

\subjclass[2020]{Primary 22A22, 55N35. Secondary 18A30, 18G35, 55U10, 68V20.}
\keywords{ample étale groupoid, groupoid homology, finite chain model, atomization, laminar family, \(n\)-Helly family, HK conjecture, formalized mathematics}

\begin{document}

\begin{abstract}
	A finite free chain model for the homology of a Hausdorff ample groupoid \(G\) is cut out of the Matui complex by a finite clopen partition of each nerve space. We ask what such a model must supply and isolate three requirements: a single model that is a quasi-isomorphism, a chain of models that is a complete system with ranks and transition maps read off the presenting data, and a bound on the number of atoms in terms of the presenting cover. An \(n\)-Helly axiom on the presenting covers supplies none of them, being satisfied by every finite atomization for every \(n\), and a \(1\)-Helly family of \(N\) compact open sets can have \(2^{N}-1\) atoms. We show that a \textbf{laminar presentation}, a laminar basis of compact open sets in each nerve degree, supplies the third, and the second as soon as it is countable: the atoms of a finite laminar family are exactly its nonempty nodes, so a subordinate model has rank at most the number of members presenting it, the subordinate models of finite height form a complete system containing, for a countable presentation, a chain that is itself complete, and the transition maps are the least-ancestor maps of the presenting subfamilies. Every second countable Hausdorff ample groupoid admits one, and the choice is made in each nerve degree separately, laminarity not being stable under products. The first requirement is a restriction on \(G\): the homology of a model is finitely generated over a Noetherian ring, whereas \(H_0\) over \(\mathbb Z\) is not for the unit groupoid on a Cantor set or for the CAR groupoid, and a truncated model carries free homology of arbitrary rank in arbitrarily high odd degree where the groupoid has none. The chain-level statements are accompanied by a Lean 4 formalization.
\end{abstract}

\maketitle

\section{Introduction}\label{sec:introduction}
Groupoid homology is the computable companion of operator \(K\)-theory in the HK comparison \cite[Conjecture~2.6]{Matui2016}, and every verified instance of that comparison rests on a homology computation driven by finite combinatorial input: level partitions of a Bratteli diagram \cite[Theorem~4.10]{Matui2012}, prefix cylinders of a path space \cite[Theorem~4.6]{NylandOrtega2021}, Kakutani--Rokhlin towers. The conjecture itself is false in general \cite{Deeley2023,Scarparo2020}, which sharpens rather than removes the interest in the finite input, since what one wants from a general mechanism is a finite chain model, not a prediction.

The chain complex of Matui \cite[Definition~3.1]{Matui2012} carries no trace of that finiteness. Two obstacles stand in the way of extracting it from \v Cech data. The boundary pushes functions forward along the face maps of the nerve, covariantly, while \v Cech comparison restricts them, contravariantly, so covers of the nerve spaces do not assemble into a double complex. And the nerve of a cover is an artifact of the cover, changed by refinement in general by homotopically redundant simplices \cite[Remark~1.4]{BauerKerberRollRolle2023}. A natural proposal answers the first by \textbf{atomization}, replacing a cover by the partition into the atoms of the Boolean algebra it generates, which the pushforward does respect, and the second by a Helly-type axiom on the presenting covers, after Helly's intersection theorem \cite{Helly1923} and its relatives \cite[p.~102]{DanzerGrunbaumKlee1963}. \Cref{sec:models} carries this out. The outcome is a poset \(\Part(G)\) of \textbf{finite atomizations}, a finite free subcomplex \(A_\bullet(D;R)\subseteq C_\bullet(G;R)\) for each \(D\in\Part(G)\), and a colimit formula recovering \(C_\bullet(G;R)\) and \(H_\bullet(G;R)\) from any \textbf{complete system} of atomizations.

What must a chain model of this kind supply in order to compute anything? Three requirements are available, and they are not equivalent.

\begin{enumerate}[label=\textup{R\arabic*},ref=\textup{R\arabic*}]
	\item\label{itm:R1} \textbf{A resolution.} A single finite atomization \(D\) with \(A_\bullet(D;R)\hookrightarrow C_\bullet(G;R)\) a quasi-isomorphism.
	\item\label{itm:R2} \textbf{A controlled chain.} A chain \(D^{(0)}\leq D^{(1)}\leq\cdots\) that is a complete system, with ranks and transition maps read off the presenting data, which is what a Bratteli diagram supplies.
	\item\label{itm:R3} \textbf{An atom bound.} A bound on \(\lvert\mathcal A(\mathcal U)\rvert\) in terms of the cover \(\mathcal U\) presenting the partition.
\end{enumerate}

Requirement \labelcref{itm:R1} is a property of \(G\), \labelcref{itm:R2} is a construction, and \labelcref{itm:R3} is a hypothesis on covers. The main point of this note is that \labelcref{itm:R3}, and with a countability proviso \labelcref{itm:R2}, are supplied together by one datum, and that the datum is a nestedness condition and not an intersection condition.

\begin{theoremx}[\ref{prop:laminar}, \ref{prop:laminar-exists}, \ref{thm:laminar-model}]\label{thmx:laminar}
	Call a family of sets \textbf{laminar} if any two members are disjoint or comparable under inclusion, and call \(\mathcal L=(\mathcal L_p)_{p\geq 0}\) a \textbf{laminar presentation} of a Hausdorff ample groupoid \(G\) if each \(\mathcal L_p\) is a laminar family of compact open subsets of \(G_p\) of which every compact open subset of \(G_p\) is a finite union. For a finite laminar cover \(\mathcal U=\{U_a\}_{a\in A}\) of \(K\) by subsets of \(K\) the atoms are exactly the nonempty sets \(U_a\setminus\bigcup\{U_b : U_b\subsetneq U_a\}\), hence are indexed by the members, so \(\lvert\mathcal A(\mathcal U)\rvert\leq\lvert A\rvert\). The finite atomizations of finite height subordinate to \(\mathcal L\) form a complete system, their ranks are bounded by the numbers of members presenting them, and their transition maps are the least-ancestor maps of the presenting subfamilies. If the \(\mathcal L_p\) are countable, the system contains a chain that is itself complete. Every second countable Hausdorff ample groupoid admits a countable laminar presentation.
\end{theoremx}

The remaining three theorems say why the datum is needed and why the Helly axiom is not it.

\begin{theoremx}[\ref{prop:no-finite-resolution}, \ref{ex:unit-groupoid}, \ref{prop:car}, \ref{prop:spurious}]\label{thmx:nofinite}
	Let \(R\) be a commutative unital Noetherian ring. For every finite atomization \(D\) of a Hausdorff ample groupoid \(G\) the modules \(H_m(A_\bullet(D;R))\) are finitely generated, so \labelcref{itm:R1} restricts \(G\) to those with degreewise finitely generated homology. Over \(R=\mathbb Z\) it already fails for \(H_0\) of the unit groupoid on a Cantor set and for \(H_0\) of the CAR groupoid, which is minimal, principal and ample. Truncation does not help: for every \(R\neq 0\), every odd \(\ell\geq 1\) and every \(r\geq 1\) the unit groupoid on a Cantor set carries a finite atomization \(D\) with \(H_\ell(A_\bullet(D;R))\cong R^r\) while \(H_\ell(G;R)=0\).
\end{theoremx}

\begin{theoremx}[\ref{thm:completeness-automatic}, \ref{cor:hypothesis-empty}]\label{thmx:vacuous}
	Let \(G\) be a Hausdorff ample groupoid and \(n\geq 1\). The finite atomizations of finite height form a complete system in \(\PartH(G)\), and neither the poset nor the system depends on the coefficient ring. Hence the hypothesis of the colimit model theorem \ref{thm:global-colimit} is satisfied by every Hausdorff ample groupoid, for every \(n\) and every ring at once, and the theorem is equivalent to the degreewise exhaustion \(\Cc(G_p;R)=\bigcup_{(L,\mathcal Q)}M(L,\mathcal Q)\). A completeness hypothesis therefore selects no groupoids and supplies no instance of \labelcref{itm:R2}.
\end{theoremx}

\begin{theoremx}[\ref{prop:helly-vacuous}, \ref{prop:atom-blowup}]\label{thmx:count}
	Every finite atomization of a Hausdorff ample groupoid is \(n\)-Helly-generated for every \(n\geq 1\), each partition being presented by itself, so \(\PartH(G)=\Part(G)\) and the Helly decoration is empty. It is also inert: for every \(N\geq 1\) there is a cover \(\mathcal U\) of a compact open subset of a Cantor set by \(N\) compact open sets with \(\bigcap\mathcal U\neq\varnothing\), hence \(n\)-Helly for every \(n\) with nerve the full simplex on \(N\) vertices, whose atom partition has \(2^N-1\) members. So the Helly axiom supplies neither \labelcref{itm:R3} nor any restriction at all.
\end{theoremx}

The same self-presentation argument applies verbatim to laminarity, a partition being laminar, so \labelcref{itm:R3} cannot be read as a condition on \(\Part(G)\). This is \ref{rem:laminar-vacuous}, and it is why \ref{thmx:laminar} makes the presentation the datum rather than a property to be verified after the fact.

\Cref{sec:models} sets up the objects, \Cref{sec:resolution,sec:chain,sec:count} treat \labelcref{itm:R1}, \labelcref{itm:R2} and \labelcref{itm:R3} in turn, \Cref{sec:laminar} proves \ref{thmx:laminar}, and \Cref{sec:survives} records the parts of the construction that work independently of all this: the atomization of a single cover contracts its augmented \v Cech complex, and the K\"unneth sequence of \cite[Theorem~2.4]{Matui2016} extends to a principal ideal domain. \Cref{rem:colimit} disposes of a variant proposal, an invariant of a coverage space defined by a colimit over \(n\)-Helly bases, which is that of a point already on a three-point space.

\subsection*{Formalization}
The chain-level content of this note is formalized in Lean 4, and the development is available at
\begin{center}
	\url{https://codeberg.org/Jiren/HellyHomology}
\end{center}
(Lean \texttt{v4.34.0-rc2}, Mathlib rev \texttt{85e3a25}). It contains no \texttt{sorry}, no \texttt{admit} and no \texttt{native\_\allowbreak decide}, and every declaration listed in its \texttt{Axioms.lean} depends only on the trusted Mathlib baseline \texttt{propext}, \texttt{Classical.\allowbreak choice} and \texttt{Quot.\allowbreak sound}. What it covers is the following.

\begin{itemize}
	\item \textbf{The chain complex.} Over \labelcref{itm:I1}: the module \(\Cc(X;R)\) of \ref{def:chain-complex} with the block decomposition of \ref{lem:counting}, the pushforward with its \(R\)-linearity, its functoriality and the identity \labelcref{eq:ring-independence}, the boundary \labelcref{eq:chain-complex} as an \(R\)-linear map with \(\partial\circ\partial=0\), the objects of \ref{def:fin} with the reflexivity and transitivity of the refinement order and the linear independence of the indicators of the atoms, the exhaustion \labelcref{eq:exhaustion}, and the assertion of \ref{def:atomization} that \labelcref{itm:D1} and \labelcref{itm:D2} make \(A_\bullet(D;R)\) a subcomplex for every \(R\) at once.
	\item \textbf{The combinatorics.} \Cref{prop:helly-vacuous} and \ref{rem:laminar-vacuous} in their set-theoretic clauses, \ref{prop:laminar} in the sharp form \labelcref{eq:laminar-atoms}, \ref{lem:nested-laminar}, \ref{lem:refine}\,\labelcref{itm:refine-le}, the contraction \labelcref{eq:cone} of \ref{lem:cone}, the combinatorial steps of \ref{rem:colimit}, and the combinatorial core of \ref{prop:atom-blowup}, namely that \(2^N-1\) pairwise disjoint nonempty sets assemble into a cover which is \(n\)-Helly for every \(n\), has the full simplex on \(N\) vertices as intersection nerve, and has exactly \(2^N-1\) atoms.
	\item \textbf{The models.} \Cref{prop:no-finite-resolution}, the non-finite-generation of \(\mathbb Z[1/2]\) and the injectivity step of \ref{prop:car}, the arithmetic of \ref{ex:unit-groupoid} and \ref{prop:spurious} over \labelcref{itm:I3}, the recursion of \ref{constr:repair} with \ref{lem:repair-works} and \ref{thm:completeness-automatic} over \labelcref{itm:I2}, and the degreewise content of \ref{thm:laminar-model}: the atom partitions of the finite subfamilies of a basis of compact open sets are cofinal in \(\mathrm{Fin}(X)\) and exhaust \(\Cc(X;R)\), with rank at most the number of members used when the basis is laminar.
	\item \textbf{Not formalized.} \Cref{def:nerve} and \ref{lem:nerve-geometry}, replaced by \labelcref{itm:I1}. \Cref{rem:ring-dependence}. \Cref{thm:global-colimit}, together with the transport of \labelcref{eq:exhaustion} into it in \ref{cor:hypothesis-empty}, which needs filtered colimits of \(R\)-modules over the index posets. The poset conclusions \labelcref{eq:parts-agree} and its laminar analogue, the development carrying no object corresponding to \(\Part(G)\). The realization of the configuration of \ref{prop:atom-blowup} inside a Cantor space. \Cref{prop:laminar-exists}, \ref{rem:no-products} and \ref{rem:laminar-limits}. \Cref{lem:refine}\,\labelcref{itm:refine-parent}, which compares nodes across two families, with \ref{thm:laminar-model}\,\labelcref{itm:lm-transition}, which rests on it, and the rounded repair of \ref{thm:laminar-model} with the cross-degree assembly it drives. In \Cref{sec:survives}, the block decomposition of \ref{prop:local-cech} and the K\"unneth argument over a principal ideal domain.
\end{itemize}

Mathlib has no theory of ample étale groupoids, so three inputs are taken as an interface rather than constructed. They are hypotheses, never axioms, and are marked as such in the development.

\begin{enumerate}[label=\textup{I\arabic*},ref=\textup{I\arabic*}]
	\item\label{itm:I1} \textbf{The nerve.} In place of \ref{def:nerve} and \ref{lem:nerve-geometry}, a sequence of Hausdorff spaces with a basis of compact open sets and face maps that are local homeomorphisms and satisfy the simplicial identities, which is exactly what \ref{lem:nerve-geometry} produces.
	\item\label{itm:I2} \textbf{The repair.} The common refinement of two objects of \(\mathrm{Fin}(G_p)\), the one-step repair, and the clauses of \ref{lem:repair-works} asserting that its output is an object of \(\mathrm{Fin}\), satisfies \labelcref{itm:D1} and \labelcref{itm:D2}, and dominates the prescribed lower bound. These rest on \ref{lem:face-image} and \ref{lem:counting}. Proved from them are the recursion, its termination at degree \(0\) and the directedness argument. The interface is not instantiated, so \ref{thm:completeness-automatic} exists in the development as a statement about an arbitrary such structure and not about the atomizations of a groupoid.
	\item\label{itm:I3} \textbf{The unit groupoid.} In \ref{ex:unit-groupoid} and \ref{prop:spurious}, the identification of every face map with the identity, a one-line consequence of \ref{def:nerve}.
\end{enumerate}

\section{The Atomized Chain Models}\label{sec:models}
We fix the objects under discussion. Throughout, \(R\) is a commutative unital ring and \(G\rightrightarrows\Gz\) is a \textbf{Hausdorff ample} groupoid, that is, a locally compact Hausdorff étale groupoid with a basis of compact open bisections, with source and range \(s,r\colon G\to\Gz\).

\begin{definition}\label{def:nerve}
	For \(p\geq 1\) let \(G_p\coloneqq\{(\gamma_1,\dots,\gamma_p)\in G^p : s(\gamma_i)=r(\gamma_{i+1}),\ 1\leq i<p\}\) and \(G_0\coloneqq\Gz\). The \textbf{face maps} \(d_i\colon G_p\to G_{p-1}\), \(0\leq i\leq p\), delete the first arrow for \(i=0\), compose the \(i\)-th and \((i{+}1)\)-st for \(0<i<p\), and delete the last arrow for \(i=p\), with \(d_0=s\) and \(d_1=r\) on \(G_1=G\).
\end{definition}

\begin{lemma}\label{lem:nerve-geometry}
	Each \(G_p\) is locally compact, Hausdorff and totally disconnected with a basis of compact open sets, and each \(d_i\) is a local homeomorphism.
\end{lemma}

\begin{proof}~
	\begin{itemize}
		\item \textbf{The nerve spaces.} For \(p=0\) the unit space \(\Gz\) is open in \(G\) and inherits the three properties, the compact open bisections contained in it forming a basis. For \(p\geq 1\) the set \(G_p\) is the locus in \(G^p\) where the continuous maps \(s\circ\mathrm{pr}_i\) and \(r\circ\mathrm{pr}_{i+1}\) agree, hence closed since \(\Gz\) is Hausdorff, and a closed subspace of the locally compact Hausdorff totally disconnected space \(G^p\) inherits these three properties. For compact open bisections \(B_1,\dots,B_p\) the set \(B_1\times_{s,r}\cdots\times_{s,r}B_p\) is open in \(G_p\) and closed in the compact set \(B_1\times\cdots\times B_p\), hence compact open, and these sets form a basis.
		\item \textbf{The face maps.} For \(p=1\) the maps \(d_0=s\) and \(d_1=r\) restrict to homeomorphisms of a compact open bisection onto its source and range sets, so both are local homeomorphisms. For \(p\geq 2\) work on a basic set \(B=B_1\times_{s,r}\cdots\times_{s,r}B_p\). There \(d_0\) is inverted by \((\gamma_2,\dots,\gamma_p)\mapsto\bigl((s|_{B_1})^{-1}(r(\gamma_2)),\gamma_2,\dots,\gamma_p\bigr)\), and \(d_p\) symmetrically by \(\gamma_p=(r|_{B_p})^{-1}(s(\gamma_{p-1}))\), both restrictions of \(s\) and \(r\) to a bisection being homeomorphisms onto compact open sets. For \(0<i<p\) multiplication \(B_i\times_{s,r}B_{i+1}\to B_iB_{i+1}\) is inverted by \(\gamma\mapsto(\alpha,\alpha^{-1}\gamma)\) with \(\alpha\coloneqq(r|_{B_i})^{-1}(r(\gamma))\), so \(d_i=\id\times\cdots\times m\times\cdots\times\id\) is a homeomorphism on \(B\). \qedhere
	\end{itemize}
\end{proof}

\begin{definition}\label{def:chain-complex}
	For a totally disconnected locally compact Hausdorff space \(X\) let \(\Cc(X;R)\) be the \(R\)-module of locally constant \(u\colon X\to R\) with compact support. For a local homeomorphism \(f\colon X\to Y\) the \textbf{pushforward} is \((f_*u)(y)\coloneqq\sum_{x\in f^{-1}(y)}u(x)\), a finite sum defining an \(R\)-linear map \(\Cc(X;R)\to\Cc(Y;R)\), functorial in \(f\). The \textbf{groupoid chain complex} \cite[Definition~3.1]{Matui2012} is
	\begin{equation}\label{eq:chain-complex}
		C_p(G;R)\coloneqq\Cc(G_p;R),\qquad \partial_p\coloneqq\sum_{i=0}^{p}(-1)^i(d_i)_*,
	\end{equation}
	and \(H_\bullet(G;R)\) is its homology. That \(\partial_{p}\circ\partial_{p+1}=0\) uses only the functoriality of the pushforward and the simplicial identities of \ref{def:nerve}.
\end{definition}

\begin{lemma}\label{lem:face-image}
	Let \(p\geq 1\), \(0\leq i\leq p\) and let \(K\subseteq G_p\) be compact open. Then \(d_i(K)\subseteq G_{p-1}\) is compact open.
\end{lemma}

\begin{proof}
	The map \(d_i\) is continuous and, being a local homeomorphism by \ref{lem:nerve-geometry}, open. Hence \(d_i(K)\) is open and compact, and compact subsets of the Hausdorff space \(G_{p-1}\) are closed.
\end{proof}

\begin{lemma}\label{lem:counting}
	Let \(p\geq 1\), \(0\leq i\leq p\) and let \(P\subseteq G_p\) be compact open. Define
	\begin{equation}\label{eq:counting}
		N_{i,P}\colon G_{p-1}\to\mathbb Z,\qquad y\mapsto\#\bigl(d_i^{-1}(y)\cap P\bigr).
	\end{equation}
	Then \(N_{i,P}\in\Cc(G_{p-1};\mathbb Z)\) with \(\supp N_{i,P}\subseteq d_i(P)\), and for every commutative unital ring \(R\), with \(\chi_R\colon\mathbb Z\to R\) the unique ring homomorphism,
	\begin{equation}\label{eq:ring-independence}
		(d_i)_*1_P=\chi_R\circ N_{i,P}.
	\end{equation}
\end{lemma}

\begin{proof}~
	\begin{itemize}
		\item \textbf{Finiteness and local constancy.} Every \(x\in P\) has a compact open neighbourhood inside \(P\) on which \(d_i\) is injective, and finitely many such neighbourhoods \(V_1,\dots,V_t\) cover the compact set \(P\). The nonempty sets \(P\cap V_1^{\epsilon_1}\cap\cdots\cap V_t^{\epsilon_t}\) with \(\epsilon\in\{0,1\}^t\), where \(V^1\coloneqq V\) and \(V^0\coloneqq G_p\setminus V\), form a finite clopen partition \(P=E_1\sqcup\cdots\sqcup E_u\). Every block has some \(\epsilon_j=1\), the \(V_j\) covering \(P\), hence lies in that \(V_j\), so \(d_i\) is injective on it and maps it homeomorphically onto a compact open set, \(d_i\) being open. Counting preimages blockwise gives \(N_{i,P}=\sum_{l=1}^{u}1_{d_i(E_l)}\), a finite sum of indicators of compact open subsets of \(d_i(P)\), which is compact open by \ref{lem:face-image}. Hence \(N_{i,P}\) is locally constant with compact support inside \(d_i(P)\).
		\item \textbf{Independence of the ring.} For \(y\in G_{p-1}\) the fibre \(d_i^{-1}(y)\cap P\) is finite by the preceding step, and
		      \(\bigl((d_i)_*1_P\bigr)(y)=\sum_{x\in d_i^{-1}(y)\cap P}1_R=\#\bigl(d_i^{-1}(y)\cap P\bigr)\cdot 1_R=\chi_R\bigl(N_{i,P}(y)\bigr)\). \qedhere
	\end{itemize}
\end{proof}

\begin{definition}\label{def:fin}
	For \(X\) as above let \(\mathrm{Fin}(X)\) be the poset whose objects are the pairs \((L,\mathcal Q)\) with \(L\subseteq X\) compact open and \(\mathcal Q\) a partition of \(L\) into finitely many nonempty clopen \textbf{atoms}, the empty set carrying exactly the empty partition, ordered by \((L,\mathcal Q)\leq(L',\mathcal Q')\) if \(L\subseteq L'\) and every atom of \(\mathcal Q\) is a union of atoms of \(\mathcal Q'\). Put \(M(L,\mathcal Q)\coloneqq\bigoplus_{Q\in\mathcal Q}R\cdot 1_Q\subseteq\Cc(X;R)\), a free \(R\)-module of rank \(\lvert\mathcal Q\rvert\), the indicators of distinct atoms being independent.
\end{definition}

\begin{definition}\label{def:atomization}
	A \textbf{finite atomization} of \(G\) is a family \(D=(K_p,\mathcal P_p)_{p\geq 0}\) with \((K_p,\mathcal P_p)\in\mathrm{Fin}(G_p)\) such that
	\begin{enumerate}[label=\textup{D\arabic*},ref=\textup{D\arabic*}]
		\item\label{itm:D1} \(d_i(K_p)\subseteq K_{p-1}\) for all \(p\geq 1\) and \(0\leq i\leq p\),
		\item\label{itm:D2} \(N_{i,P}\) is constant on every atom of \(\mathcal P_{p-1}\), for all \(p\geq 1\), \(0\leq i\leq p\) and \(P\in\mathcal P_p\).
	\end{enumerate}
	\(D\) has \textbf{finite height} if there is \(p_0\) with \(K_p=\varnothing\) for all \(p>p_0\), and the least such \(p_0\) is its \textbf{height}. The atomizations of \(G\) form a poset \(\Part(G)\) under the componentwise order of \ref{def:fin}, and \(A_\bullet(D;R)\) denotes the graded submodule with \(A_p(D;R)\coloneqq M(K_p,\mathcal P_p)\). By \labelcref{itm:D2} and \labelcref{eq:ring-independence} the pushforward \((d_i)_*1_P\) is constant on every atom of \(\mathcal P_{p-1}\) for every \(R\), so the boundary \labelcref{eq:chain-complex} restricts to \(A_\bullet(D;R)\), which is thereby a subcomplex of \(C_\bullet(G;R)\), free of rank \(\lvert\mathcal P_p\rvert\) in degree \(p\), and \(D\leq D'\) induces an inclusion of subcomplexes. Neither \labelcref{itm:D1} nor \labelcref{itm:D2} mentions \(R\), so \(\Part(G)\) is one poset serving all coefficient rings at once.
\end{definition}

\begin{remark}\label{rem:ring-dependence}
	Replacing \labelcref{itm:D2} by the \(R\)-relative condition that \((d_i)_*1_P\) be constant on every atom of \(\mathcal P_{p-1}\) makes the poset depend on \(R\) and is strictly weaker for some \(R\). Let \(G\) be the pair groupoid on \(\{x,y\}\), so that \(G_1=\{x,y\}\times\{x,y\}\) with \(r(a,b)=a\) and \(s(a,b)=b\), and put \(K_0\coloneqq\{x,y\}\), \(\mathcal P_0\coloneqq\{\{x,y\}\}\), \(K_1\coloneqq P\coloneqq\{(x,x),(y,x)\}\), \(\mathcal P_1\coloneqq\{P\}\) and \(K_p\coloneqq\varnothing\) for \(p\geq 2\). Then \labelcref{itm:D1} holds, \(N_{1,P}\equiv 1\) on \(K_0\), and \(N_{0,P}=2\cdot 1_{\{x\}}\) is not constant on the single atom \(\{x,y\}\), so \labelcref{itm:D2} fails. Over \(R=\mathbb Z/2\), however, \((d_0)_*1_P=2\cdot 1_{\{x\}}=0\) is constant, and the \(R\)-relative condition holds. The integral condition \labelcref{itm:D2} is the one that is stable under change of coefficients.
\end{remark}

\begin{definition}\label{def:helly}
	Fix \(n\geq 1\). A family \(\mathsf B\) of subsets of a set is \textbf{\(n\)-Helly} if for every \(m\geq n\) and all \(B_0,\dots,B_m\in\mathsf B\) with \(\bigcap_{i\in J}B_i\neq\varnothing\) for every \(J\subseteq\{0,\dots,m\}\) of cardinality \(n+1\), one has \(\bigcap_{i=0}^m B_i\neq\varnothing\). Its \textbf{intersection nerve} \(N_\bullet(\mathsf B)\) is the simplicial set with \(N_m(\mathsf B)=\{(B_0,\dots,B_m)\in\mathsf B^{m+1} : \bigcap_iB_i\neq\varnothing\}\), faces deleting and degeneracies repeating entries. For a finite cover \(\mathcal U=\{U_a\}_{a\in A}\) of a compact open set \(K\) by compact open subsets, the \textbf{atom partition} \(\mathcal A(\mathcal U)\) consists of the nonempty sets
	\begin{equation}\label{eq:atoms}
		P_S\coloneqq\bigcap_{a\in S}U_a\cap\bigcap_{a\notin S}(K\setminus U_a),\qquad \varnothing\neq S\subseteq A,
	\end{equation}
	a finite clopen partition of \(K\) refining every \(U_a\). A finite atomization is \textbf{\(n\)-Helly-generated} if each \(\mathcal P_p\) equals \(\mathcal A(\mathcal U_p)\) for some finite compact open cover \(\mathcal U_p\) of \(K_p\) whose underlying family is \(n\)-Helly, and \(\PartH(G)\subseteq\Part(G)\) is the subposet of \(n\)-Helly-generated finite atomizations.
\end{definition}

\begin{definition}\label{def:complete}
	A subposet \(\mathcal S\subseteq\PartH(G)\) is a \textbf{complete system} if
	\begin{enumerate}[label=\textup{K\arabic*},ref=\textup{K\arabic*}]
		\item\label{itm:K1} \(\mathcal S\) is nonempty and any two of its elements admit an upper bound in \(\mathcal S\),
		\item\label{itm:K2} for every \(p\geq 0\) and every \((L,\mathcal Q)\in\mathrm{Fin}(G_p)\) there is \(D\in\mathcal S\) with \((L,\mathcal Q)\leq(K_p,\mathcal P_p)\).
	\end{enumerate}
\end{definition}

\begin{theorem}\label{thm:global-colimit}
	Let \(\mathcal S\subseteq\PartH(G)\) be a complete system. Then the inclusions \(A_\bullet(D;R)\hookrightarrow C_\bullet(G;R)\) induce isomorphisms
	\begin{equation}\label{eq:colimit}
		\colim_{D\in\mathcal S}A_\bullet(D;R)\ \cong\ C_\bullet(G;R),
		\qquad
		\colim_{D\in\mathcal S}H_m\bigl(A_\bullet(D;R)\bigr)\ \cong\ H_m(G;R),\quad m\geq 0.
	\end{equation}
\end{theorem}

The proof is the exhaustion \(\Cc(G_p;R)=\bigcup_{(L,\mathcal Q)}M(L,\mathcal Q)\) over \(\mathrm{Fin}(G_p)\), transported along the final projections \(\mathcal S\to\mathrm{Fin}(G_p)\) supplied by \labelcref{itm:K1} and \labelcref{itm:K2}, together with the exactness of filtered colimits, and is spelled out in \ref{cor:hypothesis-empty}. Before turning to the requirements we dispose of the Helly decoration, which constrains the presenting cover \(\mathcal U_p\) and never the partition \(\mathcal P_p\).

\begin{proposition}\label{prop:helly-vacuous}
	Let \(K\) be a compact open set and \(\mathcal Q\) a finite clopen partition of \(K\) into nonempty atoms, regarded as a cover of \(K\). Then \(\mathcal Q\) is \(n\)-Helly for every \(n\geq 1\) and \(\mathcal A(\mathcal Q)=\mathcal Q\). Consequently every finite atomization is \(n\)-Helly-generated for every \(n\), and
	\begin{equation}\label{eq:parts-agree}
		\PartH(G)=\Part(G)\qquad\text{for every }n\geq 1.
	\end{equation}
\end{proposition}

\begin{proof}~
	\begin{itemize}
		\item \textbf{The Helly condition.} Let \(m\geq n\geq 1\) and \(Q_0,\dots,Q_m\in\mathcal Q\) with every \((n{+}1)\)-element subfamily having nonempty intersection. Since \(n+1\geq 2\), the pair \(\{Q_i,Q_j\}\) is contained in such a subfamily for all \(i\neq j\), so \(Q_i\cap Q_j\neq\varnothing\), and distinct atoms are disjoint, whence \(Q_i=Q_j\). All entries agree and \(\bigcap_iQ_i=Q_0\neq\varnothing\). The hypothesis \(n\geq 1\) is needed: for \(n=0\) the condition would force all singleton subfamilies to intersect, which they do, and then all of \(\mathcal Q\) to intersect, which fails as soon as \(\lvert\mathcal Q\rvert\geq 2\).
		\item \textbf{The atom partition.} For \(\varnothing\neq S\subseteq\mathcal Q\) the set \(P_S\) of \labelcref{eq:atoms} is empty unless \(S=\{Q\}\) is a singleton, two distinct atoms being disjoint, and \(P_{\{Q\}}=Q\cap\bigcap_{Q'\neq Q}(K\setminus Q')=Q\), the atoms partitioning \(K\). Hence \(\mathcal A(\mathcal Q)=\mathcal Q\), and taking \(\mathcal U_p\coloneqq\mathcal P_p\) presents every finite atomization. \qedhere
	\end{itemize}
\end{proof}

\section{\texorpdfstring{\labelcref{itm:R1}}{R1}: A Single Model as a Resolution}\label{sec:resolution}
The strongest requirement asks for one finite atomization whose subcomplex computes \(H_\bullet(G;R)\). Rank considerations decide when this is possible.

\begin{proposition}\label{prop:no-finite-resolution}
	Let \(R\) be Noetherian and let \(G\) be a Hausdorff ample groupoid. Then \(H_m(A_\bullet(D;R))\) is a finitely generated \(R\)-module for every finite atomization \(D\) of \(G\) and every \(m\). If \(H_m(G;R)\) is not finitely generated over \(R\), then for every finite atomization \(D\) the map \(H_m(A_\bullet(D;R))\to H_m(G;R)\) induced by the inclusion is not surjective, and in particular \(A_\bullet(D;R)\hookrightarrow C_\bullet(G;R)\) is not a quasi-isomorphism.
\end{proposition}

\begin{proof}~
	\begin{itemize}
		\item \textbf{Finite generation.} \(A_m(D;R)\) is free of finite rank \(\lvert\mathcal P_m\rvert\), hence a Noetherian module over the Noetherian ring \(R\). Its submodule of cycles is therefore finitely generated, and \(H_m(A_\bullet(D;R))\) is a quotient of that submodule.
		\item \textbf{Nonsurjectivity.} A surjection onto \(H_m(G;R)\) from a finitely generated module exhibits \(H_m(G;R)\) as finitely generated. \qedhere
	\end{itemize}
\end{proof}

\begin{example}\label{ex:unit-groupoid}
	Let \(X\) be a Cantor space and \(G\coloneqq X\) the unit groupoid, in which every arrow is a unit. Then \(G_p\cong X\) for every \(p\) with all face maps the identity, so \(C_p(G;R)=C(X;R)\) and \(\partial_p=\sum_{i=0}^p(-1)^i\id\) vanishes for \(p\) odd and equals \(\id\) for \(p\) even, whence
	\begin{equation}\label{eq:unit-homology}
		H_0(G;R)\cong C(X;R),\qquad H_m(G;R)=0\ \text{ for }m\geq 1.
	\end{equation}
	For \(R=\mathbb Z\) the group \(C(X;\mathbb Z)\) is not finitely generated: for every \(k\) a clopen partition of \(X\) into \(k\) nonempty sets has \(\mathbb Z\)-independent indicators, so \(C(X;\mathbb Z)\) contains free subgroups of unbounded rank, whereas every subgroup of a finitely generated abelian group is generated by at most that many elements. By \ref{prop:no-finite-resolution} no finite atomization of \(G\) computes \(H_0(G;\mathbb Z)\).
\end{example}

\begin{proposition}\label{prop:car}
	Let \(X\coloneqq\{0,1\}^{\mathbb N}\) and let \(\mathcal T\) be the tail equivalence relation on \(X\), the AF groupoid of the Bratteli diagram with one vertex at each level and two edges between consecutive levels, whose reduced \(C^\ast\)-algebra is the CAR algebra. Then \(\mathcal T\) is Hausdorff ample, principal and minimal, and
	\begin{equation}\label{eq:car-homology}
		H_0(\mathcal T;\mathbb Z)\cong\mathbb Z[1/2],
	\end{equation}
	which is not a finitely generated abelian group. Hence \ref{prop:no-finite-resolution} applies inside the class of minimal principal ample groupoids to which the HK comparison is addressed.
\end{proposition}

\begin{proof}~
	\begin{itemize}
		\item \textbf{The groupoid.} Write \(S_n\coloneqq\{0,1\}^n\) and \(Z\coloneqq\{0,1\}^{\mathbb N}\), and identify \(X\cong S_n\times Z\) by splitting off the first \(n\) letters. Set \(\mathcal T^{[n]}\coloneqq\{(x,y)\in X\times X : x_k=y_k\ \text{for }k>n\}\), a subgroupoid of the pair groupoid, identified with \(S_n\times S_n\times Z\) by \((qz,q'z)\mapsto(q,q',z)\) and topologized accordingly, so that it is compact, Hausdorff and totally disconnected. Inside \(\mathcal T^{[n+1]}\cong S_{n+1}\times S_{n+1}\times Z\) the subgroupoid \(\mathcal T^{[n]}\) is the set of triples whose first two entries have the same last letter, a clopen condition on a finite discrete factor, so \(\mathcal T^{[n]}\) is clopen in \(\mathcal T^{[n+1]}\), and \(\mathcal T=\bigcup_{n\geq 0}\mathcal T^{[n]}\) carries the inductive limit topology, in which every \(\mathcal T^{[n]}\) is compact open. Two points lie in a common \(\mathcal T^{[n]}\), so \(\mathcal T\) is Hausdorff, locally compact and totally disconnected. The sets \(\{(q,q')\}\times W\) with \(W\subseteq Z\) clopen form a basis, and on each of them the source and range maps are homeomorphisms onto the compact open sets \(q'W\) and \(qW\), so they are compact open bisections and \(\mathcal T\) is Hausdorff ample. It is principal, being an equivalence relation, and minimal, every tail equivalence class being dense.
		\item \textbf{Degree zero.} By compactness every compact open subset of \(\mathcal T\) lies in some \(\mathcal T^{[n]}\), and there it is a finite disjoint union of sets \(\{(q,q')\}\times W\) with \(q,q'\in S_n\) and \(W\subseteq Z\) clopen, the factor \(S_n\times S_n\) being finite discrete. Hence \(\Cc(\mathcal T;\mathbb Z)\) is spanned by the indicators of such sets. On \(\{(q,q')\}\times W\) the maps \(d_0=s\) and \(d_1=r\) are injective with images \(q'W\coloneqq\{q'z : z\in W\}\) and \(qW\), so \(\partial_1 1_{\{(q,q')\}\times W}=1_{q'W}-1_{qW}\) and
		      \begin{equation}\label{eq:car-coinvariants}
			      H_0(\mathcal T;\mathbb Z)=C(X;\mathbb Z)\big/\bigl\langle 1_{qW}-1_{q'W}\ :\ n\geq 0,\ q,q'\in S_n,\ W\subseteq Z\ \text{clopen}\bigr\rangle.
		      \end{equation}
		\item \textbf{The invariant.} Let \(\mu\) be the product measure on \(X\) with \(\mu(\{x_1=0\})=\mu(\{x_1=1\})=1/2\), and let \(\theta\colon C(X;\mathbb Z)\to\mathbb Z[1/2]\), \(u\mapsto\int u\,d\mu\), which lands in \(\mathbb Z[1/2]\) because \(u\) is a finite integral combination of indicators of cylinders and \(\mu\) gives a cylinder of length \(n\) the mass \(2^{-n}\). It kills the relations of \labelcref{eq:car-coinvariants}, since \(\mu(qW)=2^{-n}\mu(W)=\mu(q'W)\), and it is surjective, its image containing \(2^{-n}\) for every \(n\).
		\item \textbf{Injectivity.} Let \(u\in C(X;\mathbb Z)\) with \(\theta(u)=0\). Being locally constant on a compact space, \(u\) is constant on the cylinders of some length \(n\), so \(u=\sum_{q\in S_n}c_q1_{qZ}\) with \(2^{-n}\sum_qc_q=\theta(u)=0\). Taking \(W=Z\) in \labelcref{eq:car-coinvariants} makes all \(1_{qZ}\) with \(q\in S_n\) congruent to one another, so \(u\) is congruent to \(\bigl(\sum_qc_q\bigr)1_{q_0Z}=0\) for any fixed \(q_0\). Hence \(\theta\) induces an isomorphism \labelcref{eq:car-homology}.
		\item \textbf{Not finitely generated.} Put \(\Lambda_k\coloneqq 2^{-k}\mathbb Z\), an increasing chain of subgroups whose union is \(\mathbb Z[1/2]\), every element of \(\mathbb Z[1/2]\) being \(a2^{-k}\) for some \(a\in\mathbb Z\) and some \(k\). A finite subset of \(\mathbb Z[1/2]\) therefore lies in a single \(\Lambda_{k_0}\), and so does the subgroup it generates. But \(2^{-k_0-1}\notin\Lambda_{k_0}\), an equation \(2^{-k_0-1}=a2^{-k_0}\) forcing \(2a=1\) in \(\mathbb Z\), so no finite subset generates \(\mathbb Z[1/2]\). \qedhere
	\end{itemize}
\end{proof}

Truncating the model is the obvious way to keep it finite. It creates homology that is not there.

\begin{proposition}\label{prop:spurious}
	Let \(X\) be a Cantor space, \(G\coloneqq X\) the unit groupoid, \(R\neq 0\), \(\ell\geq 1\) odd and \(r\geq 1\). Let \(\mathcal Q\) be a clopen partition of \(X\) into \(r\) nonempty sets and put \(K_p\coloneqq X\), \(\mathcal P_p\coloneqq\mathcal Q\) for \(0\leq p\leq\ell\), and \(K_p\coloneqq\varnothing\) for \(p>\ell\). Then \(D\coloneqq(K_p,\mathcal P_p)_{p\geq 0}\) is a finite atomization of \(G\) of height \(\ell\) and
	\begin{equation}\label{eq:spurious}
		H_\ell\bigl(A_\bullet(D;R)\bigr)\cong R^r,\qquad\text{while}\qquad H_\ell(G;R)=0.
	\end{equation}
	Moreover \(H_0(A_\bullet(D;R))\cong R^r\) and the map to \(H_0(G;R)\cong C(X;R)\) is injective and not surjective.
\end{proposition}

\begin{proof}~
	\begin{itemize}
		\item \textbf{Atomization.} All face maps are the identity of \(X\), so \(d_i(K_p)=X\subseteq K_{p-1}\) for \(1\leq p\leq\ell\) and \(d_i(\varnothing)=\varnothing\) for \(p>\ell\), which is \labelcref{itm:D1}, and \(N_{i,Q}=1_Q\) is constant on the atoms of \(\mathcal Q\), which is \labelcref{itm:D2}.
		\item \textbf{The complex.} \(A_p(D;R)=M(X,\mathcal Q)\cong R^r\) for \(0\leq p\leq\ell\) and \(0\) above, with \(\partial_p=\sum_{i=0}^p(-1)^i\id\), so \(\partial_p=0\) for \(p\) odd and \(\partial_p=\id\) for \(p\) even.
		\item \textbf{Top degree.} \(\ell\) is odd, so \(\partial_\ell=0\), and \(A_{\ell+1}(D;R)=0\), whence \(H_\ell(A_\bullet(D;R))=A_\ell(D;R)\cong R^r\). By \labelcref{eq:unit-homology} the group \(H_\ell(G;R)\) vanishes, \(\ell\geq 1\).
		\item \textbf{Degree zero.} \(\partial_1=0\) on both complexes, so \(H_0(A_\bullet(D;R))=M(X,\mathcal Q)\) and \(H_0(G;R)=C(X;R)\), and the induced map is the inclusion \(M(X,\mathcal Q)\subseteq C(X;R)\), which is injective and misses the indicator of any proper nonempty clopen subset of an atom. \qedhere
	\end{itemize}
\end{proof}

So a finite model may have free homology of any prescribed rank in any prescribed odd degree while the groupoid has none there, and in the degree where the groupoid does have homology the model sees an arbitrarily small part of it. Requirement \labelcref{itm:R1} is therefore available exactly for groupoids whose homology is degreewise finitely generated over \(R\), and for those it is a hypothesis on \(G\), not a mechanism.

\section{\texorpdfstring{\labelcref{itm:R2}}{R2}: A Controlled Cofinal Chain}\label{sec:chain}
Requirement \labelcref{itm:R2} asks not for one model but for a chain of them with known ranks and known transition maps, which is what the verified computations use. \Cref{thm:global-colimit} produces a chain only from a complete system, so one may hope that requiring a complete system is a real hypothesis. It is not. We compute the supply of finite atomizations directly. The construction is a downward repair: prescribe a partition in one degree, take the images of the faces below it, and refine the target by the level sets of the counting functions \labelcref{eq:counting}. \Cref{lem:face-image,lem:counting} make the repair well defined.

\begin{construction}\label{constr:repair}
	Let \(p_0\geq 0\), let \((L,\mathcal Q)\in\mathrm{Fin}(G_{p_0})\) and let \(F_p\subseteq G_p\) be compact open for \(0\leq p<p_0\), with finite clopen partitions \(\mathcal F_p\) of \(F_p\). Define \((K_p,\mathcal P_p)_{p\geq 0}\) by \(K_p\coloneqq\varnothing\) for \(p>p_0\), by \((K_{p_0},\mathcal P_{p_0})\coloneqq(L,\mathcal Q)\), and downward for \(q=p_0,p_0-1,\dots,1\) by
	\begin{equation}\label{eq:repair}
		K_{q-1}\coloneqq F_{q-1}\cup\bigcup_{i=0}^{q}d_i(K_q),
	\end{equation}
	with \(\mathcal P_{q-1}\) the set of nonempty members of the common refinement inside \(K_{q-1}\) of the partition \(\mathcal F_{q-1}\cup\{K_{q-1}\setminus F_{q-1}\}\) and of the level-set partitions of the functions \(N_{i,P}\) of \labelcref{eq:counting}, for \(0\leq i\leq q\) and \(P\in\mathcal P_q\).
\end{construction}

\begin{lemma}\label{lem:repair-works}
	\Cref{constr:repair} produces a finite atomization \(D\) of height at most \(p_0\) with \((K_{p_0},\mathcal P_{p_0})=(L,\mathcal Q)\) and \((F_p,\mathcal F_p)\leq(K_p,\mathcal P_p)\) for \(0\leq p<p_0\).
\end{lemma}

\begin{proof}~
	\begin{itemize}
		\item \textbf{Objects of \(\mathrm{Fin}\).} By \ref{lem:face-image} each \(d_i(K_q)\) is compact open, so \(K_{q-1}\) is a finite union of compact open sets and hence compact open. Each \(N_{i,P}\) is locally constant with compact support by \ref{lem:counting}, so it takes finitely many values, and each of its level sets meets \(K_{q-1}\) in a clopen subset. Finitely many functions are involved, \(\mathcal P_q\) being finite, so their common refinement with \(\mathcal F_{q-1}\cup\{K_{q-1}\setminus F_{q-1}\}\) is a finite clopen partition of \(K_{q-1}\), and discarding its empty members leaves an object of \(\mathrm{Fin}(G_{q-1})\).
		\item \textbf{Axiom \labelcref{itm:D1}.} For \(1\leq q\leq p_0\) the inclusion \(d_i(K_q)\subseteq K_{q-1}\) is part of \labelcref{eq:repair}, and for \(q>p_0\) both sides are empty.
		\item \textbf{Axiom \labelcref{itm:D2}.} For \(1\leq q\leq p_0\), \(P\in\mathcal P_q\) and \(0\leq i\leq q\) the partition \(\mathcal P_{q-1}\) refines the level-set partition of \(N_{i,P}\), so \(N_{i,P}\) is constant on every atom of \(\mathcal P_{q-1}\). For \(q>p_0\) the set \(\mathcal P_q\) is empty and the condition is vacuous.
		\item \textbf{Comparison.} \(\mathcal P_{q-1}\) refines \(\mathcal F_{q-1}\cup\{K_{q-1}\setminus F_{q-1}\}\), so \(F_{q-1}\subseteq K_{q-1}\) and every atom of \(\mathcal F_{q-1}\) is a union of atoms of \(\mathcal P_{q-1}\), which is \((F_{q-1},\mathcal F_{q-1})\leq(K_{q-1},\mathcal P_{q-1})\). The value at \(p_0\) is prescribed, and the repair does not revisit a degree, so it terminates at degree \(0\). \qedhere
	\end{itemize}
\end{proof}

\begin{theorem}\label{thm:completeness-automatic}
	Let \(G\) be a Hausdorff ample groupoid and \(n\geq 1\). The set
	\begin{equation}\label{eq:sfh}
		\mathcal S_{\mathrm{fh}}(G)\coloneqq\{D\in\Part(G) : D\ \text{has finite height}\}
	\end{equation}
	is a complete system in \(\PartH(G)\). It does not depend on the coefficient ring, and neither does \(\PartH(G)\), which therefore contains this one complete system for every Hausdorff ample groupoid, every \(n\geq 1\) and every commutative unital ring at once.
\end{theorem}

\begin{proof}~
	\begin{itemize}
		\item \textbf{Admissibility.} \(\mathcal S_{\mathrm{fh}}(G)\subseteq\Part(G)=\PartH(G)\) by \ref{prop:helly-vacuous}, and \labelcref{itm:D1} and \labelcref{itm:D2} do not mention \(R\), so \(\mathcal S_{\mathrm{fh}}(G)\) is the same set for every coefficient ring.
		\item \textbf{Nonemptiness.} The atomization with \(K_p=\varnothing\) for all \(p\) lies in \(\mathcal S_{\mathrm{fh}}(G)\).
		\item \textbf{Cofinality \labelcref{itm:K2}.} Let \(p_0\geq 0\) and \((L,\mathcal Q)\in\mathrm{Fin}(G_{p_0})\). Apply \ref{constr:repair} with this \((L,\mathcal Q)\) and with \((F_p,\mathcal F_p)\coloneqq(\varnothing,\varnothing)\) for \(p<p_0\). By \ref{lem:repair-works} the result is a finite atomization of height at most \(p_0\) whose \(p_0\)-th component is \((L,\mathcal Q)\) itself.
		\item \textbf{Upper bounds \labelcref{itm:K1}.} Let \(D=(K,\mathcal P)\) and \(D'=(K',\mathcal P')\) lie in \(\mathcal S_{\mathrm{fh}}(G)\) and let \(p_0\) bound both heights. Put \(L\coloneqq K_{p_0}\cup K'_{p_0}\), a compact open set, and let \(\mathcal Q\) consist of the nonempty members of the common refinement of \(\mathcal P_{p_0}\cup\{L\setminus K_{p_0}\}\) and \(\mathcal P'_{p_0}\cup\{L\setminus K'_{p_0}\}\), a finite clopen partition of \(L\) with \((K_{p_0},\mathcal P_{p_0})\leq(L,\mathcal Q)\geq(K'_{p_0},\mathcal P'_{p_0})\). Run \ref{constr:repair} on \((L,\mathcal Q)\) with \(F_p\coloneqq K_p\cup K'_p\) and \(\mathcal F_p\) the nonempty members of the common refinement of \(\mathcal P_p\cup\{F_p\setminus K_p\}\) and \(\mathcal P'_p\cup\{F_p\setminus K'_p\}\), for \(p<p_0\). The output \(\widehat D\) has height at most \(p_0\) by \ref{lem:repair-works}, and in each degree \(p\leq p_0\) its component refines \((F_p,\mathcal F_p)\), which dominates both \((K_p,\mathcal P_p)\) and \((K'_p,\mathcal P'_p)\), while in degrees \(p>p_0\) all three components are empty. Hence \(D\leq\widehat D\geq D'\). \qedhere
	\end{itemize}
\end{proof}

\begin{corollary}\label{cor:hypothesis-empty}
	The hypothesis of \ref{thm:global-colimit} is satisfied by every Hausdorff ample groupoid, every \(n\geq 1\) and every commutative unital ring \(R\). The conclusion \labelcref{eq:colimit} holds for \(\mathcal S=\mathcal S_{\mathrm{fh}}(G)\) and is equivalent to the degreewise exhaustion
	\begin{equation}\label{eq:exhaustion}
		\Cc(G_p;R)=\bigcup_{(L,\mathcal Q)\in\mathrm{Fin}(G_p)}M(L,\mathcal Q),\qquad p\geq 0.
	\end{equation}
\end{corollary}

\begin{proof}~
	\begin{itemize}
		\item \textbf{From the exhaustion to the colimit.} By \ref{thm:completeness-automatic} the system \(\mathcal S_{\mathrm{fh}}(G)\) is filtered, and the projections \(\pi_p\colon\mathcal S_{\mathrm{fh}}(G)\to\mathrm{Fin}(G_p)\) are final, the comma poset over \((L,\mathcal Q)\) being nonempty by \labelcref{itm:K2} and connected by \labelcref{itm:K1}, and every triangle in a poset commuting. Hence \(\colim_{\mathcal S_{\mathrm{fh}}}A_p(-;R)\cong\colim_{\mathrm{Fin}(G_p)}M\). The poset \(\mathrm{Fin}(G_p)\) is directed by the common refinement used in the upper-bound step of \ref{thm:completeness-automatic}, so the second colimit is the union of the submodules \(M(L,\mathcal Q)\) of \(\Cc(G_p;R)\), transition maps and legs all being inclusions, and it equals \(\Cc(G_p;R)\) exactly when \labelcref{eq:exhaustion} holds. The differentials agree because every \(A_\bullet(D;R)\) carries the restriction of the one boundary \labelcref{eq:chain-complex}, and homology commutes with filtered colimits.
		\item \textbf{From the colimit to the exhaustion.} Conversely the degreewise surjectivity of the first isomorphism in \labelcref{eq:colimit} reads \(\Cc(G_p;R)=\bigcup_{D\in\mathcal S}A_p(D;R)\), and each \(A_p(D;R)=M(K_p,\mathcal P_p)\).
		\item \textbf{The exhaustion.} Given \(u\in\Cc(G_p;R)\) nonzero, the support \(L\coloneqq\supp u=\{u\neq 0\}\) is compact open, the level sets \(u^{-1}(c)\cap L\) with \(c\in u(L)\) are open, pairwise disjoint and cover \(L\), so there are finitely many of them, they are clopen in \(L\), and \(u=\sum_c c\cdot 1_{u^{-1}(c)\cap L}\in M(L,\mathcal Q_u)\). \qedhere
	\end{itemize}
\end{proof}

\begin{remark}\label{rem:examples-not-special}
	Exhibiting a complete system for a particular class of groupoids therefore establishes nothing about that class, and \labelcref{eq:exhaustion} is all that \ref{thm:global-colimit} says. The level partitions of a Bratteli diagram, the cylinder partitions of a graph groupoid and the translate-refined partitions of a Cantor \(\mathbb Z\)-system are instances of \ref{thm:completeness-automatic}, distinguished only by being written in the symbolic coordinates of their models. What distinguishes them is not that they are complete but that their ranks and transition maps are prescribed, which is exactly \labelcref{itm:R2} and is extra data on top of \ref{thm:completeness-automatic}.
\end{remark}

\section{\texorpdfstring{\labelcref{itm:R3}}{R3}: Bounding the Atom Partition}\label{sec:count}
Requirement \labelcref{itm:R3} is the only one of the three that is a condition on covers, and it is the one an intersection axiom might be expected to supply. It does not. By \ref{prop:helly-vacuous} the Helly condition constrains the presenting cover \(\mathcal U_p\) and never the partition \(\mathcal P_p\), and the two are independent in the strongest sense: a cover can be \(1\)-Helly with the largest possible nerve and the largest possible atom partition at once.

\begin{proposition}\label{prop:atom-blowup}
	Let \(N\geq 1\). There are a compact open subset \(K\) of a Cantor space and a cover \(\mathcal U=\{U_a\}_{a=1}^{N}\) of \(K\) by compact open sets with \(\bigcap_{a}U_a\neq\varnothing\), so that \(\mathcal U\) is \(n\)-Helly for every \(n\geq 1\) and its intersection nerve is the full simplex on \(N\) vertices, while
	\begin{equation}\label{eq:blowup}
		\lvert\mathcal A(\mathcal U)\rvert=2^{N}-1.
	\end{equation}
\end{proposition}

\begin{proof}~
	\begin{itemize}
		\item \textbf{The cover.} Index the nonempty subsets of \(\{1,\dots,N\}\) by \(T\) and choose pairwise disjoint nonempty compact open sets \(K_T\) in a Cantor space, one for each of the \(2^N-1\) such \(T\), which is possible because a Cantor space admits clopen partitions of every finite cardinality. Put \(K\coloneqq\bigsqcup_TK_T\) and \(U_a\coloneqq\bigsqcup_{T\ni a}K_T\), a compact open subset of \(K\). Every \(K_T\) has \(T\neq\varnothing\), so it lies in some \(U_a\) and \(\mathcal U\) covers \(K\).
		\item \textbf{Helly and the nerve.} \(\bigcap_{a=1}^NU_a\supseteq K_{\{1,\dots,N\}}\neq\varnothing\), so every subfamily has nonempty intersection, every tuple of members is a simplex of the intersection nerve, and the Helly condition of \ref{def:helly} holds for every \(n\geq 1\) with nothing to check.
		\item \textbf{The atoms.} For \(\varnothing\neq S\subseteq\{1,\dots,N\}\) the atom \labelcref{eq:atoms} is \(P_S=\bigcap_{a\in S}U_a\cap\bigcap_{a\notin S}(K\setminus U_a)=\bigsqcup\{K_T : T\supseteq S\ \text{and}\ T\cap S^{\mathrm c}=\varnothing\}=K_S\), which is nonempty. Distinct \(S\) give distinct atoms, so \(\lvert\mathcal A(\mathcal U)\rvert=2^N-1\). \qedhere
	\end{itemize}
\end{proof}

The hypothesis that does bound the count is nestedness.

\begin{definition}\label{def:laminar}
	A family \(\mathcal U=\{U_a\}_{a\in A}\) of sets is \textbf{laminar} if any two members are disjoint or comparable under inclusion, so that the members containing a given point form a chain. The \textbf{node} of \(U_a\) in \(\mathcal U\) is
	\begin{equation}\label{eq:node}
		\nu_{\mathcal U}(U_a)\coloneqq U_a\setminus\bigcup\{U_b : U_b\subsetneq U_a\}.
	\end{equation}
\end{definition}

\begin{proposition}\label{prop:laminar}
	Let \(\mathcal U=\{U_a\}_{a\in A}\) be a laminar family with \(\lvert A\rvert=N\) finite. Then \(\mathcal U\) is \(1\)-Helly. If moreover \(\mathcal U\) covers \(K\) by subsets of \(K\), then for every \(x\in K\) the chain \(\{U_a : x\in U_a\}\) has a least member \(U_\star(x)\), the atom of \(\mathcal A(\mathcal U)\) containing \(x\) is \(\nu_{\mathcal U}(U_\star(x))\), conversely \(U_a=U_\star(x)\) for every \(x\in\nu_{\mathcal U}(U_a)\), and
	\begin{equation}\label{eq:laminar-atoms}
		\mathcal A(\mathcal U)=\bigl\{\nu_{\mathcal U}(U_a) : a\in A\bigr\}\setminus\{\varnothing\},
		\qquad\lvert\mathcal A(\mathcal U)\rvert\leq N.
	\end{equation}
	Only the set-theoretic content of \labelcref{eq:atoms} enters, so neither \(K\) nor the \(U_a\) need carry a topology here.
\end{proposition}

\begin{proof}~
	\begin{itemize}
		\item \textbf{The Helly condition.} Let \(m\geq 1\) and \(U_{a_0},\dots,U_{a_m}\in\mathcal U\) with \(U_{a_i}\cap U_{a_j}\neq\varnothing\) for all \(i\neq j\). Pairwise intersecting members of a laminar family are comparable, so \(\{U_{a_0},\dots,U_{a_m}\}\) is a finite chain under inclusion and has a least member \(U_{a_k}\), which meets any other member and is therefore nonempty. Then \(\bigcap_iU_{a_i}=U_{a_k}\neq\varnothing\).
		\item \textbf{The least member of a signature.} Let \(x\in K\) and \(S(x)\coloneqq\{a\in A : x\in U_a\}\), nonempty because \(\mathcal U\) covers \(K\). Any two members of \(\{U_a\}_{a\in S(x)}\) contain \(x\), hence meet, hence are comparable, so this chain is finite and nonempty and has a least member \(U_\star(x)\).
		\item \textbf{The atom is the node.} We show \(P_{S(x)}=\nu_{\mathcal U}(U_\star(x))\) from \labelcref{eq:atoms}. If \(y\in P_{S(x)}\), then \(S(y)=S(x)\), so \(y\in U_\star(x)\), and \(U_b\subsetneq U_\star(x)\) forces \(b\notin S(x)\) by minimality and hence \(y\notin U_b\). Conversely let \(y\in\nu_{\mathcal U}(U_\star(x))\) and \(a\in A\). If \(a\in S(x)\), then \(U_\star(x)\subseteq U_a\) and \(y\in U_a\). If \(a\notin S(x)\), then \(U_a\) and \(U_\star(x)\) are disjoint or comparable, while \(U_\star(x)\subseteq U_a\) would give \(x\in U_a\) and \(U_a=U_\star(x)\) would give \(a\in S(x)\), so they are disjoint or \(U_a\subsetneq U_\star(x)\), and \(y\notin U_a\) in either case. Hence \(S(y)=S(x)\) and \(y\in P_{S(x)}\).
		\item \textbf{Every nonempty node is an atom.} Let \(x\in\nu_{\mathcal U}(U_a)\). Then \(a\in S(x)\), and a member \(U_b\) with \(b\in S(x)\) meets \(U_a\) and is therefore comparable with it, while \(U_b\subsetneq U_a\) is excluded by \(x\in\nu_{\mathcal U}(U_a)\). So \(U_a=U_\star(x)\) and \(\nu_{\mathcal U}(U_a)=P_{S(x)}\in\mathcal A(\mathcal U)\) by the preceding step. This proves the equality in \labelcref{eq:laminar-atoms}, and the bound follows, the right-hand side having at most \(N\) elements. \qedhere
	\end{itemize}
\end{proof}

Laminarity is thus stronger than the \(1\)-Helly condition, and strictly stronger by \ref{prop:atom-blowup}, whose cover is \(n\)-Helly for every \(n\) and, for \(N\geq 2\), not laminar. The gap between \labelcref{eq:blowup} and \labelcref{eq:laminar-atoms} is the whole of \labelcref{itm:R3}: the Helly number measures the cost of deciding which tuples are simplices of the intersection nerve and is insensitive to the size of the Boolean algebra generated, whereas laminarity indexes the atoms by the members. What laminarity does not do is select atomizations.

\begin{remark}\label{rem:laminar-vacuous}
	Read as a condition on \(\Part(G)\), laminarity of the presenting covers is as empty as the Helly condition, and for the same reason. Distinct atoms of a partition are disjoint, so every finite clopen partition is laminar, and \(\mathcal A(\mathcal P_p)=\mathcal P_p\) by \ref{prop:helly-vacuous}. Taking \(\mathcal U_p\coloneqq\mathcal P_p\) therefore presents every finite atomization by a laminar cover, the subposet of laminar-generated finite atomizations is again all of \(\Part(G)\), and \labelcref{eq:laminar-atoms} degenerates to \(\lvert\mathcal P_p\rvert\leq\lvert\mathcal P_p\rvert\).

	What \labelcref{eq:laminar-atoms} bounds is the cost of a presentation one is \emph{given}, and a presentation is data, not a property. This is how the finite input arises in practice: the prefix cylinders of a path space and the level cylinders of a Bratteli diagram come first and the partitions second. \Cref{sec:laminar} makes that datum the hypothesis.
\end{remark}

\section{Laminar Presentations}\label{sec:laminar}
By \ref{rem:laminar-vacuous} a nestedness condition imposed on \(\Part(G)\) is empty. We therefore fix the nested family first and read the atomizations off it.

\begin{definition}\label{def:laminar-pres}
	Let \(X\) be totally disconnected, locally compact and Hausdorff. A \textbf{laminar basis} of \(X\) is a laminar family \(\mathcal L\) of compact open subsets of \(X\) such that every compact open subset of \(X\) is a finite union of members of \(\mathcal L\). A \textbf{laminar presentation} of \(G\) is a family \(\mathcal L=(\mathcal L_p)_{p\geq 0}\) with \(\mathcal L_p\) a laminar basis of \(G_p\). A finite atomization \(D=(K_p,\mathcal P_p)\) is \textbf{subordinate} to \(\mathcal L\) if for every \(p\) there is a finite \(\mathcal U_p\subseteq\mathcal L_p\) with \(K_p=\bigcup\mathcal U_p\) and \(\mathcal P_p=\mathcal A(\mathcal U_p)\), and \(\Part^{\mathcal L}(G)\subseteq\Part(G)\) is the subposet of \(\mathcal L\)-subordinate finite atomizations.
\end{definition}

Two lemmas do the work. The first says that the nested partitions of the standard examples are laminar families, the second that enlarging the presenting family refines the partition in a way one can write down.

\begin{lemma}\label{lem:nested-laminar}
	Let \(\mathcal Q_0,\mathcal Q_1,\dots\) be partitions of one set, each refining the previous. Then \(\bigcup_k\mathcal Q_k\) is laminar.
\end{lemma}

\begin{proof}
	Let \(U\in\mathcal Q_j\) and \(V\in\mathcal Q_k\). For \(j=k\) the two are equal or disjoint. For \(j<k\) the partition \(\mathcal Q_k\) refines \(\mathcal Q_j\), refinement of partitions being transitive, so \(U\) is a union of members of \(\mathcal Q_k\). If \(V\) is one of them, then \(V\subseteq U\), and otherwise \(V\) is disjoint from each of them and hence from \(U\). The case \(k<j\) is symmetric.
\end{proof}

\begin{lemma}\label{lem:refine}
	Let \(\mathcal U\subseteq\mathcal U'\) be families of sets, \(K\coloneqq\bigcup\mathcal U\) and \(K'\coloneqq\bigcup\mathcal U'\), regarded as covers of \(K\) and of \(K'\), with \(\mathcal A(-)\) read as in \ref{prop:laminar} through the set-theoretic content of \labelcref{eq:atoms}.
	\begin{enumerate}[label=\textup{\arabic*},ref=\textup{\arabic*}]
		\item\label{itm:refine-le} Every atom of \(\mathcal A(\mathcal U')\) is contained in \(K\) or disjoint from it, and every atom of \(\mathcal A(\mathcal U)\) is the union of the atoms of \(\mathcal A(\mathcal U')\) contained in it. Hence every union of members of \(\mathcal U\) is a union of atoms of \(\mathcal A(\mathcal U')\), and \((K,\mathcal A(\mathcal U))\leq(K',\mathcal A(\mathcal U'))\) whenever both pairs are objects of \(\mathrm{Fin}(X)\).
		\item\label{itm:refine-parent} Let \(\mathcal U'\) be laminar and finite and let \(U'\in\mathcal U'\) have \(\nu_{\mathcal U'}(U')\) meeting \(K\). Then \(\{V\in\mathcal U : U'\subseteq V\}\) is a nonempty chain, and \(\nu_{\mathcal U'}(U')\subseteq\nu_{\mathcal U}(U)\) for its least member \(U\).
	\end{enumerate}
\end{lemma}

\begin{proof}~
	\begin{itemize}
		\item \textbf{Signatures.} Write \(S(x)\coloneqq\{V\in\mathcal U : x\in V\}\) and \(S'(x)\coloneqq\{V\in\mathcal U' : x\in V\}\), so that \(S(x)=S'(x)\cap\mathcal U\), and \(x\in K\) exactly when \(S(x)\neq\varnothing\). By \labelcref{eq:atoms} the atom of \(\mathcal A(\mathcal U')\) containing \(x\in K'\) is the set of \(y\in K'\) with \(S'(y)=S'(x)\), and likewise for \(\mathcal U\).
		\item \textbf{Refinement,} \labelcref{itm:refine-le}\textbf{.} Points of one atom of \(\mathcal A(\mathcal U')\) share their signature \(S'\), hence share \(S=S'\cap\mathcal U\), hence lie all in \(K\) or all outside it, and in the first case they lie in one atom of \(\mathcal A(\mathcal U)\). So each atom of \(\mathcal A(\mathcal U)\) is the union of those atoms of \(\mathcal A(\mathcal U')\) it contains, and \(K\subseteq K'\). Each member of \(\mathcal U\) is in turn a union of atoms of \(\mathcal A(\mathcal U)\), an atom being contained in or disjoint from every member, so a union of members of \(\mathcal U\) is a union of atoms of \(\mathcal A(\mathcal U')\).
		\item \textbf{The least ancestor,} \labelcref{itm:refine-parent}\textbf{.} Let \(x\in\nu_{\mathcal U'}(U')\cap K\). By \ref{prop:laminar} applied to \(\mathcal U'\) the set \(U'\) is the least member of \(S'(x)\), so every \(V\in S(x)\subseteq S'(x)\) satisfies \(U'\subseteq V\), and conversely \(U'\subseteq V\) with \(V\in\mathcal U\) gives \(x\in V\). Hence \(S(x)=\{V\in\mathcal U : U'\subseteq V\}\), which is nonempty because \(x\in K\) and is a chain because its members all contain \(x\) and \(\mathcal U'\) is laminar. Its least member \(U\) satisfies \(\nu_{\mathcal U}(U)=P_{S(x)}\) by \ref{prop:laminar} applied to \(\mathcal U\), laminar and finite as a subfamily of \(\mathcal U'\), and \(\nu_{\mathcal U'}(U')=P'_{S'(x)}\subseteq P_{S(x)}\) by \labelcref{itm:refine-le}. \qedhere
	\end{itemize}
\end{proof}

Finiteness is used only in \labelcref{itm:refine-parent}, to produce the least members. \Cref{prop:laminar-exists} below shows that the hypothesis of \ref{def:laminar-pres} is satisfiable, and \ref{rem:no-products} that it has to be arranged degree by degree.

\begin{proposition}\label{prop:laminar-exists}
	Every second countable, locally compact, Hausdorff, totally disconnected space has a countable laminar basis. Hence every second countable Hausdorff ample groupoid has a countable laminar presentation.
\end{proposition}

\begin{proof}~
	\begin{itemize}
		\item \textbf{Decomposition.} Let \(X\) be as stated. The compact open sets form a basis, \(X\) being locally compact Hausdorff and totally disconnected, and \(X\) is \(\sigma\)-compact, being locally compact Hausdorff and second countable, hence Lindelöf. Covering each member of a compact exhaustion by finitely many compact open sets and taking unions gives compact open \(Y_1\subseteq Y_2\subseteq\cdots\) with union \(X\). Put \(X_1\coloneqq Y_1\) and \(X_m\coloneqq Y_m\setminus Y_{m-1}\) for \(m\geq 2\), which are open, \(Y_{m-1}\) being compact and hence closed, and compact, being closed in \(Y_m\). They are pairwise disjoint with union \(X\), and we discard those that are empty.
		\item \textbf{One block.} Fix \(m\). The clopen subsets of \(X_m\) are exactly its compact open subsets, \(X_m\) being compact, and they form a basis of \(X_m\). There are at most countably many of them, because \(X_m\) is second countable and a clopen subset, being open, is a union of members of a fixed countable basis and, being compact, a finite such union. Enumerate them as \(V_1,V_2,\dots\), with repetitions if there are finitely many. Let \(\mathcal Q^{(k)}\) be the atom partition of \(\{X_m,V_1,\dots,V_k\}\) inside \(X_m\), a finite clopen partition, so that \(\mathcal Q^{(0)}=\{X_m\}\) and \(\mathcal Q^{(k)}\) refines \(\mathcal Q^{(k-1)}\) by \ref{lem:refine}\,\labelcref{itm:refine-le}. Put \(\mathcal L_{(m)}\coloneqq\bigcup_k\mathcal Q^{(k)}\), countable and laminar by \ref{lem:nested-laminar}, and consisting of compact open sets. It is a laminar basis of \(X_m\): a compact open \(W\subseteq X_m\) is one of the \(V_j\), hence a union of atoms of \(\mathcal Q^{(j)}\), each atom being contained in or disjoint from \(V_j\).
		\item \textbf{Assembly.} Put \(\mathcal L\coloneqq\bigcup_m\mathcal L_{(m)}\), countable, and containing every \(X_m\). It is laminar: members of one \(\mathcal L_{(m)}\) are nested or disjoint, and members of different blocks are disjoint, the \(X_m\) being disjoint. It is a basis: a compact open \(W\subseteq X\) is covered by the open sets \(X_m\), hence by finitely many of them, and each \(W\cap X_m\) is compact open in \(X_m\) and so a finite union of members of \(\mathcal L_{(m)}\).
		\item \textbf{The nerve.} By \ref{lem:nerve-geometry} each \(G_p\) is locally compact, Hausdorff and totally disconnected, and it is second countable, being an open subspace of \(G\) for \(p=0\) and a subspace of \(G^p\) for \(p\geq 1\). Applying the above in each degree gives a countable laminar presentation. \qedhere
	\end{itemize}
\end{proof}

\begin{remark}\label{rem:no-products}
	Laminarity is not stable under products: if \(U_1\subsetneq U_1'\) and \(U_2'\subsetneq U_2\) are members of a laminar family with \(U_1,U_2'\neq\varnothing\), then \((U_1\times U_2)\cap(U_1'\times U_2')=U_1\times U_2'\) is nonempty and properly contained in each of the two. A laminar basis of \(G\) therefore carries no guarantee that the basic sets \(B_1\times_{s,r}\cdots\times_{s,r}B_p\) of \ref{lem:nerve-geometry} are laminar, which is why \(\mathcal L_p\) is chosen in each degree separately in \ref{prop:laminar-exists} rather than built from \(\mathcal L_0\). We do not claim that the fibre products always fail: for the unit groupoid every face map is the identity, so \(B_1\times_{s,r}B_2\) is \(B_1\cap B_2\), which is a member of a laminar family or empty, and the family of fibre products is laminar.
\end{remark}

\begin{theorem}\label{thm:laminar-model}
	Let \(G\) be a Hausdorff ample groupoid and \(\mathcal L\) a laminar presentation of \(G\).
	\begin{enumerate}[label=\textup{\arabic*},ref=\textup{\arabic*}]
		\item\label{itm:lm-complete} The \(\mathcal L\)-subordinate finite atomizations of finite height form a complete system in \(\PartH(G)\), which is \(\Part(G)\) by \ref{prop:helly-vacuous}.
		\item\label{itm:lm-rank} If \(D\in\Part^{\mathcal L}(G)\) is presented by families \(\mathcal U_p\), then \(\mathcal P_p=\{\nu_{\mathcal U_p}(U)\}_{U\in\mathcal U_p}\setminus\{\varnothing\}\) and the atoms of \(\mathcal P_p\) are pairwise disjoint nonempty nodes, so \(A_p(D;R)\) is free of rank \(\lvert\mathcal P_p\rvert\leq\lvert\mathcal U_p\rvert\).
		\item\label{itm:lm-transition} If \(D,D'\in\Part^{\mathcal L}(G)\) are presented by families with \(\mathcal U_p\subseteq\mathcal U'_p\) for all \(p\), then \(D\leq D'\), and for \(U\in\mathcal U_p\) with \(\nu_{\mathcal U_p}(U)\neq\varnothing\) the inclusion \(A_p(D;R)\hookrightarrow A_p(D';R)\) sends \(1_{\nu_{\mathcal U_p}(U)}\) to the sum of the \(1_{\nu_{\mathcal U'_p}(U')}\) over those \(U'\in\mathcal U'_p\) for which \(U\) is the least \(V\in\mathcal U_p\) with \(U'\subseteq V\).
		\item\label{itm:lm-chain} If every \(\mathcal L_p\) is countable, then \(\Part^{\mathcal L}(G)\) contains a chain \(D^{(0)}\leq D^{(1)}\leq\cdots\) of finite-height atomizations which is itself a complete system, with \(\mathcal U^{(k)}_p\subseteq\mathcal U^{(k+1)}_p\) for all \(k\) and \(p\).
	\end{enumerate}
	Requirement \labelcref{itm:R3} therefore holds for every laminar presentation, and \labelcref{itm:R2} for every countable one, in the form \labelcref{itm:lm-rank}--\labelcref{itm:lm-chain}: the presenting families are determined by \(\mathcal L\), the presentation function \(\pi\) and the enumerations fixed in the proof, the ranks are bounded by their cardinalities, and the transition maps are read off the inclusions.
\end{theorem}

\begin{proof}~
	\begin{itemize}
		\item \textbf{Ranks,} \labelcref{itm:lm-rank}\textbf{.} A subfamily of a laminar family is laminar, so this is \labelcref{eq:laminar-atoms} together with the freeness recorded in \ref{def:fin}, distinct atoms of a partition being disjoint.
		\item \textbf{Transition maps,} \labelcref{itm:lm-transition}\textbf{.} \Cref{lem:refine}\,\labelcref{itm:refine-le} gives \(D\leq D'\) degreewise, and the inclusion sends \(1_P\) to the sum of \(1_Q\) over the atoms \(Q\) of \(\mathcal P'_p\) contained in \(P\), these being disjoint with union \(P\). By \labelcref{itm:lm-rank} the atoms of \(\mathcal P'_p\) are the nonempty \(\nu_{\mathcal U'_p}(U')\), and by \ref{lem:refine}\,\labelcref{itm:refine-parent} such an atom meeting \(K_p\) lies in \(\nu_{\mathcal U_p}(U)\), where \(U\) is the least member of \(\mathcal U_p\) containing \(U'\). Distinct atoms of \(\mathcal P_p\) are disjoint, so this \(U\) is the only one whose node contains it.
		\item \textbf{Admissibility and nonemptiness.} \(\Part^{\mathcal L}(G)\subseteq\Part(G)=\PartH(G)\) by \ref{prop:helly-vacuous}, and the atomization with \(K_p=\varnothing\) for all \(p\) is subordinate to \(\mathcal L\) with \(\mathcal U_p=\varnothing\).
		\item \textbf{The rounded repair.} We record the construction used three times below. Fix once and for all, for every \(q\) and every compact open \(W\subseteq G_q\), a finite \(\pi_q(W)\subseteq\mathcal L_q\) with \(\bigcup\pi_q(W)=W\), which exists because \(\mathcal L_q\) is a basis. Let \(p_0\geq 0\), let \(\mathcal U_{p_0}\subseteq\mathcal L_{p_0}\) be finite, and let \(\mathcal V_p\subseteq\mathcal L_p\) be finite for \(p<p_0\). Put \(\mathcal U_p\coloneqq\varnothing\), \(K_p\coloneqq\varnothing\) and \(\mathcal P_p\coloneqq\varnothing\) for \(p>p_0\), put \(K_{p_0}\coloneqq\bigcup\mathcal U_{p_0}\) and \(\mathcal P_{p_0}\coloneqq\mathcal A(\mathcal U_{p_0})\), and descend for \(q=p_0,p_0-1,\dots,1\): with \(\mathcal U_q\) and \(\mathcal P_q=\mathcal A(\mathcal U_q)\) fixed, put
	      \begin{equation}\label{eq:rounded}
		      W_{q-1}\coloneqq\bigcup\mathcal V_{q-1}\cup\bigcup_{i=0}^{q}d_i(K_q),\qquad
		      \mathcal U_{q-1}\coloneqq\mathcal V_{q-1}\cup\pi_{q-1}(W_{q-1})\cup\!\!\bigcup_{\substack{0\leq i\leq q,\ P\in\mathcal P_q\\ c\in N_{i,P}(G_{q-1})\setminus\{0\}}}\!\!\!\!\pi_{q-1}\bigl(N_{i,P}^{-1}(c)\bigr),
	      \end{equation}
	      and \(K_{q-1}\coloneqq\bigcup\mathcal U_{q-1}\), \(\mathcal P_{q-1}\coloneqq\mathcal A(\mathcal U_{q-1})\). The set \(W_{q-1}\) is compact open by \ref{lem:face-image}, and the union in \labelcref{eq:rounded} is finite: by \ref{lem:counting} each \(N_{i,P}\) is locally constant with compact support, so it takes finitely many nonzero values, and each \(N_{i,P}^{-1}(c)\) with \(c\neq 0\) is clopen and contained in the compact set \(d_i(P)\), hence compact open. Each degree is fixed before the one below it is computed, so the functions separated at degree \(q-1\) are those of the final \(\mathcal P_q\).
	      The output is an \(\mathcal L\)-subordinate finite atomization of height at most \(p_0\) with \(\mathcal V_p\subseteq\mathcal U_p\) for \(p<p_0\). Each \((K_q,\mathcal P_q)\) is an object of \(\mathrm{Fin}(G_q)\), the carrier being a finite union of compact open sets and the atoms being nonempty by \ref{def:helly} and clopen in it. Axiom \labelcref{itm:D1} holds, since \(d_i(K_q)\subseteq W_{q-1}\subseteq K_{q-1}\). For \labelcref{itm:D2} fix \(i\) and \(P\in\mathcal P_q\): each \(N_{i,P}^{-1}(c)\) with \(c\neq 0\) is a union of members of \(\mathcal U_{q-1}\), so every atom of \(\mathcal A(\mathcal U_{q-1})\) is contained in or disjoint from it, and these finitely many level sets are pairwise disjoint, so the atom lies in exactly one of them and carries the value \(c\), or in none of them and carries the value \(0\).
	\item \textbf{Cofinality,} \labelcref{itm:K2}\textbf{.} Let \(p_0\geq 0\) and \((L,\mathcal Q)\in\mathrm{Fin}(G_{p_0})\). Each \(Q\in\mathcal Q\) is compact open, hence a finite union of members of \(\mathcal L_{p_0}\), so let \(\mathcal U_{p_0}\) be the union of these finite families. An atom of \(\mathcal A(\mathcal U_{p_0})\) is contained in or disjoint from each member of \(\mathcal U_{p_0}\), hence from each \(Q\), so \((L,\mathcal Q)\leq(\bigcup\mathcal U_{p_0},\mathcal A(\mathcal U_{p_0}))\). Run the rounded repair on this \(\mathcal U_{p_0}\) with \(\mathcal V_p\coloneqq\varnothing\) for \(p<p_0\).
		\item \textbf{Upper bounds,} \labelcref{itm:K1}\textbf{.} Let \(D,D'\in\Part^{\mathcal L}(G)\) have height at most \(p_0\) and presenting families \(\mathcal U_p,\mathcal U'_p\). Run the rounded repair on \(\mathcal U_{p_0}\cup\mathcal U'_{p_0}\) with \(\mathcal V_p\coloneqq\mathcal U_p\cup\mathcal U'_p\) for \(p<p_0\). Its output \(\widehat D\) has presenting families containing \(\mathcal U_p\cup\mathcal U'_p\) in every degree \(p\leq p_0\), so \(D\leq\widehat D\geq D'\) by \ref{lem:refine}\,\labelcref{itm:refine-le}, while above \(p_0\) all three components are empty.
		\item \textbf{The chain,} \labelcref{itm:lm-chain}\textbf{.} Enumerate \(\mathcal L_p=\{U_{p,1},U_{p,2},\dots\}\), with repetitions if \(\mathcal L_p\) is finite. Let \(D^{(0)}\) be the empty atomization, with \(\mathcal U^{(0)}_p\coloneqq\varnothing\). For \(k\geq 1\) let \(D^{(k)}\) be the output of the rounded repair with \(p_0\coloneqq k\), top family \(\mathcal U^{(k-1)}_k\cup\{U_{k,1},\dots,U_{k,k}\}\), and \(\mathcal V_p\coloneqq\mathcal U^{(k-1)}_p\cup\{U_{p,1},\dots,U_{p,k}\}\) for \(p<k\). Then \(\mathcal U^{(k-1)}_p\subseteq\mathcal U^{(k)}_p\) for every \(p\), so \(D^{(k-1)}\leq D^{(k)}\) by \ref{lem:refine}\,\labelcref{itm:refine-le}, which is \labelcref{itm:K1} for the chain. For \labelcref{itm:K2}, let \((L,\mathcal Q)\in\mathrm{Fin}(G_p)\). The cofinality step gives a finite \(\mathcal U\subseteq\mathcal L_p\) with \((L,\mathcal Q)\leq(\bigcup\mathcal U,\mathcal A(\mathcal U))\), and \(\mathcal U\subseteq\{U_{p,1},\dots,U_{p,k}\}\subseteq\mathcal U^{(k)}_p\) for every \(k\) large enough, whence \((L,\mathcal Q)\leq(K^{(k)}_p,\mathcal P^{(k)}_p)\) by \ref{lem:refine}\,\labelcref{itm:refine-le} and transitivity of the order of \ref{def:fin}. \qedhere
	\end{itemize}
\end{proof}

\begin{remark}\label{rem:laminar-limits}
	Three comments delimit what \ref{thm:laminar-model} says.

	First, laminarity enters only in \labelcref{itm:lm-rank} and \labelcref{itm:lm-transition}. Parts \labelcref{itm:lm-complete} and \labelcref{itm:lm-chain} use nothing about \(\mathcal L_p\) beyond the basis property, and for \labelcref{itm:lm-chain} countability. They are \ref{thm:completeness-automatic} run inside \(\mathcal L\). Nestedness buys the rank bound and the transition maps, which is exactly \labelcref{itm:R2} and \labelcref{itm:R3}, and exactly what completeness by itself does not give.

	Second, \labelcref{itm:R1} is untouched, and cannot be repaired here: for Noetherian \(R\) no member of the system is a quasi-isomorphism unless \(H_\bullet(G;R)\) is degreewise finitely generated, by \ref{prop:no-finite-resolution}, and \ref{prop:spurious} measures what truncating to one member costs. What a laminar presentation supplies is the best available, a chain whose ranks are bounded by \(\lvert\mathcal U^{(k)}_p\rvert\) and whose transitions are computed from the inclusions \(\mathcal U^{(k)}_p\subseteq\mathcal U^{(k+1)}_p\), which is what a Bratteli diagram records.

	Third, having a laminar presentation is no restriction on \(G\) within the second countable case, by \ref{prop:laminar-exists}. Outside it the hypothesis has content. A laminar basis \(\mathcal L\) makes \(\{U\in\mathcal L : x\in U\}\) a chain and a neighbourhood base at \(x\), a neighbourhood of \(x\) containing a compact open \(W\ni x\) and hence a member of \(\mathcal L\) through \(x\). The space \(\{0,1\}^{\omega_1}\) is not first countable, so that chain has no countable coinitial subset and a transfinite recursion extracts from it a strictly decreasing \(\omega_1\)-sequence of nonempty clopen sets, which the strict monotonicity of Haar measure excludes. The unit groupoid on \(\{0,1\}^{\omega_1}\) therefore has no laminar presentation. The point of the datum is not that it selects groupoids but that it is a \emph{choice} with computational consequences, where the Helly condition is a property with none.
\end{remark}

\section{What the Construction Delivers}\label{sec:survives}
Three components are correct and independent of the analysis above.

\begin{lemma}\label{lem:cone}
	Let \(\mathsf B\) be a nonempty family of subsets of \(X\) with \(\bigcap\mathsf B\neq\varnothing\). Then \(H_0(N_\bullet(\mathsf B);\mathbb Z)\cong\mathbb Z\), generated by the class of any \(B\in\mathsf B\), and \(H_k(N_\bullet(\mathsf B);\mathbb Z)=0\) for \(k\geq 1\). The same contraction works over any commutative unital ring.
\end{lemma}

\begin{proof}~
	\begin{itemize}
		\item \textbf{Setting.} By hypothesis every tuple has nonempty total intersection, so \(N_m(\mathsf B)=\mathsf B^{m+1}\) and the unnormalized chain complex is \(C_\bullet(N_\bullet(\mathsf B))=\mathbb Z[\mathsf B^{\bullet+1}]\) with \(\partial_m(B_0,\dots,B_m)=\sum_{j=0}^m(-1)^j(B_0,\dots,\widehat{B_j},\dots,B_m)\).
		\item \textbf{Contraction.} Fix \(B_\ast\in\mathsf B\) and set \(h_m(B_0,\dots,B_m)\coloneqq(B_\ast,B_0,\dots,B_m)\) and \(\eta(1)\coloneqq(B_\ast)\), with augmentation \(\varepsilon(B)\coloneqq 1\). For \(m\geq 1\) the term of \(\partial_{m+1}h_m\) omitting \(B_\ast\) is the identity, and the substitution \(k=j-1\) cancels the remaining terms against \(h_{m-1}\partial_m\):
		      \begin{equation}\label{eq:cone}
			      \begin{aligned}
				      \partial_{m+1}h_m(B_0,\dots,B_m) & =(B_0,\dots,B_m)+\sum_{j=1}^{m+1}(-1)^j(B_\ast,B_0,\dots,\widehat{B_{j-1}},\dots,B_m), \\
				      h_{m-1}\partial_m(B_0,\dots,B_m)  & =\sum_{k=0}^{m}(-1)^k(B_\ast,B_0,\dots,\widehat{B_k},\dots,B_m).
			      \end{aligned}
		      \end{equation}
		      Hence \(\partial_{m+1}h_m+h_{m-1}\partial_m=\id\) for \(m\geq 1\), and \(\partial_1h_0(B_0)+\eta\varepsilon(B_0)=\bigl((B_0)-(B_\ast)\bigr)+(B_\ast)=(B_0)\) with \(\varepsilon\eta=\id\).
		\item \textbf{Conclusion.} The augmented complex is contractible, so \(\varepsilon\) induces an isomorphism \(H_0\cong\mathbb Z\) carrying the class of each \(B\) to \(1\), and \(H_k=0\) for \(k\geq 1\). \qedhere
	\end{itemize}
\end{proof}

\begin{proposition}\label{prop:local-cech}
	Let \(K\) be compact open in a totally disconnected locally compact Hausdorff space and \(\mathcal U=\{U_a\}_{a\in A}\) a finite cover of \(K\) by compact open subsets. Write \(U_\sigma\coloneqq U_{a_0}\cap\cdots\cap U_{a_q}\) for \(\sigma\in A^{q+1}\). Then the augmented \v Cech complex with \(\bigoplus_{\sigma\in A^{q+1}}\Cc(U_\sigma;R)\) in degree \(q\), \(\Cc(K;R)\) in degree \(-1\) and differentials the alternating sums of the extensions by zero, is contractible.
\end{proposition}

\begin{proof}~
	\begin{itemize}
		\item \textbf{Block decomposition.} Let \(\mathcal A(\mathcal U)=\{P_b\}_{b\in B}\) be the atom partition and \(S_b\coloneqq\{a\in A : P_b\subseteq U_a\}\), nonempty by \labelcref{eq:atoms}. Restriction along \(U_\sigma=\bigsqcup_{P_b\subseteq U_\sigma}P_b\) and extension by zero are mutually inverse, and \(P_b\subseteq U_\sigma\) holds precisely when every entry of \(\sigma\) lies in \(S_b\), so the complex is isomorphic to \(\bigoplus_{b\in B}\Cc(P_b;R)\otimes_R\widetilde C_\bullet(\Delta^{S_b};R)\) with \(\widetilde C_\bullet(\Delta^{S_b};R)\) the augmented ordered chain complex of the full simplex on \(S_b\), free over \(R\) on the tuples of elements of \(S_b\).
		\item \textbf{Contraction.} Each \(\widetilde C_\bullet(\Delta^{S_b};R)\) is contractible by the cone operator of \ref{lem:cone} at a chosen \(a_b\in S_b\), the computation \labelcref{eq:cone} being \(R\)-linear, and the additive functor \(\Cc(P_b;R)\otimes_R(-)\) carries a chain contraction to a chain contraction. A finite direct sum of contractible complexes is contractible. \qedhere
	\end{itemize}
\end{proof}

This is the mechanism behind the vanishing \(H_m(\Gamma_S;\mathbb Z)=0\) for \(m\geq 1\) and \(H_0(\Gamma_S;\mathbb Z)\cong\mathbb Z\) for the pair groupoid \(\Gamma_S\) on a nonempty finite set \(S\), whose nerve is the codiscrete simplicial set on \(S\) and whose chain complex is contracted by the same cone. It uses one cover and one compact open set. It does not produce a system of resolutions compatible with the groupoid boundary across nerve degrees, and by \ref{prop:atom-blowup} the Helly number of the cover does not bound the size of the blocks.

Second, the K\"unneth sequence for a product of Hausdorff ample groupoids is \cite[Theorem~2.4]{Matui2016} for \(\mathbb Z\)-coefficients, obtained there from the identification \((G\times H)_p=G_p\times H_p\) with \(d_i^{G\times H}=d_i^G\times d_i^H\), the Eilenberg--Zilber theorem and the algebraic K\"unneth formula \cite[Theorem~3.6.3 and Theorem~8.5.1]{Weibel1994}. Over a principal ideal domain the same route applies verbatim: the multiplication \(u\otimes v\mapsto u\boxtimes v\) identifies \(\Cc(G_p;R)\otimes_R\Cc(H_p;R)\) with \(\Cc(G_p\times H_p;R)\), the modules \(\Cc(G_p;R)\) are filtered colimits of finitely generated free modules by \labelcref{eq:exhaustion} and therefore flat, and over a principal ideal domain flatness is torsion-freeness, which the boundary submodules inherit. This is a change of coefficients, not a new structural result.

Third, the Helly axiom also admits a formulation that avoids atomization altogether, by making the intersection nerve itself the object of study. It carries no information either.

\begin{remark}\label{rem:colimit}
	A \textbf{coverage} on a set \(X\) is a relation \(\triangleright\) between subsets \(U\subseteq X\) and finite families \(\mathcal U\) of subsets of \(U\) with \(U=\bigcup\mathcal U\), such that \(\{U\}\triangleright U\), such that \(\{V\cap W\}_{V\in\mathcal U}\triangleright W\) for \(W\subseteq U\), and such that \(\bigcup_{V\in\mathcal U}\mathcal V_V\triangleright U\) whenever \(\mathcal V_V\triangleright V\) for all \(V\in\mathcal U\). A \textbf{basis} is a family \(\mathsf B\subseteq2^{X}\) such that every \(\mathcal U\triangleright U\) with \(U\in\mathsf B\) is refined by some finite \(\{B_j\}\subseteq\mathsf B\) with \(\{B_j\}\triangleright U\). Let \(\mathcal I_n(X,\triangleright)\) be the category of \(n\)-Helly bases with morphisms \(\mathsf B'\to\mathsf B\) the \textbf{refinement witnesses} \(\rho\colon\mathsf B'\to\mathsf B\) satisfying \(B'\subseteq\rho(B')\), and put \(H_k^{\mathrm{Hel},n}(X,\triangleright)\coloneqq\colim_{\mathsf B}H_k(N_\bullet(\mathsf B);\mathbb Z)\). Two objects are always present and impose nothing: the empty family is initial, both defining conditions being vacuous, and \(\{X\}\) is a basis exactly when every cover of \(X\) contains \(X\), in which case it is terminal and the colimit is the homology of a point.

	The invariant does not improve when no coarsest basis exists. Take \(X\coloneqq\{1,2,3\}\), \(\mathsf D\coloneqq\{\{1,2\},\{1,3\},\{2,3\}\}\), and declare \(\mathcal U\triangleright U\) to mean \(U\in\mathcal U\) for \(U\neq X\), and \(X\in\mathcal U\) or \(\mathsf D\subseteq\mathcal U\) for \(U=X\). The coverage axioms hold. A family \(\mathsf B\) of subsets of \(X\) is \(1\)-Helly if and only if \(\mathsf D\not\subseteq\mathsf B\), by the triple \(\mathsf D\) itself for one direction and, for the other, because choosing for each \(a\in X\) a member \(B_{i_a}\not\ni a\) forces \(B_{i_a}=X\setminus\{a\}\). And a basis cannot contain \(X\), the basis property applied to \(\mathsf D\triangleright X\) forcing \(\mathsf D\subseteq\mathsf B\). The objects are therefore the \(2^7-2^4=112\) subfamilies of \(2^{X}\setminus\{X\}\) not containing \(\mathsf D\). The category is not filtered: \(\{\{1,2\}\}\) and \(\{\{1,3\},\{2,3\}\}\) admit no common target, since one containing a member above each of the three two-element sets would have to contain \(\mathsf D\) or \(X\). But each \(\mathsf H_S\coloneqq\mathsf D\setminus\{S\}\) is an object with \(\bigcap\mathsf H_S\neq\varnothing\), every object admits a refinement witness into some \(\mathsf H_S\), and \ref{lem:cone} makes \(H_k(N_\bullet(\mathsf H_S);\mathbb Z)\) that of a point, while the augmentations \(\varepsilon_{\mathsf B}\) form a cocone and pin down the generator in degree \(0\). Hence \(H_0^{\mathrm{Hel},1}(X,\triangleright)\cong\mathbb Z\) and \(H_k^{\mathrm{Hel},1}(X,\triangleright)=0\) for \(k\geq 1\): the coverage was arranged so that no basis survives the passage to a common coarsening, and the invariant returns the homology of a point regardless. The failure of filteredness costs only the description of a class by a single representative, not the value of the colimit.
\end{remark}

To summarize. Requirement \labelcref{itm:R1} is a restriction on \(G\), and it excludes the unit groupoid on a Cantor set and the CAR groupoid. Requirement \labelcref{itm:R2} is data that a completeness hypothesis does not carry, completeness holding always by \ref{thm:completeness-automatic}. Requirement \labelcref{itm:R3} is a hypothesis on the presenting covers, and the Helly axiom is not it. A laminar presentation is, and by \ref{thm:laminar-model} it carries \labelcref{itm:R2} with it.

\bibliographystyle{alpha}
\bibliography{note}

\end{document}