ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge 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.

Upper unitriangular groups are unipotent, and the additive group is U_2

Example

Let $k$ be a field. The group scheme $U_{n}$ of upper unitriangular matrices (The upper unitriangular group scheme U_n and its coordinate ring) is a smooth connected unipotent algebraic group over $k$ : it is a closed subgroup of $U_{n}$ trivially, its coordinate ring $k [X_{i j} ∣ i < j]$ is coconnected by the weight filtration, and its central series has additive quotients (The central series of U_n with additive quotients).

The map $a \mapsto (\begin{array}{cc} 1 & a \\ 0 & 1 \end{array})$ is an isomorphism $G_{a} \to U_{2}$ , so $G_{a}$ is unipotent. In characteristic $p$ , the subgroup schemes $α_{p} = Spec k [ε] / (ε^{p})$ and $(Z / p Z)_{k}$ are unipotent closed subgroups of $G_{a}$ that are not smooth, respectively not connected, showing that unipotent groups need be neither smooth nor connected.

Facts & Assumptions

Given: A field $k$ and an integer $n \geq 1$ .

[F1]

$U_{n}$ is the closed subgroup scheme of ${G L}_{n}$ of upper unitriangular matrices, with $U_{n} (R) = {(α_{i j}) \in {G L}_{n} (R) : α_{i j} = 0 (i > j), α_{i i} = 1}$ for every commutative unital $k$ -algebra $R$ , and $O (U_{n}) = k [X_{i j} : i < j]$ with the displayed comultiplication. (The upper unitriangular group scheme U_n and its coordinate ring)

[F2]

The explicit polynomial Hopf algebra $O (U_{n})$ is coconnected by its weight filtration, and any surjective Hopf-algebra quotient of a coconnected algebra is coconnected. These are the choice-free algebraic clauses of Coconnected Hopf algebras: the coordinate ring of U_n and passage to quotients. A group with coconnected coordinate Hopf algebra is unipotent, the choice-free implication(c) implies(a) of Unipotent groups are exactly the subgroups of some U_n, equivalently the groups with coconnected coordinate Hopf algebra. The explicit matrix central series of $U_{n}$ has additive quotients (The central series of U_n with additive quotients, Unipotent algebraic groups and unipotent representations).

[F3]

For every $R$ , the map $a \mapsto (\begin{array}{cc} 1 & a \\ 0 & 1 \end{array})$ identifies addition on $R$ with multiplication in $U_{2} (R)$ , and is natural in $R$ ; equivalently the coordinate Hopf algebras are both $k [x]$ with $Δ (x) = x \otimes 1 + 1 \otimes x$ . (The upper unitriangular group scheme U_n and its coordinate ring)

[F4]

In characteristic $p$ , $x^{p}$ and $x^{p} - x$ are primitive in the additive Hopf algebra, so the ideals they generate are Hopf ideals and give explicit Hopf quotients $k [x] / (x^{p})$ and $k [x] / (x^{p} - x)$ . Quotient Hopf algebras carry their canonical group scheme structures. The latter polynomial factors as $\prod_{i \in F_{p}} (x - i)$ with distinct roots, and finite Chinese remainder gives $k [x] / (x^{p} - x) ≅ \prod_{i \in F_{p}} k$ . (Hopf ideals, kernels and quotients of commutative Hopf algebras, The upper unitriangular group scheme U_n and its coordinate ring)

Proof

Given: A field $k$ , $n \geq 1$ , and the additive group $G_{a} = Spec k [x]$ .

1.1F1F2algebra

The coordinate algebra of $U_{n}$ is coconnected by the explicit polynomial filtration in [F2], so the algebraic implication(c) implies(a) gives unipotence without a geometric closed-subgroup conversion. Its explicit central series has additive quotients by [F2]. As a scheme $U_{n} ≅ A_{k}^{n (n - 1) / 2}$ by its upper entries, so it is smooth. Its polynomial coordinate ring is a domain, hence its spectrum is irreducible and connected, including $n = 1$ , where it is the trivial group.

2.1F3step 1.1

Formula [F3] is a natural group-functor isomorphism $G_{a} ≅ U_{2}$ . Thus $G_{a}$ is smooth connected unipotent, with coordinate Hopf algebra $k [x]$ . This uses the explicit coordinate construction, not a choice of faithful representation.

3.1F2F4step 2.1algebra

In characteristic $p$ , the Frobenius homomorphism $x \mapsto x^{p}$ has kernel $α_{p} = Spec k [x] / (x^{p})$ . Its coordinate Hopf algebra is the explicit surjective quotient in [F4], hence coconnected and unipotent by [F2]. The class of $x$ is nonzero nilpotent, so this scheme is not reduced and therefore not smooth over $k$ .

3.2F2F4step 2.1algebra

The homomorphism $x \mapsto x^{p} - x$ has kernel $Spec k [x] / (x^{p} - x)$ , the constant additive group $F_{p}$ by [F4]. It is again an explicit coconnected Hopf quotient, hence unipotent by [F2], and has $p > 1$ disjoint rational points, so is not connected. This is not the image of the $p$ -torsion of $G_{a}$ , which is all of $G_{a}$ in this characteristic.

4.1step 1.1step 2.1step 3.1step 3.2∎

Thus the complete Example is verified: the smooth connected $U_{n}$ have the stated filtration and central quotients, $G_{a} = U_{2}$ is its first positive-dimensional case, and $α_{p}$ and constant $F_{p}$ exhibit nonsmooth and disconnected unipotent groups. Every unipotence assertion here follows from an explicitly presented Hopf algebra, so no AC-qualified geometric embedding or quotient conversion is used.

Depends on

Used by

The fixed point theorem fails without completeness: the additive group acts on the affine line by translations Counterexample

Dependency tree · two levels

37 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

J. S. Milne, Algebraic Groups (corrected 2022 printing, Cambridge University Press) (standard reference, not scraped)