Matching works

1 work

math.KT — K-Theory and Homology

A Note on Laminar Presentations and Finite Chain Models for Ample Groupoid Homology

Contributed by Luciano Melodia

A finite free chain model for the homology of a Hausdorff ample groupoid GG 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 nn-Helly axiom on the presenting covers supplies none of them, being satisfied by every finite atomization for every nn, and a 11-Helly family of NN compact open sets can have 2N−12^{N}-1 atoms. We show that a 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 GG: the homology of a model is finitely generated over a Noetherian ring, whereas H0H_0 over Z\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.

Primarily human-written textHuman understanding: all partsAmple GroupoidsHK-Conjecture

Advanced search

Text
Human understanding
Linked formalizations