- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
Write \(\mathrm{BC}(\Gamma )\) for the proposition that \(\mu _{\Gamma ,i}\) is an isomorphism for both \(i=0\) and \(i=1\).
The actual assembly map is surjective exactly when every analytic class is the actual assembly value of a class on some cocompact piece. It is injective exactly when any two piece classes with equal assembly values become equal after transition to one common larger cocompact piece. Its bijectivity is the conjunction of these two conditions. The equivalences assert neither condition for an arbitrary group.
Assembly injectivity, surjectivity and bijectivity are unchanged by a monotone restriction \(\phi \) of the cocompact-piece indexing system satisfying the full cofinal condition \(\forall S\, \exists j,\ S\subseteq \phi (j)\). The two-degree properties agree for any two such cofinal restrictions. Pointwise covering alone is not the cofinal hypothesis of this result.
For the indicated proper locally compact Hausdorff second-countable spaces, an actual equivariant homotopy equivalence preserves injectivity, surjectivity and bijectivity of the constructed assembly map in each degree. For genuine universal proper CW models satisfying the subgroup fixed-point criterion, the two-degree property agrees with the property of the canonical geometric telescope. Universal-model comparison retains the common group and space universe required by the existing API; homotopy comparison permits an independent group universe.
On an indicated compact ambient space, the actual topological colimit is additively equivalent to the actual full equivariant KK group of the ambient space. On a proper such space, this equivalence identifies colimit assembly with the actual ambient-space cutoff/product/descent formula.
For a finite discrete group, a lifted one-point space in the group universe is an actual proper model. Its actual equivariant homotopy equivalence with the canonical telescope and the compact-model colimit equivalence reduce the canonical assembly value to the exact point cutoff/product/descent formula in both degrees. This is a reduction of assembly, not a proof of assembly bijectivity for every finite group.
The genuine scalar KK-to-operator-\(K_0\) comparison sends the native scalar identity class to the actual nonunital \(K_0\) class of the unit projection.
For a one-element group, the actual reduced group C\(^*\)-algebra scalar identification induces additive equivalences between its actual reduced \(K_0\) and \(K_1\) targets and the corresponding operator \(K\)-groups of \(\mathbb C\). The maps retain the actual entrywise projection and unitary class formulae. This statement does not compute \(K_0(\mathbb C)\) as \(\mathbb Z\), compute \(K_1(\mathbb C)\) as zero, or identify assembly.
For the literal acting group \(\mathrm{Unit}\) on an indicated compact one-point space, the actual cutoff projection is the actual scalar coefficient map evaluated at \(1\). Its scalar KK lift is the native homomorphism class of that coefficient map.
For the literal Unit group and scalar source, pulling the actual descended class back along the genuine scalar coefficient inclusion gives the actual ordinary coefficient-extension class, separately in the even and odd pictures.
The actual coefficient-free reduced assembly map for the literal one-element group \(\mathrm{Unit}:\mathrm{Type}\) is an isomorphism in both degrees.