LemmaStatement: Literature-sourcedProof: 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.

The coordinate ring of an affine group scheme is a commutative Hopf algebra

Statement

Let $k$ be a field, let $G$ be an affine group scheme of finite type over $k$ , and let $(A, Δ, ε, S)$ be its coordinate ring with the structure maps of The coordinate Hopf algebra of an affine group scheme. Then $(A, Δ, ε, S)$ is a commutative Hopf algebra over $k$ in the sense of Commutative Hopf algebras over a field. Moreover, for every morphism $f ⁣ : G \to H$ of affine group schemes (Morphisms and closed subgroup schemes of group schemes) the induced map $O (f) ⁣ : O (H) \to O (G)$ is a morphism of commutative Hopf algebras. No choice principle is used.

Facts & Assumptions

[F1]

The group-object identities of Group schemes of finite type over a field read $m \circ (m \times id) = m \circ (id \times m)$ on $G \times_{k} G \times_{k} G$ , $m \circ (e \times id) = id = m \circ (id \times e)$ under the canonical identifications, and $m \circ (i, id) = e \circ p = m \circ (id, i)$ , where $p ⁣ : G \to Spec k$ is the structure morphism. A morphism of group schemes satisfies $f \circ m_{G} = m_{H} \circ (f \times f)$ , $f \circ e_{G} = e_{H}$ and $i_{H} \circ f = f \circ i_{G}$ .

[F2]

The global-sections functor gives a contravariant equivalence between affine $k$ -schemes and commutative $k$ -algebras, with $Spec (B \otimes_{k} C) ≅ Spec B \times_{k} Spec C$ , so $O (G \times_{k} G) = A \otimes_{k} A$ and $O (G \times_{k} G \times_{k} G) = A \otimes_{k} A \otimes_{k} A$ . (Affine schemes are contravariantly equivalent to commutative rings, Affine fibre products are spectra of tensor products, Affine schemes and their coordinate rings)

[F3]

The structure maps $Δ = O (m)$ , $ε = O (e)$ and $S = O (i)$ are $k$ -algebra homomorphisms, and $O$ of a composite is the composite of the comorphisms in reverse order. (The coordinate Hopf algebra of an affine group scheme)

Proof

Given: A field $k$ , an affine group scheme $G$ of finite type over $k$ with coordinate ring $A = O (G)$ and structure maps $Δ, ε, S$ , and the group identities [F1].

1.1F2F3

Under the identification $O (G \times_{k} G \times_{k} G) = A \otimes_{k} A \otimes_{k} A$ of [F2], the comorphism of $m \times id$ is $Δ \otimes id$ and that of $id \times m$ is $id \otimes Δ$ : the product $m \times id$ is, on the level of coordinate rings, the tensor product of $Δ$ with the identity of $A$ . Hence $O (m \circ (m \times id)) = (Δ \otimes id) Δ$ and $O (m \circ (id \times m)) = (id \otimes Δ) Δ$ by [F3].

1.2F1F2F3

The comorphism of the structure morphism $p ⁣ : G \to Spec k$ is the unit $u_{A} ⁣ : k \to A$ , the comorphism of $e$ is $ε$ , and the comorphism of $e \times id$ is $ε \otimes id$ , so $O (m \circ (e \times id)) = (ε \otimes id) Δ$ and, with the canonical identifications $k \otimes_{k} A ≅ A ≅ A \otimes_{k} k$ , the identity $m \circ (e \times id) = id$ becomes $(ε \otimes id) Δ = {id}_{A}$ ; symmetrically $(id \otimes ε) Δ = {id}_{A}$ . Likewise $O (m \circ (i, id)) = m_{A} (S \otimes id) Δ$ and $O (e \circ p) = u_{A} ε$ , so the identity $m \circ (i, id) = e \circ p$ gives $m_{A} (S \otimes id) Δ = u_{A} ε$ , and symmetrically $m_{A} (id \otimes S) Δ = u_{A} ε$ .

2.1F3step 1.1step 1.2

Since the identities of [F1] hold as identities of scheme morphisms, and $O$ is a functor, the transposed identities of steps 1.1 and 1.2 are identities of $k$ -algebra homomorphisms; together with [F3] they are exactly the coassociativity, counit and antipode axioms of Commutative Hopf algebras over a field. Hence $(A, Δ, ε, S)$ is a commutative Hopf algebra.

3.1F1F2F3∎

For a morphism $f ⁣ : G \to H$ of affine group schemes, applying the contravariant functor $O$ to the identities $f \circ m_{G} = m_{H} \circ (f \times f)$ , $f \circ e_{G} = e_{H}$ and $i_{H} \circ f = f \circ i_{G}$ of [F1] gives $Δ_{G} O (f) = (O (f) \otimes O (f)) Δ_{H}$ , $ε_{G} O (f) = ε_{H}$ and $O (f) S_{H} = S_{G} O (f)$ , where the middle identity uses $O (f \times f) = O (f) \otimes O (f)$ under the product identifications of [F2]. These are exactly the three compatibility conditions for a morphism of commutative Hopf algebras, so $O (f)$ is one. No choice principle was used: every step is functoriality of $O$ or one of the given group identities.

Depends on

Used by

Cited to discharge well-definedness by The coordinate Hopf algebra of an affine group scheme.

Dependency tree · two levels

26 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)
J. Swanson (notes), J. Pevtsova (lecturer), Algebraic Groups Lecture Notes, University of Washington, Fall 2014 (standard reference, not scraped)