Skip to content

Dedekind ideal arithmetic

Reusable ideal arithmetic, module indices and intrinsic heights of normed invertible modules over rings of integers. Ideal-norm comparisons, principal-prime extraction and class-group localization sit alongside finite section quotients, common scalar multiples, integral-section heights and normalized logarithmic heights, with tensor-product, positive metric-rescaling and equivalence-pullback formulas. Rational frames evaluate the same intrinsic height through coefficient-ideal norms and weighted archimedean products. Nonzero fractional-ideal norms factor as finite-support prime-norm products with signed exponents; over number fields, negative coefficient-ideal exponents give the finite-place numerator of height. Supplied frames extend to linear coordinates over semiring algebras. Over an infinite Dedekind domain with finite quotients, invertible modules have canonical definite ultrametric seminorms on their adic fibres, characterized in every rational frame by the residue cardinality raised to the signed coefficient-ideal count, times the coordinate norm. Principal fractional-ideal counts determine scalar adic valuations and residue-cardinality completion norms. Rank-one seminorm scalar extension, relative-degree formulas for weighted infinite-place products, fractional-ideal norm extension and isometric completion maps supply further interfaces.

Quoted from the project description in formalization.yaml of FormalFrontier/dedekind-ideal-arithmetic at commit c7630759, Apache-2.0.

5 articles: 5 for highlights of its formalization.yaml whose declarations the scan finds. The headline results in its README are quoted where they stand.

Facts

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

  • Repository: FormalFrontier/dedekind-ideal-arithmetic, read at commit c7630759 (2026-11-05).
  • Lean toolchain v4.34.0-rc2, Mathlib at 83abb3e7.
  • License: Apache-2.0.
  • Authors: Formal Frontier Agents.
  • Review status: “agent-reviewed”.
  • Review notes: “AI agents reviewed the ideal-norm, principal-prime and localization results; no human review is claimed.”
  • Automation: agent; framework “AI agents using Lean and Lake”; tool setup “AI agents composed Lean proofs using mathlib APIs and ordinary tactics such as rw, simp, constructor, congr, by_cases and typeclass inference. Toolchain and dependency revisions are pinned by the repository's Lean/Lake files.”
  • Automation notes: “AI agents authored the Lean proofs and documentation. AI involvement does not itself establish origin, correctness or rights.”

Literature

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

  • The K-book: An Introduction to Algebraic K-theory, Charles A. Weibel, Complete-book build dated 2013-08-29, Chapter I, section 3 (book; background).
  • Ideal class groups under localization of Dedekind domains (folklore; independently-proves).
  • Abelian Varieties, J. S. Milne, IV section 6, 6.2–6.3 (book; background).

Builds on

No other Formal Frontier library.

Highlights

TheoremIdeal norms, factorization and principal primes#

In an infinite commutative Dedekind domain with finite quotients, a nonzero smaller ideal has strictly larger absolute norm, and nested ideals of equal absolute norm coincide. Over a Dedekind domain finite free over the integers, each nonzero fractional-ideal norm is the finite-support product of height-one prime norms raised to signed integer exponents; the fraction field needs no number-field structure. In an infinite Dedekind domain finite free over the integers, a supplied element with prime absolute algebraic norm yields a principal prime above that rational prime. Over any Dedekind domain and fraction field, a nonzero fractional ideal contains a nonzero element whose principal ideal attains the same signed exponent at a fixed height-one prime; the ideal need not be principal.

Quoted from the highlights in formalization.yaml of FormalFrontier/dedekind-ideal-arithmetic at commit c7630759, Apache-2.0.

Lean

Read from the source at commit c7630759, without running Lean.

Sources
LeanIdeal.absNorm_lt_absNorm_of_lt · Ideal.eq_of_le_of_absNorm_eq · FractionalIdeal.absNorm_eq_finprod_count · FractionalIdeal.exists_mem_count_spanSingleton_eq · Ideal.exists_principal_prime_over_of_norm_natAbs_eq

TheoremClass groups under localization#

Class extension is surjective for torsion-free localizations of Dedekind domains, and a supplied class generator killed by extension makes the target a principal ideal ring and a unique factorization domain.

Quoted from the highlights in formalization.yaml of FormalFrontier/dedekind-ideal-arithmetic at commit c7630759, Apache-2.0.

Lean

Read from the source at commit c7630759, without running Lean.

Sources
LeanClassGroup.extendedHom_surjective_of_isLocalization · ClassGroup.isPrincipalIdealRing_of_generator_of_isLocalization · ClassGroup.uniqueFactorizationMonoid_of_generator_of_isLocalization

TheoremSection indices and rational-frame coordinates#

Nonzero sections of invertible modules over commutative domains with finite quotients span finite-index submodules; any two nonzero sections of one invertible module over a commutative domain admit a common nonzero scalar multiple. A supplied frame on K tensor_R M extends to an F-linear coordinate on F tensor_R M through compatible algebras over commutative semirings R and K, with F not required commutative, without finiteness or norm hypotheses. A finitely generated module with a supplied frame over a fraction field has a nonzero coefficient fractional ideal; torsion-freeness makes the coefficient map injective, but is not required to construct the ideal.

Quoted from the highlights in formalization.yaml of FormalFrontier/dedekind-ideal-arithmetic at commit c7630759, Apache-2.0.

Lean

Read from the source at commit c7630759, without running Lean.

Sources
LeanModule.Invertible.finite_quotient_span_singleton · Module.Invertible.exists_nonzero_smul_eq · LinearEquiv.fibreCoordinate · LinearEquiv.coefficientIdeal · LinearEquiv.coefficientMap_injective

TheoremIntrinsic heights of normed invertible modules#

For a number field K, definite seminorms on the archimedean completion fibres of an invertible module over its ring of integers define a positive height equal to the section index divided by the weighted norm product for every nonzero integral section. Ordinary norms have weight one at real places and two at complex places. The normalized logarithmic height is (log index minus the weighted log norm sum) divided by [K:Q]. Tensor metrics multiply heights and add logarithmic heights. Positive placewise rescaling divides height by the weighted factor and subtracts its degree-normalized logarithm; equivalence pullback preserves both heights. Every rational frame evaluates this same height as the reciprocal of the product of its coefficient-ideal norm and the weighted archimedean product at its unit vector. Equivalently, the numerator is the finite-support product of residue cardinalities with negative coefficient-ideal exponents, with no extra finite-place weights. No integral basis is assumed, and only logarithmic height is divided by [K:Q].

Quoted from the highlights in formalization.yaml of FormalFrontier/dedekind-ideal-arithmetic at commit c7630759, Apache-2.0.

Lean

Read from the source at commit c7630759, without running Lean.

Sources
LeanNumberField.ArchimedeanNorms.height_eq · NumberField.ArchimedeanNorms.height_pos · NumberField.ArchimedeanNorms.normalizedLogHeight_eq · NumberField.ArchimedeanNorms.height_tensor · NumberField.ArchimedeanNorms.height_rescale · NumberField.ArchimedeanNorms.height_comap · NumberField.ArchimedeanNorms.height_eq_rationalFrame · NumberField.ArchimedeanNorms.normalizedLogHeight_eq_rationalFrame · NumberField.ArchimedeanNorms.height_eq_finitePlace

DefinitionAdic fibre seminorms and integral spans#

Let R be an infinite Dedekind domain with finite quotients, K its fraction field, p a height-one prime and F = p.adicCompletion K with its selected residue-cardinality norm. An invertible R-module M has a canonical definite ultrametric F-seminorm on F tensor_R M. For every rational frame e and every fibre vector x, its value is q raised to FractionalIdeal.count K p e.coefficientIdeal times the norm of e.fibreCoordinate F x, where q is the residue cardinality. The signed count appears with a plus sign, in contrast to the finite-place height factor. The seminorm is frame-independent and uniquely determined by this weight at the image of e.symm 1. On M = R the whole seminorm is the completion norm composed with the tensor right-unit equivalence; the same vector 1 tensor 1 has value one in every scalar frame. The supplied-frame constructor only needs a finitely generated module and a rational frame, not integral invertibility, freeness or torsion-freeness. No number-field structure, finite-free presentation over the integers, norm on K or norm or metric instance on a fibre is required. Over any Dedekind domain and fraction field, the valuation-integer span of integral sections is the image of the integer tensor fibre and spans the whole field fibre. It is finite for a finite module; flatness makes the image map an equivalence, and the scalar model identifies the whole span with the valuation-integer ring. These algebraic statements need no norm, infinite-ring or finite-quotient hypothesis.

Quoted from the highlights in formalization.yaml of FormalFrontier/dedekind-ideal-arithmetic at commit c7630759, Apache-2.0.

Lean

Read from the source at commit c7630759, without running Lean.

Sources
LeanModule.adicIntegralSpan · Module.adicIntegralSpanEquiv · Module.mem_adicIntegralSpan_self_iff · LinearEquiv.adicSeminorm · Module.adicSeminorm · Module.adicSeminorm_apply · Module.adicSeminorm_unique · Module.adicSeminorm_add_le_max · Module.adicSeminorm_self

Headline results

Quoted from the headline results in README.md of FormalFrontier/dedekind-ideal-arithmetic at commit c7630759, Apache-2.0.

Norm detects strict ideal inclusion and equality. In an infinite commutative Dedekind domain with finite quotients, I < J and I ≠ ⊥ imply J.absNorm < I.absNorm. If I ≤ J and the norms agree, I = J, including zero ideals. No finite-free presentation over ℤ is needed. See strict comparison and equality.

A supplied prime-norm element yields a principal prime. In an infinite Dedekind domain finite free over ℤ, a natural prime p and a supplied α with (Algebra.norm ℤ α).natAbs = p give a principal prime above (p). This is conditional existence, not a search for α, a class-number computation or a witness assertion for every prime. See principal-prime extraction.

Localization can kill the class group and give a PID/UFD. For Dedekind domains A, B in possibly different universes, an A-algebra B torsion-free over A, and IsLocalization M B, extension Cl(A) → Cl(B) is surjective. If every source class is an integral power of a supplied g and g extends to one, the library gives a PID and hence a UFD. Surjectivity needs no generator; neither class group need be finite.

Section indices and common multiples. Over a domain, scaling a nonzero section of a torsion-free module multiplies its quotient index by the principal left-ideal index, including zero scalars and infinite quotients. Invertible modules over commutative domains with finite quotients have finite quotients by nonzero sections; over any commutative domain their nonzero sections admit common nonzero scalar multiples. See module indices.

Intrinsic heights of normed invertible modules. Over 𝓞 K for a number field K, definite seminorms on all archimedean fibres give a positive, section-independent height: quotient index divided by the weighted norm product. Invertibility, not integral freeness, is assumed. Tensor products, positive rescaling and integral-equivalence pullback obey the expected multiplicative and logarithmic laws. The normalized logarithmic height can be negative. See module heights and the height guide.

Rational-frame and finite-place height formulas. Every rational frame evaluates this same intrinsic height as 1 / (N(I) * archimedeanProduct). Nonzero fractional-ideal norms factor into prime norms with signed exponents over Dedekind domains finite free over ℤ, without a number-field structure on the fraction field. For number fields the height numerator uses residue cardinalities with negative coefficient-ideal counts. See fractional norms and finite-place height factors.

Principal exponents determine scalar completion norms. Over a Dedekind domain and fraction field, a nonzero scalar has adic valuation equal to the exponential of its negative principal-ideal count. For an infinite base with finite quotients, its completion norm is the residue cardinality to that negative count. No norm on bare K is chosen. See adic norms.

Sharp signed fractional-ideal exponents. At each fixed height-one prime of any Dedekind domain, a nonzero fractional ideal contains a nonzero element attaining its signed count. Together with Mathlib's count_mono, this is an attained minimum. The witness may depend on the prime; no principality, infinite-ring, finite-residue or ℤ-freeness hypothesis is needed. See count attainment.

Algebraic integral spans in adic fibres. For any R-module M over a Dedekind domain with fraction field K and height-one prime p, the span of 1 ⊗ m over the valuation integers in F ⊗[R] M, F = p.adicCompletion K, is the image of O ⊗[R] M, O = p.adicCompletionIntegers K. It is finite over O if M is finite, and spans the whole fibre over F; flatness makes the image map an equivalence onto the span. For M = R, the whole span corresponds exactly to O. No finite-residue or infinite-ring hypothesis is used. See integral spans.

Canonical ultrametric seminorms on adic fibres. For an infinite Dedekind domain R with finite quotients, fraction field K, height-one prime p and invertible M, the fibre F ⊗[R] M has a canonical definite F-seminorm. In every rational frame, on every vector, it is the coordinate norm times the residue cardinality raised to the signed coefficient-ideal count, with a plus sign; negative counts are included. It is frame-independent and characterized by its rational-unit-vector weight. The supplied-frame constructor only needs finite M and a frame, allowing torsion. For M = R the whole seminorm is the completion norm pulled back along tensor right-unit equivalence. See adic seminorms.

Main results

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