Skip to content

Exactness of dependent… to Irreducible closed rectangles…

Quoted from the headline results in README.md of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.

Uniform finite generators of dependent reduced products

The finite-generation module proves two finite-generation criteria. For the same given semiring, additive and module records, an arbitrary filter F, a naturally finite index type J and raw vectors g : J → (∀ i, M i), Filter.Product.span_range_coe_eq_top_iff gives

Submodule.span (F.Product R) (Set.range (fun j => (g j : F.Product M))) = ⊤
  ↔ ∀ᶠ i in F, Submodule.span (R i) (Set.range (fun j => g j i)) = ⊤.

The target records are exactly Product.instSemiring, Product.addCommMonoid and Product.module of the given fibres, even when R = M. Filter.Product.moduleFinite_iff gives

Module.Finite (F.Product R) (F.Product M)
  ↔ ∃ n : ℕ, ∀ᶠ i in F, ∃ v : Fin n → M i,
      Submodule.span (R i) (Set.range v) = ⊤.

One uniform n is essential; eventual pointwise finite generation alone does not give this condition. No basis or freeness is assumed. All four carrier universes are independent. Empty J, n = 0, empty index types, bottom filters and zero semirings are included, with no properness or nontriviality hypothesis. These criteria add no new functional data or global instances.

Uniform finite presentations of dependent reduced products

The finite-presentation module proves the uniform generators-and-relations criterion. For arbitrary F, independently universed ring families R i, and given additive commutative monoids M i with their given R i-module actions, Filter.Product.moduleFinitePresentation_iff gives

Module.FinitePresentation (F.Product R) (F.Product M)
  ↔ ∃ n m : ℕ, ∀ᶠ i in F,
      ∃ f : (Fin n → R i) →ₗ[R i] M i,
      ∃ g : (Fin m → R i) →ₗ[R i] (Fin n → R i),
        Function.Surjective f ∧ Function.Exact g f.

The left side uses exactly Product.instSemiring of the ring semiring parents, Product.addCommMonoid of the given vector records, and Product.module of the given actions. Each f retains the given target addition and action, even when R = M; only coefficient function spaces use standard self-actions. Exactness uses the given vector zero. The pair (n,m) precedes the eventual quantifier; eventual individual finite presentation or a generator bound alone is weaker. Padding generators may require additional relations, so exact fixed sizes must not be confused with independently padding both sizes at unchanged bounds.

The rings may be noncommutative, and coefficients act on the left. No properness, nontriviality, freeness, coherence or Noetherian assumption is imposed. Bottom filters, empty index types, zero rings/modules and zero free sizes are included. Represented coordinate negation gives additive inverses for the named scalar semiring; the given module actions give vector inverses without a new group hypothesis. This is the genuine ring-module presentation scope. Over general semirings Mathlib's stock class concerns a finitely generated zero kernel, not a presentation by a finitely generated congruence; no such semiring claim is made.

TheoremExactness of dependent reduced-product maps#

For arbitrary functions f i : X i → Y i and g i : Y i → Z i in independent universes, an arbitrary filter F, given Zero (Z i) records and Nonempty (∀ i, X i), Filter.Product.map_exact_iff characterizes Function.Exact of the two existing Product.map functions by ∀ᶠ i in F, Function.Exact (f i) (g i). This is one eventual locus of whole fibre exactness, not exactness at every index or separately eventual tests on fixed values. The selected target zero is exactly Product.zeroPoint F Z, the represented section of the given fibre zeros; no global zero instance is added. Neither function needs to preserve zero or any algebraic operation.

A total source section is essential: an empty source fibre outside the filter's support still prevents all total source sections. No independent middle-section hypothesis is needed, since the first map sends a source section to one. Filter.Product.map_exact_iff_of_addZeroClass instead uses the existing named additive product zero, still for arbitrary functions and only target AddZeroClass records. Product.zeroPoint_eq_zero_add supplies this alignment. In particular, given linear maps between semimodules over given, possibly noncommutative, fibre semirings can be used as functions while retaining all the given additive and module records. The target zero is inherited from Product.addCommMonoid F P, and fibre source zeros discharge the section condition. No bundled product linear map, finite basis, properness, nontriviality, additive inverses or further inhabitation hypothesis is needed. Bottom filters, empty indices and zero semirings remain included.

For constant families, Product.map_const_eq_germ_map and Product.zeroPoint_eq_germ_zero identify these functions and the target zero with Mathlib's germ maps and zero.

Quoted from the headline results in README.md of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.

Lean

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

Sources
LeanFilter.Product.map_exact_iff

DefinitionCoordinate maps and zero-reflection of dependent filter products#

For any filter D and independently universed dependent type families R and S, coordinate functions φ i : R i → S i induce the canonical Filter.Product.map from D.Product R to D.Product S. Its representative law uniquely characterizes it, with identity and composition laws and agreement with the existing semiring and constant-family germ maps. No algebra, points or proper-filter hypothesis is needed for the coordinate map.

If the coordinate functions preserve selected total sections a and b eventually, the induced map reflects the represented point b to a exactly when the coordinate functions reflect these points eventually. For fibrewise ZeroHoms this gives zero-reflection using only the same selected fibre zeros: Filter.Product.zeroPoint is the class of that zero section, not a new Product zero instance. No multiplication, addition or scalar zero is required.

Filter.Product.map_surjective_iff retains the exact global-section alternatives: the total target section type is empty, or the total source section type is nonempty and the coordinate maps are surjective eventually. An empty source fibre ignored by the filter cannot be silently filled. The dependent controls include varying Fin (n + 3) → Fin (n + 4) maps that reflect zero but are neither injective nor additive, and a frequent bad locus giving a genuine nonzero kernel class.

Quoted from the headline results in README.md of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.

Lean

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

Sources
LeanFilter.Product.map

DefinitionReindexing dependent filter products#

For independently universed indices and fibres, a map u : ι → κ with Tendsto u F G induces Filter.Product.compTendsto from G.Product R to F.Product (fun i => R (u i)). It sends a section to its precomposition, respects identity and composition, and agrees with the existing Filter.Germ.compTendsto on constant families. No algebra, total-section existence or proper-filter assumption is needed. The full criterion compTendsto_injective_iff says that pullback is injective exactly when the original total-section type is empty or Filter.map u F ⊓ principal {j | Nontrivial (R j)} = G ⊓ principal {j | Nontrivial (R j)}. Exact filter-image equality therefore suffices (compTendsto_injective_of_map_eq), without injectivity of u, but is not necessary for a fixed family. An index equivalence makes pullback surjective with only forward convergence (compTendsto_surjective_of_equiv), but not necessarily injective. Convergence in both directions gives Filter.Product.compTendstoEquiv, whose inverse uses canonical dependent Pi reindexing. The dependent Bool client contrasts a four-to-two noninjective pullback with a two-to-two injective pullback for the same unequal filters, by making the ignored fibre a singleton. It also exhibits an injective, non-surjective diagonal.

The underlying Filter.forall_eventually_eq_iff works for fibres in any independently universed Sort: two filters give the same eventual equality on all pairs of total sections exactly when there is no total section or their restrictions to {i | ∃ x y : R i, x ≠ y} agree. For Type-valued families, Filter.productSetoid_eq_iff expresses this using the existing section setoids and stock Nontrivial support. An empty fibre ignored by a filter still prevents total sections; eventual inhabitation cannot replace the empty-total-section alternative.

Quoted from the headline results in README.md of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.

Lean

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

Sources
LeanFilter.Product.compTendsto

DefinitionSmall products of dependent filter products#

For an arbitrary filter D and R : ι → κ → Type w, with independent row, coordinate and fibre universes, Filter.Product.piComparison maps the class of a matrix to its family of column classes. It is surjective for arbitrary κ. If [CardinalInterFilter D c] and HasCardinalLT κ c, with c in the row universe, Filter.Product.piEquivOfHasCardinalLT makes this same comparison an equivalence. The bound is strict: the filter must be closed under intersections of fewer than c sets. Countable completeness and countable coordinates give Filter.Product.piEquivOfCountable; finite coordinates give the original Filter.Product.piEquiv for every filter. Both new equivalences agree with the finite one as equivalence data when the coordinates are finite.

The inverse transposes supplied global column representatives. Generic equivalence identities and the forward readouts give the inverse laws; existing comparison naturality gives both naturality squares, with an independent target universe. No quotient unfolding, algebra, inhabited fibres, properness, common-universe assumption or chosen finite enumeration is required. The examples include infinite even principal rows with Fin (i+j+2) fibres and proper nonprincipal cocountable rows on Set ℕ, as well as empty indices and bottom with empty global sections. The cofinite-Nat Boolean diagonal remains a failure of injectivity: countable coordinates alone do not suffice.

Quoted from the headline results in README.md of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.

Lean

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

Sources
LeanFilter.Product.piComparison

DefinitionCenters of dependent filter products#

For any filter and an independently universed family with multiplication, a section represents an element of the full intrinsic center exactly when it is central eventually. With a two-sided identity in each fibre, Filter.Product.centerEquiv identifies the product of the fibre centers with the center of the product. Neither associativity nor a proper filter is required. The representative API selects a total center-valued section agreeing eventually, not canonically at ignored indices. The varying-family client uses retained fibres of sizes four and sixteen with nonassociative multiplication; the existing constant-germ API and its client remain available.

Quoted from the headline results in README.md of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.

Lean

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

Sources
LeanFilter.Product.centerEquiv

TheoremReduced filter germs#

For independent index and value universes, any filter D, and a value type M with only zero and natural-number powers, Filter.Germ.isReduced_iff_eventually characterizes reducedness of Germ D M by eventual reducedness of M. Equivalently, D = ⊥ or M is reduced. No power laws or properness assumption are needed. The same module characterizes nilpotence by one exponent whose power is zero eventually, and supplies reducedness for germs of reduced values.

Quoted from the headline results in README.md of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.

Lean

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

Sources
LeanFilter.Germ.isReduced_iff_eventually

Reduced ranges of iterated Frobenius

For a commutative semiring of exponential characteristic p, the original image of the nth Frobenius iterate is reduced exactly when every nilpotent element has zero p ^ nth power. If the semiring is Noetherian and p is prime, all sufficiently high iterates have reduced images. The reduced-image API also gives the corresponding original subring-range statement for a given commutative ring. No field, perfectness, or reducedness of the ambient semiring is assumed.

TheoremNo zero divisors in ultrafilter products#

For an ultrafilter U and an independently universed dependent family R, Filter.Product.noZeroDivisors_iff_eventually characterizes no zero divisors in the product by eventual no zero divisors in the fibres. It requires only Zero and Mul on each fibre and uses the existing Con.hasMul and Con.zero operations on the existing product carrier. No associativity, unit, absorption by zero, addition, commutativity or nontriviality hypothesis is needed. For monoids with zero, Filter.Product.noZeroDivisors_iff uses the canonical product instances; the operation-agreement lemmas identify the same zero and multiplication. The varying finite client has no zero divisors even though zero is not absorbing.

The constant-family bridge compares the congruence zero and multiplication records with the existing germ operations for every filter. At an ultrafilter, Filter.Germ.noZeroDivisors_iff therefore characterizes no zero divisors in the germ by no zero divisors in the value type, still with only Zero and Mul. The same nonabsorbing client exercises this specialization. These generic criteria are Mathlib-upstream candidates.

Eventual fibrewise no zero divisors alone does not suffice for arbitrary filters: at the proper top filter on a two-point index type, complementary nonzero sections over a domain multiply to zero.

For arbitrary F, if each fibre has a two-sided absorbing zero (MulZeroClass), Filter.Product.noZeroDivisors_iff_eventually_and_trace characterizes no zero divisors for the same congruence operations by the conjunction of eventual fibrewise no zero divisors and D = ⊥ ∨ IsAtom D, where D = F ⊓ principal {i | Nontrivial (R i)}. Both absorption laws are material; no unit, associativity, properness or all-fibre nontriviality is required. The trace, not F itself, must be bottom or an atom, and even an atomic trace does not remove the fibrewise condition. The canonical monoid-with-zero specialization is Filter.Product.noZeroDivisors_iff_eventually_and_trace_of_monoidWithZero. The mixed-fibre client uses top on Bool with a natural-number fibre and a singleton fibre: its trace is pure false, so the product has no zero divisors although top is not an ultrafilter.

Quoted from the headline results in README.md of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.

Lean

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

Sources
LeanFilter.Product.noZeroDivisors_iff_eventually

Reduced dependent filter products

For an arbitrary filter and an independently universed dependent family of monoids with zero, the filter product is reduced exactly when its reduced fibres form a member of the filter. The criterion uses a uniform square-zero test, not an exchange of a varying nilpotence exponent with eventual equality. A representative is nilpotent exactly when one uniform natural-number exponent makes its power zero eventually; the exponent may be zero. No addition, commutativity, proper-filter or nontriviality hypothesis is needed.

If the filter contains a finite set, nilpotence of a represented section is also equivalent to eventual fibrewise nilpotence, by Filter.Product.isNilpotent_coe_iff_of_finite_mem. The whole index type need not be finite. The same module gives finite-index and finite-principal criteria; the latter tests exactly the values on the generating set, including the empty set. These results reuse the finite-member exponent bound. For monoid-with-zero coefficients, the constant-germ specialization uses the existing germ zero and power operations; the earlier germ results still need only zero and natural-number powers. The dependent client gives a nonzero nilpotent quotient element on an infinite index type with varying nonadditive fibres.

Regular elements of dependent filter products

For an arbitrary filter D and an independently universed family K with only fibrewise multiplication, a total section represents a left-regular, right-regular, or regular element of D.Product K exactly when its values have that property eventually. The criteria require neither associativity, an identity, nor a proper filter. The existing Germ criteria are their constant-family specializations. The varying finite example separates left and right regularity in noncommutative magmas with no identity.

DefinitionIntegral pullback of maximal spectra#

For an integral homomorphism f : R →+* S of commutative rings in independent universes, MaximalSpectrum.comapOfIsIntegral maps MaximalSpectrum S to MaximalSpectrum R by ideal contraction. Its image is exactly the maximal ideals containing RingHom.ker f, and it is surjective when f is injective. The API gives the underlying-ideal equation, agreement with prime-spectrum pullback, identity and contravariant composition.

For the existing Zariski topologies, this function is continuous and closed. It sends the maximal-spectrum trace of V(I) to the trace of V(I.comap f) for every ideal I of S. Zero rings are allowed; no chosen algebra structure, domain, Jacobson, Noetherian or finite-type assumption is imposed. Integral pullback need not be injective, even when the ring homomorphism is injective.

For surjective f, the same function is the embedding MaximalSpectrum.comapEmbeddingOfSurjective, with all the same compatibility laws. The product-projection client uses this embedding to transport infinitude of the maximal spectrum from a factor to the product ring with Infinite.of_injective.

Quoted from the headline results in README.md of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.

Lean

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

Sources
LeanMaximalSpectrum.comapOfIsIntegral

Other headline results

The following interfaces are implemented in this library. See the reader guide and the linked module documentation for statements, examples, proof ideas and Mathlib dependencies.

All ideals of products and standard filters (module). For a dependent family K : ι → Type v of division semirings, Ideal.piOrderIsoFilter K identifies Ideal (Π i, K i) with the order dual of Filter ι; in particular it applies to semifields. Its characteristic law is {i | f i = 0} ∈ I.piFilter K ↔ f ∈ I. Both constructors already work for semirings, but division is used to recover every ideal. The improper filter gives the whole ideal, a principal filter gives functions vanishing on its generating set, and the cofinite filter gives finite support. The API includes germ kernels, singly generated ideals, and compatibility with Mathlib's finite coordinate-ideal classification. Index and factor universes are independent; empty products are included without a nontrivial-product assumption. For arbitrary semiring fibres, coordinate ideals I i and a filter D, Filter.pi_sup_piIdeal_eq_top_iff says that Ideal.pi I ⊔ D.piIdeal R is the whole ideal exactly when {i | I i = ⊤} ∈ D. The properness criterion Filter.pi_sup_piIdeal_ne_top_iff is nonmembership of this set, not membership of its complement unless D is an ultrafilter. Zero fibres and improper filters are allowed. (examples).

Ultrafilter coordinate-locus criteria (module). For dependent semirings R i and left ideals I i, Ultrafilter.isPrime_pi_sup_piIdeal_iff and Ultrafilter.isMaximal_pi_sup_piIdeal_iff characterize the sum Ideal.pi I ⊔ (U : Filter ι).piIdeal R as prime or maximal exactly when the respective coordinate locus belongs to U. The criteria need no commutativity, nontrivial-factor or subtractivity assumption.

Prime ideals of arbitrary products of semifields (module). For any dependent family K : ι → Type v of semifields, PrimeSpectrum.piEquivUltrafilter K identifies every prime ideal of Π i, K i with an ultrafilter on ι. A function belongs to the ideal for U exactly when {i | f i = 0} ∈ U. Already for division-semiring fibres, Ultrafilter.piIdeal_isMaximal makes every such ultrafilter zero-set ideal maximal, via the ideal/filter order isomorphism. The index universe is independent of v, and no additive cancellation, ring, finite-index or nonempty-index hypothesis is imposed. The forward ideal construction works already for semiring factors, with evaluation-kernel and constant-family germ-kernel bridges. Finite products have uniquely labelled coordinate kernels; the cofinite ultrafilter gives non-coordinate primes on infinite index types. The topological extension PrimeSpectrum.piHomeomorphUltrafilter K retains this exact equivalence as a homeomorphism for the Zariski and existing Stone topologies. Its basis pullback laws use the nonzero locus and the function one on a subset and zero off it. Coordinate primes are dense, even when non-coordinate primes occur; the topology is not in general discrete. For an arbitrary index map g : κ → ι and fibrewise semifield homomorphisms φ j : K (g j) →+* L j, spectral pullback along the stock product homomorphism corresponds to Ultrafilter.map g. The API includes the inverse square, index precomposition and same-index family-map specializations; the index and fibre universes are independent, with no injectivity or finiteness assumption.

Residue fields of dependent products of fields (module). For a dependent family K : ι → Type v of fields and U : Ultrafilter ι, Ultrafilter.residueFieldProductEquiv K U canonically identifies (U.piIdeal K).ResidueField with the existing (U : Filter ι).Product K. This is a ring equivalence over the section ring R = Π i, K i: for every section r, it sends algebraMap R (U.piIdeal K).ResidueField r to the reduced-product class of r. The API includes the inverse equation, uniqueness from this property and its equality-of-homomorphisms form. Fibrewise field homomorphisms give a commuting square with Ideal.ResidueField.map and Filter.Product.mapRingHom. Index and fibre universes are independent; no common characteristic, finite-index or nonempty-index hypothesis, or global field instance on the Product, is required. The examples check the principal coordinate kernel and a dependent ZMod 2/ZMod 3 family with distinct residue characteristics and opposite-characteristic nonzero controls.

Minimal primes of finite products (module). For commutative semirings R i and a finite index type, Ideal.mem_minimalPrimes_pi_iff identifies minimal primes over any ideal of the product with unique labelled coordinate minimal primes. Ideal.minimalPrimesPiEquiv gives the corresponding equivalence with the dependent sum of the minimal primes over Ideal.piOrderIso I i. Its inverse is evaluation comap, with forward/comap and evaluation-image laws. The transport theorem Ideal.comap_eval_mem_minimalPrimes_iff works even for infinite index types; it does not classify all primes of an infinite product. No nonempty-index, nontrivial-factor, proper-base-ideal or ring assumptions are needed. Equal factors retain distinct coordinate labels.

Minimal primes and radical membership detected by localization (module). In a commutative semiring R, an element belongs to I.radical exactly when its canonical image belongs to the radical of the extension of I in Localization.AtPrime q for every minimal prime q over I (Ideal.mem_radical_iff_forall_minimalPrimes_localization). The unit ideal is included. The natural-number client shows that 2 passes these tests for (4) despite not belonging to (4), while 1 fails. For commutative semirings R, A with [Algebra R A], a prime ideal q and [IsLocalization.AtPrime A q], any ideal I also satisfies (I.map (algebraMap R A)).radical = q.map (algebraMap R A) iff q ∈ I.minimalPrimes. No separate I ≤ q is needed. Mathlib supplies the implication from minimality.

Multipliers outside a minimal prime (module). For ideals I, q in a commutative semiring, q ∈ I.minimalPrimes and x ∈ q imply ∃ s ∉ q, s * x ∈ I.radical. Over the zero ideal, the product is nilpotent.

Ideal contraction and positive powers in the image (ideals, prime spectra). For a homomorphism from a semiring R to a commutative semiring S, suppose every x : S has some positive power in Set.range f. Then I.comap f ≤ J.comap f ↔ I ≤ J for arbitrary I and radical J. For every target ideal I, Ideal.radical_map_comap_of_pos_pow_mem_range also gives (Ideal.map f (Ideal.comap f I)).radical = I.radical. The map may have any type with FunLike and RingHomClass instances, in an independent universe. No surjectivity, uniform exponent or radicality of I is assumed. For commutative semirings on both sides and a bundled homomorphism, PrimeSpectrum.isEmbedding_comap_of_pos_pow_mem_range proves that the existing PrimeSpectrum.comap f is a topological embedding, with independent source and target universes. Its image need not be closed or the whole spectrum.

Dimension under field extension. For fields K and L, a given [Algebra K L], and a commutative K-algebra A with [Algebra.FiniteType K A], the field-extension leaf proves Algebra.ringKrullDim_tensorProduct_of_finiteType: ringKrullDim (A ⊗[K] L) = ringKrullDim A. All three types may lie in independent universes. The extension need not be algebraic, and A need not be a domain, reduced or nontrivial. Dimension takes values in WithBot ℕ∞; the zero algebra has dimension ⊥.

Dimension under integral maps (module). For integral maps f : R →+* S of commutative rings, target Krull dimension is at most source dimension, with equality if f is injective. Without injectivity, ringKrullDim S = ringKrullDim (R ⧸ RingHom.ker f). A faithful integral algebra has equal source and target dimensions using its given algebra structure. Dimensions lie in WithBot ℕ∞, including zero rings and infinite dimension.

Closed-locus dimension bound for ideals containing a non-zero-divisor (module). For a commutative semiring R, PrimeSpectrum.krullDim_zeroLocus_add_one_le_of_exists_mem_nonZeroDivisors states that Order.krullDim (PrimeSpectrum.zeroLocus (J : Set R)) + 1 ≤ ringKrullDim R whenever ∃ a ∈ J, a ∈ nonZeroDivisors R. Addition is in WithBot ℕ∞, so empty loci retain dimension bottom and infinite dimensions are included. The finite-bound API PrimeSpectrum.krullDimLE_zeroLocus_of_exists_mem_nonZeroDivisors also gives dimension at most n under [Ring.KrullDimLE (n + 1) R]. The canonical closed locus carries the inherited spectrum order. No prime element, principal or prime ideal, domain, unique factorization, ring, Noetherian, properness or nonempty-locus assumption is imposed. Neither form asserts equality or exact dimension subtraction. For commutative rings, Mathlib's quotient-spectrum order isomorphism identifies the same locus with the spectrum of R ⧸ J; arbitrary semiring ideal quotients are not asserted.

Dimension from irreducible generators of prime ideals (module). In any commutative semiring, if every nonzero nonmaximal prime ideal is generated by an irreducible element, Ring.krullDimLE_two_of_forall_exists_irreducible_span_eq gives Ring.KrullDimLE 2 R. No domain, unique factorization, ring or Noetherian assumption is required, and irreducible elements need not be prime.

Height and dimension of pointwise products (module). In arbitrary preorders, Order.height_pi and Order.coheight_pi express the ranks of a section of a finite dependent product as sums of its coordinate ranks in ℕ∞, including infinite ranks and rank zero for an empty index. For arbitrary dependent products, Order.height_pi_eq_iSup_finset and Order.coheight_pi_eq_iSup_finset give the supremum of finite coordinate-rank sums, with no finite-support hypothesis. Order.krullDim_pi_eq_iSup_range_restrict expresses the dimension of an arbitrary dependent product as the supremum of its finite restriction-image dimensions, retaining empty images when the full product is empty. The binary formulas are Order.height_prod and Order.coheight_prod. Order.krullDim_prod and Order.krullDim_pi give the dimension of binary and finite dependent products as the sum of the factor dimensions in WithBot ℕ∞. Empty factors give bottom even alongside infinite dimension; an empty-index product has dimension zero. No nonemptiness, finite-dimension or antisymmetry hypothesis is required. These concern canonical pointwise orders, not lexicographic or topological products.

All-dimension bounds after deleting boundary points (module). For any preorder α : Type u, Order.krullDim_not_isMin_add_one_le states Order.krullDim {x : α // ¬ IsMin x} + 1 ≤ Order.krullDim α. The dual Order.krullDim_not_isMax_add_one_le gives the same bound for the nonmaximal locus. The original-interior bound Order.krullDim_not_isMin_not_isMax_add_two_le states Order.krullDim {x : α // ¬ IsMin x ∧ ¬ IsMax x} + 2 ≤ Order.krullDim α. Both predicates are tested in the original preorder, with canonical inherited subtype orders. Dimensions and addition lie in WithBot ℕ∞: ⊥ + k = ⊥ and ⊤ + k = ⊤ for the finite shifts. There is no antisymmetry, inhabitation, finite-dimension, finite-carrier or chain-condition assumption. The shifts are sharp on two- and three-point chains. Empty types and antichains show why these are not unconditional equalities; infinite dimension precludes a strict-drop assertion. This generic order API is a Mathlib-upstream candidate.

Finite dimension bounds after deleting boundary points (module). For any preorder α : Type u and n : ℕ, Order.krullDimLE_succ_iff_not_isMin states Order.KrullDimLE (n + 1) α ↔ Order.KrullDimLE n {x : α // ¬ IsMin x}. The dual theorem Order.krullDimLE_succ_iff_not_isMax gives the same equivalence after deleting maximal points. Their composition, Order.krullDimLE_add_two_iff_not_isMin_not_isMax, states Order.KrullDimLE (n + 2) α ↔ Order.KrullDimLE n {x : α // ¬ IsMin x ∧ ¬ IsMax x}. Both predicates refer to the original preorder, and the subtypes carry its inherited order. No antisymmetry, inhabitation, bottom, top, finite-carrier or chain-condition assumption is needed. These are finite-bound equivalences, not unconditional exact dimension subtraction; empty types and antichains are included.

Comparison in dimension at most two (order, prime ideals). In a preorder with [Order.KrullDimLE 2 α], if x ≤ y, ¬ IsMin x and ¬ IsMax y, then y ≤ x; equality needs antisymmetry. In a commutative semiring with [Ring.KrullDimLE 2 R], a nonmaximal prime ideal I containing a prime element a ∈ nonZeroDivisors R equals Ideal.span {a}. No unique factorization, global no-zero-divisors, ring or Noetherian hypothesis is required.

Prime ideals in dimension-two unique factorization semirings (module). In a commutative semiring with [UniqueFactorizationMonoid R] and [Ring.KrullDimLE 2 R], every nonzero nonmaximal prime ideal is the span of an irreducible element. Every prime is therefore zero, irreducible-principal, or maximal; the alternatives may overlap. No ring, Noetherian, normalization or global nontriviality hypothesis is required.

When a prime localization is a field (module). For commutative semirings R, A with their given R-algebra structure, any prime q and [IsLocalization.AtPrime A q] satisfy IsField A ↔ q ∈ minimalPrimes R ∧ IsReduced A. Reducedness of R gives the reduced-base corollary: arbitrary localization preserves reducedness. For semirings IsField includes semifields.

Principal prime witnesses and contraction (module). In a commutative semiring, a proper principal ideal avoids at least one of two relatively prime (IsRelPrime) elements. In a commutative semiring with unique factorization, every nonunit, including zero, belongs to a principal prime ideal with this disjunctive avoidance. No normalization or nonzero assumption is needed. Contraction from any semiring gives a prime two-sided source ideal, not necessarily a principal ideal.

Minimal primes of a principal ideal (module). For [CommSemiring R], [UniqueFactorizationMonoid R], the caller's [NormalizationMonoid R] and f ≠ 0, the minimal primes over (f) are exactly the principal ideals generated by normalized irreducible factor values. Their factor equivalence sends p to span {p}; multiplicities do not add primes.

Irreducible components of a principal zero locus (module). Under those same semiring, factorization, normalization and nonzero hypotheses, the factor values are equivalent to the order-dual subtype of irreducible components of the subspace V((f)) in PrimeSpectrum R. This is an Equiv, not an order-equivalence or homeomorphism, and does not classify arbitrary ideals.

Associated primes of a principal quotient (module). For every f in a commutative ring with unique factorization, associatedPrimes R (R ⧸ Ideal.span {f}) = (Ideal.span {f}).minimalPrimes, using base-ring R scalars. No normalization, nonzero or Noetherian hypothesis is needed; the zero ring is included.

Scalar restriction and quotient points (scalar restriction, quotients). Colon ideals of arbitrary submodules contract under compatible algebra/module towers with commutative source and semiring target. Associated primes of a compatible module contract along algebra maps of commutative semirings and reflect along surjective ones. For every principal quotient of a commutative ring with unique factorization, quotient-spectrum associated points and exact singleton-annihilator criteria correspond by ideal comap to minimal primes over the generator.

Height of a principal prime (module). In a commutative ring with [WfDvdMonoid R] and Prime p, span {p} has height at most one. Its height is one if p ∈ nonZeroDivisors R, in particular in a domain. This uses well-founded strict divisibility, not a Noetherian or UFM assumption, and concerns prime generators, not arbitrary principal ideals.

Descending prime chains at finite initial height (order, prime chains). In a preorder, finite ambient height of x makes the strict order on Set.Iic x well-founded. An antitone spectrum sequence over a commutative semiring with finite initial ambient height stabilizes. So does an antitone ideal sequence over a commutative ring when every term is prime and the initial ideal has Ideal.FiniteHeight. One common index gives both tail constancy and the all-index ideal infimum; no global dimension or chain-condition hypothesis is added. Spectrum height is not height in the full lattice of ideals.

Zero-dimensional Zariski spectra (module). For any commutative semiring, T₁ and Hausdorffness of PrimeSpectrum R are each equivalent to Ring.KrullDimLE 0 R, including the empty spectrum; under this bound all basic opens are clopen. Mathlib supplies total separation and total disconnectedness from the Hausdorff spectrum. For a reduced, nontrivial commutative ring, this bound and preconnectedness of its spectrum imply IsField R.

Non-zero-divisor loci of germs

For an arbitrary filter D and a monoid with zero M, the non-zero-divisor criteria identify intrinsic left, right and two-sided non-zero-divisors of Filter.Germ D M with eventual coordinate membership in the corresponding submonoids of M. The index and coefficient universes are independent; improper filters, empty indices and trivial monoids are included. These are zero-annihilator criteria, not full multiplicative cancellation criteria. The generic API is a Mathlib-upstream candidate.

TheoremIrreducible closed rectangles and topological product dimensions#

For spaces X : Type u and Y : Type v with their given topologies, topologicalKrullDim_prod states

topologicalKrullDim (X × Y) = topologicalKrullDim X + topologicalKrullDim Y

For ι : Type w, [Fintype ι] and given topological fibres Y : ι → Type u, topologicalKrullDim_pi gives topologicalKrullDim (∀ i, Y i) = ∑ i, topologicalKrullDim (Y i). These use the canonical topological product and ordinary dependent product, with values in WithBot ℕ∞. Empty factors give bottom, and empty index gives zero. No separation, sobriety, Noetherianity, nonemptiness, finite dimension or attainment is assumed. There is no arbitrary-infinite-index dimension sum, and these are not assertions about scheme fibre-product Zariski topologies or lexicographic orders.

The irreducible-closed product module provides set-level product irreducibility and the arbitrary-index classification closure S = Set.pi Set.univ (fun i => closure (Function.eval i '' S)) for irreducible S. The binary version needs only preirreducibility and includes empty S. Its canonical irreducible closed products have the set-product and set-rectangle carriers. TopologicalSpace.IrreducibleCloseds.prodOrderIso and piOrderIso send a closed irreducible set to the closures of its projection images, with the canonical rectangles as inverses. The dependent-product classification and order isomorphism allow arbitrary index types, and nonemptiness for factor recovery comes from the factor sets themselves. The dimension formulas reuse this library's pointwise product-order dimension formulas.

Quoted from the headline results in README.md of FormalFrontier/minimal-primes at commit 45952e34, Apache-2.0.

Lean

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

Sources
LeantopologicalKrullDim_prod

Topological dimension under inducing maps and covers

The inducing-map and open-cover module proves Topology.IsInducing.topologicalKrullDim_eq: an inducing surjection between independently universed spaces with their given topologies preserves dimension in WithBot ℕ∞. The map need not be injective, and no separation, sobriety, finiteness or nonemptiness assumption is needed.

The same module proves topologicalKrullDim_eq_iSup_of_isOpenEmbedding_cover: the dimension of a space is the supremum of the dimensions of any jointly surjective family of open-embedding charts, with independent universes for the space, index type and chart domains. Its open-subspace form, topologicalKrullDim_eq_iSup_of_isOpen_cover, applies to any family of open sets whose union is the whole space, with their induced topologies. Both equalities use WithBot ℕ∞, including bottom for an empty-index cover of the empty space and infinite or unbounded dimensions. No separation, sobriety, Noetherianity, quasi-compactness, finiteness or nonemptiness assumption is needed.

For ι : Type u, X : Type v, Y : ι → Type w, and I : Finset ι, topologicalKrullDim_le_iSup_of_isInducing_finset_cover states

topologicalKrullDim X ≤
  ⨆ J ∈ I.powerset, ⨆ (_ : J.Nonempty),
    (∑ i ∈ J, topologicalKrullDim (Y i)) + ((J.card - 1 : ℕ) : WithBot ℕ∞)

The hypotheses are ∀ i ∈ I, Topology.IsInducing (f i) and ∀ x : X, ∃ i ∈ I, ∃ y : Y i, f i y = x for f : ∀ i, Y i → X. All original topologies are retained, with independent index, ambient and domain universes. No global finiteness of the index, injectivity, separation, sobriety, Noetherianity, nonemptiness, finite dimension or attaining chain is assumed. Empty families give bottom, and mixed empty pieces are handled by the supremum over subfamilies. Subtraction is in ℕ before casting. The two point subspaces of Sierpiński space show that a maximum bound is false and the additive penalty is sharp. The order-theoretic finite-cover bound supplies the powerset expression.

The characteristic lemmas TopologicalSpace.IrreducibleCloseds.map_le_map_iff_of_isInducing and TopologicalSpace.IrreducibleCloseds.mem_range_map_iff_of_isInducing concern Mathlib's existing closure-image map, not a different map. For inducing f, it reflects inclusion, and an ambient irreducible closed Z belongs to its range exactly when closure ((Z : Set X) ∩ Set.range f) = (Z : Set X). These properties apply to noninjective maps and identify the chart orders used in the finite-cover bound.

Topological dimension on closed covers, components and point closures

The closed-cover leaf proves topologicalKrullDim_eq_iSup_of_isClosedEmbedding_cover: the dimension is the supremum of the dimensions of the given domains of a jointly surjective family of closed embeddings, provided the original indexed family of images is locally finite. The ambient, index and domain universes are independent. Its closed-subspace form, topologicalKrullDim_eq_iSup_of_locallyFinite_isClosed_cover, uses the ordinary membership subtypes with their induced topologies. Both equalities are in WithBot ℕ∞, including empty covers and unbounded dimensions, without separation, sobriety, Noetherianity, quasi-compactness, nonemptiness or attainment assumptions.

The same module proves topologicalKrullDim_eq_iSup_irreducibleComponents: for any given topological space X, its dimension equals ⨆ C : irreducibleComponents X, topologicalKrullDim (C : Set X). The index is the membership subtype of Mathlib's canonical set of components; each component carries its ordinary induced subspace topology. No local finiteness, Noetherianity, separation or sobriety assumption is imposed. The empty space has dimension ⊥, and the supremum can be unbounded without being attained.

For any X : Type u with [TopologicalSpace X] [QuasiSober X], the same module proves topologicalKrullDim_eq_iSup_closure_singleton: topologicalKrullDim X = ⨆ x : X, topologicalKrullDim (closure ({x} : Set X)). The index is every original point; each closure uses the original topology and its induced subspace topology. No T0 separation, Noetherianity, nonemptiness or local finiteness is assumed. The WithBot ℕ∞ supremum is bottom for the empty space and includes infinite and unbounded dimensions without requiring attainment.

The same module proves topologicalKrullDim_eq_iSup_connectedComponents: for arbitrary X : Type u with its given topology, its dimension equals ⨆ C : ConnectedComponents X, topologicalKrullDim ((ConnectedComponents.mk : X → ConnectedComponents X) ⁻¹' {C}). The index is Mathlib's canonical quotient of connected components. Each fibre is a membership subspace of the original X, with its induced topology, not a subspace of the quotient. Connected components partition the points, unlike irreducible components, which may intersect. No local finiteness, local connectedness or discrete quotient is assumed; empty spaces give ⊥, and unbounded suprema need not be attained.

The supporting containment theorem applies to any irreducible set, not necessarily closed. The characteristic range theorem for the existing IrreducibleCloseds.map and closed-embedding height invariance use the canonical inclusion orders. Mathlib supplies canonical components, their closedness and whole-irreducible-set extension.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.