Skip to content

Algebraic groups

Reusable Lean formalization of matrix point groups, finite algebraic group schemes and their coordinate algebras. The library covers unitriangular and upper-triangular groups, diagonal products, split kernels, closed unitriangular stages and their underlying affine-space presentations, finite additive products and positive-stage underlying projections and sections, unitriangular scalar base change and coherence, and selected dimension and geometric results. Coalgebra APIs include field subcoalgebras and finite-dimensional containment, right comodules and finitely generated subcomodule containment, coefficient matrix units, counit ranges and idempotent principal ideal constructors; split free presentations give finite tensor coordinates. Precise hypotheses and exclusions are documented in README.md and the focused mathematical guides. This is not a complete formalization of any cited source.

Quoted from the project description in formalization.yaml of FormalFrontier/algebraic-groups at commit cad2dc41, Apache-2.0.

6 articles: 5 for highlights of its formalization.yaml whose declarations the scan finds and 1 for headline results in its README whose declaration link names a declaration the scan finds in the linked file. Its other headline results are quoted where they stand.

Facts

From the repository and its formalization.yaml; the review and automation statements are quoted as written.

  • Repository: FormalFrontier/algebraic-groups, read at commit cad2dc41 (2026-11-05).
  • Lean toolchain v4.34.0-rc2, Mathlib at 83abb3e7.
  • License: Apache-2.0.
  • Authors: Formal Frontier Agents.
  • Review status: “AI-assisted development with independent agent review of individual contributions; no human mathematical review is claimed.”.
  • Review notes: “Mathematical scope and third-party credit appear in README.md and CREDITS.md; this metadata does not assert complete source coverage.”
  • Automation: agent; tool setup “Formal Frontier AI agents used Lean and Lake with pinned dependencies.”
  • Automation notes: “AI agents developed mathematical proofs and ordinary-import clients.”

Literature

The sources its formalization.yaml names, with their relationship to it.

  • Hopf Algebras, Moss E. Sweedler, W. A. Benjamin, 1969 (book; background).
  • Algebraic Groups, James S. Milne, 2017 edition (book; background).
  • Original algebraic-group and affine-localization constructions, Formal Frontier Agents (original project proofs and earlier project research; adapts).

Builds on

Used by

Highlights

TheoremClosed linear embeddings of affine algebraic groups#

Every affine group scheme locally of finite type over a field K admits a group-scheme morphism into GL_n over K for some natural number n whose underlying scheme morphism is a closed immersion. Nonreduced group schemes are included, with no representation or basis supplied.

Quoted from the highlights in formalization.yaml of FormalFrontier/algebraic-groups at commit cad2dc41, Apache-2.0.

Lean

Read from the source at commit cad2dc41, without running Lean.

Sources
LeanAlgebraicGeometry.exists_generalLinearGroupHom_isClosedImmersion

DefinitionPoint representations and comodules#

For a commutative Hopf algebra over a commutative ring and a fixed arbitrary module, natural point representations on the module's scalar extensions, tested on commutative base algebras in any universe containing the Hopf algebra, correspond bijectively to right-comodule structures on that module.

Quoted from the highlights in formalization.yaml of FormalFrontier/algebraic-groups at commit cad2dc41, Apache-2.0.

Lean

Read from the source at commit cad2dc41, without running Lean.

Sources
LeanAlgebraicGeometry.PointRepresentation.rightComoduleEquiv

TheoremFinite-dimensional subcoalgebra containment#

Every finite subset of a coalgebra over a field is contained in a finite-dimensional subcoalgebra.

Quoted from the highlights in formalization.yaml of FormalFrontier/algebraic-groups at commit cad2dc41, Apache-2.0.

Lean

Read from the source at commit cad2dc41, without running Lean.

Sources
LeanCoalgebra.exists_finite_subcoalgebra_of_finite

TheoremFinite Hopf algebras and right Hopf modules#

Every finite-dimensional Hopf algebra H over a field K admits a K-linear functional λ whose multiplication pairing (a, x) ↦ λ(a * x) is nondegenerate in both arguments. The Hopf algebra need not be commutative or cocommutative, and no restriction on the characteristic or assumption of antipode bijectivity is required. Over a commutative semiring, a specified right comodule over a possibly noncommutative semiring Hopf algebra with a given compatible right action and scalar tower is linearly equivalent to its coinvariants tensored with that Hopf algebra, without flatness or finiteness assumptions.

Quoted from the highlights in formalization.yaml of FormalFrontier/algebraic-groups at commit cad2dc41, Apache-2.0.

Lean

Read from the source at commit cad2dc41, without running Lean.

Sources
LeanHopfAlgebra.exists_nondegenerate_mul · Coalgebra.RightComodule.coinvariantsTensorEquiv

TheoremBidual coactions and the antipode square#

For a specified right comodule on a finite projective module over a commutative semiring, canonical bidual evaluation identifies its bidual with the original coaction twisted on coefficients by the antipode square. The coefficient Hopf algebra need not be commutative and its antipode need not be invertible. For commutative coefficients the twist is identity.

Quoted from the highlights in formalization.yaml of FormalFrontier/algebraic-groups at commit cad2dc41, Apache-2.0.

Lean

Read from the source at commit cad2dc41, without running Lean.

Sources
LeanCoalgebra.RightComodule.dual_dual_coaction_eval · Coalgebra.RightComodule.dual_dual_eq_transport

Headline results

Quoted from the headline results in README.md of FormalFrontier/algebraic-groups at commit cad2dc41, Apache-2.0.

Cartier's theorem. Every commutative Hopf algebra over a characteristic-zero field is reduced, and is smooth if it is finite type, for its given coefficient algebra structure and with independent scalar and carrier universes. See Hopf algebra smoothness.

Linear embeddings of affine algebraic groups. Every affine group scheme locally of finite type over a field K admits a group-scheme morphism G → GLₙ for some n : ℕ whose underlying scheme morphism is a closed immersion. No basis or representation is supplied, and nonreduced group schemes are included. See the closed linear embedding theorem.

TheoremSurjectivity and faithfully flat coordinates#

For homomorphisms of given affine group schemes locally of finite type, dominance over an algebraically closed field implies surjectivity on all scheme points; over any field, schematic dominance suffices. Over any field with reduced target H, dominance or injectivity of the compatible coordinate map A → B gives Module.FaithfullyFlat A B for its given algebra structure. The coordinate presentations may have independent universes. For finite-type commutative Hopf algebras over any field, an injective morphism f : A →ₐc[K] B with reduced source coordinate algebra A satisfies f.toAlgHom.toRingHom.FaithfullyFlat, by BialgHom.faithfullyFlat_of_injective_of_isReduced. This uses the given Hopf structures, in independent scalar and carrier universes. See surjectivity over algebraically closed fields, schematic dominance over fields, and faithful flatness of coordinates.

Quoted from the headline results in README.md of FormalFrontier/algebraic-groups at commit cad2dc41, Apache-2.0.

Lean

Read from the source at commit cad2dc41, without running Lean.

Sources
LeanBialgHom.faithfullyFlat_of_injective_of_isReduced

Hopf tensor–quotient equivalences. For a central bialgebra map from a commutative bialgebra A over a commutative ring R to a possibly noncommutative Hopf algebra B, comultiplication gives a first-factor B-linear equivalence B ⊗[A] B ≃ₗ[B] B ⊗[R] (B / (ker ε_A)B). In this generality the quotient is only a module quotient, and A need not have an antipode. When B is commutative, HopfAlgebra.tensorQuotientAlgEquiv refines the same map to a B-algebra equivalence on the canonical tensor and quotient algebras. The simp equality tensorQuotientAlgEquiv_toLinearEquiv recovers tensorQuotientEquiv, so its finite-comultiplication formulas compute both directions. For a group-like c, the inverse sends (b c) ⊗ [c] to b ⊗ c. Mixed scalar extension is the composition of inverse tensor cancellation, congruence with this refinement, and tensor cancellation. Compatible ordinary algebra maps and scalar towers suffice; the commutative coefficient algebra needs no Hopf structure. See HopfAlgebra/TensorQuotient.

Finite Hopf algebras and Hopf modules. Every finite-dimensional Hopf algebra over a field has a linear functional λ such that λ (a * x) is nondegenerate in both arguments. Its left regular module is injective (HopfAlgebra.injective_self). The algebra need not be commutative or cocommutative, and the field may have any characteristic. See the Frobenius and self-injectivity theorems. For decomposition over a commutative semiring R, let H be a possibly noncommutative semiring with full Hopf algebra structure, and X a specified right comodule on an additive-commutative-monoid R-module M. For its given right action with IsScalarTower R Hᵐᵒᵖ M, an explicit hX : X.IsHopfModule gives X.coinvariantsTensorEquiv hX : (X.weightSpace (1 : H)) ⊗[R] H ≃ₗ[R] M. The forward map is the given action. The inverse X.toCoinvariantsTensor hX corestricts the antipode contraction to coinvariants before tensoring it with H and composing with the coaction. Both inverse identities hold, including the tensor-side identity inside coinvariants tensored with H itself. Both maps intertwine the given right action with right multiplication on the H factor. Universes are independent; no flatness, finiteness or inverse antipode is required. See the decomposition and its API.

Main results

Its formalization.yaml lists 328 main results, and the scan finds 328 of them declared in the file the yaml gives; they are on their own page, not made articles.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.