SymbolLengthMilnorKTheory.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

10 declarations, 7 contain sorry, 0 declared as axioms

The symbol length of $K^M_n(\mathbb{C}(x_1, \dots, x_m))/p$

For a field $F$ and $\ell \ge 1$, the Milnor K-group $K^M_n(F)/\ell$ is generated by the symbols $\{a_1, \dots, a_n\}$ with $a_i \in F^\times$, and the symbol length of a class is the least number of symbols in a decomposition of the class as a sum of symbols. The symbol length of $K^M_n(F)/\ell$ is the supremum of the symbol lengths of its classes. When $\ell$ is invertible in $F$, the norm residue isomorphism theorem (the Bloch–Kato conjecture, [Voevodsky2011]) gives $K^M_n(F)/\ell \cong H^n(F, \mu_\ell^{\otimes n})$, so this is also the symbol length of Galois cohomology.

The symbol length problem asks, for a given field $F$ and integers $n$ and $\ell$, for a $k$ such that the symbol length of every class in $K^M_n(F)/\ell$ is at most $k$, for example in terms of a dimension of the field. That a class is a sum of some number of symbols is part of the presentation of $K^M_n(F)$ recalled above, so the content lies entirely in the bound. In degree $2$, over a field containing a primitive $\ell$-th root of unity, Merkurjev and Suslin's theorem [MerkurjevSuslin1983] that the norm residue map is an isomorphism identifies $K^M_2(F)/\ell$ with the $\ell$-torsion of the Brauer group and symbols with symbol algebras of degree $\ell$; that is the form in which the question is usually studied, namely how many symbol algebras are needed to represent a central simple algebra of exponent $\ell$. Becher and Hoffmann [BecherHoffmann2004] named the invariant $\lambda_p$ in that degree and asked it for exactly the fields considered below (their Question 4.6). The general form stated here is Problem 2.1.3.12 of Krashen's PCMI notes; Krashen notes there that over complex function fields in at least three variables no bound is known beyond Matzri's in degree $2$ and the case of $\ell$ a power of $2$, which comes from the theory of quadratic forms, and that very little is known in degree $3$ and higher [Krashen2024, §2.1.3.4].

This file states the problem for the rational function fields $\mathbb{C}(x_1, \dots, x_m)$ and a prime $\ell = p$: determine the symbol length of $K^M_n(\mathbb{C}(x_1, \dots, x_m))/p$ as a function of $m$, $n$ and $p$, where the symbol length is infinite if there is no bound.

What is known:

in degree $0$ every symbol is the empty product $1$, so $K^M_0(F)/p = \mathbb{Z}/p$ has symbol length $p - 1$ for every field $F$;
in degree $1$ every class of $K^M_1(F)/p = F^\times/(F^\times)^p$ is a single symbol, so the symbol length is at most $1$;
$\mathbb{C}(x_1, \dots, x_m)$ has cohomological dimension $m$ [Serre1997, Ch. II, §4.2], so $K^M_n(\mathbb{C}(x_1, \dots, x_m))/p = 0$ for $n > m$ and the symbol length is $0$;
$\mathbb{C}(x_1, \dots, x_m)$ is a $C_m$ field (Tsen–Lang, [Lang1952]), so by Matzri's theorem [Matzri2016, Theorem 8.2] every class in $K^M_2(\mathbb{C}(x_1, \dots, x_m))/p^t$ is a sum of at most $t(p^{m-1} - 1)$ symbols when $m \ge 1$;
in degree $2$ a tensor product of $m - 1$ symbol algebras of degree $p$ over $\mathbb{C}(x_1, \dots, x_m)$ can be a division algebra, so the symbol length is at least $m - 1$ for $m \ge 1$ [BecherHoffmann2004, Proposition 4.5], by an argument going back to Nakayama.

In degree $2$, Becher and Hoffmann ask whether that lower bound is the answer, that is whether the symbol length is exactly $m - 1$ [BecherHoffmann2004, Question 4.6]. For $m = n = 2$, the smallest case not settled above, this asks whether every class of $K^M_2(\mathbb{C}(x_1, x_2))/p$ is a single symbol; they call it "a striking open question" and note that it holds for $p \le 3$ by a theorem of Artin [BecherHoffmann2004, Introduction]. Since $m - 1$ does not involve $p$, their question is an instance of the expectation recorded in [Krashen2024, §2.1.3.4] that a bound can be taken independent of $\ell$. See also the survey [Krashen2016].

The definitions MilnorK, MilnorK.symbol, MilnorK.grade and MilnorK.symbolLengthBounds are in FormalConjecturesForMathlib/FieldTheory/MilnorKTheory.lean.

References:

[Krashen2024] D. Krashen, PCMI Summer School (not quite) notes, notes for the minicourse Field arithmetic and the complexity of algebraic objects, PCMI Graduate Summer School on Motivic Homotopy Theory, 2024, draft of 24 July 2024, pdf.
[BecherHoffmann2004] K. J. Becher and D. W. Hoffmann, Symbol lengths in Milnor $K$-theory, Homology Homotopy Appl. 6 (2004), no. 1, 17–31, doi:10.4310/HHA.2004.v6.n1.a3.
[MerkurjevSuslin1983] A. S. Merkurjev and A. A. Suslin, K-cohomology of Severi–Brauer varieties and the norm residue homomorphism, Izv. Akad. Nauk SSSR Ser. Mat. 46 (1982), 1011–1046; English translation Math. USSR-Izv. 21 (1983), no. 2, 307–340, doi:10.1070/IM1983v021n02ABEH001793.
[Krashen2016] D. Krashen, Period and index, symbol lengths, and generic splittings in Galois cohomology, Bull. London Math. Soc. 48 (2016), 985–1000, doi:10.1112/blms/bdw060.
[Matzri2016] E. Matzri, Symbol length in the Brauer group of a field, Trans. Amer. Math. Soc. 368 (2016), 413–427, doi:10.1090/tran/6326, arXiv:1402.0332.
[Lang1952] S. Lang, On quasi algebraic closure, Ann. of Math. (2) 55 (1952), 373–390, doi:10.2307/1969785.
[Serre1997] J.-P. Serre, Galois cohomology, Springer Monographs in Mathematics, Springer, 1997, doi:10.1007/978-3-642-59141-9.
[Voevodsky2011] V. Voevodsky, On motivic cohomology with Z/l-coefficients, Ann. of Math. (2) 174 (2011), 401–438, doi:10.4007/annals.2011.174.1.11.

Imports (1)

FormalConjecturesUtil

theorem SymbolLengthMilnorKTheory.symbol_length_problem Documented declaration: symbol_length_problem sorry line 120 source
Source documentation
The symbol length problem for complex rational function fields [Krashen2024, Problem 2.1.3.12 and §2.1.3.4]: determine, as a function of $m$, $n$ and the prime $p$, the symbol length of $K^M_n(\mathbb{C}(x_1, \dots, x_m))/p$, that is the least $k$ such that every class is a sum of at most $k$ symbols, or $\infty$ if there is no such $k$. The answer sl m n p : ℕ∞ is characterised by: k is such a bound if and only if sl m n p ≤ k.

depends on sorry what this means
Statement uses: Nat, ENat, sorryAx, Bool.false, Nat.Prime, Iff, Membership.mem, Set, MilnorK.symbolLengthBounds, MvRatFunc, Fin, Complex, MvPolynomial, Finsupp, LE.le
Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
43 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem symbol_length_problem :
    let sl : ℕ → ℕ → ℕ → ℕ∞ := answer(sorry)
…
```
theorem SymbolLengthMilnorKTheory.symbol_length_problem.variants.bounded Documented declaration: bounded sorry line 132 source
Source documentation
The symbol length problem in the form of [Krashen2024, Problem 2.1.3.12]: is there, for every $m$, $n$ and prime $p$, a bound $k$ such that every class in $K^M_n(\mathbb{C}(x_1, \dots, x_m))/p$ is a sum of at most $k$ symbols?

depends on sorry what this means
Statement uses: Iff, True, Nat, Nat.Prime, Set.Nonempty, MilnorK.symbolLengthBounds, MvRatFunc, Fin, Complex, MvPolynomial, Finsupp
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
35 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem symbol_length_problem.variants.bounded :
    answer(sorry) ↔ ∀ m n p : ℕ, p.Prime →
      (symbolLengthBounds (MvRatFunc (Fin m) ℂ) p n).Nonempty := by
…
```
Mentions: MvRatFunc
theorem SymbolLengthMilnorKTheory.symbol_length_problem.variants.uniform Documented declaration: uniform sorry line 145 source
Source documentation
The expectation recorded in [Krashen2024, §2.1.3.4] that the bound can be taken independent of the prime: is there, for every $m$ and every $n \ge 1$, a $k$ such that every class in $K^M_n(\mathbb{C}(x_1, \dots, x_m))/p$ is a sum of at most $k$ symbols for every prime $p$? Degree $0$ is excluded because $K^M_0(F)/p = \mathbb{Z}/p$ has symbol length $p - 1$ (symbol_length_problem.variants.degree_zero), which is not bounded independently of $p$.

depends on sorry what this means
Statement uses: Iff, True, Nat, LT.lt, OfNat.ofNat, Exists, Nat.Prime, Membership.mem, Set, MilnorK.symbolLengthBounds, MvRatFunc, Fin, Complex, MvPolynomial, Finsupp
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
40 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem symbol_length_problem.variants.uniform :
    answer(sorry) ↔ ∀ m n : ℕ, 0 < n → ∃ k : ℕ, ∀ p : ℕ, p.Prime →
      k ∈ symbolLengthBounds (MvRatFunc (Fin m) ℂ) p n := by
…
```
Mentions: MvRatFunc
theorem SymbolLengthMilnorKTheory.symbol_length_problem.variants.degree_zero Documented declaration: degree_zero line 155 source
Source documentation
The degree-$0$ case of symbol_length_problem: $K^M_0(\mathbb{C}(x_1, \dots, x_m))/p = \mathbb{Z}/p$ has symbol length $p - 1$, since every symbol of degree $0$ is the empty product $1$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.Prime, IsLeast, MilnorK.symbolLengthBounds, MvRatFunc, Fin, Complex, MvPolynomial, Finsupp, OfNat.ofNat, HSub.hSub
Proof uses: MilnorK.isLeast_symbolLengthBounds_zero, Nat.Prime.pos
38 instances, coercions and auxiliary constants left out.
```
theorem symbol_length_problem.variants.degree_zero (m p : ℕ) (hp : p.Prime) :
    IsLeast (symbolLengthBounds (MvRatFunc (Fin m) ℂ) p 0) (p - 1) :=
…
```
Mentions: MvRatFunc
theorem SymbolLengthMilnorKTheory.symbol_length_problem.variants.degree_one Documented declaration: degree_one line 165 source
Source documentation
The degree-$1$ case of symbol_length_problem: every class of $K^M_1(\mathbb{C}(x_1, \dots, x_m))/p = F^\times/(F^\times)^p$ is a single symbol, so the symbol length in degree $1$ is at most $1$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Membership.mem, Set, MilnorK.symbolLengthBounds, MvRatFunc, Fin, Complex, MvPolynomial, Finsupp, OfNat.ofNat
Proof uses: MilnorK.one_mem_symbolLengthBounds_one
36 instances, coercions and auxiliary constants left out.
```
theorem symbol_length_problem.variants.degree_one (m p : ℕ) :
    1 ∈ symbolLengthBounds (MvRatFunc (Fin m) ℂ) p 1 :=
…
```
Mentions: MvRatFunc
theorem SymbolLengthMilnorKTheory.symbol_length_problem.variants.degree_two Documented declaration: degree_two sorry line 175 source
Source documentation
Matzri's theorem [Matzri2016, Theorem 8.2] for $\mathbb{C}(x_1, \dots, x_m)$, which is a $C_m$ field by Tsen–Lang [Lang1952]: for $m \ge 1$, every class in $K^M_2(\mathbb{C}(x_1, \dots, x_m))/p^t$ is a sum of at most $t(p^{m-1} - 1)$ symbols.

depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Nat.Prime, Membership.mem, Set, MilnorK.symbolLengthBounds, MvRatFunc, Fin, Complex, MvPolynomial, Finsupp, HPow.hPow, HMul.hMul, HSub.hSub
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
56 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem symbol_length_problem.variants.degree_two (m : ℕ) (hm : 1 ≤ m) (p t : ℕ)
    (hp : p.Prime) :
    t * (p ^ (m - 1) - 1) ∈ symbolLengthBounds (MvRatFunc (Fin m) ℂ) (p ^ t) 2 := by
…
```
Mentions: MvRatFunc
theorem SymbolLengthMilnorKTheory.symbol_length_problem.variants.degree_two_ge The matching lower bound in degree sorry line 188 source
Source documentation
The matching lower bound in degree $2$ [BecherHoffmann2004, Proposition 4.5], by an argument going back to Nakayama: for distinct monic irreducibles $f_1, \dots, f_{m-1}$ in $\mathbb{C}[x_1]$ the tensor product of the symbol algebras $(f_i, x_{i+1})_p$ is a division algebra over $\mathbb{C}(x_1, \dots, x_m)$, so no $k < m - 1$ bounds the symbol length of $K^M_2(\mathbb{C}(x_1, \dots, x_m))/p$.

depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, Nat.Prime, Membership.mem, Set, MilnorK.symbolLengthBounds, MvRatFunc, Fin, Complex, MvPolynomial, Finsupp, HSub.hSub
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
44 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem symbol_length_problem.variants.degree_two_ge (m : ℕ) (hm : 1 ≤ m) (p : ℕ)
    (hp : p.Prime) :
    ∀ k ∈ symbolLengthBounds (MvRatFunc (Fin m) ℂ) p 2, m - 1 ≤ k := by
…
```
Mentions: MvRatFunc
theorem SymbolLengthMilnorKTheory.symbol_length_problem.variants.degree_two_isLeast Becher and Hoffmann's question [BecherHoffmann2004, Question 4.6]: is the symbol length of $K^M_2(\mathbb{C}(x_1, \dots, x_m))/p$ exactly $m - 1$? sorry line 204 source
Source documentation
Becher and Hoffmann's question [BecherHoffmann2004, Question 4.6]: is the symbol length of $K^M_2(\mathbb{C}(x_1, \dots, x_m))/p$ exactly $m - 1$? Their Proposition 4.5 gives the lower bound (symbol_length_problem.variants.degree_two_ge), and Matzri's theorem the much weaker upper bound $p^{m-1} - 1$ (symbol_length_problem.variants.degree_two). For $m \le 1$ the group vanishes and the answer is $0$; for $m = 2$ the question is whether every class is a single symbol, which holds for $p \le 3$ by a theorem of Artin and is open for $p \ge 5$. Since $m - 1$ does not involve $p$, an affirmative answer would settle symbol_length_problem.variants.uniform in degree $2$.

depends on sorry what this means
Statement uses: Iff, True, Nat, LE.le, OfNat.ofNat, Nat.Prime, IsLeast, MilnorK.symbolLengthBounds, MvRatFunc, Fin, Complex, MvPolynomial, Finsupp, HSub.hSub
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
42 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem symbol_length_problem.variants.degree_two_isLeast :
    answer(sorry) ↔ ∀ m p : ℕ, 1 ≤ m → p.Prime →
      IsLeast (symbolLengthBounds (MvRatFunc (Fin m) ℂ) p 2) (m - 1) := by
…
```
Mentions: MvRatFunc
theorem SymbolLengthMilnorKTheory.symbol_length_problem.variants.zero_mem_of_lt $K^M_n(\mathbb{C}(x_1, \dots, x_m))/p = 0$ for $n > m$: the field has cohomological dimension $m$ [Serre1997, Ch sorry line 215 source
Source documentation
$K^M_n(\mathbb{C}(x_1, \dots, x_m))/p = 0$ for $n > m$: the field has cohomological dimension $m$ [Serre1997, Ch. II, §4.2], so $H^n(\mathbb{C}(x_1, \dots, x_m), \mu_p^{\otimes n}) = 0$, and $K^M_n/p \cong H^n(-, \mu_p^{\otimes n})$ by the norm residue isomorphism theorem [Voevodsky2011].

depends on sorry what this means
Statement uses: Nat, LT.lt, Nat.Prime, Membership.mem, Set, MilnorK.symbolLengthBounds, MvRatFunc, Fin, Complex, MvPolynomial, Finsupp, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
40 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem symbol_length_problem.variants.zero_mem_of_lt (m n p : ℕ) (hmn : m < n) (hp : p.Prime) :
    0 ∈ symbolLengthBounds (MvRatFunc (Fin m) ℂ) p n := by
…
```
Mentions: MvRatFunc
theorem SymbolLengthMilnorKTheory.symbol_length_problem.variants.isAlgClosed Documented declaration: isAlgClosed line 227 source
Source documentation
$K^M_n(F)/\ell = 0$ for an algebraically closed field $F$ and $n, \ell \ge 1$, since every unit is an $\ell$-th power: every symbol $\{a_1, \dots, a_n\}$ with $a_1 = b^\ell$ equals $\ell \{b, a_2, \dots, a_n\} = 0$. This generalizes the case $m = 0$ of symbol_length_problem.variants.zero_mem_of_lt, which concerns a prime $\ell$ and the field $\mathbb{C}(x_1, \dots, x_0) \cong \mathbb{C}$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, IsAlgClosed, Nat, LT.lt, OfNat.ofNat, Membership.mem, Set, MilnorK.symbolLengthBounds
Proof uses: Eq.mpr, Eq, AddSubgroup, MilnorK, TensorAlgebra, Int, Additive, Units, MilnorK.Rel, MilnorK.grade, Bot.bot, id, congrArg, propext, MilnorK.zero_mem_symbolLengthBounds_iff, MilnorK.grade_eq_bot_of_forall_exists_pow_eq, HPow.hPow, Exists, IsAlgClosed.exists_pow_nat_eq, Ne and 13 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem symbol_length_problem.variants.isAlgClosed (F : Type*) [Field F] [IsAlgClosed F]
    (n ℓ : ℕ) (hn : 0 < n) (hℓ : 0 < ℓ) : 0 ∈ symbolLengthBounds F ℓ n := by
…
```