- 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 a group \(\Gamma \), regarded as discrete, write
for the actual abstract reduced-norm completion constructed earlier. Equip this \(C^*\)-algebra with its canonical spectral order and form \(V(A_r(\Gamma ))\), \(K_0(A_r(\Gamma ))\), and the canonical group-completion map \(\iota _A:V(A_r(\Gamma ))\to K_0(A_r(\Gamma ))\). These definitions use the existing matrix-projection and Grothendieck-group constructions applied to the abstract completion itself.
The analytic \(S\)-connection predicate on the actual tensor records both the operator and adjoint compactness conditions \(\theta _\xi S-(-1)^{|\xi |}R\theta _\xi \in \mathcal K\) for every homogeneous \(\xi \), with the analogous condition for \(S^*,R^*\). A globally compact perturbation of \(R\) preserves all four compactness conditions. The odd degree of a graded connection must be proved separately for the actual tensor grading; preserving that degree also requires an odd perturbation. Existence of a graded connection or a Kasparov product is not assumed.
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.
For a discrete group \(\Gamma \), equip the already constructed algebra \(C_r^*(\Gamma )\) with its canonical spectral order. Define the abelian group \(K_0(C_r^*(\Gamma ))\) by the preceding unital construction, together with its projection-class map and universal property. Countability is not needed for this construction. No computation of this group or assembly map is asserted here.
For a countable discrete group \(\Gamma \), the analytic target groups of the coefficient-free reduced Baum–Connes assembly map are
Both groups are defined using the canonical spectral order and the preceding unital constructions. The definitions also apply without countability. No computation of these groups or construction of the assembly map is asserted.
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
Given an actual left action \(\Psi :B\to \mathcal L_C(F)\), quotient the complex algebraic tensor by the span of \(xb\otimes y-x\otimes \Psi (b)y\). This constructed quotient has the genuine balanced universal property. Its coefficient pairing descends to a Hermitian form on the constructed quotient. The elementary formula is \(\langle y,\Psi (\langle x,x'\rangle )y'\rangle \), respects both balance relations, is positive on elementary vectors and satisfies the four-factor norm bound. Separation and norm completion are additional obligations.
- BC4lean.KKTheory.BalancedModuleTensor
- BC4lean.KKTheory.moduleTensorMk_balance
- BC4lean.KKTheory.moduleTensorLift
- BC4lean.KKTheory.moduleTensorLift_unique
- BC4lean.KKTheory.moduleTensorPureInner
- BC4lean.KKTheory.moduleTensorPureInner_self_nonneg
- BC4lean.KKTheory.moduleTensorPureInner_norm_le
- BC4lean.KKTheory.moduleTensorInner
- BC4lean.KKTheory.moduleTensorInner_star
Write \(\mathrm{BC}(\Gamma )\) for the proposition that \(\mu _{\Gamma ,i}\) is an isomorphism for both \(i=0\) and \(i=1\).
For a given \(\Gamma \)-space \(E\), a closed cocompact piece is a closed invariant subset \(X\subseteq E\) whose image in \(E/\Gamma \) is compact. For continuous actions, this is equivalent to compactness of its intrinsic quotient \(X/\Gamma \). Pieces are ordered by inclusion.
For a countable discrete group \(\Gamma \), choose the concrete geometric telescope \(E\) of the finite-orbit stages of the weak labeled join. This same space is a genuine finite-isotropy equivariant CW complex, is locally compact and second-countable, has a proper action, and has contractible fixed spaces for finite subgroups and empty fixed spaces for infinite subgroups. It has the universal cellular mapping property and is unique up to equivariant homotopy among genuine CW models with the fixed-point criterion. Its closed invariant subsets with compact quotient form the directed cocompact indexing system proved above, and their union is \(E\).
- BC4lean.ProperActions.LabeledOrbitRealization.allowedEquivariantCWComplex
- BC4lean.ProperActions.EquivariantCWComplex.transportIso
- BC4lean.ProperActions.LabeledOrbitTelescope.fixedPointCriterion
- BC4lean.ProperActions.LabeledOrbitTelescope.equivariantCWComplex
- BC4lean.ProperActions.LabeledOrbitTelescope.universalProperCWModel
- BC4lean.ProperActions.LabeledOrbitTelescope.homotopyTerminal
- BC4lean.ProperActions.LabeledOrbitTelescope.unique
- BC4lean.ProperActions.LabeledPrismProjection.homeomorph
- BC4lean.ProperActions.LabeledPrismProjection.actionIso
The finite-rank module maps are the complex linear span of the \(\theta _{x,y}\). The compact module maps \(\mathcal K_B(E,F)\) are its operator-norm closure. Equivalently, for every \(\epsilon {\gt}0\) a compact map has a finite-rank module approximation within \(\epsilon \). This definition does not use complex finite-dimensionality of the range.
For a discrete group \(\Gamma \) acting on \(B\) by complex star-algebra automorphisms \(\alpha _g\), a compatible action on \(E\) consists of complex-linear isometries \(U_g\) satisfying the group laws and \(\langle U_gx,U_gy\rangle =\alpha _g(\langle x,y\rangle )\). Then \(U_g(xb)=(U_gx)\alpha _g(b)\), and the action is jointly continuous. A graded action also commutes with \(J\). The individual \(U_g\) are generally semilinear over \(B\).
A right Hilbert module is countably generated if there is a sequence \(\xi _n\) such that the complex linear span of the vectors \(\xi _n b\), \(b\in B\), is norm dense. This property is preserved by coefficient-compatible complex-linear isometric module isomorphisms, including semilinear coefficient twists.
Use the \(C^*\)-norm on \(M_n(A)\), and let \(P_n(A)=\operatorname {Proj}(M_n(A))\). For \(p\in P_n(A)\) and \(q\in P_m(A)\), their block sum is
Projection stabilization is \(p\mapsto p\oplus 0_m\). The Lean implementation initially uses arbitrary finite index types and their disjoint sums. Mathlib’s matrix norm requires a compatible star order on \(A\); the matrix declarations retain this explicit implementation assumption.
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
In the category of topological \(\Gamma \)-actions, use the boundary inclusions \(\Gamma /H\times \partial D^n\to \Gamma /H\times D^n\), indexed by finite subgroups \(H\), as the generating cells at stage \(n\). A relative equivariant CW structure is a sequential relative cell complex for this family: its data contain the coproducts, pushout squares, skeleta, and colimit witnesses. An equivariant CW structure starts from the initial, empty action. The categorical morphisms between actions obtained from \(\Gamma \)-spaces correspond exactly to the continuous equivariant maps defined above.
These are cellular data. Topological properness of the resulting colimit is not assumed in this definition and remains to be proved.
A finite-isotropy \(\Gamma \)-CW structure consists of a sequential cellular construction from the empty action, with cells \(\Gamma /H\times D^n\) for finite subgroups \(H\). The construction includes the coproduct, pushout, and colimit witnesses. Its skeleta are closed embedded subspaces, and Hausdorffness follows from the cellular data. For countable discrete \(\Gamma \), the resulting action is topologically proper.
An equivariant homotopy from \(f_0\) to \(f_1\) is a jointly continuous map \(F:[0,1]\times X\to Y\) with \(F(0,x)=f_0(x)\), \(F(1,x)=f_1(x)\), and \(F(t,gx)=gF(t,x)\). The interval has trivial action. Write \(f_0\simeq _\Gamma f_1\) when such a homotopy exists. The Lean definition specializes Mathlib’s ContinuousMap.HomotopyWith.
For separable \(\Gamma \)-\(C^*\)-algebras \(A,B\), construct \(KK_i^\Gamma (A,B)\) from graded equivariant Kasparov cycles and homotopy. The raw even and ungraded odd cycle conditions are specified above. Construct a homotopy quotient with direct sum and inverse laws, and prove the parity identification before claiming the resulting abelian groups. For the intended applications, \(A,B\) are separable and \(\Gamma \) is countable discrete.
- BC4lean.KKTheory.BundledGradedKasparovCycle.fullHomotopySetoid
- BC4lean.KKTheory.BundledOddKasparovCycle.fullHomotopySetoid
- BC4lean.KKTheory.BundledOddKasparovCycle.homotopic_iff_full
- BC4lean.KKTheory.CliffordCommutingRepresentation.maximalNorm_eq
- BC4lean.KKTheory.FullGradedKasparovHomotopy
- BC4lean.KKTheory.GradedKasparovCycle
- BC4lean.KKTheory.GradedKasparovHomotopyClass
- BC4lean.KKTheory.GroupUniverseCommonParityProduct.universeEquivalence
- BC4lean.KKTheory.GroupUniverseParityGroup.KKParityGroup
- BC4lean.KKTheory.GroupUniverseParityGroup.evenParityIdentification
- BC4lean.KKTheory.GroupUniverseParityGroup.kkParityGroupAddCommGroup
- BC4lean.KKTheory.GroupUniverseParityGroup.oddParityIdentification
- BC4lean.KKTheory.KasparovCycle
- BC4lean.KKTheory.KasparovHomotopyClass.instAddCommGroup
- BC4lean.KKTheory.OddKK
- BC4lean.KKTheory.OddKK.instAddCommGroup
- BC4lean.KKTheory.OddKasparovCycle
- BC4lean.KKTheory.cliffordTensorParityAddEquiv
For topological spaces \(X,Y\) with \(\Gamma \)-actions, a continuous equivariant map \(f:X\to Y\) is a continuous map satisfying \(f(gx)=gf(x)\). The underlying equivariant function uses Mathlib’s MulActionHom. The constructions in this section do not require properness, a discrete group topology, local compactness, or Hausdorffness.
For trivially graded complex possibly nonunital \(A,B\) and a discrete group \(\Gamma \), an even equivariant Kasparov cycle consists of a complete, countably generated graded right Hilbert \(B\)-module \(E\), a compatible action commuting with the grading, an even equivariant possibly degenerate star representation \(\phi :A\to \mathcal L_B(E)\) and an odd adjointable operator \(F\). For all \(a\in A\) and \(g\in \Gamma \) require
A degenerate cycle has all four expressions zero. A zero representation with zero operator is such a cycle on every countably generated compatible graded module. The group action on \(F\) is required only modulo compactness in the stated local sense.
On a fixed module, grading, representation and action, an operator homotopy is an operator-norm-continuous path satisfying oddness and all four compact defect conditions at every parameter. It yields actual cycles throughout, including both endpoints. Constant paths, reversal and concatenation preserve these conditions. Equivalence to homotopies over \(C([0,1],B)\) and the full KK quotient are further targets.
- BC4lean.KKTheory.KasparovCycle.OperatorConditions
- BC4lean.KKTheory.KasparovCycle.withOperator
- BC4lean.KKTheory.KasparovOperatorHomotopy
- BC4lean.KKTheory.KasparovOperatorHomotopy.cycleAt
- BC4lean.KKTheory.KasparovOperatorHomotopy.continuous_operator
- BC4lean.KKTheory.KasparovOperatorHomotopy.source_cycleAt
- BC4lean.KKTheory.KasparovOperatorHomotopy.target_cycleAt
- BC4lean.KKTheory.KasparovOperatorHomotopy.refl
- BC4lean.KKTheory.KasparovOperatorHomotopy.symm
- BC4lean.KKTheory.KasparovOperatorHomotopy.trans
For compatible algebra gradings \(\delta _A,\delta _B\), a genuine graded cycle uses a \(\delta _B\)-semilinear module grading, an equivariant graded representation, an odd Fredholm operator, and the same localized compact defects with commutator \(F\phi (a)-\phi (\delta _A(a))F\). Algebra actions preserve their gradings. The trivial-grading specialization is exactly the earlier even cycle definition. Actual whole-cycle unitaries give reflexive, symmetric and transitive isomorphisms across module carriers.
The complex vector space \(\mathbb C[\Gamma ]\) consists of finitely supported functions \(a:\Gamma \to \mathbb C\), with pointwise vector operations. Write \(\operatorname {supp}(a)=\{ g:a(g)\ne 0\} \) and let \(\delta _g\) be \(1\) at \(g\) and \(0\) elsewhere. Define
These sums are finite. The proposed multiplicative identity is \(\delta _e\).
A Hilbert-module unitary equivalence is an actual complex-linear isometry preserving the coefficient-valued inner product. It is coefficient-linear, its inverse is its adjoint, and conjugation preserves operator norm, adjoints and compactness, including rectangular operators.
The preceding constructions give graded right Hilbert \(C^*\)-modules, with a complete module norm, their adjointable and compact operators, and continuous compatible actions of discrete groups. Coefficient algebras may be nonunital and may have a nontrivial grading. Module completeness is an explicit hypothesis, and compatibility of actions with the grading is explicit.
Define the complex-linear map
This is a finite sum of bounded operators, and \(\rho (\delta _g)=\lambda _g\).
Cycle isomorphisms are genuine Hilbert-module unitaries intertwining the grading, action, representation and Fredholm operator. They give an equivalence relation across actual module types in a fixed explicit universe. Unitary transport constructs all target cycle data and preserves degeneracy. This is the isomorphism relation; the full homotopy quotient is a separate construction.
- BC4lean.KKTheory.KasparovCycleIso
- BC4lean.KKTheory.KasparovCycleIso.refl
- BC4lean.KKTheory.KasparovCycleIso.symm
- BC4lean.KKTheory.KasparovCycleIso.trans
- BC4lean.KKTheory.KasparovCycle.transport
- BC4lean.KKTheory.KasparovCycle.transportIso
- BC4lean.KKTheory.KasparovCycle.transport_isDegenerate
- BC4lean.KKTheory.BundledKasparovCycle
- BC4lean.KKTheory.BundledKasparovCycle.isomorphismSetoid
For a nonnegative family, define its sum as the supremum of its finite partial sums. Put
with pointwise vector operations and \(\langle \xi ,\eta \rangle =\sum _h\overline{\xi (h)}\eta (h)\). The notation \(\delta _g\) also denotes the corresponding vector in \(\ell ^2(\Gamma )\); the ambient space determines its meaning.
For any group \(\Gamma \), let \(V=\coprod _{H\leq \Gamma ,\ H\text{ finite}}\Gamma /H\). Label its copies by \(\mathbb N\). A labeled orbit simplex is a finite subset of \(\mathbb N\times V\) whose projection to \(\mathbb N\) is injective. Translation acts on the orbit coordinate and fixes the label. Every finite subset of a simplex is again a simplex, so the family is closed under taking faces. The empty simplex is allowed. These are combinatorial data; no topology or geometric realization is asserted here.
The weak realization consists of nonnegative real vertex coordinates with sum one and finite support contained in an admissible labeled simplex. Equip it with the final topology of all finite simplex charts. A map out of this realization is continuous exactly when it is continuous on every chart; the same criterion holds after taking a product with a locally compact space. The coordinate map into the product of real lines is continuous and injective, so the weak realization is Hausdorff.
The left regular representation is the group homomorphism \(\lambda :\Gamma \to U(\ell ^2(\Gamma ))\), \(g\mapsto \lambda _g\), where \(U(H)\) denotes the unitary operators on \(H\). It is distinct from the linear extension defined below.
For \(g\in \Gamma \), prescribe
The next lemma verifies that this defines an operator on \(\ell ^2(\Gamma )\).
Let \(U_n(A)=\{ u\in M_n(A):u^*u=uu^*=1\} \), with the subspace topology from the matrix \(C^*\)-norm. Block sums of unitaries are unitary. Unitary stabilization is \(u\mapsto u\oplus 1_m\).
A coefficient grading is an involutive complex star-algebra automorphism \(\beta \) of \(B\). A compatible module grading is an involutive complex-linear isometry \(J\) with \(\langle Jx,Jy\rangle =\beta (\langle x,y\rangle )\). An operator is even when it commutes with the grading and odd when it anticommutes. For trivially graded coefficients, \(J\) is a selfadjoint unitary adjointable operator. Completeness of the module is imposed when using it as a Hilbert module.
For \(x\in F\) and \(y\in E\), define the rank-one module operator
This is a bounded adjointable map. “Rank-one” is in the Hilbert-module sense; it need not have one-dimensional complex range.
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.
The ungraded Fredholm picture of odd cycles uses the same complete, countably generated equivariant module and the same four compactness conditions, with no module grading. Its equivalence to the Clifford-graded picture, and the homotopy quotient in either parity, require further proofs.
For a possibly nonunital complex \(C^*\)-algebra \(A\), use the forced unitization \(A^+\) and its scalar quotient \(\epsilon :A^+\to \mathbb C\) to define
Both are abelian groups with injective kernel inclusions. The spectral order supplies the matrix API’s compatible star order. The superscript distinguishes the kernel construction from the unital construction until the next comparison.
- BC4lean.OperatorKTheory.scalarQuotient
- BC4lean.OperatorKTheory.scalarSection
- BC4lean.OperatorKTheory.scalarQuotient_section
- BC4lean.OperatorKTheory.OperatorK0
- BC4lean.OperatorKTheory.OperatorK1
- BC4lean.OperatorKTheory.operatorK0AddCommGroup
- BC4lean.OperatorKTheory.operatorK1AddCommGroup
- BC4lean.OperatorKTheory.operatorK0Inclusion
- BC4lean.OperatorKTheory.operatorK1Inclusion
Define the unital group \(K_0(A)\) as the Grothendieck group of \(V(A)\). The canonical additive map \(V(A)\to K_0(A)\) sends a matrix projection to its \(K_0\) class and sends block sum to addition. Cancellation in \(V(A)\) is not assumed, and injectivity of this canonical map is not asserted.
A finite matrix unitary records a small finite index set \(I\) and \(u\in U_I(A)\). Define stable equivalence to be the equivalence relation generated by norm homotopies after bijective changes of finite coordinates and by adjoining identity blocks \(u\mapsto u\oplus 1_J\). Define \(K_1(A)\) as the quotient by this relation. Thus equality of classes means a finite chain of these geometric moves and their reverses; additive and inverse relations are not imposed as extra generators.
A projection in \(A\) is an element \(p\) satisfying \(p^*=p\) and \(p^2=p\). Write \(\operatorname {Proj}(A)\) for these projections. The elements \(0\), \(1\), and \(1-p\) are projections.
For a subgroup \(H\) and a space \(D\), the orbit cell is \(\Gamma /H\times D\) with action \(g(q,d)=(gq,d)\) and the product topology. Projection onto \(\Gamma /H\) is continuous and equivariant. Taking \(D\) to be a disk gives the cell shape for the intended CW construction; cell attachment is a separate target below.
For each closed invariant cocompact piece \(S\), define its K-homology to be the genuine full Chapter 5 group \(KK_i^\Gamma (C_0(S,\mathbb C),\mathbb C)\) for \(i=0,1\). The source action is \((g\cdot a)(x)=a(g^{-1}x)\) and the scalar coefficient action is trivial. Separability of the actual supremum-norm \(C_0\) algebra follows by isometric extension by zero to the one-point compactification.
An endomorphism is positive modulo compact operators when it differs from an actual positive endomorphism by a compact module operator. This is equivalent to having a star-square lift. The condition is preserved by sums, adjointable compression and compact perturbations. These assertions use the spectral order on the complete endomorphism \(C^*\)-algebra and its actual closed compact ideal.
Let \(P(\Gamma )\) be the space of functions \(p:\Gamma \to \mathbb R\) such that \(p(g)\geq 0\), \(p\) is summable, and \(\sum _g p(g)=1\). Give it the subspace topology of pointwise convergence in \(\mathbb R^\Gamma \) and the action \((a\cdot p)(g)=p(a^{-1}g)\). Each translation is continuous. This definition supplies a topological action; it does not supply a CW structure or local compactness.
For a topological group \(\Gamma \) acting on a topological space \(X\), the action is proper when
is a proper map. This is exactly Mathlib’s ProperSMul predicate; it includes continuity of the action. In the applications below \(\Gamma \) is discrete. Finite stabilizers alone do not replace properness.
The fixed-point criterion for a prospective model \(E\) requires \(E^H\) to be contractible for every finite subgroup \(H\) and empty for every infinite subgroup \(H\). This predicate alone does not supply an equivariant CW structure or a proof of the universal mapping property.
For finite index sets \(I,J\), projections \(p\in M_I(A)\) and \(q\in M_J(A)\) are rectangularly equivalent if there is \(v\in M_{I,J}(A)\) with
Unlike the earlier relation in one fixed algebra, this relation can compare different matrix sizes directly.
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
Define
with inherited operations and norm. The closure is in the operator norm, not the weak or strong operator topology.
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.
The entrywise map descends to an additive map
These maps preserve identities and composition.
Let \(V(A)\) be finite matrix projections modulo rectangular equivalence. The Lean objects record a small finite index type, its finite structure, and a projection. The relation is the existence of an actual rectangular partial-isometry witness; block-sum relations are not imposed separately.
A point-norm homotopy from \(\phi :A\to B\) to \(\psi :A\to B\) is a family of complex star homomorphisms \(H_t\), \(t\in [0,1]\), such that \(H_0=\phi \), \(H_1=\psi \), and \(t\mapsto H_t(a)\) is norm-continuous for each \(a\in A\). In the unital version every \(H_t\) preserves the unit. Homomorphisms of possibly nonunital algebras admit a unitalized point-norm homotopy \(H_t^+(r,a)=(r,H_t(a))\). Continuity of \(t\mapsto H_t\) in operator norm is not required.
Construct
Here \(S\) ranges over all closed invariant cocompact pieces of the chosen model. The constructed additive group satisfies the colimit universal property; two representatives agree exactly when they agree in a larger piece. Replacing this system by any monotone cofinal directed family induces a canonical additive equivalence. The cofinality condition is \(\forall S\, \exists j\colon S\subseteq S_j\).
The group is independent of the locally compact second-countable genuine universal proper CW model satisfying the Chapter 4 fixed-point criterion. Every equivariant comparison map induces the same additive equivalence. The canonical implementation uses the actual geometric telescope.
- BC4lean.TopologicalKHomology.diagram
- BC4lean.TopologicalKHomology.group
- BC4lean.TopologicalKHomology.ofPiece_eq_iff
- BC4lean.TopologicalKHomology.existsUnique_desc
- BC4lean.TopologicalKHomology.cofinalIndexEquiv
- BC4lean.TopologicalKHomology.pushforward_homotopy
- BC4lean.TopologicalKHomology.homotopyEquiv
- BC4lean.TopologicalKHomology.universalModelEquiv
- BC4lean.TopologicalKHomology.universalComparison_unique
- BC4lean.TopologicalKHomology.topologicalGroup
- BC4lean.TopologicalKHomology.toCanonicalModelEquiv
The universal property of the Grothendieck group extends \(V(\phi )\) to
Here \([p]\) denotes the \(K_0\) class of a finite matrix projection, and \(\phi (p)\) denotes its entrywise image. The canonical maps \(V(A)\to K_0(A)\) are natural with respect to these homomorphisms.
Two elements of \(U_n(A)\) are norm homotopic if they are endpoints of a continuous path \([0,1]\to U_n(A)\). Form the quotient by this equivalence relation at each fixed size.
For every discrete group \(\Gamma \), the weak labeled join constructed above is an explicit universal proper \(\Gamma \)-CW complex. It has a genuine finite-isotropy CW structure, a proper action, contractible fixed-point spaces for finite subgroups, and empty fixed-point spaces for infinite subgroups. Every finite-isotropy equivariant CW complex admits an equivariant map to this model, and any two such maps are equivariantly homotopic. Every other equivariant CW model satisfying the same fixed-point criterion is equivariantly homotopy equivalent to it.
Convolution and involution preserve finite support, with
Moreover,
For \(a\in \mathbb C[\Gamma ]\), \(\xi \in \ell ^2(\Gamma )\) and \(h\in \Gamma \),
Each \(\lambda _g\) is a complex-linear isometry, and
where the final norm is the operator norm.
The canonical star-algebra isomorphism \(e_\Gamma :A_r(\Gamma )\to C_r^*(\Gamma )\) induces additive isomorphisms
For a finite matrix projection \(p\) over \(A_r(\Gamma )\), its image is represented by the matrix obtained by applying \(e_\Gamma \) to every entry. In particular, \(K_0(e_\Gamma )([p])=[e_\Gamma (p)]\). The inverse maps are induced by \(e_\Gamma ^{-1}\), and
where \(\iota _C:V(C_r^*(\Gamma ))\to K_0(C_r^*(\Gamma ))\) is the concrete model’s group-completion map. This equation uniquely determines the underlying homomorphism \(K_0(e_\Gamma )\). Countability of \(\Gamma \) is not required.
- BC4lean.reducedCompletionProjectionMap
- BC4lean.reducedCompletionProjectionMap_entry
- BC4lean.reducedCompletionProjectionEquiv
- BC4lean.reducedCompletionProjectionEquiv_of
- BC4lean.reducedCompletionProjectionEquiv_symm_of
- BC4lean.reducedCompletionK0Equiv
- BC4lean.reducedCompletionK0Equiv_class
- BC4lean.reducedCompletionK0Equiv_symm_class
- BC4lean.reducedCompletionK0Equiv_comp_class
- BC4lean.reducedCompletionK0Equiv_projection
- BC4lean.reducedCompletionK0Equiv_unique
For the two full scalar input cycles described above, creation at \(1\) into the constructed general interior tensor is noncompact. Its actual adjoint square is the identity on the infinite-dimensional second module. This verifies the counterexample within the constructed tensor, without substituting a different tensor model.
The adjoint is unique, and \(T\) is automatically right \(B\)-linear. Adjointable maps are closed under addition, complex scalar multiplication and composition. They have identity and zero maps, composition is associative, and
- BC4lean.KKTheory.AdjointableMap.adjoint_unique
- BC4lean.KKTheory.AdjointableMap.map_op_smul
- BC4lean.KKTheory.AdjointableMap.adjoint_adjoint
- BC4lean.KKTheory.AdjointableMap.adjoint_comp
- BC4lean.KKTheory.AdjointableMap.id_comp
- BC4lean.KKTheory.AdjointableMap.comp_id
- BC4lean.KKTheory.AdjointableMap.comp_assoc
- BC4lean.KKTheory.AdjointableMap.adjoint_add
- BC4lean.KKTheory.AdjointableMap.adjoint_smul
Adjoints preserve the operator norm and satisfy \(\| T^*T\| =\| T\| ^2\), also for maps between different right pre-Hilbert modules.
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
For an arbitrary Hilbert \(C(X,B)\)-module over compact Hausdorff \(X\), evaluate its actual inner product at \(t\), quotient its null radical, and complete the resulting pre-Hilbert module. This constructs the fibre \(E_t\) and its canonical dense map, with the prescribed evaluated inner product. Countable generation descends. Adjointable operators induce a contractive unital star homomorphism on fibres, and rank-one evaluation proves that compact module operators descend to compact operators.
An actual equivariant Kasparov cycle on an arbitrary complete countably generated Hilbert \(C(X,B)\)-module, with coefficient action acting pointwise and fixing \(X\), induces a whole cycle on every evaluated fibre. Its grading, semilinear action, representation and Fredholm operator are the induced actual fibre maps, and all four compact defects descend. Degeneracy is preserved. For a fixed-module operator path, these general fibres are unitarily identified with its original parameterwise cycles.
For complete \(E\) over compact Hausdorff \(X\), its actual closed evaluated radical quotient has Banach quotient norm equal to the evaluated inner-product norm. Continuous cutoffs and the coefficient approximate unit give arbitrarily close norm-controlled representatives. Consequently the evaluated quotient is already complete and the canonical map \(E\to E_t\) is surjective.
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 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.
The actual balanced tensor form is positive on every algebraic tensor, for complete Hilbert modules. Amplifying the positive finite Gram matrix by the left representation and using its genuine matrix positive cone proves positivity on finite tensor sums. A zero quadratic vector pairs to zero with every vector in the same positive matrix form. This uses actual second-module inner products, with no assumed tensor norm or separation axiom.
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.
Let \(A\longrightarrow X\) carry a relative equivariant CW structure, with skeletal sequence \((X_n)_{n\geq 0}\). The map \(A\longrightarrow X\), every transition \(X_m\longrightarrow X_n\) for \(m\leq n\), and every inclusion \(X_n\longrightarrow X\) are closed embeddings. In particular, no distinct points of a skeleton are identified in later stages or in the colimit.
A continuous real-valued function on the source of an orbit-cell attachment extends to its target. More generally, every continuous real-valued function on a skeleton \(X_n\) of a relative equivariant CW complex extends to the whole space \(X\). These scalar functions need not be equivariant.
Every point of \(X\) comes from some finite skeletal stage. A subset of \(X\) is open, respectively closed, exactly when its inverse image in every \(X_n\) is open, respectively closed. A function \(X\longrightarrow Z\) into any topological space is continuous exactly when its restriction to every skeletal stage is continuous.
The actual algebraic tensor \(B\otimes _{\mathbb C}\mathrm{Cl}_1\) has coordinate map \(b\otimes (z_+,z_-)\mapsto (z_+b,z_-b)\) and norm \(\max (\| b_+\| ,\| b_-\| )\). Its constructed complete \(C^*\)-algebra is star-isomorphic to \(B\times B\). The norm is the maximal norm over commuting representations, including nonunital and degenerate coefficient representations. No spatial tensor-norm comparison is claimed here.
For a proper \(\Gamma \)-space \(E\), every compact subset \(K\subseteq E\) is contained in a closed cocompact invariant piece, namely its saturation \(q^{-1}(q(K))\), where \(q:E\to E/\Gamma \). In particular the pieces cover \(E\).
The closed cocompact pieces form a nonempty directed indexing system: the empty set is a piece, and \(X\cup Y\) is a common upper bound. For continuous actions every piece has compact intrinsic quotient. If \(E\) is locally compact, every piece is locally compact.
The actual increasing positive contractive coefficient approximate unit acts strongly as the identity on every right Hilbert module. A finite family of vectors can be approximated simultaneously by one positive selfadjoint contractive coefficient. A unit, completeness of the module and an extra essentiality hypothesis are not required.
The exact identity \(\| \theta _{x,x}\| =\| x\| ^2\) implies that the actual compact-operator approximate unit acts strongly as the identity on \(E\). The residual rank-one compression bounds vector errors by compact approximate-unit errors. This uses the original \(B\)-valued inner product; it does not retype \(E\) as a module with a compact-operator-valued inner product.
Evaluation gives a surjective nonunital star homomorphism \(\mathcal K_{C(X,B)}(E)\to \mathcal K_B(E_t)\), with norm-preserving lifts. Its kernel is exactly the closed complex span of the rank-one maps \(\theta _{x,y}\) with \(x_t=0\). Fibre-vector surjectivity lifts rank-one maps; closed \(C^*\)-homomorphism range gives the full epimorphism, and the actual compact-algebra approximate unit proves the kernel description.
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.
Strongly convergent selfadjoint contractions approximate every compact Hilbert-module map in operator norm after composition on either side. The finite-coordinate projections of \(H_B\oplus H_B\) commute with the reference projection onto its second summand. Their compressions of a compact perturbation of that reference converge in norm, uniformly over a norm-compact family of perturbations.
- BC4lean.KKTheory.isModuleCompact_tendsto_comp_left_of_strong_contractions
- BC4lean.KKTheory.isModuleCompact_tendsto_comp_right_of_strong_selfadjoint_contractions
- BC4lean.KKTheory.standardCountableCutoff_mul_mul_tendsto
- BC4lean.KKTheory.standardCountablePairedCutoff_commutes_reference
- BC4lean.KKTheory.standardCountableReferenceCompression_tendsto
- BC4lean.KKTheory.isCompact_eventually_uniform_moduleSandwich
- BC4lean.KKTheory.continuous_eventually_uniform_moduleSandwich
Compact module maps are closed under adjoints. Composition with an adjointable map on either side preserves compactness. Thus \(\mathcal K_B(E)\) is a closed adjoint-stable two-sided ideal of \(\mathcal L_B(E)\), and is a possibly nonunital \(C^*\)-algebra for complete \(E\).
Two admissible operators \(F_0,F_1\) on the same cycle frame give an actual norm-continuous affine operator homotopy if \((F_1-F_0)\phi (a)\) is compact for every \(a\). The exact noncommutative square identity controls the additional term \((F_1-F_0)^2\phi (a)\); commutation of the operators and global compactness of their difference are not required.
For a proper action of a discrete group, \(T(K,L)\) is finite whenever \(K,L\) are compact. If \(X\) is locally compact Hausdorff and the action is continuous, the converse holds. Under these hypotheses properness is also equivalent to compactness of \(\alpha ^{-1}(C)\) for every compact \(C\subseteq X\times X\).
Adjointable maps carry the norm \(\| T\| =\| T:E\to F\| \). For complete \(E,F\) this space is complete. Adjointable endomorphisms of complete \(E\) form a unital complex \(C^*\)-algebra, with multiplication by composition and involution by adjoint.
- BC4lean.KKTheory.AdjointableMap.instNormedAddCommGroup
- BC4lean.KKTheory.AdjointableMap.instNormedAlgebra
- BC4lean.KKTheory.AdjointableMap.instStarRing
- BC4lean.KKTheory.AdjointableMap.isClosed_range_toCLMPair
- BC4lean.KKTheory.AdjointableMap.toCLMPair_isometry
- BC4lean.KKTheory.AdjointableMap.instCompleteSpace
- BC4lean.KKTheory.AdjointableMap.instCStarAlgebra
For complete Hilbert modules and an actual possibly degenerate nonunital left representation, the tensor form’s zero quadratic vectors are precisely its pairing radical. The coefficient action descends through that radical. The induced norm on the separated balancing quotient and its actual norm completion construct \(E\otimes _B F\). Elementary tensors have the prescribed inner product, obey balance and span a dense subspace.
- BC4lean.KKTheory.moduleTensorInner_eq_zero_of_self
- BC4lean.KKTheory.moduleTensorNull
- BC4lean.KKTheory.preModuleTensorCStarModule
- BC4lean.KKTheory.PreHilbertModuleTensor
- BC4lean.KKTheory.InteriorModuleTensor
- BC4lean.KKTheory.interiorModuleTensorInner_mk_mk
- BC4lean.KKTheory.interiorModuleTensorMk_balance
- BC4lean.KKTheory.interiorModuleTensor_span_dense
A coefficient-preserving first-factor unitary induces a unitary of the completed interior tensor products, intertwining the corresponding first-factor operators. Interior tensoring also distributes over an actual second-factor Hilbert-module sum. This completed sum unitary preserves the full coefficient-valued inner product and intertwines the grading, group action, creation maps and their adjoints.
- BC4lean.KKTheory.InteriorModuleTensorFirstFactorEquiv.hilbertEquiv
- BC4lean.KKTheory.InteriorModuleTensorFirstFactorEquiv.hilbertEquiv_operator
- BC4lean.KKTheory.InteriorModuleTensorSecondDirectSum.hilbertEquiv
- BC4lean.KKTheory.InteriorModuleTensorSecondDirectSum.hilbertEquiv_creation
- BC4lean.KKTheory.InteriorModuleTensorSecondDirectSum.hilbertEquiv_creation_adjoint
- BC4lean.KKTheory.InteriorModuleTensorSecondDirectSum.hilbertEquiv_grading
- BC4lean.KKTheory.InteriorModuleTensorSecondDirectSum.hilbertEquiv_action
The complex one-generator Clifford algebra is the actual \(C^*\)-algebra \(\mathbb C\times \mathbb C\) with grading exchanging the coordinates. Its odd generator \(\varepsilon =(1,-1)\) is a selfadjoint unitary. Every selfadjoint unitary in a unital complex \(C^*\)-algebra gives a unique unital star homomorphism sending \(\varepsilon \) to that unitary.
Suppose the homotopy-terminal mapping condition holds for each of the four ordered pairs \((X,X),(X,Y),(Y,X),(Y,Y)\). Then \(X\) and \(Y\) are equivariantly homotopy equivalent, and their \(H\)-fixed-point spaces are homotopy equivalent for every subgroup \(H\). The mapping condition is preserved when its target is replaced by an equivariantly homotopy-equivalent space. These are conditional statements; they do not establish the mapping condition for a general model satisfying the fixed-point criterion.
The actual closed section space \(\{ x\in C([0,1],E):x(0)=0\} \) is a complete Hilbert \(C([0,1],B)\)-module with pointwise form and action. Uniform ramp regularization proves the density needed for its explicit countable generators when \(E\) is countably generated. Constant adjointable operators act on this cone and give a norm-contracting unital star homomorphism. No general closed-submodule countable-generation assertion is used.
For compact Hausdorff \(X\), continuous sections \(C(X,E)\) with their supremum norm form a right Hilbert \(C(X,B)\)-module under pointwise action and inner product. Norm-continuous compact operator fields lift to compact module operators by uniform finite partition approximation. Constant sections of a countable generating family generate densely. The evaluation-kernel quotient has its proved quotient norm and is unitarily identified with \(E\). This fibre assertion concerns continuous-section modules; fibres of arbitrary \(C(X,B)\)-modules require a further construction.
- BC4lean.KKTheory.exists_finite_partition_approximation
- BC4lean.KKTheory.continuousSectionCStarModule
- BC4lean.KKTheory.continuousSectionOperator
- BC4lean.KKTheory.continuousSectionOperator_isModuleCompact
- BC4lean.KKTheory.continuousSection_isCountablyGenerated
- BC4lean.KKTheory.continuousSectionFibreIsometryEquiv
- BC4lean.KKTheory.continuousSectionFibreModuleEquiv
Every continuous map \(f:\partial D^n\to Y\) into a contractible space \(Y\) extends to a continuous map \(F:D^n\to Y\), including when \(n=0\). More generally, a null-homotopic map from the unit sphere of a proper real normed vector space extends over its closed unit ball.
If \(X^H\) is contractible, every continuous equivariant map \(\Gamma /H\times \partial D^n\to X\) extends to \(\Gamma /H\times D^n\). In particular, a target satisfying the fixed-point criterion has this extension property for every finite subgroup \(H\).
Complete the finitely supported vectors with their actual coefficient form \(\langle x,y\rangle =\sum _i\langle x_i,y_i\rangle \) to construct the countable Hilbert-module sum. Norm convergence of coefficient-square partial sums gives an actual realized sequence, with its coordinates and mixed inner products. Summability of the real numbers \(\| x_i\| ^2\) is not required.
- BC4lean.KKTheory.CountableHilbertModuleSum
- BC4lean.KKTheory.countableModuleFinitePositiveForm
- BC4lean.KKTheory.countableModuleFinite_nullRadical_eq_bot
- BC4lean.KKTheory.countableModuleSequenceSum
- BC4lean.KKTheory.countableModuleSequenceSum_inner
- BC4lean.KKTheory.countableModuleEvaluation_sequenceSum
A separable possibly nonunital \(C^*\)-algebra has a positive contractive two-sided approximate-unit sequence, which commutes asymptotically with each element of that same algebra. Weakly null families admit arbitrarily small finite convex combinations on every eventual tail by Hahn–Banach separation. Quasicentrality in a larger multiplier algebra and the technical theorem require further proofs.
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.
Actual summed whole-cycle unitaries give exchange and associativity of even raw direct sums. A cycle’s opposite reverses its grading and Fredholm operator. The explicit cosine–sine rotation on the sum of a cycle and its opposite is an admissible norm-continuous operator homotopy ending at the exactly degenerate flip cycle. Operator homotopies can be summed. These statements do not themselves construct the full homotopy quotient.
- BC4lean.KKTheory.KasparovCycleIso.directSum
- BC4lean.KKTheory.KasparovCycleIso.sumComm
- BC4lean.KKTheory.KasparovCycleIso.sumAssoc
- BC4lean.KKTheory.KasparovCycle.opposite
- BC4lean.KKTheory.KasparovOperatorHomotopy.inverseRotation
- BC4lean.KKTheory.KasparovOperatorHomotopy.inverseRotation_target_isDegenerate
- BC4lean.KKTheory.KasparovOperatorHomotopy.directSum
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.
Let \(Y\) be contractible, let \(f_0,f_1:D^n\to Y\) be continuous, and let \(H:[0,1]\times \partial D^n\to Y\) be a homotopy between their restrictions. There is a homotopy \(F:[0,1]\times D^n\to Y\) from \(f_0\) to \(f_1\) satisfying \(F(t,s)=H(t,s)\) on the whole boundary, including when \(n=0\). Equivalently, every family of boundary paths with prescribed disk endpoints extends to a continuous family of disk paths, with those endpoints unchanged.
Let \(A\to B\) have a relative equivariant CW structure with finite cell stabilizers, and let \(X\) satisfy the fixed-point criterion. Every continuous equivariant map \(A\to X\) extends to \(B\to X\). Consequently every equivariant CW complex admits a continuous equivariant map to \(X\). No uniqueness up to equivariant homotopy is asserted here.
Let \(A\) have a finite-isotropy equivariant CW structure and let \(X\) satisfy the fixed-point criterion. Continuous equivariant maps \(A\to X\) exist, and any two such maps are equivariantly homotopic.
Conjugation \(T\mapsto U_gTU_{g^{-1}}\) preserves adjointability, its operator norm, and compact module operators. This applies to compatible maps between different modules as well as endomorphisms.
Every equivariant CW space built from the stated orbit cells is Hausdorff. More precisely, continuous real-valued functions separate its distinct points. This conclusion is derived from the categorical cell-attachment data; Hausdorffness is not an additional hypothesis.
Equivariant homotopy is reflexive, symmetric, transitive, and compatible with composition. Every time slice of an equivariant homotopy is a continuous equivariant map, with the specified maps at times zero and one.
- BC4lean.ProperActions.EquivariantHomotopy.refl
- BC4lean.ProperActions.EquivariantHomotopy.symm
- BC4lean.ProperActions.EquivariantHomotopy.trans
- BC4lean.ProperActions.EquivariantHomotopy.comp
- BC4lean.ProperActions.EquivariantHomotopy.atTime
- BC4lean.ProperActions.EquivariantHomotopy.at_apply
- BC4lean.ProperActions.EquivariantHomotopy.at_zero
- BC4lean.ProperActions.EquivariantHomotopy.at_one
- BC4lean.ProperActions.EquivariantlyHomotopic.refl
- BC4lean.ProperActions.EquivariantlyHomotopic.symm
- BC4lean.ProperActions.EquivariantlyHomotopic.trans
- BC4lean.ProperActions.EquivariantlyHomotopic.comp
Continuous equivariant maps have identity and associative composition, with both identity laws. Equality of maps is determined pointwise.
- BC4lean.ProperActions.EquivariantMap.ext
- BC4lean.ProperActions.EquivariantMap.map_smul
- BC4lean.ProperActions.EquivariantMap.continuous
- BC4lean.ProperActions.EquivariantMap.id
- BC4lean.ProperActions.EquivariantMap.comp
- BC4lean.ProperActions.EquivariantMap.id_apply
- BC4lean.ProperActions.EquivariantMap.comp_apply
- BC4lean.ProperActions.EquivariantMap.id_comp
- BC4lean.ProperActions.EquivariantMap.comp_id
- BC4lean.ProperActions.EquivariantMap.comp_assoc
For trivially graded coefficients and separable \(B\), the quotient of actual bundled even cycles by full homotopy is an abelian group under direct sum. Opposite grading and opposite operator give the inverse. Degenerate cycles vanish by an actual cone interval witness; the inverse law follows from the constructed rotation witness. Module carriers use a fixed explicit universe. The Clifford parity identification remains a separate obligation.
- BC4lean.KKTheory.KasparovHomotopyClass
- BC4lean.KKTheory.KasparovHomotopyClass.instAddCommGroup
- BC4lean.KKTheory.KasparovHomotopyClass.mk_eq_mk_iff_full
- BC4lean.KKTheory.KasparovHomotopyClass.mk_directSum
- BC4lean.KKTheory.KasparovHomotopyClass.mk_opposite
- BC4lean.KKTheory.KasparovHomotopyClass.mk_eq_zero_of_degenerate
- BC4lean.KKTheory.FullKasparovHomotopy.degenerateCone
- BC4lean.KKTheory.FullKasparovHomotopy.inverseRotation
For finite \(\Gamma \), the single zero-cell orbit \(\Gamma /\Gamma \times D^0\) is a locally compact second-countable universal proper equivariant CW model, with contractible subgroup fixed-point spaces and the universal mapping property for equivariant CW sources.
- BC4lean.ProperActions.FiniteGroupCWModel
- BC4lean.ProperActions.FiniteGroupCWModel.cwComplex
- BC4lean.ProperActions.FiniteGroupCWModel.fixedPoints_contractible
- BC4lean.ProperActions.FiniteGroupCWModel.fixedPointCriterion
- BC4lean.ProperActions.FiniteGroupCWModel.proper_locallyCompact_secondCountable
- BC4lean.ProperActions.FiniteGroupCWModel.homotopyTerminal
For a finite discrete group, the trivial action on a point is proper and satisfies the fixed-point criterion. For every \(\Gamma \)-space \(X\), maps from \(X\) to this point exist and are unique, hence unique up to equivariant homotopy. This verifies the topological and mapping claims for the finite-group point model; a formal CW structure is not asserted here.
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.
Equivariant homotopy equivalences have identity, reversal, and composition. Every equivariant homotopy equivalence \(X\simeq _\Gamma Y\) induces an ordinary homotopy equivalence \(X^H\simeq Y^H\) for every subgroup \(H\).
- BC4lean.ProperActions.EquivariantHomotopyEquiv.refl
- BC4lean.ProperActions.EquivariantHomotopyEquiv.symm
- BC4lean.ProperActions.EquivariantHomotopyEquiv.trans
- BC4lean.ProperActions.EquivariantHomotopyEquiv.fixedPoints
- BC4lean.ProperActions.EquivariantHomotopyEquiv.fixedPoints_toFun_apply
- BC4lean.ProperActions.EquivariantHomotopyEquiv.fixedPoints_invFun_apply
An equivariant homotopy \(F:f_0\simeq _\Gamma f_1\) restricts to an ordinary continuous homotopy \(F^H:f_0^H\simeq f_1^H\) for every subgroup \(H\). Restriction preserves constant homotopies, reversal, concatenation with the chosen half-interval parametrization, and composition of homotopies.
- BC4lean.ProperActions.EquivariantHomotopy.onFixedPoints
- BC4lean.ProperActions.EquivariantHomotopy.onFixedPoints_apply
- BC4lean.ProperActions.EquivariantHomotopy.onFixedPoints_refl
- BC4lean.ProperActions.EquivariantHomotopy.onFixedPoints_symm
- BC4lean.ProperActions.EquivariantHomotopy.onFixedPoints_trans
- BC4lean.ProperActions.EquivariantHomotopy.onFixedPoints_comp
- BC4lean.ProperActions.EquivariantlyHomotopic.onFixedPoints
For every subgroup \(H\leq \Gamma \), an equivariant map \(f:X\to Y\) restricts to a continuous map \(f^H:X^H\to Y^H\). Restriction preserves identity and composition. The subgroup need not be normal.
For an action by continuous translations on a Hausdorff space, \(X^H\) is closed for every subgroup \(H\). If \(X\) is locally compact, so is \(X^H\).
A point \(x\) lies in \(X^H\) exactly when \(H\leq \Gamma _x\). If \(H\leq K\), then \(X^K\subseteq X^H\), and \(X^{\{ 1\} }=X\).
The fibre of the direct sum is unitarily the direct sum of the two actual fibres, with all cycle data intertwined. Direct sums of full interval witnesses therefore prove congruence of the homotopy relation in both variables.
For trivially graded coefficients and separable \(B\), full homotopy uses an actual complete countably generated interval module and whole-cycle unitary identifications of both endpoint fibres. Reversal and matching-module gluing prove symmetry and transitivity. The generated relation is precisely the existence of one such interval witness. The group action fixes the interval parameter and acts pointwise on its coefficients.
Every finite Gram coefficient quadratic expression \(\sum _{i,j} b_i^*\langle x_i,x_j\rangle b_j\) equals \(\langle \sum _i x_i b_i,\sum _j x_j b_j\rangle \) and is positive. This follows directly from the coefficient inner-product identities and does not assume a tensor norm or tensor positivity.
The operations make \(\mathbb C[\Gamma ]\) a unital complex \(*\)-algebra: convolution is associative and bilinear, its identity is \(\delta _e\), and
The actual norm completion of a right pre-Hilbert \(B\)-module carries its extended coefficient action and inner product, satisfies every Hilbert-module law and retains the inherited completion norm. The canonical inclusion is a dense coefficient-inner-preserving linear isometry. Countable generation is preserved. Adjointable maps extend uniquely to completions, preserving adjoints, norm, composition and the endomorphism star-algebra structure. Completeness of the original module and a coefficient unit are not required.
- BC4lean.KKTheory.completionModuleSMul
- BC4lean.KKTheory.completionCStarModule
- BC4lean.KKTheory.completionInner_coe
- BC4lean.KKTheory.completion_norm_eq_sqrt_inner
- BC4lean.KKTheory.hilbertModuleToCompletion
- BC4lean.KKTheory.hilbertModuleToCompletion_denseRange
- BC4lean.KKTheory.IsCountablyGeneratedModule.completion
- BC4lean.KKTheory.AdjointableMap.completion
- BC4lean.KKTheory.AdjointableMap.norm_completion
- BC4lean.KKTheory.AdjointableMap.completionHom
The Hilbert-module direct sum has inner product \(\langle (x,y),(x',y')\rangle =\langle x,x'\rangle +\langle y,y'\rangle \) and norm \(\sqrt{\| \langle x,x\rangle +\langle y,y\rangle \| }\). Complete summands give a complete sum. Coordinate maps are adjointable, diagonal compact maps are compact, and countable generation is preserved. Swapping and reassociating summands give coefficient-inner-preserving isometries.
For any finite family in a complete Hilbert \(B\)-module, its matrix of coefficient inner products is positive in the actual \(C^*\)-matrix algebra over \(B\). Finite synthesis has the adjoint given by coefficient analysis. A faithful matrix action and its linking-module embedding realize the Gram matrix as \(T^*T\) and reflect positivity. Nonunital \(B\) is allowed.
An injective nonunital complex star homomorphism between \(C^*\)-algebras reflects selfadjointness and the given star-compatible positive order. Functoriality of the continuous functional calculus for the negative part proves positivity reflection.
Regard \(a\in \mathbb C[\Gamma ]\) also as a finitely supported \(\ell ^2\)-vector. Then
In particular, \(\rho \) is injective.
The map \(\rho \) is a unital complex \(*\)-algebra homomorphism:
Creation \(\theta _\xi (y)=\xi \otimes y\) on the actual completed tensor is adjointable, has norm at most \(\| \xi \| \), and satisfies \(\theta _\xi ^*(\zeta \otimes y)=\Psi (\langle \xi ,\zeta \rangle )y\) and \(\theta _\xi ^*\theta _\zeta =\Psi (\langle \xi ,\zeta \rangle )\). Precisely, \(\theta _\xi \) is compact if and only if \(\Psi (\langle \xi ,\xi \rangle )\) is compact. Compactness of the entire left action is sufficient; arbitrary creation maps are not asserted compact.
- BC4lean.KKTheory.moduleCreationMap
- BC4lean.KKTheory.moduleCreationMap_adjoint_mk
- BC4lean.KKTheory.moduleCreationMap_norm_le
- BC4lean.KKTheory.moduleCreationMap_adjoint_comp
- BC4lean.KKTheory.moduleCreationMap_isModuleCompact_iff
- BC4lean.KKTheory.moduleCreationMap_isModuleCompact_of_compact_left_action
An adjointable coefficient-linear \(T:E\to E\) induces the actual \(T\otimes 1\) on the completed interior tensor. It maps \(x\otimes y\) to \(Tx\otimes y\), has norm at most \(\| T\| \), and preserves adjoints. The construction is a unital complex star-algebra homomorphism on the adjointable endomorphism algebra.
For invariant subsets \(S\subseteq T\) of a \(\Gamma \)-space, the inclusion \(S\to T\) is continuous, equivariant and injective. These inclusions obey identity and composition laws and commute with inclusion into the ambient space. In particular, they give the inclusion maps between ordered cocompact pieces.
- BC4lean.ProperActions.InvariantSubset.inclusionMap
- BC4lean.ProperActions.InvariantSubset.inclusionMap_refl
- BC4lean.ProperActions.InvariantSubset.inclusionMap_comp
- BC4lean.ProperActions.InvariantSubset.inclusion_comp_inclusionMap
- BC4lean.ProperActions.InvariantSubset.inclusionMap_injective
- BC4lean.ProperActions.CocompactPiece.inclusionMap
- BC4lean.ProperActions.CocompactPiece.inclusionMap_comp
For a continuous \(\Gamma \)-action on \(E\) and an invariant subset \(X\) with its subspace topology, \(X/\Gamma \to E/\Gamma \) is a topological embedding. Thus \(X/\Gamma \) is compact if and only if the image of \(X\) in \(E/\Gamma \) is compact. No closedness or properness is needed for this assertion.
For unital complex \(C^*\)-algebras \(A,B\), the coordinate maps induce
Even and odd raw cycles have genuine direct sums, with diagonal representations and Fredholm operators and the compatible summed actions. Every localized compact defect is the diagonal sum of the original defects. Direct sums of degenerate cycles are degenerate. Group laws on a homotopy quotient remain a further target.
Construct the Kasparov product, with existence, well-definedness, associativity, and units. Record contravariance in the first algebra and covariance in the second. This is a substantial development, to be split into supporting lemmas in the detailed blueprint.
- BC4lean.KKTheory.CliffordExternalOddCoefficient.grading_tmul
- BC4lean.KKTheory.CliffordExternalOddCoefficient.mul_tmul
- BC4lean.KKTheory.CliffordExternalOddCoefficient.starTensor_tmul
- BC4lean.KKTheory.CliffordTwoGradedTensor.grading_tensor
- BC4lean.KKTheory.CliffordTwoGradedTensor.star_tensor
- BC4lean.KKTheory.CliffordTwoGradedTensor.tensor_mul
- BC4lean.KKTheory.GradedKasparovConnection
- BC4lean.KKTheory.GroupUniverseCommonParityProduct.product
- BC4lean.KKTheory.GroupUniverseCommonParityProduct.productAddHom
- BC4lean.KKTheory.GroupUniverseCommonParityProduct.product_add_first
- BC4lean.KKTheory.GroupUniverseCommonParityProduct.product_add_second
- BC4lean.KKTheory.GroupUniverseCommonParityProduct.product_assoc
- BC4lean.KKTheory.GroupUniverseExternalOddSemantics.action_tmul
- BC4lean.KKTheory.GroupUniverseExternalOddSemantics.grading_tmul
- BC4lean.KKTheory.GroupUniverseExternalOddSemantics.inner_tmul
- BC4lean.KKTheory.GroupUniverseExternalOddSemantics.moduleEquiv
- BC4lean.KKTheory.GroupUniverseExternalOddSemantics.op_smul_tmul
- BC4lean.KKTheory.GroupUniverseExternalOddSemantics.operator_tmul
- BC4lean.KKTheory.GroupUniverseExternalOddSemantics.representation_tmul
- BC4lean.KKTheory.GroupUniverseMatrixMoritaBridge.addEquivalence
- BC4lean.KKTheory.GroupUniverseMatrixMoritaBridge.coefficient_roundtrip
- BC4lean.KKTheory.GroupUniverseMatrixMoritaBridge.matrix_roundtrip
- BC4lean.KKTheory.GroupUniverseMatrixMoritaProduct.toCoefficientClass_eq_product
- BC4lean.KKTheory.GroupUniverseMatrixMoritaProduct.toCoefficientClass_product
- BC4lean.KKTheory.GroupUniverseMatrixMoritaProduct.toMatrixClass_eq_product
- BC4lean.KKTheory.GroupUniverseOddFirstParityProduct.evenOddEvenProduct_assoc
- BC4lean.KKTheory.GroupUniverseOddFirstParityProduct.evenOddOddProduct_assoc
- BC4lean.KKTheory.GroupUniverseOddFirstParityProduct.oddEvenEvenProduct_assoc
- BC4lean.KKTheory.GroupUniverseOddFirstParityProduct.oddEvenOddProduct_assoc
- BC4lean.KKTheory.GroupUniverseOddFirstParityProduct.oddEvenProduct
- BC4lean.KKTheory.GroupUniverseOddFirstParityProduct.oddOddEvenProduct_assoc
- BC4lean.KKTheory.GroupUniverseOddFirstParityProduct.oddOddOddProduct_assoc
- BC4lean.KKTheory.GroupUniverseOddFirstParityProduct.oddOddProduct
- BC4lean.KKTheory.GroupUniverseOrdinaryEven.coefficientPushforward_shrink
- BC4lean.KKTheory.GroupUniverseOrdinaryOdd.coefficientPushforward_mk_coefficientTensor
- BC4lean.KKTheory.GroupUniverseParityFunctoriality.coefficientPushforwardHom
- BC4lean.KKTheory.GroupUniverseParityFunctoriality.coefficientPushforward_comp
- BC4lean.KKTheory.GroupUniverseParityFunctoriality.coefficientPushforward_graded_even
- BC4lean.KKTheory.GroupUniverseParityFunctoriality.coefficientPushforward_graded_odd
- BC4lean.KKTheory.GroupUniverseParityFunctoriality.coefficientPushforward_id
- BC4lean.KKTheory.GroupUniverseParityFunctoriality.coefficientPushforward_product
- BC4lean.KKTheory.GroupUniverseParityFunctoriality.coefficientPushforward_product_eq_sourcePullback
- BC4lean.KKTheory.GroupUniverseParityFunctoriality.homClass_leftProduct_eq_sourcePullback
- BC4lean.KKTheory.GroupUniverseParityFunctoriality.sourcePullbackHom
- BC4lean.KKTheory.GroupUniverseParityFunctoriality.sourcePullback_coefficientPushforward
- BC4lean.KKTheory.GroupUniverseParityFunctoriality.sourcePullback_comp
- BC4lean.KKTheory.GroupUniverseParityFunctoriality.sourcePullback_graded_even
- BC4lean.KKTheory.GroupUniverseParityFunctoriality.sourcePullback_graded_odd
- BC4lean.KKTheory.GroupUniverseParityFunctoriality.sourcePullback_id
- BC4lean.KKTheory.GroupUniverseParityFunctoriality.sourcePullback_product
- BC4lean.KKTheory.GroupUniverseParityProduct.evenEvenOddProduct_assoc
- BC4lean.KKTheory.GroupUniverseParityProduct.evenOddProduct
- BC4lean.KKTheory.GroupUniverseParityProduct.evenProduct
- BC4lean.KKTheory.GroupUniverseParityProduct.evenProduct_assoc
- BC4lean.KKTheory.GroupUniverseParityUnits.identity
- BC4lean.KKTheory.GroupUniverseParityUnits.left_identity
- BC4lean.KKTheory.GroupUniverseParityUnits.right_identity
- BC4lean.KKTheory.GroupUniverseProduct.bundledProduct_fullHomotopic_first
- BC4lean.KKTheory.GroupUniverseProduct.bundledProduct_fullHomotopic_second
- BC4lean.KKTheory.GroupUniverseProduct.identity
- BC4lean.KKTheory.GroupUniverseProduct.product
- BC4lean.KKTheory.GroupUniverseProduct.productOperator
- BC4lean.KKTheory.GroupUniverseProduct.productOperator_isProduct
- BC4lean.KKTheory.GroupUniverseProduct.product_assoc
- BC4lean.KKTheory.GroupUniverseProduct.product_left_identity
- BC4lean.KKTheory.GroupUniverseProduct.product_mk_eq_of_isProduct
- BC4lean.KKTheory.GroupUniverseProduct.product_right_identity
- BC4lean.KKTheory.IsGradedKasparovProductOperator
- BC4lean.KKTheory.exists_actualGradedKasparovProductOperator
- BC4lean.KKTheory.exists_fullGradedKasparovProductOperatorHomotopy
- BC4lean.KKTheory.exists_kasparovDiscreteTechnicalPartition
- BC4lean.KKTheory.exists_odd_gradedKasparovConnection
For the trivial group, establish \(KK_i(\mathbb C,B)\cong K_i(B)\).
- BC4lean.KKTheory.nonunitalRelativeK0KasparovMapAtUniverse_leftInverse
- BC4lean.KKTheory.nonunitalRelativeK0KasparovMapAtUniverse_rightInverse
- BC4lean.KKTheory.nonunitalRelativeK0KasparovMapAtZero_natural
- BC4lean.KKTheory.oddKKIndependentCoefficientPushforward_comparison_square
- BC4lean.KKTheory.oddKKOperatorK1AllModuleUniversesAddEquiv
- BC4lean.KKTheory.oddKKOperatorK1AllModuleUniversesAddEquiv_independentCoefficient_natural
- BC4lean.KKTheory.oddKKOperatorK1Index_independentCoefficientPushforward_anyModuleUniverse
- BC4lean.KKTheory.oddOperatorK1KKInverseAllModuleUniverses_independentCoefficient_natural
- BC4lean.KKTheory.oddOperatorK1KKInverseAllModuleUniverses_leftInverse_index
- BC4lean.KKTheory.oddOperatorK1KKInverseAllModuleUniverses_rightInverse_index
- BC4lean.KKTheory.scalarCliffordOperatorK1AllModuleUniversesAddEquiv
- BC4lean.KKTheory.scalarKKOperatorK0AddEquiv
- BC4lean.KKTheory.scalarKKOperatorK0AddEquiv_natural
- BC4lean.KKTheory.scalarKKOperatorK0IndexHom
- BC4lean.KKTheory.scalarKKOperatorK0IndexHom_natural
- BC4lean.KKTheory.scalarKKOperatorK0Index_universe
The inner product is well defined, and \(\ell ^2(\Gamma )\) is a complex Hilbert space. The delta vectors are orthonormal and have dense finite linear span. For every \(h\), \(|\xi (h)|\leq \| \xi \| _2\) and \(\langle \delta _h,\xi \rangle =\xi (h)\).
Every finite subgroup \(H\) has an explicitly constructed fixed vertex at each natural-number label: use the identity coset in the \(H\)-tagged summand.
If a group element stabilizes a labeled orbit simplex setwise, it fixes each of its vertices. Every nonempty simplex has finite stabilizer subgroup. The nonempty hypothesis is essential: the empty simplex is stabilized by all of \(\Gamma \).
- BC4lean.ProperActions.FiniteOrbitVertex.finite_fixing
- BC4lean.ProperActions.LabeledOrbitSimplex.Stabilizes
- BC4lean.ProperActions.LabeledOrbitSimplex.fixes_vertex_of_stabilizes
- BC4lean.ProperActions.LabeledOrbitSimplex.stabilizes_iff_smul_eq
- BC4lean.ProperActions.LabeledOrbitSimplex.finite_stabilizer
- BC4lean.ProperActions.LabeledOrbitSimplex.stabilizer_finite
The actual fixed-point space of every finite subgroup is contractible, and that of every infinite subgroup is empty.
- BC4lean.ProperActions.LabeledOrbitRealization.globalShift
- BC4lean.ProperActions.LabeledOrbitRealization.continuous_globalShift
- BC4lean.ProperActions.LabeledOrbitRealization.fixedGlobalShiftHomotopy
- BC4lean.ProperActions.LabeledOrbitRealization.fixedConeHomotopy
- BC4lean.ProperActions.LabeledOrbitRealization.fixedPoints_contractible
- BC4lean.ProperActions.LabeledOrbitRealization.fixedPointCriterion
The weak labeled realization has a genuine finite-isotropy equivariant CW structure, with its dimension filtration as the actual skeletal sequence.
Every nonempty simplex chart is homeomorphic to a closed disk of dimension one less than its number of vertices. Its full face boundary corresponds exactly to the unit sphere, including the zero-dimensional case. Each chart is compact and closed embedded in the weak realization.
Each \(\lambda _g\) is unitary, with \(\lambda _g^{-1}=\lambda _{g^{-1}}=\lambda _g^*\).
Let \(Q,R\) be adjointable endomorphisms of a complete Hilbert \(B\)-module, with \(Q\) selfadjoint, and let \(r\in \mathbb R\). If \((Q-r)R\) is compact, then \((f(Q)-f(r))R\) is compact for every continuous real function \(f\). The statement requires neither commutation of \(Q\) and \(R\) nor global compactness of \(Q-r\). Continuous-function induction on the spectrum with \(r\) adjoined uses the actual closed compact-module ideal.
For two interval modules with a specified unitary between their meeting fibres, compact operators on the matching module are exactly the matching pairs of compact operators. The closed algebra generated by actual matching rank-one pairs equals this pullback algebra. This gives compactness of compatible compact operator pairs without assuming a compact lifting theorem.
Let \(\phi :A\to B\) be a unital complex star homomorphism. Applying \(\phi \) entrywise sends finite matrix projections over \(A\) to projections over \(B\), preserves block sums and zero projections, and preserves rectangular equivalence. The finite index types are unchanged.
- BC4lean.OperatorKTheory.matrixMap
- BC4lean.OperatorKTheory.matrixProjectionMap
- BC4lean.OperatorKTheory.projectionMatrix_map
- BC4lean.OperatorKTheory.matrixProjectionMap_blockSum
- BC4lean.OperatorKTheory.rectEquivalent_map
- BC4lean.OperatorKTheory.FiniteProjection.map
- BC4lean.OperatorKTheory.FiniteProjection.equivalent_map
The coefficient action satisfies \(x(b+d)=xb+xd\), \((x+y)b=xb+yb\), \((xb)d=x(bd)\), \(x(cb)=c(xb)\) for \(c\in \mathbb C\), and \(\| xb\| \leq \| x\| \| b\| \). These properties follow from the module-valued inner-product identities and its norm, rather than being additional assumptions on the action.
The absolute value of a compact module endomorphism is compact. A selfadjoint compact endomorphism also has compact positive part. The compactness criterion for the actual adjoint square proves these statements in the given module.
Every adjointable map between complete modules has the actual contractive normalization \(T(\max (1,T^*T))^{-1/2}\). This analytic norm statement does not assume a Fredholm defect or establish preservation of cycle conditions.
The inner product separates points in either variable. In particular, if \(\langle z,x\rangle =\langle z,y\rangle \) for all \(z\in E\), then \(x=y\); the same holds when the test vector is in the second variable.
For a contractive adjointable \(T:F\to E\) between complete modules, functional calculus constructs \(D=(1-TT^*)^{1/2}\) and \(S=(1-T^*T)^{1/2}\) and proves \(DT=TS\). The block operator \(\left[\begin{smallmatrix} D & T \\ -T^* & S \end{smallmatrix}\right]\) is an actual coefficient-inner-product-preserving unitary of \(E\oplus F\).
For all appropriately typed vectors and adjointable maps,
In particular, \(\theta _{x,y}\theta _{u,v}=\theta _{x\langle y,u\rangle ,v}\).
A countably generated Hilbert module over separable \(B\) is separable as a complex normed space. Conversely, a separable Hilbert module is countably generated, also when \(B\) is nonunital. The coefficient approximate unit puts each vector of a dense sequence in the closure of its coefficient span.
Every nonunital complex star homomorphism of complete \(C^*\)-algebras has closed range. The norm on its actual kernel quotient equals the image norm, and every element in the image has a lift with exactly its image norm. Continuous functional calculus trims a representative without changing its image and gives the quotient isometry.
Complex star homomorphisms, including nonunital ones, induce homomorphisms on \(K_i^{\mathrm{op}}\) that preserve identities and composition. For unital homomorphisms between unital algebras, these maps agree with the unital constructions under the preceding comparison isomorphisms.
- BC4lean.OperatorKTheory.scalarQuotient_natural
- BC4lean.OperatorKTheory.operatorK0Map
- BC4lean.OperatorKTheory.operatorK1Map
- BC4lean.OperatorKTheory.operatorK0Map_id
- BC4lean.OperatorKTheory.operatorK1Map_id
- BC4lean.OperatorKTheory.operatorK0Map_comp
- BC4lean.OperatorKTheory.operatorK1Map_comp
- BC4lean.OperatorKTheory.operatorK0UnitalEquiv_natural
- BC4lean.OperatorKTheory.operatorK1UnitalEquiv_natural
Point-norm homotopic complex star homomorphisms \(\phi ,\psi :A\to B\) induce the same maps on both operator \(K\)-groups:
This holds for possibly nonunital algebras and homomorphisms. For a homotopy through unital homomorphisms, equality also holds directly for the unital projection and stable-unitary constructions, and for \(V(\phi ),V(\psi )\).
- BC4lean.OperatorKTheory.UnitalStarHomotopy.continuous_matrixMap
- BC4lean.OperatorKTheory.UnitalStarHomotopy.projectionPath
- BC4lean.OperatorKTheory.UnitalStarHomotopy.unitaryPath
- BC4lean.OperatorKTheory.finiteProjection_equivalent_of_homotopy
- BC4lean.OperatorKTheory.stableProjectionMap_homotopy
- BC4lean.OperatorKTheory.k0Map_homotopy
- BC4lean.OperatorKTheory.k1Map_homotopy
- BC4lean.OperatorKTheory.operatorK0Map_homotopy
- BC4lean.OperatorKTheory.operatorK1Map_homotopy
If \(A\) is unital, there are canonical additive isomorphisms \(K_i^{\mathrm{op}}(A)\cong K_i(A)\) for \(i=0,1\). They send a kernel class by the map induced by \((r,a)\mapsto r1_A+a\).
For every abelian group \(G\), composition with the canonical map induces a bijection
Block sum makes \(K_1(A)\) an abelian group, with
Norm-homotopic unitaries have the same class, and \([u\oplus 1_J]=[u]\). Every class has a representative indexed by \(\operatorname {Fin}(n)\).
- BC4lean.OperatorKTheory.FiniteUnitary.blockSum_congr
- BC4lean.OperatorKTheory.FiniteUnitary.adjoint_congr
- BC4lean.OperatorKTheory.K1.instAddCommGroup
- BC4lean.OperatorKTheory.K1.of_blockSum
- BC4lean.OperatorKTheory.K1.of_adjoint
- BC4lean.OperatorKTheory.K1.of_identity
- BC4lean.OperatorKTheory.K1.of_homotopic
- BC4lean.OperatorKTheory.K1.of_stabilize
- BC4lean.OperatorKTheory.K1.exists_finRepresentative
An admissible fixed-module operator path gives an actual equivariant cycle on the continuous-section Hilbert \(C([0,1],B)\)-module. Its evaluation-kernel fibres carry the induced whole cycles, and genuine cycle unitaries identify them with the original parameterwise cycles, including the endpoints. This does not assert that every interval cycle has a fixed-module path model.
Every orbit boundary inclusion is injective. For finite \(H\), both \(\Gamma /H\times D^n\) and \(\Gamma /H\times \partial D^n\) are proper \(\Gamma \)-spaces, including when \(n=0\).
Let \(H\) be any subgroup and let the action on the parameter spaces \(D,E\) be trivial. For a target \(\Gamma \)-space \(X\), evaluation on the identity-coset slice gives a bijection between continuous equivariant maps \(\Gamma /H\times D\to X\) and continuous maps \(D\to X^H\). For a continuous map \(i:D\to E\), a map on \(\Gamma /H\times D\) extends across \(\mathrm{id}\times i\) if and only if its fixed-point slice extends across \(i\). This is a bijection of sets of maps, not a claimed homeomorphism of mapping spaces.
For subgroups \(H,K\leq \Gamma \) and a topological parameter space \(D\) with trivial action, there is a natural homeomorphism \(((\Gamma /H)\times D)^K\cong (\Gamma /H)^K\times D\). The fixed cell is nonempty exactly when both factors are nonempty; an empty factor gives an empty fixed cell. Neither subgroup needs to be finite or normal.
- BC4lean.ProperActions.OrbitCell.fixedSpaceHomeomorph
- BC4lean.ProperActions.OrbitCell.fixedSpaceHomeomorph_fst
- BC4lean.ProperActions.OrbitCell.fixedSpaceHomeomorph_snd
- BC4lean.ProperActions.OrbitCell.fixedSpaceHomeomorph_symm_coe
- BC4lean.ProperActions.OrbitCell.fixedSpace_nonempty_iff
- BC4lean.ProperActions.OrbitCell.fixedSpace_isEmpty_of_cosets
- BC4lean.ProperActions.OrbitCell.fixedSpace_isEmpty_of_parameter
Suppose \(X^H\) is contractible. A continuous equivariant family of paths on \(\Gamma /H\times \partial D^n\) extends to \(\Gamma /H\times D^n\) whenever its two endpoint maps are prescribed on the disk and agree on the boundary. Both endpoint maps and every prescribed boundary path are preserved exactly.
For a discrete group \(\Gamma \), any subgroup \(H\), and any \(\Gamma \)-space \(X\), evaluation at \(H\in \Gamma /H\) is a bijection
for continuous equivariant maps. Its inverse sends \(x\) to \(gH\mapsto gx\). The bijection is natural under continuous equivariant maps in \(X\). No normality or finiteness hypothesis on \(H\) is required.
For any family of finite subgroups \((H_i)_{i\in J}\), the disjoint union
has a zero-dimensional equivariant CW structure.
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 positive semidefinite coefficient-valued module form satisfies Cauchy–Schwarz and gives the seminorm \(\| x\| _q=\sqrt{\| \langle x,x\rangle \| }\). Its null vectors form a coefficient-invariant complex submodule. Quotienting that actual radical, with this induced form norm, constructs a separated pre-Hilbert module. No definiteness or pre-existing vector norm is assumed.
Every finite-isotropy equivariant CW complex admits a map to \(P(\Gamma )\), unique up to equivariant homotopy. For countable discrete groups the target is proper. This is a mapping theorem for CW sources; a CW structure on \(P(\Gamma )\) has not been constructed.
For finite \(H\leq \Gamma \), \(P(\Gamma )^H\) is contractible. For infinite \(H\leq \Gamma \), it is empty. Thus \(P(\Gamma )\) satisfies the fixed-point criterion.
For countable discrete \(\Gamma \), \(P(\Gamma )\) is a proper second-countable \(\Gamma \)-space. More generally, compact subsets of \(P(\Gamma )\) have finite transporters for every discrete group.
If \(p\sim p'\) and \(q\sim q'\), then \(p\oplus q\sim p'\oplus q'\). Thus block sum and stabilization descend to equivalence classes at the indicated matrix sizes.
The endpoints of a norm-continuous path of projections are Murray–von Neumann equivalent.
If projections \(p,q\) admit an invertible element \(s\) with \(sp=qs\), then \(p\) and \(q\) are Murray–von Neumann equivalent. In particular, every projection has a norm neighborhood of equivalent projections.
A unital complex star homomorphism \(\phi :A\to B\) sends projections to projections and preserves Murray–von Neumann equivalence. It therefore induces a map on the preceding quotients.
Every continuous action of a finite discrete group on a locally compact Hausdorff space is proper. Left translation of a topological group on itself is proper. If a discrete group acts properly on a nonempty compact space, the group is finite.
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 left action on \(\Gamma /H\) is proper if and only if \(H\) is finite. When \(H\) is finite, the projection \(\Gamma \to \Gamma /H\) is a proper map.
For a proper discrete-group action, any subgroup fixing a point is finite. Consequently \(X^H=\varnothing \) whenever \(H\) is infinite.
A continuous equivariant map from a locally compact Hausdorff \(\Gamma \)-space to a proper \(\Gamma \)-space implies properness of the source. In particular, \(\Gamma /H\times D\) is proper if \(H\) is finite and \(D\) is locally compact Hausdorff.
A proper action has Hausdorff orbit space \(X/\Gamma \). If \(X\) is locally compact, then \(X/\Gamma \) is locally compact as well.
Rectangular equivalence is an equivalence relation on finite matrix projections of varying sizes. It is unchanged by reindexing and zero-padding. Moreover,
where the relation on the right is ordinary Murray–von Neumann equivalence. Thus rectangular witnesses give a model for stable projection equivalence.
- BC4lean.OperatorKTheory.rectangular_right_support
- BC4lean.OperatorKTheory.rectangular_left_support
- BC4lean.OperatorKTheory.rectEquivalent_refl
- BC4lean.OperatorKTheory.rectEquivalent_symm
- BC4lean.OperatorKTheory.rectEquivalent_trans
- BC4lean.OperatorKTheory.rectEquivalent_stabilize
- BC4lean.OperatorKTheory.rectEquivalent_of_reindex
- BC4lean.OperatorKTheory.rectEquivalent_iff_padded
For an adjointable map \(T:E\to F\) with complete source module, \(T\) is compact if and only if \(T^*T\) is compact. The target need not be complete. An approximate unit of \(\mathcal K_B(E)\) and the rectangular \(C^*\)-identity show that \(T\) is a norm limit of compact maps \(Te\).
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
With codomain restricted to \(C_r^*(\Gamma )\), \(\rho \) is an isometric unital \(*\)-homomorphism for \(\| \cdot \| _r\) and has dense range. It extends uniquely to an isometric \(*\)-isomorphism from the norm completion of \((\mathbb C[\Gamma ],\| \cdot \| _r)\) onto \(C_r^*(\Gamma )\).
- BC4lean.ReducedNormGroupAlgebra
- BC4lean.ReducedNormGroupAlgebra.ofGroupAlgebra
- BC4lean.ReducedNormGroupAlgebra.norm_ofGroupAlgebra
- BC4lean.ReducedNormGroupAlgebra.toReduced_isometry
- BC4lean.ReducedNormGroupAlgebra.toReduced_denseRange
- BC4lean.ReducedCompletion
- BC4lean.completion_star_coe
- BC4lean.completionMap_star
- BC4lean.completionCStarAlgebra
- BC4lean.groupAlgebraToCompletion
- BC4lean.norm_groupAlgebraToCompletion
- BC4lean.reducedCompletionEquiv
- BC4lean.reducedCompletionEquiv_isometry
- BC4lean.reducedCompletionEquiv_extends
- BC4lean.reducedCompletionEquiv_unique
- BC4lean.reducedCompletionEquiv_unique_isometric
The algebra \(C_r^*(\Gamma )\) is the norm closure of \(\operatorname {span}_{\mathbb C}\{ \lambda _g:g\in \Gamma \} \). It is the smallest norm-closed \(*\)-subalgebra of \(\mathcal B(\ell ^2(\Gamma ))\) containing every \(\lambda _g\).
The inherited operations make \(C_r^*(\Gamma )\) a unital complex \(C^*\)-algebra with identity \(I=\lambda _e\).
For the one-element group, \(z\mapsto zI\) is an isometric unital \(*\)-isomorphism \(\mathbb C\to C_r^*(\{ e\} )\).
The reduced norm is a norm, with
Completeness of \(\mathbb C[\Gamma ]\) in this norm is not asserted.
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\).
Scalar creation maps in \(\mathbb C\otimes _{\mathbb C}H\) are bounded adjointable maps, but are not automatically compact. In the scalar correspondence \(\mathbb C\otimes _{\mathbb C}\ell ^2(\mathbb N)\cong \ell ^2(\mathbb N)\), creation at \(1\) is the identity under this identification, hence is not a compact Hilbert-space operator. The same actual tensor creation map is also noncompact for the scalar Hilbert-module compactness predicate. The failure persists for two actual complete, countably generated graded Kasparov cycles: the first is \(\mathbb C\) with operator zero, and the second is \(\ell ^2(\mathbb N)\oplus \ell ^2(\mathbb N)\) with diagonal grading and odd selfadjoint unitary flip. The second cycle has exactly zero defects.
- BC4lean.KKTheory.scalarCreationMap_adjoint_identity
- BC4lean.KKTheory.scalarCreationMap_one_not_compact
- BC4lean.KKTheory.ScalarHilbertModule.isCompactOperator_of_isModuleCompact
- BC4lean.KKTheory.scalarCreationModuleMap_one_not_moduleCompact
- BC4lean.KKTheory.ScalarCreationCycleCounterexample.firstCycle
- BC4lean.KKTheory.ScalarCreationCycleCounterexample.secondCycle
- BC4lean.KKTheory.ScalarCreationCycleCounterexample.secondCycle_isDegenerate
- BC4lean.KKTheory.ScalarCreationCycleCounterexample.fullCycleCounterexample
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.
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.
Every class in \(V(A)\) has a representative indexed by \(\{ 0,\ldots ,n-1\} \) for some \(n\geq 0\).
A unital complex star-algebra isomorphism \(e:A\to B\) induces an additive isomorphism \(V(e):V(A)\to V(B)\) sending \([p]\) to \([e(p)]\). Its inverse is \(V(e^{-1})\). This construction preserves identity isomorphisms and composition and takes inverses to inverses.
- BC4lean.OperatorKTheory.StableProjectionMonoid.map_leftInverse
- BC4lean.OperatorKTheory.StableProjectionMonoid.map_rightInverse
- BC4lean.OperatorKTheory.StableProjectionMonoid.mapEquiv
- BC4lean.OperatorKTheory.StableProjectionMonoid.mapEquiv_of
- BC4lean.OperatorKTheory.StableProjectionMonoid.mapEquiv_refl
- BC4lean.OperatorKTheory.StableProjectionMonoid.mapEquiv_symm
- BC4lean.OperatorKTheory.StableProjectionMonoid.mapEquiv_trans
Block sum makes \(V(A)\) an additive commutative monoid. Any zero projection represents its zero, and \([p\oplus 0]=[p]\).
- BC4lean.OperatorKTheory.rectEquivalent_blockSum
- BC4lean.OperatorKTheory.FiniteProjection.blockSum_congr
- BC4lean.OperatorKTheory.FiniteProjection.blockSum_assoc
- BC4lean.OperatorKTheory.FiniteProjection.blockSum_comm
- BC4lean.OperatorKTheory.FiniteProjection.zero_blockSum
- BC4lean.OperatorKTheory.StableProjectionMonoid.instAddCommMonoid
- BC4lean.OperatorKTheory.StableProjectionMonoid.of_zeroProjection
- BC4lean.OperatorKTheory.StableProjectionMonoid.of_stabilize
For separable possibly nonunital \(B\), the standard right module \(B_B\) is countably generated. With all-even grading, the coefficient action, left multiplication representation and \(F=0\), it is an actual even equivariant Kasparov cycle. These are the standard identity-cycle data; product unit laws require the product construction below.
Left multiplication identifies \(B\) isometrically as a complex star-algebra with \(\mathcal K_B(B_B)\), also for nonunital \(B\).
The standard right module \(B_B\) is complete, has inner product \(\langle x,y\rangle =x^*y\), and its rank-one operator \(\theta _{x,y}\) is left multiplication by \(xy^*\).
Every complete countably generated Hilbert \(B\)-module \(E\) admits a \(B\)-linear inner-product-preserving unitary \(E\oplus H_B\cong H_B\). The construction combines the dense synthesis, the countable Julia unitary, and the coefficient-preserving reindexing \(H_B^\infty \cong H_B\).
For a complete countably generated Hilbert \(B\)-module \(E\), rescaling a countable generating family by positive summable weights constructs a compact adjointable synthesis \(H_B\to E\) with dense range. Its adjoint has the coefficient inner products as coordinates, with a convergent \(B\)-valued sum of their squares.
For a possibly degenerate left representation \(\Psi :B\to \mathcal L_C(F)\), the actual map \(b\otimes y\mapsto \Psi (b)y\) identifies \(B_B\otimes _B F\) unitarily with the closed complex span of \(\Psi (B)F\). Surjectivity onto all of \(F\) is not asserted for a degenerate representation, and no complement for this essential range is assumed.
For \(S\subseteq T\), actual restriction \(C_0(T)\to C_0(S)\) is an equivariant nonunital complex star homomorphism. It induces the forward additive map on K-homology by contravariance in the first KK-variable. Identity inclusions act as identities and successive inclusions compose.
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.
For unital complex star homomorphisms \(\phi :A\to B\) and \(\psi :B\to C\),
Moreover, \(K_0(\phi )\) is the unique group homomorphism satisfying the projection-class formula above.
A unital complex star-algebra isomorphism \(e:A\to B\) induces a canonical additive isomorphism
with inverse \(K_0(e^{-1})\). The induced isomorphisms preserve identities and composition, and the group-completion maps \(V(A)\to K_0(A)\) commute with these isomorphisms.
- BC4lean.OperatorKTheory.k0Map_leftInverse
- BC4lean.OperatorKTheory.k0Map_rightInverse
- BC4lean.OperatorKTheory.k0Equiv
- BC4lean.OperatorKTheory.k0Equiv_toAddMonoidHom
- BC4lean.OperatorKTheory.k0Equiv_class
- BC4lean.OperatorKTheory.k0Equiv_projection
- BC4lean.OperatorKTheory.k0Equiv_refl
- BC4lean.OperatorKTheory.k0Equiv_symm
- BC4lean.OperatorKTheory.k0Equiv_trans
A unital complex star homomorphism \(\phi :A\to B\) induces an additive map \(K_1(\phi ):K_1(A)\to K_1(B)\), given by entrywise application on representatives. These maps preserve identities and composition.
A unital complex star-algebra isomorphism \(e:A\to B\) induces an additive isomorphism \(K_1(e)\), with inverse \(K_1(e^{-1})\). These isomorphisms preserve identities, inverses, and composition.
For \(u,v\in U_n(A)\), there is an explicit norm-continuous path
- BC4lean.OperatorKTheory.rotationMatrix
- BC4lean.OperatorKTheory.rotationMatrix_mem_unitary
- BC4lean.OperatorKTheory.rotationUnitary
- BC4lean.OperatorKTheory.continuous_rotationUnitary
- BC4lean.OperatorKTheory.rotationUnitary_zero
- BC4lean.OperatorKTheory.rotationUnitary_conjugate
- BC4lean.OperatorKTheory.unitaryBlockProductPath
- BC4lean.OperatorKTheory.unitaryHomotopic_blockSum_mul
Norm homotopy is an equivalence relation and is preserved by multiplication of pairs of unitaries and by inversion.
Block sum is continuous and preserves norm homotopies. Consequently, stabilization induces maps on the fixed-size norm-path components.
For every \(u\in U_n(A)\), both \(u\oplus u^*\) and \(u^*\oplus u\) are norm homotopic to \(1_{2n}\).
For countable discrete \(\Gamma \), take one zero-cell orbit \(\Gamma /H\) for every finite subgroup \(H\). The resulting space is countable, discrete, locally compact, second countable, and proper. Every finite subgroup has an explicitly constructed fixed vertex, and infinite subgroups have no fixed vertices.
- BC4lean.ProperActions.finiteIsotropy_countable
- BC4lean.ProperActions.UniversalZeroSkeleton
- BC4lean.ProperActions.UniversalZeroSkeleton.fixedVertex
- BC4lean.ProperActions.UniversalZeroSkeleton.cwComplex
- BC4lean.ProperActions.UniversalZeroSkeleton.countable
- BC4lean.ProperActions.UniversalZeroSkeleton.locallyCompact_secondCountable
- BC4lean.ProperActions.UniversalZeroSkeleton.proper
- BC4lean.ProperActions.UniversalZeroSkeleton.infinite_fixedPoints_empty
The actual coefficient-free reduced assembly map for the literal one-element group \(\mathrm{Unit}:\mathrm{Type}\) is an isomorphism in both degrees.