Skip to content

Simplicial rings

Central polynomial simplices over arbitrary unital rings, their coefficient-natural polynomial retraction and explicit algebraic simplicial homotopy on the polynomial extension.

Quoted from the project description in formalization.yaml of FormalFrontier/simplicial-rings at commit 72878574, Apache-2.0.

No articles: its formalization.yaml lists no highlights, and none of its 3 headline results links a declaration that the scan finds in the linked file at this commit, so they are quoted below.

Facts

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

  • Repository: FormalFrontier/simplicial-rings, read at commit 72878574 (2026-11-04).
  • Lean toolchain v4.34.0-rc2, Mathlib at 83abb3e7.
  • License: Apache-2.0.
  • Authors: Formal Frontier Agents.
  • Review status: “self-assessed”.
  • Automation: agent; framework “Formal Frontier agents using Lean 4”; tool setup “AI-assisted proof development”

Literature

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

  • The K-book: An Introduction to Algebraic K-theory, Charles A. Weibel, Chapter IV, section 11 (mathematical motivation) (book; background).

Builds on

No other Formal Frontier library.

Headline results

Quoted from the headline results in README.md of FormalFrontier/simplicial-rings at commit 72878574, Apache-2.0.

PolyRing R n has n central indeterminates over any Ring R; homogeneous coordinate values sum to one. substitute evaluates free generators at whole-target-center elements (a sufficient, not necessarily minimal, condition); hom_ext determines ring maps by coefficients and generators.

simplexFunctor sends a ring to an actual simplicial ring, with contravariant ordinalMap for every ordinal arrow, including empty fibres. Polynomial constantInclusion followed by evalAtZero is strictly the identity on the unextended simplex; both maps are coefficient-natural.

contraction is a native seven-identity SimplicialObject.Homotopy from evaluation-then-inclusion to the identity on the polynomially extended simplex. Its first face is the identity endpoint and its last face is evaluation-then-inclusion; homotopyMap_natural handles every unital coefficient map. Whiskering along a supplied covariant functor uses mathlib's existing Homotopy.whiskerRight, not a new wrapper here.

See the simplex guide and homotopy guide for the precise coordinate, degree, face, degeneracy and universe conventions.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.