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.
The deficiency-one Fox calculus rule for the Alexander invariant
Statement
Assume the Axiom of Choice (The Axiom of Choice) for the library's Alexander module. Let be an oriented link, let be its complement group, and take a deficiency-one presentation (Group presentation by generators and relations, Free group on a set of generators). Let be a homomorphism to a finitely generated free abelian group, with induced ring map (The group ring of finitely supported formal -linear combinations of group elements). Form the evaluated Fox matrix . If is a presentation generator with , delete its column and define The Fox rule identifies this quotient, up to a group-ring unit, with the corresponding specialization of the link's Alexander invariant; admissible deleted columns and presentations give the same invariant up to units. For the natural meridian abelianization , it is the multivariable Alexander polynomial when , and for a knot it is , where is the one-variable Alexander polynomial of The Alexander polynomial from the zeroth elementary ideal. Specializations are asserted only when the displayed denominator remains nonzero. A generator with is not an admissible deleted column; the denominator then vanishes. For several components the equal-variable specialization of the multivariable invariant is distinguished from the library's absolute-homology one-variable polynomial.
Facts & Assumptions
Given: AC, an oriented link , a deficiency-one presentation of its group, a homomorphism to a finitely generated free abelian group , and an admissible deleted generator . AC is inherited from the Alexander module.
Literature input. Morton's standard method, printed pp. 4–5, applies to a presentation of a LINK group: evaluate its Fox derivatives, delete a generator column with , and divide the determinant by . It computes the specialized Alexander invariant; under natural abelianization this is the multivariable polynomial for more than one component and for a knot. Relations written may use derivatives of . This is a literature input, not a local derivation of the Fox theorem (Morton, section 2 and proof of Theorem 1).
The one-variable absolute homology Alexander module and its polynomial are the conventions of The one-variable Alexander module of an oriented link and The Alexander polynomial from the zeroth elementary ideal. For a knot the invariant is the fraction ; the library's one-variable normalization for several components does not identify its polynomial with every specialization of the multivariable polynomial.
The multiplication of a group ring is (The group ring is a unital -algebra with basis , and each is a unit of ). For a basis of the finite-rank free abelian group , identify its elements with integer exponent vectors: the basis elements of are then precisely Laurent monomials, with exponent-addition multiplication. This is a commutative domain: in two nonzero finite sums, the product of the lexicographically largest exponent terms is the unique largest term, with nonzero integer coefficient. Thus evaluated determinants and quotients by nonzero elements lie in its fraction field (The group ring of finitely supported formal -linear combinations of group elements, Group presentation by generators and relations, Free group on a set of generators).
Proof
Application of the source rule. All source hypotheses in [F1] hold for the specified link group and admissible deleted column. Thus the evaluated deleted determinant divided by computes the source invariant. The evaluation takes place in the commutative target of [F3], even though the initial Fox coefficients need not commute.
The codomain and specializations. The denominator is nonzero by hypothesis, so the quotient exists in the fraction field. Under natural meridian abelianization [F1] gives the multivariable polynomial for several components and the rational knot invariant of [F2]. Other homomorphisms substitute meridian images into this rule, provided their denominator stays nonzero; no polynomial divisibility is claimed for the knot fraction. When , one cannot use that column because .
Unit ambiguity. The source's invariance clause gives independence of admissible presentations and columns for the quotient, up to group-ring units, not a claim that the deleted determinants themselves differ by a unit when their denominators differ. In one variable these are the units of the polynomial convention. This proves exactly the asserted Fox computation and its normalization.
Remarks
The axis computation in The Burau determinant formula for a closed braid and its axis uses the axis meridian with its independent variable , hence is an admissible application. The absolute one-variable polynomial is fixed separately by the E0 convention; the multivariable specialization and its extra factor are stated explicitly in that consumer.
Depends on
- The Axiom of Choice
- The Alexander polynomial from the zeroth elementary ideal
- The one-variable Alexander module of an oriented link
- Free group on a set of generators
- Group presentation by generators and relations
- The group ring $R[G]$ of finitely supported formal $R$-linear combinations of group elements
- Finitely presented modules and finitely presented algebras
- The group ring $R[G]$ is a unital $R$-algebra with basis $G$, and each $g\in G$ is a unit of $R[G]$
Used by
Dependency tree · two levels
46 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
- H. R. Morton, The multivariable Alexander polynomial for a closed braid, arXiv:math/9803138, section 2 (the standard Fox-calculus method, printed pp. 4-5) and the proof of Theorem 1 (printed pp. 5-6) (standard reference, not scraped)
- Anthony Conway, Burau maps and twisted Alexander polynomials, arXiv:1510.06678, section 3.3 and Theorem 3.15 with its proof (printed pp. 16-17) (standard reference, not scraped)
- R. H. Crowell and R. H. Fox, Introduction to Knot Theory, Ginn and Co. (1963), chapters VII-VIII (free differential calculus and the Alexander matrix) (standard reference, not scraped)