Is a smooth affine group scheme over the dual numbers linear? (MathOverflow 22078)

### What is the conjecture

Every affine group scheme of finite type over a field $k$ is a closed subgroup scheme of some
$\mathrm{GL}_n$. Brian Conrad asked whether this stays true over the ring of dual numbers
$k[\epsilon] = k[x]/(x^2)$, or over any artinian local ring, even for smooth group schemes. The
proof over a field produces a finite-dimensional subcomodule of the coordinate ring that generates
it as an algebra, and uses that a finitely generated submodule of a vector space is free; over
$k[\epsilon]$ a finitely generated submodule need not be free.

**The answer is no in characteristic zero.** Push out the Heisenberg central extension
$1 \to \mathbb{G}_a \to H \to \mathbb{G}_a^2 \to 1$ over $k[\epsilon]$ along the homomorphism
$\mathbb{G}_a \to \mathbb{G}_m$, $x \mapsto 1 + \epsilon x$. The result is a smooth affine central
extension $1 \to \mathbb{G}_m \to G \to \mathbb{G}_a^2 \to 1$ with no faithful representation on a
finite free $k[\epsilon]$-module. Any such representation $M$ is the direct sum of the weight
spaces $M_i$ of the central $\mathbb{G}_m$, and each $M_i$ is a subrepresentation. The element
$1 + \epsilon$ of $\mathbb{G}_m(k[\epsilon])$ is a commutator in $G(k[\epsilon])$, so it acts on
$M_i$ with determinant $1$; it acts by the scalar $1 + i\epsilon$, so that determinant is
$1 + i \operatorname{rank}(M_i)\epsilon$, forcing $i \operatorname{rank}(M_i) = 0$ in $k$. In
characteristic zero this kills every weight $i \neq 0$, so $\mathbb{G}_m$ acts trivially and no
representation is faithful.

**Characteristic $p$ is open.** There the ranks may be multiples of $p$ and the determinant
argument gives nothing.

Known affirmative cases:

* over a field, for every affine group scheme of finite type (smoothness is not needed);
* over a Dedekind domain, for flat affine group schemes of finite type (Bruhat-Tits II, 1.4.5).
That gives a closed immersion into $\mathrm{GL}(M)$ for $M$ finitely generated projective;
choosing $N$ with $M \oplus N$ finite free embeds it into a $\mathrm{GL}_n$.

**Sources:**
- MathOverflow 22078, *Smooth linear algebraic groups over the dual numbers*, asked by Brian
Conrad, https://mathoverflow.net/questions/22078 ; the characteristic zero counterexample is the
answer at https://mathoverflow.net/a/513098
- B. Conrad, *Reductive group schemes*, Rem. 2.3.3, which states the question and refers to
SGA 3, Exp. VI$_B$, 13.2 and 13.5, and Exp. XI, 4.3,
http://math.stanford.edu/~conrad/papers/luminysga3.pdf
- F. Bruhat and J. Tits, *Groupes réductifs sur un corps local II*, Publ. Math. IHÉS 60 (1984),
1.4.5, http://www.numdam.org/item/PMIHES_1984__60__5_0/
- G. Battiston and M. Romagny, *Representations of affine group schemes over general rings*,
https://arxiv.org/abs/1807.01009 , which claimed an affirmative answer over an artinian base and
was withdrawn because of an error in its Thm. 4.1

### Prerequisites needed

Everything needed is in Mathlib: `HopfAlgebra` with `Coalgebra.comul` and `Coalgebra.counit`,
`DualNumber`, `Algebra.Smooth`, `Algebra.FiniteType`, `Module.Flat` and `IsDedekindDomain`.
Mathlib has no comodules, but a homomorphism `Spec A → GLₙ` is the same as a matrix `a` over `A`
with `Δ aᵢⱼ = ∑ₖ aᵢₖ ⊗ aₖⱼ` and `ε aᵢⱼ = δᵢⱼ`, and by Bruhat-Tits 1.4.5 it is a closed immersion
exactly when the entries generate `A` as an `R`-algebra, so no comodule API is required.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-14
* ams-16
* ams-20

### Choose either option
- [x] I plan on adding this conjecture to the repository

No target file or test is named. Start by reviewing the existing HopfAlgebra, DualNumber, Algebra.Smooth, Algebra.FiniteType, Module.Flat, and IsDedekindDomain APIs, then formalize the stated conjecture and ensure the resulting Lean declarations compile.

Written by the indexing model from the issue text.