Dependencies

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.

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.

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.

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\).

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.

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.

Projections \(p,q\in A\) are Murray–von Neumann equivalent, written \(p\sim q\), if some \(v\in A\) satisfies \(v^*v=p\) and \(vv^*=q\).

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.

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.

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.

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.

For unital complex \(C^*\)-algebras \(A,B\), the coordinate maps induce

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.

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.

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 )\).

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)\).

If \(p\in \operatorname {Proj}(A)\) and \(v^*v=p\), then \(vp=v\).

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 relation \(\sim \) is an equivalence relation, so its quotient is defined.

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.

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.

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.

Block sum makes \(V(A)\) an additive commutative monoid. Any zero projection represents its zero, and \([p\oplus 0]=[p]\).

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.

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

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 same-size unitaries \(w,u\), there is a norm homotopy

For every \(u\in U_n(A)\), both \(u\oplus u^*\) and \(u^*\oplus u\) are norm homotopic to \(1_{2n}\).