§5 · Agent 5 · Audit: transfer, hypotheses · 2026-10-18T03:59:53Z

Audit 5.1 · Audit of A4-2: truncated rings and finite determinacy

proved audit: correct

Second audit: correct. I re-derived Lemma 4.2 (a)-(e): Teichmueller expansions give the Lambda-algebra isomorphism O'/varpi'^m = F_q[t]/t^m for e >= m, Hensel holds for smooth Y, Cartan and Iwasawa detection follow from the lowest-weight coefficient and the primitivity of rows of GL_n(O), {c dominant: c <= d} is finite because fundamental weights are non-negative combinations of simple roots, and D = N+c+1 works. I checked zhu-satake-v2: Lecture II assumes k algebraically closed, so Audit 5.1's remark on Zhu (2.1.2) is accurate and Bruhat-Tits/Iwahori-Matsumoto is the right citation for F_q((t)). The verdict 'holds' is right and nothing was missed.

Every part of the truncation lemma Lemma 4.2 is re-derived; it holds as stated, with a determinacy bound \(D\) that depends only on the formal shape of the conditions, never on the test field.

Audit 5.1.

Outcome: holds. Parts (a)–(e) of Lemma 4.2 are correct. In (e), for a condition \(\operatorname{val}M(z)\ge c\) or \(=c\) whose entries have at most \(\varpi^{-N}\) as denominator, \(D=N+c+1\) works, and \(N,c\) are read off the expression, so \(D\) is independent of \(E\). The only citation to adjust: Zhu's (2.1.2) is stated for \(k(\!(t)\!)\) with \(k\) algebraically closed; for \(\mathbb F_q(\!(t)\!)\) the Cartan and Iwasawa decompositions of a split group come from Bruhat–Tits I (or Iwahori–Matsumoto), which Lemma 4.2 also cites.

  1. (a) Close rings. Let \(F'\supseteq\mathbb Q_q\) be totally ramified of degree \(e\ge m\). Then \(p\in\varpi'^e\mathcal O'\subseteq\varpi'^m\mathcal O'\), so \(\Lambda\to R:=\mathcal O'/\varpi'^m\) factors through \(\Lambda/p=\mathbb F_q\) (checklist item 2: \(R\) has characteristic \(p\) although \(F'\) has characteristic \(0\)). The Teichmüller representatives lie in \(\Lambda\subseteq\mathcal O'\), so every element of \(\mathcal O'\) is \(\sum_i[a_i]\varpi'^i\). Hence \(\mathbb F_q[T]\to R\), \(T\mapsto\bar\varpi'\), is onto with \(T^m\mapsto0\). Both sides have \(\mathbb F_q\)-dimension \(m\), so it is an isomorphism of \(\Lambda\)-algebras sending \(\bar t\mapsto\bar\varpi'\).
  2. (b) Hensel's lemma for smooth affine schemes over a complete local ring (EGA IV\(_4\) 18.5.17). \(G\), \(H\), \(X\) are smooth over \(\Lambda\) (Proposition 3.2 works over any complete DVR with \(2\) invertible).
  3. (c) Cartan detection. \(\rho_i(K)\subseteq\mathrm{GL}_n(\mathcal O)\), and multiplying by matrices of \(\mathrm{GL}_n(\mathcal O)\) on either side preserves \(\operatorname{val}\). For dominant \(\nu\), \(\min_\chi\langle\nu,\chi\rangle=\langle\nu,w_0\omega_i\rangle\) over the weights \(\chi\) of the Weyl module, since \(\chi-w_0\omega_i\) is a sum of positive roots. The vectors \(w_0\omega_i=-\omega_{i^*}\) span \(X^*(T)_{\mathbb Q}\), so the six values determine \(\nu\). From \(\operatorname{val}(AB)\ge\operatorname{val}A+\operatorname{val}B\): \(\langle a+b-c,\omega_{i^*}\rangle\ge0\) for all \(i\). For dominant \(c\), \(0\le\langle c,\omega_j\rangle\le\langle d,\omega_j\rangle\) (fundamental weights are non-negative rational combinations of simple roots), so \(\{c\preceq d\}\) is finite.
  4. (d) Iwasawa detection. For \(u\in U(E)\), \(\rho_i(u)\) adds only strictly higher weight components, so \(\ell_i\rho_i(u)=\ell_i\). Next \(\ell_i\rho_i(t^\nu)=\varpi^{\langle\nu,w_0\omega_i\rangle}\ell_i\), and \(\ell_i\rho_i(k)\) is a row of a matrix in \(\mathrm{GL}_n(\mathcal O)\). The Iwasawa decomposition holds for split groups over every non-archimedean local field.
  5. (e) Determinacy. Write \(\varpi^NM(z)\) with entries in \(\Lambda[\varpi][\text{coordinates}]\). The coordinates of \(\rho_i(z^{-1})\) and \(\rho_i(\theta(z))\) are regular functions on \(G_\Lambda\) (\(\theta\) is defined over \(\mathbb Z\)). So \(z\equiv z'\bmod\varpi^D\) changes \(\varpi^NM\) by an element of \(\varpi^DM_n(\mathcal O)\), and "\(\operatorname{val}=c\)" means "\(\equiv0\bmod\varpi^{N+c}\), \(\not\equiv0\bmod\varpi^{N+c+1}\)". A \(\Lambda\)-algebra isomorphism \(\mathcal O/\varpi^D\cong\mathcal O'/\varpi'^D\) with \(\bar\varpi\mapsto\bar\varpi'\) carries the reduced polynomial conditions to each other, and also carries \(Y(\mathcal O/\varpi^D)\) to \(Y(\mathcal O'/\varpi'^D)\) because \(Y\) is a functor on \(\Lambda\)-algebras. Existential quantifiers over \(Y(\mathcal O)\) descend to \(Y(\mathcal O/\varpi^D)\) by (b).
  6. Checklist. Item 1: the inputs are Hensel and the Cartan and Iwasawa decompositions of split groups, all characteristic-free. Item 2: handled in step 1. Items 5–6 do not arise.

Builds on

  • Lemma 4.2 · Lemma: truncated rings agree and valuation conditions are fixed mod \(\varpi^D\)

Built on by

  • Summary 5.13 · Verdict of audit A5: transfer route A4-2…A4-9 and char-p hypotheses A3-1…A3-10

Sources