LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generated

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.

Finite direct summands over a formal-series ring are free with rank read from reduction

Statement

Let $k$ be a field and $R : = k ⟦ h ⟧$ . For $n \geq 0$ , let $p : R^{n} \to R^{n}$ be an $R$ -linear map with $p^{2} = p$ , and put $M : = p (R^{n})$ . Then $M$ is free of finite rank equal to $r : = \dim_{k} (M / h M)$ . This includes $M = 0$ and $r = 0$ .

Facts & Assumptions

Given: A field $k$ , the formal power-series ring $R = k ⟦ h ⟧$ , a finite integer $n \geq 0$ , an idempotent $R$ -linear map $p : R^{n} \to R^{n}$ , and $M = p (R^{n})$ .

[F1]

A field has $0 \neq 1$ and every nonzero element has a multiplicative inverse (Field).

[F2]

A free module has a standard basis and every element has a unique finite coordinate expansion (The free module on a set and its standard basis).

[F3]

A series is a coefficient function and products are defined by finite Cauchy convolution (Formal power series over a commutative ring and the coefficient-extraction functional $[x^{n}]$ ).

[F4]

The ring $R$ is a domain, $R / h R ≅ k$ , and $R^{n}$ is complete and separated for the $h$ -adic topology (The one-parameter formal-series ring is complete, separated, and has residue field $k$ ).

Proof

technique · direct

1.1givenF1F2F3F4algebra

Every nonzero power series has a least degree with nonzero coefficient. By [F3], the coefficient of the least-degree term in a product of two nonzero series is the product of their two leading coefficients, which is nonzero by [F1]; hence [F4] confirms that $R$ is a domain. The module $M \subseteq R^{n}$ is therefore torsion-free: if $c \neq 0$ and $c m = 0$ , every coordinate of $m$ is zero. The elements $p (e_{1}), \dots, p (e_{n})$ from the standard basis of [F2] generate $M$ , so $M / h M$ is a finite-dimensional vector space over $k ≅ R / h R$ by [F4].

2.1step 1.1F4chooseconstruct

Choose a basis ${\overset{ˉ}{m}}_{1}, \dots, {\overset{ˉ}{m}}_{r}$ of $M / h M$ and lifts $m_{i} \in M$ . Let $N : = \sum_{i = 1}^{r} R m_{i}$ and $Q : = M / N$ . The quotient $Q$ is finitely generated, and the spanning property modulo $h$ gives $M = N + h M$ , hence $Q = h Q$ .

3.1step 2.1F4givenalgebra

Choose finite generators $q_{1}, \dots, q_{s}$ of $Q$ . From $Q = h Q$ , write $q_{i} = h \sum_{j = 1}^{s} c_{i j} q_{j}$ with $c_{i j} \in R$ . For the column $q = (q_{i})$ this is $(I - h C) q = 0$ . The matrix series $\sum_{t \geq 0} (h C)^{t}$ converges entrywise by [F4] and is a two-sided inverse of $I - h C$ , since the finite partial products leave remainder $(h C)^{t + 1} \in h^{t + 1} M_{s} (R)$ , which tends to zero; separatedness in [F4] makes the limiting products exactly the identity. Therefore every $q_{i} = 0$ , so $Q = 0$ and the lifts $m_{i}$ span $M$ . This also proves $M = 0$ when $r = 0$ .

4.1step 1.1step 3.1F4algebra

If $\sum_{i} a_{i} m_{i} = 0$ for $a_{i} \in R$ , reducing modulo $h$ and using that the ${\overset{ˉ}{m}}_{i}$ are a basis gives $a_{i} \in h R$ for every $i$ . Write $a_{i} = h b_{i}$ and cancel $h$ in $R^{n}$ , which is torsion-free by step 1.1, to get $\sum_{i} b_{i} m_{i} = 0$ . Repeating shows each $a_{i} \in h^{t} R$ for every $t \geq 1$ . A nonzero power series has a finite least degree, so $⋂_{t \geq 1} h^{t} R = 0$ by separatedness [F4], and every $a_{i} = 0$ . Thus the spanning family is linearly independent.

5.1step 3.1step 4.1F2given∎

Steps 3.1 and 4.1 show that $(m_{1}, \dots, m_{r})$ spans $M$ and is linearly independent, hence is an $R$ -basis in the sense of [F2]. Its cardinality is $r = \dim_{k} (M / h M)$ by construction, proving the statement, including the empty basis when $r = 0$ .

Depends on

Used by

Matrix units lift through a finite free split formal deformation Lemma

Dependency tree · two levels

13 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

Pavel Etingof, Structure of Finite Dimensional Algebras, MIT OpenCourseWare 18.712, Chapter 7 (standard reference, not scraped)