Skip to content

Minimal primes

Classifies minimal primes over nonzero principal ideals in commutative semirings with unique factorization by normalized irreducible factor values. Relates these factors to order-dual irreducible components of principal zero loci. For principal quotients in commutative rings with unique factorization, identifies associated primes with minimal primes over the principal ideal for every generator, and characterizes quotient-spectrum points by associated primes and exact annihilators. For arbitrary dependent families of semifields, classifies all prime ideals of the product by ultrafilters, with zero-set membership, evaluation and germ-kernel bridges, and finite-coordinate and infinite non-coordinate controls. The same equivalence is a homeomorphism for the Zariski and existing Stone topologies, with both basis pullback laws and dense coordinate primes. For arbitrary filters and independently universed dependent monoids with zero, the total-section filter product is reduced exactly when its reduced fibres form a filter member. For dependent semiring fibres, equips the existing total-section Filter.Product with semiring operations, fibrewise maps and principal-filter restriction equivalences. Ultrafilters give division semirings and semifields with pointwise inversion. The section-map kernels are the existing zero-set ideals, compatibly with constant-family germs. For arbitrary dependent type families, the total-section filter product is nontrivial exactly when a total section exists and nontrivial fibres occur frequently. Associated primes also transport along compatible algebra maps. In commutative rings with well-founded DvdNotUnit, prime generators give principal ideals of height at most one, with height one for non-zero-divisors and for prime elements in domains. Finite ambient initial height gives well-founded lower intervals in preorders and stabilization of antitone prime chains over commutative semirings, with an ideal interface over commutative rings using only initial FiniteHeight and primeness at every index. Both chain interfaces identify the all-index ideal infimum at the same tail index. For integral homomorphisms of arbitrary commutative rings in independent universes, bounds target Krull dimension by source dimension, with equality for injective maps. Without injectivity, the target has the dimension of the source modulo the kernel. A faithful integral algebra has the dimension of its base ring for its given algebra structure. These results use the full WithBot ℕ∞ dimension, including zero rings and infinite dimension. Minimal primes over arbitrary ideals of finite dependent products of commutative semirings correspond to labelled coordinate minimal primes, using the evaluation-image coordinates of Ideal.piOrderIso. Evaluation comap transports minimality over arbitrary ideals without finiteness of the index. The finite classification includes empty indices, subsingleton factors and whole base ideals, and retains the labels of repeated isomorphic factors. For arbitrary finite sets and WithBot ℕ∞ values, the bottom-aware successor of the nonempty-subset product sum equals the product of successors in ℕ∞, including empty indices and arbitrary bottom and top values. For arbitrary dependent families of given preorders in independent universes, the height and coheight of a supplied section in the original pointwise order are the suprema of finite coordinate-rank sums in ENat. For finite indices these are the coordinate sums, including empty indices and infinite ranks. The dimension of an arbitrary dependent pointwise product is the supremum of its finite coordinate-restriction image dimensions, with inherited subtype orders. An empty full product makes every image empty, including at the empty coordinate set. Over a finite linearly ordered index, their canonical lexicographic point ranks are sums of original coordinate ranks weighted by the whole later fibres' strict-chain vertex heights, with the same suffix priority for height and coheight. For any relation and finite family of disjoint cross-comparable sets, chain height is the sum of piece heights, with both hypotheses restricted to the chosen support.

Quoted from the project description in formalization.yaml of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.

30 articles: 5 for highlights of its formalization.yaml whose declarations the scan finds and 25 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/minimal-primes, read at commit 45952e34 (2026-11-05).
  • Lean toolchain v4.34.0-rc2, Mathlib at 83abb3e7.
  • License: Apache-2.0.
  • Authors: Formal Frontier Agents.
  • Review status: “reviewed”.
  • Automation: agent

Literature

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

  • Foundations of Algebraic Geometry, Ravi Vakil, Exercise 3.7.H (October 21, 2025 draft) (book; background).
  • The Rising Sea: Foundations of Algebraic Geometry, Ravi Vakil, Exercise 6.6.F (book; background).

Builds on

Used by

Highlights

DefinitionPrime spectra of products of semifields#

The prime spectrum of an arbitrary dependent product of semifields is canonically homeomorphic to the Stone space of ultrafilters on its index type.

Quoted from the highlights in formalization.yaml of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.

Lean

Read from the source at commit 45952e34, without running Lean.

Sources
LeanPrimeSpectrum.piHomeomorphUltrafilter

TheoremIdeals in products of division semirings#

Every left ideal of an arbitrary dependent product of division semirings is the zero-set ideal of its characteristic-test filter.

Quoted from the highlights in formalization.yaml of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.

Lean

Read from the source at commit 45952e34, without running Lean.

Sources
LeanIdeal.piIdeal_piFilter

TheoremNontrivial dependent reduced products#

For every filter and independently universed dependent type family, the total-section reduced product is nontrivial exactly when a total section exists and nontrivial fibres occur frequently.

Quoted from the highlights in formalization.yaml of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.

Lean

Read from the source at commit 45952e34, without running Lean.

Sources
LeanFilter.Product.nontrivial_iff

TheoremKrull dimension and chain cardinalities of lexicographic sums#

For arbitrary subsets of independently universed dependent preorders whose active indices form a finite strict chain, the stock lexicographic Sigma dimension is the active-index dimension plus the sum of active fiber dimensions. Empty support and infinite fiber dimensions are included. For two arbitrary preorder subsets, the tagged lexicographic union has the maximum of their dimensions and their sum plus one. For arbitrary subsets of independently universed dependent sums with raw relations, chain height is the supremum of finite sums of fiber heights, assuming only pairwise comparability and irreflexivity of the active indices. Empty fibers and infinite heights are allowed, with no transitivity, global order, finiteness or attainment hypothesis.

Quoted from the highlights in formalization.yaml of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.

Lean

Read from the source at commit 45952e34, without running Lean.

Sources
LeanOrder.krullDim_toLex_sigma · Order.krullDim_toLex_sum · Set.chainHeight_sigma_lex

TheoremDimension and point ranks of finite dependent lexicographic products#

For arbitrary subsets of independently universed given preorders over a finite linearly ordered index, lexicographic dimension is the WithBot map of ENat decrement applied to the product of the shifted fibre dimensions. Product and addition are in WithBot ENat, with only the decrement in ENat. Empty index, empty fibres and infinite dimensions are included. The canonical partial order is equality or strict lexicographic comparison with equality prefixes; it needs only strict less-than relations on the fibres and agrees as a whole record with Mathlib's construction when the fibres have partial orders. For a given section of arbitrary given fibre preorders, height and coheight are sums of the original coordinate ranks weighted by the strict-chain vertex heights of whole later fibres. Both use the same original suffix priority. These ENat formulas include empty indices and unattained infinite heights, with no fibre partial-order, linearity, finiteness or extra inhabitation premise.

Quoted from the highlights in formalization.yaml of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.

Lean

Read from the source at commit 45952e34, without running Lean.

Sources
LeanOrder.krullDim_toLex_pi · Order.height_toLex_pi · Order.coheight_toLex_pi · Pi.Lex.isStrictOrderOfLT · Pi.Lex.partialOrderOfLT · Pi.Lex.partialOrderOfLT_lt · Pi.Lex.partialOrderOfLT_le_iff · Pi.Lex.partialOrderOfLT_eq

Headline results

The 67 headline results of its README are on a page of their own: 25 articles, 37 quoted as text, and 5 that link an article above.

Main results

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