3 Operator K-theory and the analytic side
Unless stated otherwise, \(A\) is a unital complex \(C^*\)-algebra. The verified definitions include the stable projection monoid \(V(A)\), the unital groups \(K_0(A)\) and \(K_1(A)\), and their functoriality. For possibly nonunital complex \(C^*\)-algebras, the scalar kernels of the forced unitization define both operator \(K\)-groups. For unital algebras, these kernel definitions are naturally isomorphic to the preceding unital constructions. Point-norm homotopy invariance of induced maps is also verified. Exact sequences and Bott periodicity remain separate formalization targets.
3.1 Projections and Murray–von Neumann equivalence
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.
If \(p\in \operatorname {Proj}(A)\) and \(v^*v=p\), then \(vp=v\).
For \(x=vp-v\), expansion using \(p^*=p\), \(p^2=p\), and \(v^*v=p\) gives \(x^*x=0\). The \(C^*\)-identity implies \(x=0\).
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\).
The relation \(\sim \) is an equivalence relation, so its quotient is defined.
Reflexivity uses \(v=p\) and symmetry uses \(v^*\). If \(v\) implements \(p\sim q\) and \(w\) implements \(q\sim r\), then \(wv\) implements \(p\sim r\). The support identities \(vp=v\), \(qv=v\), and \(wq=w\) give the two required equations. These quotients concern one algebra at a time; they are not yet stable classes.
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.
Apply \(\phi \) to the projection equations and, for equivalence, to the witness \(v\) and its two defining equations.
3.2 Matrix stabilization and the construction of \(K_0\)
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.
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.
If \(v\) and \(w\) are the respective witnesses, use \(v\oplus w\). Block multiplication and adjoints give both defining equations.
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.
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.
Embed a rectangular matrix as an off-diagonal block in \(M_{I\sqcup J}(A)\). The square-matrix support lemma gives \(vq=v\) from \(v^*v=q\) and, by taking adjoints, \(pv=v\) from \(vv^*=p\). These identities prove transitivity using the product of rectangular witnesses. Reindexing uses submatrices along bijections. Zero projections of any sizes are equivalent using the zero rectangular matrix; block sum and reindexing then give zero-padding invariance. Combine these equivalences with the fixed-size equivalence relation to obtain the displayed common-corner characterization.
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.
Block sum makes \(V(A)\) an additive commutative monoid. Any zero projection represents its zero, and \([p\oplus 0]=[p]\).
Block sums of rectangular witnesses prove independence of representatives. The associativity and block-switching bijections of finite index sets prove associativity and commutativity in the quotient. The empty matrix gives the identity. Zero-padding invariance follows from rectangular equivalence.
Every class in \(V(A)\) has a representative indexed by \(\{ 0,\ldots ,n-1\} \) for some \(n\geq 0\).
Reindex a projection using the bijection from its finite index type to the standard finite ordinal of the same cardinality. Reindexing preserves its class.
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.
For every abelian group \(G\), composition with the canonical map induces a bijection
Apply the universal property of Mathlib’s additive Grothendieck group to the verified commutative monoid \(V(A)\). The resulting extension agrees on projection classes and is unique.
3.3 Functoriality of unital \(K_0\)
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.
The entrywise map commutes with matrix multiplication and adjoints. If \(vv^*=p\) and \(v^*v=q\), then the entrywise image of \(v\) witnesses the corresponding equations for the images of \(p\) and \(q\). Zero off-diagonal blocks remain zero, so block sums are preserved. No injectivity of \(\phi \) is required.
The entrywise map descends to an additive map
These maps preserve identities and composition.
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.
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.
The universal property implies that homomorphisms out of \(K_0(A)\) are determined by their values on projection classes. Evaluate both sides of each asserted equality on such a class and use the identity and composition laws of the entrywise maps. This proof does not assume cancellation in \(V(A)\).
3.4 Invariance under unital star-algebra isomorphism
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.
Apply the identity and composition laws for \(V\) to \(e^{-1}\circ e=\mathrm{id}_A\) and \(e\circ e^{-1}=\mathrm{id}_B\). The two induced additive maps are mutual inverses. The projection-class formula and coherence laws follow from those for the entrywise maps.
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.
The verified functorial laws give \(K_0(e^{-1})K_0(e)=\mathrm{id}_{K_0(A)}\) and \(K_0(e)K_0(e^{-1})=\mathrm{id}_{K_0(B)}\). These two identities supply the inverse data for a bundled additive equivalence. The class formula and compatibility with identity, inverse, and composition follow from the corresponding laws for \(K_0\) homomorphisms.
3.5 Unitaries, norm homotopy, and \(K_1\)
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\).
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.
Norm homotopy is an equivalence relation and is preserved by multiplication of pairs of unitaries and by inversion.
Use constant paths, reversal, concatenation, pointwise multiplication, and pointwise inversion in the topological unitary group.
Block sum is continuous and preserves norm homotopies. Consequently, stabilization induces maps on the fixed-size norm-path components.
The finite matrix topology agrees with the entrywise product topology, in which block sum is continuous. Apply block sum to a pair of paths; for stabilization, use a constant identity path in the second factor.
For \(u,v\in U_n(A)\), there is an explicit norm-continuous path
Put \(\theta =\pi t/2\) for \(0\leq t\leq 1\) and let
The identity \(\cos ^2\theta +\sin ^2\theta =1\) proves that \(R(\theta )\) is unitary. Its entries depend continuously on \(\theta \), hence it is continuous in the finite-matrix \(C^*\)-norm. The required path is
At \(t=0\) the rotation is the identity. At \(t=1\) its conjugation exchanges the two diagonal blocks, giving \((uv)\oplus 1_n\).
For every \(u\in U_n(A)\), both \(u\oplus u^*\) and \(u^*\oplus u\) are norm homotopic to \(1_{2n}\).
Specialize the preceding path to \(v=u^*\) and use \(uu^*=1_n\). Apply the same result to \(u^*\) for the second assertion. This proves the inverse homotopy needed for the stable quotient; it does not by itself construct that quotient or its abelian group structure.
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.
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)\).
Block sum and adjoint preserve the generating moves and hence the generated relation. Associativity and commutativity follow from bijections of finite index sets. The empty matrix represents zero. The verified rotation path contracts \(u^*\oplus u\) to an identity matrix, proving the inverse law. Reindexing along a finite enumeration gives a standard finite representative.
For same-size unitaries \(w,u\), there is a norm homotopy
Conjugate \(u\oplus 1\) along the verified path from \(w\oplus w^*\) to \(1\). This supplies the geometric mechanism for stable invariance under unitary changes of coordinates.
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.
Entrywise star homomorphisms are continuous for the matrix \(C^*\)-norm, so they preserve norm homotopies. They commute with coordinate bijections, identity padding, and block sum. The resulting quotient maps satisfy the functorial laws on representatives.
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.
Apply the identity and composition laws to \(e\) and its inverse.
3.6 Nonunital algebras and structural properties
For unital complex \(C^*\)-algebras \(A,B\), the coordinate maps induce
For \(K_0\), the inverse uses the two nonunital coordinate inclusions. A product projection is rectangularly equivalent to the block sum of its coordinate projections: use the row matrix consisting of the two orthogonal coordinate pieces. For \(K_1\), insert identity matrices in the other coordinate. The rotation path gives \([uv]=[u]+[v]\) for same-size unitaries, proving that these constructions are inverse to the coordinate maps.
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.
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\).
The star-algebra isomorphism \(A^+\cong \mathbb C\times A\) sends \((r,a)\) to \((r,r1_A+a)\). Under the verified product decomposition, the scalar quotient induces projection onto \(K_i(\mathbb C)\). Its kernel is the second factor.
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.
Extend the homomorphism to forced unitizations and use naturality of the scalar quotient to restrict the induced maps to their kernels. Identity and composition laws descend from the unital functors. Naturality of evaluation proves compatibility with the unital comparison isomorphisms.
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.
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.
Put \(t=s^*s\) and \(z=t^{-1/2}\) using continuous functional calculus. The intertwining equation implies that \(t\), and hence \(z\), commutes with \(p\). Then \(u=sz\) is unitary, \(up=qu\), and \(v=up\) satisfies \(v^*v=p\), \(vv^*=q\). For the local assertion use \(s(q)=qp+(1-q)(1-p)\). This is continuous in \(q\), satisfies \(s(p)=1\) and \(s(q)p=qs(q)\), and is invertible for \(q\) in a neighborhood of \(p\), since the invertible elements form an open subset of the Banach algebra.
The endpoints of a norm-continuous path of projections are Murray–von Neumann equivalent.
The preceding neighborhood result makes the equivalence-class map locally constant. Its composite with the path is locally constant on the connected interval \([0,1]\), so the endpoint classes coincide.
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 )\).
For a unital homotopy, apply \(H_t\) entrywise to a finite matrix. Entrywise continuity implies continuity in the finite-matrix \(C^*\)-norm. A matrix projection therefore gives a norm path of projections, whose endpoints are equivalent by the preceding result. Equality on projection classes gives equality on \(V(A)\) and, by the Grothendieck universal property, on \(K_0(A)\). A matrix unitary gives a norm path of unitaries, so the endpoint classes agree in the stable quotient \(K_1(B)\). For a possibly nonunital homotopy, unitalize it and apply these two unital results. Restrict equality of the induced maps to the scalar kernels.
The six-term exact sequence and Bott periodicity require separate future nodes and proofs. They are not consequences of the formalized foundations merely by being part of the usual theory.
3.7 The analytic target
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 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 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.
Apply the verified isomorphism-invariance constructions to the previously verified star-algebra equivalence \(e_\Gamma \), choosing the canonical spectral order on both algebras. The entrywise and projection-class formulas specialize the general formulas. Naturality gives the displayed commuting equation, and extensionality on projection classes proves uniqueness. This identifies two models of the analytic target; it does not compute that target or construct the Baum–Connes assembly map.
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.