Skip to content

Graded rings

Graded quotients and localizations, degree-multiplying maps of homogeneous localizations, homogeneous component surjectivity and polynomial lifts, irrelevant-ideal finiteness, homogeneous prime correspondence, symmetric algebras, their first-order quotients by the square of the augmentation ideal over arbitrary commutative rings and modules, natural square-zero algebra and conormal linear equivalences, selected-component Veronese rings, coherent-tail equivalences of whole selected rings, positive-index degree-one generation under an old-ring generation hypothesis, weighted evaluation at arbitrary homogeneous elements over actual degree-zero coefficients, finite positive-weight blocks of finitely supported natural exponent vectors, positive-weight polynomial monomial-adjoin membership, prescribed-index weighted-polynomial generation with arbitrary weights and coefficients, finite type of every prescribed positive whole selected ring over its actual new zero component from arbitrary-weight homogeneous generators or native finite-type input, all-index equivalence of actual selected degree-zero rings and finite type of the zero-index external selected ring over its actual new degree-zero ring, finiteness of the canonical inclusion from every positive selected-component ring when the original ring is finite type over its whole degree-zero ring, positive-index residue projections linear over the whole external selected ring and their exact finite images, whole-Veronese convolution on shifted sums of entire old components, canonical coefficient evaluation, positive reduced-index projection-range equivalence and finite-module transport from the full old zero ring, and prime-multiplicity valuations with homogeneous polynomial applications, and weighted generation of separated compatible integer filtrations over precomplete coefficient rings, with separately qualified stability, ambient-finiteness and stage-finiteness consequences.

Quoted from the project description in formalization.yaml of FormalFrontier/graded-rings at commit 6a459e8e, Apache-2.0.

5 articles: 4 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/graded-rings, read at commit 6a459e8e (2026-11-05).
  • Lean toolchain v4.34.0-rc2, Mathlib at 83abb3e7.
  • License: Apache-2.0.
  • Authors: Formal Frontier Agents.
  • Review status: “Independently reviewed mathematical library”.
  • Review notes: “The library provides algebraic results; source-specific exercise correspondence and complete source coverage are not asserted.”
  • Automation: agent; tool setup “Formal Frontier agents using Lean, Lake and pinned mathlib.”
  • Automation notes: “AI agents authored mathematical constructions, proofs, interfaces, examples and documentation.”

Literature

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

  • The Rising Sea: Foundations of Algebraic Geometry, Ravi Vakil, October 21, 2025 draft, exercises 4.5.F–H, 5.4.N and §7.4.4/7.4.D–E (printed p. 215) (book; background).
  • Foundations of Rigid Geometry I, Kazuhiro Fujiwara, Fumiharu Kato, arXiv:1308.4734v5, Proposition 0.7.5.2 (book; background).
  • mathlib, The mathlib contributors (formalization; background).
  • The Rising Sea: Foundations of Algebraic Geometry — §7.4.4, Exercise 7.4.F, Ravi Vakil, October 21, 2025 draft, printed p. 215; coefficient conventions pp. 151–152 (book; background).
  • The Rising Sea: Foundations of Algebraic Geometry — §7.4.4, Exercise 7.4.G, Ravi Vakil, October 21, 2025 draft, original printed/physical PDF p. 215; continuation p. 216; grading conventions pp. 151–152 (book; background).
  • The Rising Sea: Foundations of Algebraic Geometry — §7.4.4, Exercise 7.4.H, Ravi Vakil, October 21, 2025 draft, printed/physical PDF pp. 215–216; grading conventions pp. 151–152 (book; background).

Builds on

Used by

Highlights

DefinitionQuotient Rees algebra of a regular principal ideal#

For any commutative ring R and a in R such that multiplication by a is injective, the quotient Rees_R((a))/(a)Rees_R((a)) is isomorphic as an R/(a)-algebra to (R/(a))[T].

Quoted from the highlights in formalization.yaml of FormalFrontier/graded-rings at commit 6a459e8e, Apache-2.0.

Lean

Read from the source at commit 6a459e8e, without running Lean.

Sources
LeanreesAlgebra.principalPolynomialEquiv

TheoremFinite weighted normal forms for Rees modules#

For any ideal I of a commutative ring R and any R-module M, a natural I-filtration has finitely generated Rees module exactly when one finite family of elements x_i and natural weights w_i satisfies H.N n = sum_i I^(n-w_i) • R x_i for every natural n, with truncated natural subtraction.

Quoted from the highlights in formalization.yaml of FormalFrontier/graded-rings at commit 6a459e8e, Apache-2.0.

Lean

Read from the source at commit 6a459e8e, without running Lean.

Sources
LeanIdeal.Filtration.submodule_fg_iff_exists_weighted_normal_form

TheoremFinite generation of associated graded modules#

For any ideal I of a commutative ring R and any R-module M, let C = Rees_R(I)/I Rees_R(I). The associated graded module gr_I(M) is finitely generated over C if and only if M/IM is finitely generated over R.

Quoted from the highlights in formalization.yaml of FormalFrontier/graded-rings at commit 6a459e8e, Apache-2.0.

Lean

Read from the source at commit 6a459e8e, without running Lean.

Sources
LeanIdeal.AssociatedGradedModule.finite_iff

InstancePolynomial scalar extension over semirings#

For any possibly noncommutative semiring R and any left R-module M with additive commutative-monoid structure, finitely supported coefficient sequences form a canonical R[X]-module. Constant polynomials act by the original coefficient action and X shifts degree. This module represents C-semilinear maps from M and is natural under semilinear coefficient maps. Under the original commutative-ring and additive-group hypotheses, it agrees with Mathlib's PolynomialModule, including its fixed polynomial action and ordered coefficient formula.

Quoted from the highlights in formalization.yaml of FormalFrontier/graded-rings at commit 6a459e8e, Apache-2.0.

Lean

Read from the source at commit 6a459e8e, without running Lean.

Sources
LeanPolynomialModule.Extension.polynomialModule · PolynomialModule.Extension.coeff_smul · PolynomialModule.Extension.universalProperty · PolynomialModule.Extension.coordinate · PolynomialModule.Extension.polynomialLinearEquivPolynomialModule

Headline results

The 52 headline results of its README are on a page of their own: 1 article, 50 quoted as text, and 1 that links an article above.

Main results

Its formalization.yaml lists 61 main results, and the scan finds 61 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.