- 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
For an action \(\alpha \) of \(\Gamma \) by complex star automorphisms of \(B\), form the actual finite-support coefficient star algebra \(C_c(\Gamma ,B)\). Its operations are
The sum is finite, and associativity and the star-algebra laws are proved for these operations.
Apply the actual Chapter 6 directed additive-group colimit to the concrete compatible piece family to construct
Its restriction along each actual piece inclusion is exactly \(\mu _{S,i}\), and the colimit universal property determines it uniquely. On the actual universal proper telescope and established Chapter 6 canonical topological group obtain
Both parity endpoints have the established analytic reduced K-group codomains. No arbitrary compatible family or desired compatibility witness is an additional input to these constructions.
For an actual closed cocompact piece \(S\) of the indicated proper space, construct the additive homomorphism
Here \(c\) is an actual normalized cutoff on \(S\). Its genuine nonunital operator \(K_0\) class is viewed in scalar KK by the inverse established comparison. The map \(\chi _i\) uses the established scalar KK-to-operator-K comparison and actual scalar crossed-product identification. The even and odd codomains are exactly the existing \(\mathrm{ReducedK0}(\Gamma )\) and \(\mathrm{ReducedK1}(\Gamma )\) groups. The homomorphism is independent of the choice of cutoff.
- BC4lean.Assembly.cutoffKKClass
- BC4lean.Assembly.cutoffProductHom
- BC4lean.Assembly.spaceAssemblyHom
- BC4lean.Assembly.spaceAssemblyHom_independent
- BC4lean.Assembly.pieceAssemblyHom
- BC4lean.Assembly.pieceAssemblyHom_eq_of_cutoff
- BC4lean.Assembly.pieceAssemblyEvenHom
- BC4lean.Assembly.pieceAssemblyOddHom
- BC4lean.Assembly.reducedScalarKKToAnalyticHom
For a locally compact Hausdorff proper cocompact \(\Gamma \)-space, choose \(c\in C_c(X,[0,\infty ))\) with \(\sum _g c(g^{-1}x)^2=1\) and set \(p_c(g)(x)=c(x)c(g^{-1}x)\). Such a cutoff exists, \(p_c\) is a projection in \(C_0(X)\rtimes _r\Gamma \), and its K-class is independent of \(c\). The class is in the actual nonunital operator \(K_0\) group of the constructed reduced crossed product. Its independence follows from the explicit mixed-cutoff partial isometry in that completed algebra.
- BC4lean.ProperActions.Cutoff.exists_cutoffFunction
- BC4lean.ProperActions.CocompactPiece.exists_cutoffFunction
- BC4lean.ProperActions.Cutoff.reducedCutoffProjection
- BC4lean.ProperActions.Cutoff.reducedCutoffProjection_isStarProjection
- BC4lean.ProperActions.Cutoff.reducedCutoffProjection_partialIsometry
- BC4lean.ProperActions.Cutoff.cutoffK0
- BC4lean.ProperActions.Cutoff.cutoffK0_independent
For \(C=B\rtimes _r\Gamma \) and a complete Hilbert \(B\)-module \(E\), construct the completed interior module \(E\otimes _B C\) using the actual coefficient inclusion \(B\to C\). Elementary vectors obey the balancing relation and the inner-product formula
Every adjointable \(T\) acts by \(T\otimes 1\), with its adjoint and norm bound proved; compact module operators remain compact under this coefficient extension. If \(\Gamma \) is countable, \(B\) is separable and \(E\) is countably generated, the constructed module is countably generated. The integrated source action and quotient homomorphisms are separate statements below.
- BC4lean.KKTheory.KasparovDescent.coefficientRepresentation
- BC4lean.KKTheory.KasparovDescent.Module
- BC4lean.KKTheory.KasparovDescent.countablyGenerated
- BC4lean.KKTheory.KasparovDescent.mk_balance
- BC4lean.KKTheory.KasparovDescent.mk_inner
- BC4lean.KKTheory.KasparovDescent.operatorHom_mk
- BC4lean.KKTheory.KasparovDescent.norm_operatorHom_le
- BC4lean.KKTheory.KasparovDescent.operatorHom_adjoint
- BC4lean.KKTheory.KasparovDescent.operatorHom_compact
An actual projection in a possibly nonunital C\(^*\)-algebra \(A\) defines its singleton-matrix projection class in the forced unitization. The scalar quotient of that matrix is zero, so the class belongs to the existing scalar-kernel group \(K_0(A)\). An actual partial isometry between two projections proves equality of these classes.
Define \(B\rtimes _{\alpha ,r}\Gamma \) as the operator-norm closed nonunital star subalgebra generated by the concrete \(\pi _\alpha (b)\lambda _g\) in \(\mathcal L_B(\ell ^2(\Gamma ,B))\). It is a C\(^*\)-algebra. The coefficient inclusion \(B\to B\rtimes _{\alpha ,r}\Gamma \) is isometric. Finite twisted convolution integrates by \(f\mapsto \sum _g\pi _\alpha (f(g))\lambda _g\) to a star homomorphism with dense range in this actual algebra.
- BC4lean.KKTheory.ReducedCrossedProduct
- BC4lean.KKTheory.reducedCrossedProduct_nonUnitalCStarAlgebra
- BC4lean.KKTheory.coefficientToReducedCrossed
- BC4lean.KKTheory.norm_coefficientToReducedCrossed
- BC4lean.KKTheory.algebraicCrossedOperatorHom_eq_sum
- BC4lean.KKTheory.algebraicToReducedCrossed
- BC4lean.KKTheory.algebraicToReducedCrossed_denseRange
Construct reduced descent on both actual quotient groups,
The representative formula uses the completed coefficient-extension module, the actual integrated reduced source action and \(F\otimes 1\). Prove compatibility with all four existing native Kasparov products in the common carrier universe stated above, and identify \(\mathbb C\rtimes _r\Gamma \cong C_r^*(\Gamma )\) by the actual scalar regular-module unitary.
- BC4lean.KKTheory.KasparovDescent.evenClassHom
- BC4lean.KKTheory.KasparovDescent.oddClassHom
- BC4lean.KKTheory.KasparovDescent.classHom
- BC4lean.KKTheory.KasparovDescent.evenClass_mk
- BC4lean.KKTheory.KasparovDescent.oddClass_mk
- BC4lean.KKTheory.KasparovDescent.evenClassHom_evenProduct
- BC4lean.KKTheory.KasparovDescent.oddClassHom_evenOddProduct
- BC4lean.KKTheory.KasparovDescent.oddClassHom_oddEvenProduct
- BC4lean.KKTheory.KasparovDescent.evenClassHom_oddOddProduct
- BC4lean.KKTheory.KasparovDescent.classHom_product
- BC4lean.KKTheory.reducedCrossedScalarProductEquiv
Complete the finite vectors \(\Gamma \to B\) in the genuine right Hilbert \(B\)-module norm
The finite-vector coefficient-valued form is positive and definite; its null radical is proved zero. The canonical finite-vector image in the completed module \(\ell ^2(\Gamma ,B)\) is dense.
For normalized cutoffs \(c,d\), the exact mixed coefficient \(v_{c,d}(g)(x)=c(x)d(g^{-1}x)\) defines a finite-support element of \(C_c(\Gamma ,C_0(X))\). The actual twisted convolution and involution give \(v_{c,d}^*=v_{d,c}\) and \(v_{c,d}v_{d,e}=v_{c,e}\). Consequently \(p_c=v_{c,c}\) is a self-adjoint idempotent, and the mixed element implements Murray–von Neumann equivalence of \(p_c\) and \(p_d\).
- BC4lean.ProperActions.CutoffCoefficients.convolution_mixed_of_normalized
- BC4lean.ProperActions.CutoffCoefficients.involution_mixed
- BC4lean.ProperActions.Cutoff.mixedAlgebraic
- BC4lean.ProperActions.Cutoff.coeff_mixedAlgebraic
- BC4lean.ProperActions.Cutoff.algebraicProjection
- BC4lean.ProperActions.Cutoff.star_algebraicProjection
- BC4lean.ProperActions.Cutoff.algebraicProjection_mul_self
- BC4lean.ProperActions.Cutoff.mixedAlgebraic_partialIsometry
Let \(\varphi :J\to \mathcal C_\Gamma (X)\) be a monotone map from a nonempty directed preorder to the actual cocompact pieces. The restricted assembly is the colimit of the same actual piece family. If
the established cofinal indexing equivalence preserves its assembly value. The comparison between two such genuinely cofinal systems does likewise.
The actual piece assembly homomorphisms commute with Chapter 6 transitions and bounded piece maps. They are independent of cutoff choice and compatible with the actual genuinely cofinal indexing equivalences. The resulting colimit assembly homomorphisms commute with actual ambient equivariant pushforwards, the established homotopy equivalences and genuine universal proper-model comparison.
- BC4lean.Assembly.pieceAssemblyHom_transition
- BC4lean.Assembly.spaceAssemblyHom_independent
- BC4lean.Assembly.pieceAssemblyHom_eq_of_cutoff
- BC4lean.Assembly.pieceAssemblyHom_boundedMap
- BC4lean.Assembly.assemblyHom_comp_pushforward
- BC4lean.Assembly.assemblyHom_homotopyEquiv
- BC4lean.Assembly.assemblyHom_universalModelEquiv
- BC4lean.Assembly.assemblyHom_cofinalIndexEquiv
- BC4lean.Assembly.indexedAssemblyHom_cofinalComparisonEquiv
The actual cutoff \(K_0\) class is natural under coefficient restrictions between cocompact pieces and under proper equivariant pullback, in the existing nonunital operator \(K_0\) groups of the actual reduced crossed products.
A compatible equivariant Hilbert \(B\)-module action \(U\) induces actual conjugation actions on \(\mathcal L_B(E)\) and \(\mathcal K_B(E)\). The compact inclusion intertwines them, and \(g\cdot \theta _{x,y}=\theta _{U_gx,U_gy}\).
Descent preserves genuine whole-cycle isomorphisms and full even, odd and graded homotopies. An interval witness may use any Hilbert module over \(C([0,1],B)\), rather than only an operator path on a fixed module.
For all four existing native parity branches,
The group and coefficient universes are independent. This native comparison uses the common original module universe \(W=\max (u,u_\Gamma ,u_A,u_B,u_C)\); the target acting group remains \(\mathrm{Unit}\) at universe zero.
The actual descended cycles induce additive homomorphisms on the existing even and odd homotopy quotients. Their representative values are the constructed descended cycles. The ordinary target group action is \(\mathrm{Unit}\), and the coefficient and module carriers retain their actual enlarged universes.
For an equivariant Hilbert \(B\)-module \(E\) and a possibly degenerate equivariant star representation of \(A\), finite source integration extends to the actual star homomorphism
It agrees with finite integration on generators and is bounded by the concrete reduced regular norm.
An actual equivariant coefficient star homomorphism induces the actual reduced crossed-product map. The constructed parity descent commutes with the existing native source-pullback homomorphism used in Chapter 6.
There is an actual graded Hilbert-module unitary
Transport of an actual original product operator satisfies the genuine descended cycle, connection and localized positivity conditions.
Actual piece assembly homomorphisms commute with the existing Chapter 6 transitions and are independent of cutoff choice. They preserve assembly values under the actual bounded piece maps induced by ambient equivariant maps.
A continuous proper action of a discrete group on a locally compact Hausdorff space with compact orbit quotient admits a nonnegative \(c\in C_c(X,\mathbb R)\) with \(\sum _g c(g^{-1}x)^2=1\). The sum has finite support at every point, and its topological sum has the same value. For any two compactly supported continuous functions \(c,d\), the coefficient family \(g\mapsto (x\mapsto c(x)d(g^{-1}x))\) has finite group support.
Every actual closed cocompact piece of a locally compact Hausdorff proper ambient action inherits properness and admits such a cutoff. Countability is not needed for these assertions.
- BC4lean.ProperActions.Cutoff.CutoffFunction
- BC4lean.ProperActions.Cutoff.exists_cutoffFunction
- BC4lean.ProperActions.Cutoff.normalized_tsum
- BC4lean.ProperActions.Cutoff.finite_mixedCoefficient_support
- BC4lean.ProperActions.CocompactPiece.proper
- BC4lean.ProperActions.CocompactPiece.exists_cutoffFunction
The regular integrated representation is faithful on the finite-support algebra. Its operator norm is therefore a norm, and satisfies \(\| f^*f\| _r=\| f\| _r^2\). The reduced algebra is the closure of the actual finite generator span. If \(\Gamma \) is countable and \(B\) is separable, the constructed reduced crossed product is separable.
- BC4lean.KKTheory.algebraicToReducedCrossed_injective
- BC4lean.KKTheory.algebraicCrossedReducedNorm
- BC4lean.KKTheory.algebraicCrossedReducedNorm_eq_zero
- BC4lean.KKTheory.algebraicCrossedReducedNorm_cstar
- BC4lean.KKTheory.reducedCrossedAlgebra_coe_eq_closure_span
- BC4lean.KKTheory.reducedCrossedProduct_separableSpace
The actual adjointable regular operators satisfy
They obey the star and group laws, the covariance identity \(\pi _\alpha (\alpha _g(b))\lambda _g=\lambda _g\pi _\alpha (b)\), and \(\| \pi _\alpha (b)\| =\| b\| \), including for nonunital \(B\).
For the trivial scalar action, the completed regular coefficient module is unitarily identified with the existing \(\ell ^2(\Gamma )\). The unitary sends \(z\delta _g\) to the actual scalar delta vector and intertwines the regular operators. It induces the concrete star-algebra equivalence
taking the scalar coefficient identity to the existing reduced group-algebra unit.