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