LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

Jantzen layer dimensions sum to the Gram determinant valuation

Statement

In the setting of The Jantzen filtration of a lifted cell module ( $R$ a PID, $π$ a prime element, $F = R / π R$ , $M$ free of finite rank with a form whose extension to $K = Frac (R)$ is non-degenerate), let $ν_{π}$ be the $π$ -adic valuation normalised by $ν_{π} (π) = 1$ and let $G \in R ∖ {0}$ be the Gram determinant of the form with respect to any $R$ -basis of $M$ . Then $ν_{π} (G) = \sum_{i > 0} \dim_{F} M_{F} (i),$ where $M_{F} (i)$ are the Jantzen layers of The Jantzen filtration of a lifted cell module; in particular the sum is finite and independent of the chosen basis.

Facts & Assumptions

Given: A PID $R$ with prime element $π$ , residue field $F = R / π R$ , fraction field $K$ , a free $R$ -module $M$ of finite rank $d$ with a symmetric $R$ -bilinear form $⟨, ⟩$ that is non-degenerate over $K$ , and its Jantzen filtration $M (i) \subseteq M$ with layers $M_{F} (i) = (M (i) + π M) / π M$ (The Jantzen filtration of a lifted cell module).

[F1]

(The Jantzen filtration of a lifted cell module) The $M (i)$ , $i \geq 0$ , are submodules with $M (0) = M$ and $M (i + 1) \subseteq M (i)$ , and $M_{F} (i) = 0$ for all sufficiently large $i$ .

[F2]

(Every matrix over a PID has a Smith normal form) There are $R$ -bases $e_{1}, \dots, e_{d}$ of $M$ and $f_{1}, \dots, f_{d}$ of $M$ together with nonzero $r_{1}, \dots, r_{d} \in R$ such that $⟨ e_{i}, f_{j} ⟩ = δ_{i j} r_{i}$ for all $i, j$ ; the $r_{i}$ are the elementary divisors of the Gram matrix.

[F3]

For any $R$ -basis of $M$ with Gram matrix $G$ one has $\det G = r_{1} \dots r_{d}$ up to a unit, so $ν_{π} (G) = \sum_{i} ν_{π} (r_{i})$ , and $ν_{π}$ is normalised by $ν_{π} (π) = 1$ and takes the value $0$ on units.

Proof

technique · direct

1.1givenF1F2

Description of the Jantzen layers: write $x = \sum_{i} a_{i} e_{i}$ in the basis of [F2]. Since $f_{1}, \dots, f_{d}$ is an $R$ -basis of $M$ , the condition $⟨ x, y ⟩ \in π^{k} R$ for all $y \in M$ is equivalent to $⟨ x, f_{j} ⟩ \in π^{k} R$ for all $j$ ; as $⟨ x, f_{j} ⟩ = a_{j} r_{j}$ , this gives $M (k) = {\sum_{i} a_{i} e_{i} : ν_{π} (a_{i} r_{i}) \geq k for all i}$ with the convention $ν_{π} (0) = \infty$ . Reducing modulo $π M$ , whose basis is $π e_{1}, \dots, π e_{d}$ , shows that $M_{F} (k)$ has as an $F$ -basis the images of those $e_{i}$ with $ν_{π} (r_{i}) \geq k$ : if $ν_{π} (r_{i}) \geq k$ then the image of $e_{i}$ lies in $M_{F} (k)$ , while if $ν_{π} (r_{i}) < k$ then every element of $M (k)$ has $e_{i}$ -coefficient divisible by $π$ . Hence $\dim_{F} M_{F} (k) = # {i : ν_{π} (r_{i}) \geq k}$ .

2.1step 1.1F1

Summation: since each $r_{i}$ is nonzero, the sets ${k > 0 : ν_{π} (r_{i}) \geq k}$ are finite of cardinality $ν_{π} (r_{i})$ ; by step 1.1 and [F1], $\sum_{k > 0} \dim_{F} M_{F} (k) = \sum_{k > 0} # {i : ν_{π} (r_{i}) \geq k} = \sum_{i} ν_{π} (r_{i}) .$

3.1step 2.1F3∎

Conclusion: by [F3] the right-hand side is $ν_{π} (G)$ for any Gram matrix $G$ of the form in any $R$ -basis of $M$ ; the left-hand side is defined purely in terms of $M$ and the form, so the identity holds for every basis and the sum is finite and basis-independent.

Depends on

Used by

The q-Schaper virtual radical-layer formula Theorem

Dependency tree · two levels

10 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

Andrew Mathas, Hecke algebras and Schur algebras of the symmetric group, complete prepublication manuscript (1998; expanded published edition: AMS University Lecture Series 15, 1999); complete 79-page manuscript, SHA-256 8cfeb611a95a3ff25cb95ad22bfd3a68475818301c34b04d131a8480a1b997e0 (standard reference, not scraped)