LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-12

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.

Filtered freeness lifts from associated graded algebras

Statement

Let $A$ be a unital algebra over a field, with increasing exhaustive vector-space filtrations $F_{n} A$ for integers $n \geq 0$ , $F_{- 1} A = 0$ , $1 \in F_{0} A$ , and $F_{m} A F_{n} A \subseteq F_{m + n} A$ . Let $R \subseteq Z (A)$ be a unital subalgebra with an increasing exhaustive nonnegative multiplicative filtration, $F_{- 1} R = 0$ , $1 \in F_{0} R$ , and $F_{n} R \subseteq F_{n} A$ . Inclusion induces a graded algebra map $gr R \to gr A$ and hence the module structure used below; here $gr A = ⨁_{n \geq 0} F_{n} A / F_{n - 1} A$ .

Suppose a specified family $(b_{j})_{j \in J}$ is a homogeneous free basis of $gr A$ over $gr R$ , with degrees $d_{j} \geq 0$ . Here free basis means that every element has a unique finite expansion in the $b_{j}$ . Suppose specified $a_{j} \in F_{d_{j}} A$ have images $b_{j}$ in degree $d_{j}$ . Then $(a_{j})_{j \in J}$ is both a left and a right $R$ -basis of $A$ .

Proof

Given: The filtrations, graded basis and lifts in the statement. For negative $n$ put $F_{n} R = 0$ . Only finite sums occur in a direct sum; no family of additional lifts is chosen simultaneously.

1.1

Define $D = ⨁_{j \in J} R u_{j}$ , with $F_{n} D = ⨁_{j} (F_{n - d_{j}} R) u_{j}$ , and $ϕ : D \to A$ by $ϕ (\sum_{j} r_{j} u_{j}) = \sum_{j} r_{j} a_{j}$ . Finite support makes the formula meaningful. Multiplicativity of the filtration makes $ϕ$ filtered, and its degree- $n$ map sends the class of $r_{j} u_{j}$ to the product of the degree- $(n - d_{j})$ class of $r_{j}$ and $b_{j}$ . The given graded-basis property therefore makes $gr ϕ$ an isomorphism in every degree.

givenconstruct

2.1

We prove that every $x \in F_{n} A$ belongs to $ϕ (F_{n} D)$ by induction on $n \geq - 1$ . For $n = - 1$ , both spaces are zero. For $n \geq 0$ , surjectivity of the degree- $n$ map in 1.1 gives a finite homogeneous expansion of $x + F_{n - 1} A$ . Choose representatives in $F_{n - d_{j}} R$ for its finitely many nonzero coefficients. They define $y \in F_{n} D$ with $x - ϕ (y) \in F_{n - 1} A$ . The induction hypothesis gives $z \in F_{n - 1} D$ with $ϕ (z) = x - ϕ (y)$ , whence $x = ϕ (y + z)$ . Exhaustivity now proves surjectivity of $ϕ$ .

step 1.1algebra

2.2

If $0 \neq y = \sum_{j} r_{j} u_{j} \in D$ , each nonzero coefficient has a least filtration degree $e_{j}$ , since its filtration is exhaustive and indexed by the nonnegative integers. Set $n = \max_{r_{j} \neq 0} (e_{j} + d_{j})$ , a maximum of a nonempty finite set. At least one coefficient has nonzero image in its degree $e_{j}$ quotient, so $y + F_{n - 1} D \neq 0$ . Injectivity of $gr ϕ$ in 1.1 gives $ϕ (y) + F_{n - 1} A \neq 0$ . Thus $ϕ (y) \neq 0$ , proving injectivity.

step 1.1algebra

3.1

Hence $ϕ$ is a left $R$ -module isomorphism. As $R \subseteq Z (A)$ , $r_{j} a_{j} = a_{j} r_{j}$ for each coefficient, so the same finite expressions give unique right expansions. If $J$ is empty, the degreewise argument in 2.1 forces $A = 0$ ; the empty basis assertion remains valid whenever the zero algebra is admitted. Degree zero, a singleton basis, and the zero element require no change in the argument. All choices in 2.1 are finite choices for a single induction step; the proof asserts existence separately for each $x$ , and uses no axiom of choice. This establishes both bases. [step 2.1, step 2.2, given] QED

Used by

Nothing in the library uses this result yet.

Dependency tree · 0 levels

Nothing. This result depends on no other item in the library.

Sources

Etingof, Representations of Lie Groups, Theorem 13.1, filtered lifting argument (standard reference, not scraped)