DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-generatedjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Reduced and relative real K-theory and compact support

Definition

For a based compact Hausdorff space $(Y, *)$ , set ${\tilde{K O}}^{0} (Y) = \ker (K O^{0} (Y) \to K O^{0} (*))$ . For a compact pair with closed subspace $A \subset X$ , set $K O^{0} (X, A) = {\tilde{K O}}^{0} (X / A)$ , where all of $A$ is collapsed to one basepoint. If $A = \emptyset$ , use $X_{+} = X ⨿ {*}$ instead. Set $K O^{- j} (X, A) = {\tilde{K O}}^{0} (S^{j} \land (X / A))$ for $j \geq 0$ , and $K O^{- j} (X) = K O^{- j} (X, \emptyset)$ . The same conventions define reduced, relative and negative-degree $K S p$ .

For a finite-rank metric real bundle $V \to X$ over compact $X$ , write $Th (V) = D (V) / S (V)$ and $K O_{c}^{- j} (V) = {\tilde{K O}}^{0} (S^{j} \land Th (V))$ . At rank zero use $Th (0) = X_{+}$ . These definitions do not assert any periodicity or an isomorphism between successive degrees.

Depends on

Used by

Dependency tree · two levels

4 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

M. F. Atiyah, K-Theory, §§1.3–1.4 and 2.4 (complex source; real arguments supplied locally) (standard reference, not scraped)