Skip to content

Headline results

Quoted from the headline results in README.md of FormalFrontier/graded-rings at commit 6a459e8e, Apache-2.0.

These are reusable algebraic APIs, not claims of source-specific correspondence or complete book coverage. Selected-ring and evaluation results below concern naturally graded commutative rings unless another base is stated. Old and new degree-zero coefficients mean the entire actual components, not a smaller chosen coefficient ring.

Browse the results by topic:

Polynomial and Rees constructions

DefinitionPolynomial covers and equivalences for principal ideals#

For any commutative ring R and a : R, evaluation at the class of a t defines a surjective R/(a)-algebra map (R/(a))[T] → C, where C is the Rees algebra modulo its coefficient ideal. If a is regular, this same map is an R/(a)-algebra equivalence, including unit generators and the zero ring. Composition with augmentation is evaluation at zero (reesAlgebra.principalPolynomialHom, surjective_principalPolynomialHom, bijective_principalPolynomialHom, principalPolynomialEquiv, and augmentation_comp_principalPolynomialEquiv).

Quoted from the headline results in README.md of FormalFrontier/graded-rings at commit 6a459e8e, Apache-2.0.

Lean

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

Sources
LeanreesAlgebra.principalPolynomialHom

Finite products of polynomial semirings. For any finite index type and family of semirings R i, the polynomial comparison identifies (Π i, R i)[X] with Π i, (R i)[X]. Its forward map projects coefficients, and its inverse assembles their coordinate functions. The API computes coefficients in both directions, constants, the indeterminate and inverse monomials. Index and coefficient universes are independent; empty products and noncommutative coefficient semirings are included.

Finite products of polynomial modules. For a finite family of commutative rings R i and additive commutative groups M i with their given R i-module structures, the semilinear comparison identifies PolynomialModule (Π i, R i) (Π i, M i) with Π i, PolynomialModule (R i) (M i). It carries the original polynomial action to the coordinate polynomial actions along Polynomial.piRingEquiv R. Coefficients and singles are computed in both directions. The index, ring and module universes are independent; empty products are included, with no finiteness hypothesis on the rings or modules.

Rees subalgebras over commutative semirings. For every ideal I of a commutative semiring R, the coefficient-power subalgebra I.reesSubalgebra contains exactly the polynomials whose degree-n coefficient belongs to I ^ n. Constants are unrestricted; a monomial of degree n belongs exactly when its coefficient belongs to I ^ n. In particular, C r * X belongs exactly when r ∈ I. Over a commutative ring it equals Mathlib's reesAlgebra I.

Coefficient homomorphisms and equivalences of Rees algebras. For commutative rings R, S, a ring homomorphism f : R →+* S and ideals I, J with I.map f ≤ J, coefficient change defines reesAlgebra I →+* reesAlgebra J. Its underlying polynomial map applies f to every coefficient, and it respects identities and composition. A source element belongs to its kernel exactly when every coefficient belongs to RingHom.ker f. The map is surjective exactly when f is surjective and I.map f = J, and injective exactly when f is injective. A coefficient-ring equivalence e : R ≃+* S induces reesAlgebra I ≃+* reesAlgebra (I.map e.toRingHom), with polynomial/coefficient formulas for the equivalence and its inverse and identity/composition laws under the standard image-ideal identifications. The ring universes are independent; no Algebra R S structure, regularity, nontriviality or finiteness assumption is required.

Graded quotients, localization and finiteness

Quotients and localizations. For commutative rings, homogeneous-ideal quotients inherit the image grading for additive-monoid degrees with decidable equality. Full localization at homogeneous denominators uses an additive commutative group of degrees; its degree-zero component is equivalent to equal-degree homogeneous fractions. Both allow zero rings without a domain assumption; localization also permits zero-divisor denominators.

Localization maps and reducedness. The degree-multiplying map uses natural gradings, an ordinary unital ring homomorphism, explicit degree compatibility and mapped denominators. Even factor zero requires its degree witness; source charts may be arbitrary, but restriction factors are homogeneous. Separately, homogeneous localization preserves reducedness for a reduced commutative ring, additive commutative monoid degrees with decidable equality and any denominator submonoid. Neither interface requires a domain, regular denominators or nontriviality; the map needs no positive factor.

Finiteness and primes. In a naturally graded commutative ring, finite type over old degree zero is equivalent to finite generation of the irrelevant ideal; Noetherianity is equivalent to that finite generation plus Noetherian degree zero. For an integer-graded commutative ring with a positive-degree homogeneous unit, homogeneous primes correspond to degree-zero primes by contraction and radical extension.

Natural Rees modules

Finite Rees modules and stable filtrations. For any ideal I in a commutative ring R and any R-module M, with independent universes, an I-filtration with finitely generated Rees module is stable: I • F.N n = F.N (n + 1) for all sufficiently large n. Neither I, the stages, nor M need be finitely generated. Conversely, stability from a given degree and finite generation through that degree suffice for finite generation of the Rees module; no finiteness of later stages is needed. Both directions use the natural-number filtration and polynomial Rees-module constructions.

Noetherian Rees modules. For any ideal I of a commutative ring R and any natural I-filtration H of an R-module, the original Rees module is Noetherian over reesAlgebra I exactly when its original initial stage H.N 0 is Noetherian over R and the filtration is stable. The initial stage may be proper; no finite generation of I or Noetherianity of the ambient ring or module is required. If H.submodule is Noetherian, every stagewise subfiltration is stable. For each original submodule N, there is a bound c such that H.N (n + c) ⊓ N = I ^ n • (H.N c ⊓ N) for every natural n. The bound may depend on N, which need not be finitely generated.

Lattice operations on Rees submodules. For any ideal I of a commutative ring R and any R-module M, Rees-submodule inclusion is equivalent to inclusion at every natural filtration stage. The construction preserves binary suprema and arbitrary indexed infima and suprema. For a finite family whose Rees submodules are finitely generated over reesAlgebra I, the supremum filtration again has a finitely generated Rees submodule; no finiteness of the ideal, individual stages, or ambient module is required.

Monic multiplication and polynomial-module evaluation kernels. Over any commutative ring R and any R-module M, multiplication by a monic polynomial g is injective on PolynomialModule R M. For any antitone family P : ℕ → Submodule R M, the product has degree-n coefficient in P n for every n exactly when the source has degree-n coefficient in P (n + g.natDegree) (monic_smul_coeff_mem_iff and monic_smul_injective). At every r : R, a module-valued polynomial evaluates to zero exactly when it is (X - C r) • q; for M = R, equivPolynomialSelf identifies this factor-existence statement with ordinary polynomial divisibility (eval_eq_zero_iff_exists_smul_X_sub_C and exists_smul_X_sub_C_eq_iff_dvd). Ring and module universes are independent; no regularity, nontriviality or finiteness hypothesis is needed.

Rees-module evaluation and initial-stage finiteness. For any ideal I of a commutative ring R, any R-module M and natural I-filtration H, evaluation at every r : R maps H.submodule onto the original H.N 0, semilinearly along polynomial evaluation composed with the Rees-algebra inclusion. The original-R-linear constant-single map is a section at every point; the maps are natural under stage-preserving linear maps. At zero this is the constant-coefficient augmentation, and H.submodule.FG implies (H.N 0).FG. No ideal, stage or ambient finiteness, stability or zero-stage normalization is assumed, and ring and module universes are independent.

Positive Rees augmentation and stability from degree zero. For any ideal I of a commutative ring R, any R-module M and natural I-filtration H, let B = reesAlgebra I, E = H.submodule, and K₀ be the kernel of the constant-coefficient augmentation B → R. The coefficient criterion says that f : E belongs to K₀ • ⊤ exactly when its constant coefficient vanishes and its coefficient of degree n + 1 belongs to I • H.N n for every n. The equality ker (H.evalRees (0 : R)) = K₀ • ⊤ holds if and only if ∀ n, I • H.N n = H.N (n + 1), equivalently ∀ n, H.N n = I ^ n • H.N 0. Evaluation retains its original target H.N 0; the augmentation is to R, not R/I. Ring and module universes are independent, with no finiteness, regularity, completeness, separation or initial-stage normalization assumption.

Unique successor-tail factors for Rees evaluation kernels. For any ideal I of a commutative ring R, any R-module M, any natural I-filtration H, and every r : R, H.mulXSubC r is a reesAlgebra I-linear map from the canonical tail (H.toIntFiltration.natTail (1 : ℤ)).submodule into H.submodule. Its underlying value is multiplication by the ambient polynomial X - C r. It is injective, its range is LinearMap.ker (H.evalRees r), and every evaluation-zero element has a unique factor in this tail, whose degree-n coefficient lies in H.N (n + 1). Coefficient and admissible-single formulas, compatibility at zero with the existing cutoff transition, and naturality under stage-preserving linear maps describe the map. No regularity of r, ideal/stage/ambient finiteness, stability, separatedness, exhaustivity, Noetherianity, flatness or normalization of H.N 0 is required; ring and module universes are independent. The evaluator still lands semilinearly in the original, possibly proper H.N 0, with only an original-R-linear constant section. This is not a reesAlgebra I-linear short exact sequence ending there or an ideal-product kernel formula; X - C r need not belong to the Rees algebra.

Finite 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 = ⨆ i, I ^ (n - w i) • span_R {x i} for every natural n (submodule_fg_iff_exists_weighted_normal_form). Subtraction is truncated natural subtraction. The family may be empty and ring and module universes are independent. The exists_fin_generating_family_single_le_of_submodule_fg construction also selects x i ∈ H.N (w i) whose singles in all degrees q ≤ w i span the same Rees module. No finiteness of the ideal, individual stages or ambient module, or normalization at degree zero is required. The bounded-degree criterion in GradedRings.ReesModule gives eventual stability, without ideal finiteness. If I is finitely generated, finite generation of the Rees module is equivalent to finite generation of every original-ring stage together with eventual stability (submodule_fg_iff_fg_stable in the same module).

Weighted generators for Rees modules. A natural filtration satisfies H.N n = ⨆ i, I ^ (n - w i) • span_R {x_i} for every n if and only if its Rees module is spanned over reesAlgebra I by single R q x_i for every q ≤ w i, including zero and all intermediate degrees. The characterization allows an arbitrary index type, independent of the ring and module universes, with no separate stage-membership assumption on the family. A finite index type gives finite generation without assuming the ideal, the individual stages, or the ambient module to be finitely generated.

Integer filtrations and associated graded modules

Integer-filtered associated gradeds and Rees actions. Over a commutative ring R, for an antitone family of submodules of an R-module M, F.N : ℤ → Submodule R M with I • F.N n ≤ F.N (n + 1), the integer associated graded is the direct sum of F.N n modulo the next stage inside it. It retains the original componentwise R-module structure and has a surjective coefficientwise representative map, with next-stage kernel and a first-isomorphism comparison. No finiteness, exhaustivity, separatedness, lower bound or normalization at degree zero is required. The Rees grading gives the polynomial Rees algebra its degree grading and its coefficient-ideal quotient the image grading. On the same associated-graded carrier, the canonical representation constructs an action of C = reesAlgebra I ⧸ I.map (algebraMap R (reesAlgebra I)). Constants act by the original R-action, and I annihilates the carrier. For q : ℕ, a ∈ I ^ q and m ∈ F.N n, the class of aX^q sends the class of m to the class of a • m in degree n + q.

Natural Rees and associated-graded finiteness. For any natural I-filtration H in an R-module, if the coefficients R are I-adically precomplete and ⨅ n, H.N n = ⊥, its original Rees submodule is finitely generated over reesAlgebra I if and only if the associated graded of its canonical integer extension is finite over C = reesAlgebra I ⧸ I.map (algebraMap R (reesAlgebra I)). The extension is constant at H.N 0 in negative degrees. Ring and module universes are independent; no ideal, stage or ambient finite generation, exhaustivity, normalization at zero or coefficient Hausdorffness is required.

Shifted Rees projections. For every integer cutoff k, the natural tail of an integer filtration has stages F.N (k + q). Its polynomial Rees submodule maps semilinearly to the full associated graded along B → C, by summing the homogeneous classes of its coefficients. The kernel is the next tail pulled back to this source, not generally the coefficient-ideal multiple. Its range consists exactly of elements whose components below k vanish. If all lower pieces vanish, a finite tail over B gives a finite associated graded over C, without ideal finiteness, Noetherianity, completeness or normalization. In particular, an exhaustive integer filtration on a finite original module has finite associated graded over C if, at one common threshold c, it is stable at and above c and its stages at and below c are finitely generated.

Ideal-adic associated graded comparison. For any ideal I and module M, the canonical integer-adic associated graded is linearly equivalent over the quotient Rees algebra to Ideal.AssociatedGradedModule I M, with both original scalar actions retained. The map sends homogeneous representatives to polynomial singleton classes; coefficients recover the inverse components, and negative components vanish. No finiteness, completeness or separatedness assumption is needed. In the regular specialization, composition with (Ideal.AssociatedGradedModule.regularEquiv I).symm identifies it with the quotient Rees algebra and sends the degree-zero unit to 1.

Maps of quotient Rees modules. For every ideal I of a commutative ring R, an original-R-linear map between arbitrary, independently universed modules induces a quotient-Rees-linear map between their Ideal.AssociatedGradedModule modules. It applies the polynomial module map to each Rees representative, preserves singleton degrees, and commutes with each coefficient map via the ordinary quotient by I ^ (q + 1) • ⊤. Identities and composition are preserved, without finiteness or completeness assumptions.

Naturality of the ideal-adic comparison. Every original-R-linear map f : M →ₗ[R] N induces the canonical integer-adic map Ideal.adicAssociatedGradedHom I f, linear over the existing quotient Rees algebra, with representative, component, identity and composition laws. The comparison and its inverse are natural for this map and the independently defined quotient Rees map: both forward routes send [m] in degree q : ℕ to the old polynomial singleton class of f m in degree q. The original scalar actions and independent module universes are retained, with no finiteness, completeness, separatedness or nontriviality assumption.

Residue-linear integer graded pieces. For the same arbitrary ideal-compatible integer filtration, the original pieces carry named R ⧸ I-module structures compatible with their original R actions. Insertion and projection are residue-linear for the whole associated graded's existing residue action, with the same functions, representative formulas and finite reconstruction. Piece modules and towers are activated locally rather than registered globally. No residue action on the stages or ambient stage quotients, finiteness or degree-zero normalization is required.

Maps of integer-filtered associated gradeds. An original-R-linear map preserving every stage of two integer filtrations induces a canonical quotient-Rees-linear map. It sends each homogeneous representative to its image, preserves the original R action, and respects identities and composition. For stage-preserving maps f, g : M →ₗ[R] N with filtrations F and H, their induced maps agree exactly when f m - g m ∈ H.N (n + 1) for every n : ℤ and m ∈ F.N n (map_eq_iff). An induced map vanishes exactly when f m ∈ H.N (n + 1) for all such representatives (map_eq_zero_iff), without requiring the original map to vanish. It is injective exactly when, for every n : ℤ and x ∈ F.N n, membership f x ∈ H.N (n + 1) implies x ∈ F.N (n + 1). It is surjective exactly when H.N n ≤ (F.N n).map f ⊔ H.N (n + 1) for every integer n. Thus stagewise pullback equality F.N n = (H.N n).comap f gives injectivity, and stagewise image equality (F.N n).map f = H.N n gives surjectivity, without ambient injectivity or surjectivity of f or normalization at degree zero. A module equivalence carrying each filtration stage onto the corresponding stage induces a quotient-Rees-linear equivalence, compatibly with inverses, identities and composition. The modules have independent universes; no finiteness, exhaustivity, separatedness or lower bound is required.

Integer translations. For every integer d, translation of an integer filtration has stage (F.shift d).N n = F.N (n + d). Its graded-piece equivalence preserves representatives, and shiftEquiv identifies the whole associated gradeds linearly over the canonical quotient Rees algebra, taking degree n to degree n + d. Representative, inclusion, component and residue-scalar formulas accompany zero, composition and inverse identities using the canonical filtration comparisons. Translation commutes with maps induced by stage-preserving R-linear maps, both on the whole associated graded and on each graded piece. It also commutes with pullback and image filtrations. The induced equivalence between the quotients by inclusion ranges commutes with the subquotient equivalence. No additional hypotheses are needed.

Pullbacks and images of integer filtrations. Pullback and image along an original-R-linear map have the submodule inverse images and direct images as their integer stages. They preserve ideal compatibility, respect identities and composition, and satisfy the stagewise image–preimage universal property. The existing canonical associated-graded map is injective from the pullback and surjective onto the image, without ambient injectivity or surjectivity. No degree-zero normalization, finiteness, exhaustivity, separation, completeness or degree bound is imposed.

Binary products of integer filtrations. For any ideal I of a commutative ring R and ideal-compatible integer filtrations F, H on independently universed R-modules M, N, the product has stages (F.N n).prod (H.N n) on the original M × N. Its associated graded comparison is linear over C = reesAlgebra I ⧸ I.map (algebraMap R (reesAlgebra I)) for the canonical actions, with forward map given by the two projections and inverse given by the sum of the two inclusions. No degree-zero normalization, finiteness, exhaustivity, separatedness, completeness or degree bound is required.

Dependent direct sums of integer filtrations. For an arbitrary family of ideal-compatible integer filtrations over a commutative ring, the componentwise filtration on the dependent direct sum has associated graded canonically equivalent to the direct sum of the associated gradeds, linearly over the quotient Rees algebra. Coordinates are the filtered component maps; the inverse is assembled from the filtered summand inclusions. Homogeneous representatives retain their summand and absolute integer degree, naturally under stage-preserving linear maps. The scalar, index and module universes are independent. No finite index set, common lower degree bound, finiteness, exhaustivity, separatedness or completeness is required.

Exactness of integer associated graded maps. For compatible original linear maps f : M →ₗ[R] N and g : N →ₗ[R] P, the image of the first canonical quotient-Rees-linear associated graded map equals the kernel of the second exactly when, for every integer n and y ∈ H.N n, membership g y ∈ K.N (n + 1) is equivalent to y ∈ (F.N n).map f ⊔ H.N (n + 1). The ambient composite need not vanish. An ambient exact pair with strict stage images induces an exact pair, without ambient injectivity or surjectivity. The three module universes are independent; no finiteness, exhaustivity, separatedness, completeness or degree bound is needed.

Induced submodules and filtered quotients. For any submodule S, the subquotient equivalence identifies the associated graded of F.image S.mkQ with the quotient of F.AssociatedGraded by the range of the canonical map from (F.comap S.subtype).AssociatedGraded, linearly over the quotient Rees algebra. The submodule filtration is induced, not intrinsic ideal-adic. Representative formulas and the quotient universal property apply in all integer degrees, with no finiteness, normalization, separation or completeness hypotheses.

Naturality of associated graded subquotients. For ideal-compatible integer filtrations F, H on independently universed modules over a commutative ring R, a stage-preserving R-linear map f with f(S) ≤ T commutes with the induced-submodule and quotient maps. The subquotient equivalences intertwine the quotient-by-range map induced by the ambient associated graded map with the associated graded original quotient map, over the canonical quotient Rees actions. No strictness, ambient injectivity or surjectivity, finiteness or degree bound is required.

Nested induced quotients. For submodules S ≤ T of an integer-filtered module, the nested quotient comparison identifies the filtration induced on T.map S.mkQ with the image of the filtration induced on T. The third isomorphism carries every iterated image stage onto the direct image stage. On whole associated gradeds, the subquotient equivalence for S carries the second graded range onto the induced quotient range; quotienting twice then agrees with quotienting directly by the T range, via the third isomorphisms over the original ring and the canonical quotient Rees algebra. No finiteness, normalization, exhaustivity, separatedness, completeness or splitting is required.

Ideal-power quotients and coefficient multiplication. For any ideal I of a commutative ring R and every natural degree q, the quotient of I ^ q by its ideal multiple has an R ⧸ I-linear comparison quotientMonomialEquivCoefficients with the degree-q component of the coefficient-ideal quotient of the Rees algebra. Residue scalars are inherited on the same component with its original R-action; restricting the comparison to R recovers quotientMonomialEquiv, with the same forward and inverse functions. The denominator is exactly the next ideal power, viewed inside I ^ q. On these same quotient modules, coefficient multiplication powerQuotientMul is bilinear over R ⧸ I; powerQuotientMul_mk sends [a] and [b] to [a * b] in degree q + r. Multiplication is commutative and associative under the degree-sum identifications, with the class of 1 in degree zero as a two-sided unit. The quotient monomial maps preserve this multiplication and send that class of 1 to the quotient Rees unit. No finiteness, Noetherianity, nontriviality or positive-degree assumption is needed.

The algebra of ideal-power quotients. The direct sum of the ideal-power quotients is an R ⧸ I-algebra canonically equivalent to the coefficient-ideal quotient of the Rees algebra. It retains componentwise addition and the original R and R ⧸ I actions. Its unit is the degree-zero class of 1, and homogeneous multiplication is powerQuotientMul. The equivalence sends each homogeneous insertion to its quotient monomial; its inverse decomposes arbitrary elements into coefficient classes. No finiteness or nontriviality assumption is needed.

Ideal-power quotients acting on integer associated gradeds. The ideal-power quotient action restricts the existing quotient-Rees action along powerQuotientSumAlgEquiv I : D ≃ₐ[R ⧸ I] C, in the direction D → C, where D = reesAlgebra.powerQuotientSum I. Use powerQuotientSum_of_mk_smul_single to send [a] in degree q and [m] in degree n to [a • m] in degree n + q. The original R, R ⧸ I and C actions are unchanged, and both coefficient actions form scalar towers with the D-action. Quotient-Rees-linear maps and equivalences between associated gradeds restrict to D using Mathlib's restrictScalars constructors, with unchanged forward and inverse functions. No additional filtration hypotheses are required.

Filtered finite generation

Weighted generation of integer filtrations. For a separated, antitone integer-indexed filtration satisfying I • F n ≤ F (n + 1) over an I-adically precomplete commutative coefficient ring, finite degree-weighted lifts generating the successive quotients generate every stage with coefficients in I ^ ((n - d i).toNat). Ring, module and finite indexing type have independent universes; the family may be empty and the degrees may be negative. The finiteness consequences keep their extra hypotheses separate: eventual stability needs none, finiteness of the original module needs exhaustivity, and finite generation of every stage needs I.FG. The equality and ambient finiteness require neither I.FG nor a Hausdorff coefficient ring. This independently generalizes the filtered lifting ingredient underlying Fujiwara--Kato, Foundations of Rigid Geometry I, Proposition 0.7.5.2; it is not the full proposition or a full associated-graded construction.

Finite integer associated gradeds and weighted generators. For the canonical quotient-Rees action, finiteness of the whole integer associated graded is equivalent to finite homogeneous original-module lifts generating every successive quotient with ideal-power weights. This algebraic equivalence needs no completeness, separation, exhaustivity or finiteness of the ideal. Over an ideal-adically precomplete coefficient ring, separation gives exact weighted descriptions in every integer degree and eventual stability. Under these two hypotheses, finiteness is also equivalent to the existence of a finitely generated natural Rees tail whose prescribed projection onto the whole associated graded is surjective; neither exhaustivity nor finiteness of the ideal or individual stages is needed. Exhaustivity additionally gives finiteness of the original module; I.FG instead gives finite generation of every stage, without exhaustivity. With both exhaustivity and I.FG, the intrinsic criterion finite_associatedGraded_iff_finite_fg_stable says that finiteness over the same quotient Rees algebra is equivalent to Module.Finite R M, finite generation of every original R-stage in every integer degree, and eventual equality I • F.N n = F.N (n + 1). No Noetherianity, coefficient Hausdorffness, ambient-module precompleteness, degree-zero normalization or chosen top stage is required, and the generator family may be empty.

Quotient Rees modules

Associated graded modules from the first quotient. For any ideal I in a commutative ring R and any R-module M, with independent universes, the Rees-quotient associated graded module G is finite over C = B / IB, where B = reesAlgebra I, whenever Q = M / IM is finite over R / I. The canonical map C ⊗[R/I] Q → G is surjective, not generally an isomorphism. More generally, for a subideal K ≤ I with IⁿM = KⁿM + Iⁿ⁺¹M for every natural n, the canonical reesAlgebra K ⊗[R] Q → G is surjective without a finiteness hypothesis, and Q finite over R / I makes G finite over reesAlgebra K, with no finite-generation assumption on K. If Q is Noetherian over R and K is finitely generated, then G is Noetherian over C. None of these results requires finiteness of the original M, Noetherianity of R, or finite generation of I.

Quotient Rees augmentation. For any ideal I of a commutative ring R, constant coefficient induces an R/I-algebra homomorphism from C = reesAlgebra I / I·reesAlgebra I to R/I. The composite C → R/I → C is the degree-zero projection, and the image of R/I → C is exactly the degree-zero component. No finiteness or nontriviality assumption is needed; this does not identify the whole ring C with R/I.

The regular associated graded module. For any ideal I of a commutative ring R, the regular associated graded module Ideal.AssociatedGradedModule I R is canonically free of rank one over C = reesAlgebra I / I·reesAlgebra I. The equivalence regularEquiv sends c to c • regularUnit, where the generator is the degree-zero unit class. Rees-representative and every-coefficient formulas, unique scalar expressions, and linear-map extensionality expose this comparison without unfolding its quotients. No finiteness, completeness, separatedness or nontriviality is assumed.

Symmetric algebras and prime multiplicity

Symmetric algebras and first order. Basis-free grading and graded maps are functorial for arbitrary modules over a commutative semiring; only polynomial coordinates need a basis. Over a commutative ring, for any module M, the augmentation-square quotient and conormal give SymmetricAlgebra R M ⧸ augmentationIdeal² ≃ₐ[R] TrivSqZeroExt R M and augmentationIdeal.Cotangent ≃ₗ[R] M, without freeness, projectivity or finiteness. Generator formulas, ideal transport and both whole-map naturalities use open scoped TrivSqZeroExt and the released coherent-modules kernel equivalence. The quotient's image cotangent ideal corresponds to TrivSqZeroExt.kerIdeal, not the original augmentation ideal; no scheme or sheaf comparison.

Prime multiplicity. A multiplicative valuation measures a prime element in a commutative domain with well-founded divisibility; extension to localization requires non-zero-divisor denominators. Its homogeneous restriction uses additive commutative monoid degrees. The polynomial applications work over a field, with arbitrary variables; irreducibility at denominator order one uses a positive-degree homogeneous prime polynomial.

Veronese rings and homogeneous generation

Whole selected rings, including index zero. The Veronese ring is the external sum of whole old components in multiples of n, with a native grading for every natural n. Its actual zero ring is equivalent to old degree zero at every index; whole-ring inclusion is injective for n > 0, but need not be at zero. At zero, old-zero copies occupy separate external summands: each factors as a power of the new degree-one variable with its arbitrary coefficient in the entire new zero ring. Polynomial evaluation is surjective, hence that external sum is finite type over its new zero ring, without old-ring finite type, field, domain or nontriviality. No polynomial equivalence or source index-zero convention is asserted.

Evaluation and homogeneous lifts. Weighted evaluation at chosen homogeneous elements of arbitrary natural weights, including zero, preserves degrees, is a native graded map and commutes with actual components. Only lifting every homogeneous target element requires the chosen family to generate over old degree zero. The degree-one specialization uses all of 𝒮 1 and exactly Algebra.adjoin (𝒮 0) (𝒮 1 : Set S) = ⊤, including degree-zero targets. No finite-variable, domain, field or nontriviality assumption is needed.

Degree-one generation: all versus finite. Under that old degree-one generation hypothesis, every positive selected index is generated by all new degree one over its entire actual new zero ring, without finite generation. A finite positive-weight homogeneous generating family over old zero instead gives a finite new degree-one family at D = Finsupp.weightedBlockSize w; native old-zero finite type gives some positive index. These need no field, domain, nontriviality, equal weights or Noetherianity; the finite-family conclusions are not all-index claims.

Positive-weight blocks and monomial adjoin. For finite indices and strictly positive natural weights, exponent decomposition recovers a whole finitely supported natural exponent vector of weight k * D as exactly k weight-D blocks, with positive, not necessarily minimal D = max 1 (Fintype.card ι) * ∏ i, w i. Over any commutative semiring, monomial-adjoin membership puts weight-k * D polynomials in the coefficient subalgebra generated by coefficient-one weight-D monomials, including arbitrary coefficients and k = 0. Neither result alone gives polynomial factorization or whole-ring generation.

Selected weighted-polynomial components. For finite variables, arbitrary natural weights including zero, any commutative semiring, and each prescribed n > 0, one finite homogeneous family generates all polynomial degrees divisible by n over the entire coefficient semiring—not whole selected-ring finite type or degree-one generation.

Finite type at each positive index. Finite homogeneous generators of arbitrary natural weights over entire old zero, or native old-zero finite type, make every prescribed positive whole selected ring finite type over its entire actual new zero ring. No domain, nontriviality, field, Noetherianity, positive or equal weights are required. This is distinct from index-zero finite type and from degree-one generation at every index.

Finite inclusion and whole-ring residue modules. Under old-zero finite type, the inclusion at each n > 0 makes the old ring finite over the whole external selected ring via the actual inclusion.toAlgebra. For n > 0, r < n, the residue projection is linear for that same action and has exactly the elements supported in residue r as its range. Ambient module finiteness makes this image finite; old-zero finite type suffices. The shifted sum ⨁ k, 𝒮 (n * k + r) has whole selected-ring convolution; coefficient evaluation is linear and injective for n > 0 and any r, and identifies the projection range when also r < n. Ambient finiteness, or full old-zero finite type, transports under those positive reduced-index bounds. No individual-fiber whole-ring action, arbitrary-submodule finiteness or zero-index bijection follows.

Coherent high tails. Tail equivalence requires N > 0, an actual zero-ring equivalence, additive equivalences in all degrees at least N, and coefficient/high-product compatibility. For N ≤ n it identifies the entire selected rings with native degree-preserving inverse maps; for n > 0, selected_zero is the exact coefficient square. No maps across missing original low degrees or Proj/scheme equivalence follow.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.