pith. sign in
theorem

D3_admits_circle_linking

proved
show as:
module
IndisputableMonolith.Foundation.AlexanderDuality
domain
Foundation
line
154 · github
papers citing
52 papers (below)

plain-language theorem explainer

The theorem establishes that the 3-sphere admits nontrivial linking of embedded circles, detected by the nontriviality of the first reduced homology of the complement. Algebraic topologists studying embeddings and duality would cite this when fixing spatial dimension via linking invariants. The proof is a one-line wrapper that applies the right-to-left direction of the biconditional alexander_duality_circle_linking at D=3 together with reflexivity.

Claim. The 3-sphere $S^3$ admits nontrivial linking of disjoint embedded circles, i.e., the reduced cohomology group $H^{1}(S^1;Z)$ is nontrivial under the Alexander duality isomorphism $H_1(S^3setminus S^1;Z)cong H^{D-2}(S^1;Z)$ evaluated at $D=3$.

background

The AlexanderDuality module replaces the earlier tautological definition of SphereAdmitsCircleLinking D with a predicate based on reduced cohomology: SphereAdmitsCircleLinking D holds precisely when CircleReducedCohomologyNontrivial((D:Z)-2). By the module's statement of Hatcher Theorem 3.44, this predicate encodes that the complement S^D minus an embedded circle has nontrivial first homology if and only if D=3. The upstream theorem alexander_duality_circle_linking supplies the full biconditional SphereAdmitsCircleLinking D iff D=3, obtained by unfolding the definition and applying the circle cohomology computation circle_reduced_cohomology_iff.

proof idea

One-line wrapper that applies the right-to-left implication of alexander_duality_circle_linking specialized to D=3, followed by reflexivity on the equality 3=3.

why it matters

This supplies the forward direction of the linking characterization of D=3, completing the topological replacement for the prior definitional tautology in the module. It directly supports the framework landmark T8 that selects three spatial dimensions by giving a cohomological reason why nontrivial circle linking occurs precisely in D=3 and not in other dimensions. The parent result is the biconditional alexander_duality_circle_linking; the declaration closes the historical axiom decomposition noted in the module documentation.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.

papers checked against this theorem (showing 30 of 52)

The full set is indexed internally; the public theorem page shows a capped sample so high-use declarations do not become many-thousand-row pages.