Main results

The main results that the formalization.yaml of FormalFrontier/dedekind-ideal-arithmetic lists under status.main_results at commit c7630759, each that the scan finds declared in the file the yaml gives, with its line. They are listed here, not made articles: in several Formal Frontier libraries this list is close to the whole API. The notes are the yaml's.

Declaration	Kind	Where	Note
FractionalIdeal.exists_mem_count_spanSingleton_eq	theorem	DedekindIdealArithmetic/Ideal/CountAttainment.lean, line 84	Over any Dedekind domain and fraction field, a nonzero fractional ideal has a nonzero member whose principal fractional ideal attains its signed exponent at a fixed height-one prime. The witness may depend on the prime; no principality, infinite-ring, finite-quotient or number-field hypothesis is required.
Module.adicIntegralSpan	def	DedekindIdealArithmetic/Module/AdicIntegralSpan.lean, line 49	For any module over a Dedekind domain and fraction field, the span over O = p.adicCompletionIntegers K of all sections in the algebraic adic fibre is the range of adicIntegralSpanMap. It is finite over O when M is finite over R, and its span over the completion field is the whole fibre. No norm or arithmetic-finiteness hypothesis is used.
Module.adicIntegralSpanEquiv	def	DedekindIdealArithmetic/Module/AdicIntegralSpan.lean, line 122	For a flat R-module M, the canonical map from O tensor_R M is an O-linear equivalence onto its integral span. Invertibility supplies flatness through Mathlib's projective-module instances.
Module.mem_adicIntegralSpan_self_iff	theorem	DedekindIdealArithmetic/Module/AdicIntegralSpan.lean, line 140	On every vector of the scalar fibre, membership in the integral span is exactly valuation-integrality of its coordinate under the tensor right-unit equivalence, not merely a statement at one pure tensor.
LinearEquiv.adicSeminorm	def	DedekindIdealArithmetic/Module/AdicSeminorm.lean, line 73	For an infinite Dedekind domain R with finite quotients, fraction field K, height-one prime p and finitely generated R-module M with a supplied rational frame e, construct an F-seminorm on F tensor_R M, where F = p.adicCompletion K. It is definite, ultrametric and independent of the supplied frame. No integral invertibility, freeness or torsion-freeness of M, number-field structure on K or finite-free presentation over the integers is assumed.
Module.adicSeminorm	def	DedekindIdealArithmetic/Module/AdicSeminorm.lean, line 205	For Module.Invertible R M under the same ring and field hypotheses, this is the canonical adic fibre seminorm, without a supplied frame or additional metric data. It agrees with the supplied-frame construction in every rational frame. The construction uses A = WithAbs (NumberField.HeightOneSpectrum.adicAbv K p), proves NormedAlgebra A F using the norm-preserving algebra map, and reuses Seminorm.extendScalarsRankOne followed by F-linear base-change cancellation. No norm or metric instance is installed on K or a fibre.
Module.adicSeminorm_apply	theorem	DedekindIdealArithmetic/Module/AdicSeminorm.lean, line 221	For every rational frame e and every x in F tensor_R M, the value is (Ideal.absNorm p.asIdeal : ℝ) raised to FractionalIdeal.count K p e.coefficientIdeal, times the norm of e.fibreCoordinate F x. The count is signed and occurs with a plus sign. Pure-tensor, integral-section and rational-fibre evaluations are also provided; on the rational fibre the scalar factor is NumberField.HeightOneSpectrum.adicAbv K p (e x).
Module.adicSeminorm_unique	theorem	DedekindIdealArithmetic/Module/AdicSeminorm.lean, line 264	Among F-seminorms, the coefficient-ideal weight at the image of e.symm 1 uniquely determines the canonical seminorm. That image has value q raised to FractionalIdeal.count K p e.coefficientIdeal, where q is the residue cardinality.
Module.adicSeminorm_eq_zero_iff	theorem	DedekindIdealArithmetic/Module/AdicSeminorm.lean, line 275	The canonical seminorm vanishes exactly at the zero fibre vector. Definiteness is a conclusion of the construction, not extra data.
Module.adicSeminorm_add_le_max	theorem	DedekindIdealArithmetic/Module/AdicSeminorm.lean, line 282	On all adic fibre vectors x and y, N(x + y) is at most max(N(x), N(y)). As an F-seminorm it also satisfies N(a smul x) = norm(a) * N(x) for every a in F.
Module.adicSeminorm_self	theorem	DedekindIdealArithmetic/Module/AdicSeminorm.lean, line 304	On the scalar module M = R, the entire canonical seminorm is normSeminorm F F composed with the tensor right-unit equivalence, not merely an equality on integral pure tensors. The same integral vector 1 tensor 1 has value one in every rational frame; its coefficient-ideal weight cancels its coordinate norm.
IsDedekindDomain.HeightOneSpectrum.valuation_eq_exp_neg_count_spanSingleton	theorem	DedekindIdealArithmetic/Ideal/AdicNorm.lean, line 42	For any Dedekind domain R, fraction field K, height-one prime p and nonzero a, p.valuation K a is the exponential of the negative count of the principal fractional ideal generated by a. No finite-quotient or finite-free-over-integers assumption is required.
IsDedekindDomain.HeightOneSpectrum.norm_algebraMap_eq_zpow_neg_count_spanSingleton	theorem	DedekindIdealArithmetic/Ideal/AdicNorm.lean, line 96	With R infinite and having finite quotients, the norm of a nonzero scalar in p.adicCompletion K is the residue cardinality raised to its negative principal fractional-ideal count. The positive count weight therefore cancels the norm; no norm on K is chosen.
LinearEquiv.scalarExtensionCoordinate	def	DedekindIdealArithmetic/Module/TensorCoordinates.lean, line 33	A supplied linear coordinate M equiv_R R extends to an F-linear coordinate on F tensor_R M over a semiring algebra. Its pure-tensor and inverse formulas hold without finiteness or norm hypotheses.
LinearEquiv.fibreCoordinate	def	DedekindIdealArithmetic/Module/CoefficientIdeal.lean, line 110	A frame on K tensor_R M induces an F-linear coordinate on F tensor_R M through compatible scalar towers over commutative semirings R and K and a semiring F. Pure-tensor, rational-fibre, inverse, frame-change and whole-equivalence unit formulas require no arithmetic, module finiteness, torsion-free, invertibility or norm hypotheses.
Ideal.absNorm_lt_absNorm_of_lt	theorem	DedekindIdealArithmetic/Ideal/AbsNorm.lean, line 29	In an infinite commutative Dedekind domain with finite quotients, strict inclusion with nonzero smaller ideal strictly reverses absolute norms. The nonzero hypothesis is not omitted.
Ideal.eq_of_le_of_absNorm_eq	theorem	DedekindIdealArithmetic/Ideal/AbsNorm.lean, line 42	Under the same ambient hypotheses, nested ideals with equal absolute norm are equal, including the zero-ideal case.
Ideal.exists_principal_prime_over_of_norm_natAbs_eq	theorem	DedekindIdealArithmetic/Ideal/PrincipalPrime.lean, line 27	In an infinite commutative Dedekind domain finite free over the integers, a supplied element with prime absolute algebraic norm yields a principal prime above that rational prime. The element and norm equality are hypotheses, not outputs.
ClassGroup.extendedHom_surjective_of_isLocalization	theorem	DedekindIdealArithmetic/ClassGroup/Localization.lean, line 37	For Dedekind domains A and B with B an A-algebra torsion-free as an A-module and a localization at M, class extension is onto. No injectivity or finiteness of either class group is asserted.
ClassGroup.isPrincipalIdealRing_of_generator_of_isLocalization	theorem	DedekindIdealArithmetic/ClassGroup/Localization.lean, line 59	With the same localization hypotheses, if every source class is an integral power of a supplied class g and g extends to one, then B is a principal ideal ring. Both generation and killing are inputs.
ClassGroup.uniqueFactorizationMonoid_of_generator_of_isLocalization	theorem	DedekindIdealArithmetic/ClassGroup/Localization.lean, line 81	The same exact hypotheses imply unique factorization in B through the proved principal-ideal-ring criterion.
Submodule.cardQuot_map_of_injective	theorem	DedekindIdealArithmetic/Module/Index.lean, line 44	For an injective linear map f over a ring, the quotient index of p.map f equals p.cardQuot times the quotient index of the range of f, without assuming either quotient finite. For a nonzero section of a torsion-free module over a domain, scalar multiplication multiplies its index by the principal left-ideal index, including zero scalars and infinite quotients. Over an infinite commutative Dedekind domain, the scalar factor is the principal ideal's absolute norm.
Module.Invertible.finite_quotient_span_singleton	theorem	DedekindIdealArithmetic/Module/Index.lean, line 101	Over a commutative domain with finite quotients, the quotient of an invertible module by the span of any nonzero section is finite.
Module.Invertible.exists_nonzero_smul_eq	theorem	DedekindIdealArithmetic/Module/Index.lean, line 122	Any two nonzero sections of an invertible module over a commutative domain admit a common nonzero scalar multiple. No finite-quotient hypothesis or principal presentation is required.
Module.Invertible.cardQuot_span_singleton_tmul	theorem	DedekindIdealArithmetic/Module/Index.lean, line 149	Over a commutative Dedekind domain with finite quotients, for two invertible modules and nonzero sections m and n, the index of the span of m tensor n is the product of their section indices. The ring may be finite and the modules need not be free.
NumberField.ArchimedeanNorms.height_eq	theorem	DedekindIdealArithmetic/NumberField/ModuleHeight.lean, line 141	For a number field K and Module.Invertible (O_K) M, definite seminorms on all vectors of each completion fibre give a positive height equal to cardQuot (span {m}) divided by the weighted norm product for every nonzero integral m. Ordinary unsquared completion norms carry weight one at real places and two at complex places. No integral freeness or stored section-independence premise is assumed.
NumberField.ArchimedeanNorms.normalizedLogHeight_eq	theorem	DedekindIdealArithmetic/NumberField/ModuleHeight.lean, line 170	Under the same height hypotheses, the normalized logarithmic height at every nonzero integral section is (log index minus the weighted logarithmic norm sum) divided by [K:Q] and may be negative. The standard metric on O_K has multiplicative height one and normalized logarithmic height zero.
NumberField.ArchimedeanNorms.height_tensor	theorem	DedekindIdealArithmetic/NumberField/MetricTensorProduct.lean, line 203	For a number field K and invertible O_K-modules M and N with archimedean norms P and Q, (P.tensor Q).height = P.height * Q.height. The tensor metric is defined on every fibre vector and multiplies norms on arbitrary pure tensors of completion-fibre vectors under the canonical base-change comparison. No integral basis is assumed.
NumberField.ArchimedeanNorms.normalizedLogHeight_tensor	theorem	DedekindIdealArithmetic/NumberField/MetricTensorProduct.lean, line 233	Under the same tensor hypotheses, the normalized logarithmic height of P.tensor Q equals the sum of those of P and Q.
NumberField.ArchimedeanNorms.height_rescale	theorem	DedekindIdealArithmetic/NumberField/MetricRescaling.lean, line 126	For a number field K, an invertible O_K-module and positive factors c : InfinitePlace K → ℝ≥0ˣ, rescale multiplies each ordinary fibre norm by c_v. Its height is the original height divided by the product of c_v raised to InfinitePlace.mult v. The multiplicities are one at real places and two at complex places.
NumberField.ArchimedeanNorms.normalizedLogHeight_rescale	theorem	DedekindIdealArithmetic/NumberField/MetricRescaling.lean, line 140	Under the same rescaling hypotheses, normalized logarithmic height is the original value minus the sum of InfinitePlace.mult v times log c_v divided by [K:Q]. Height need not be at least one and logarithmic height need not be nonnegative.
NumberField.ArchimedeanNorms.height_comap	theorem	DedekindIdealArithmetic/NumberField/MetricTransport.lean, line 119	For a number field K, invertible O_K-modules M and N, a metric Q on N and an equivalence e : M ≃ₗ[𝓞 K] N, (Q.comap e).height = Q.height. The source metric is the pullback on every completion fibre; no arbitrary metric change is permitted.
NumberField.ArchimedeanNorms.normalizedLogHeight_comap	theorem	DedekindIdealArithmetic/NumberField/MetricTransport.lean, line 135	Under the same pullback hypotheses, normalized logarithmic height is preserved. Metric pullback itself needs neither module invertible and satisfies the identity and contravariant composition laws.
FractionalIdeal.absNorm_spanSingleton_eq_cardQuot_mul	theorem	DedekindIdealArithmetic/Ideal/FractionalNorm.lean, line 78	For a Dedekind domain finite free over the integers and a fraction field, the principal fractional ideal generated by any element x of a fractional ideal I has norm cardQuot (span {x}) times norm I. Zero ideals and elements are included; infinite indices are zero. No number-field structure on the fraction field is required.
FractionalIdeal.absNorm_eq_finprod_count	theorem	DedekindIdealArithmetic/Ideal/FractionalNorm.lean, line 53	For a Dedekind domain R finite free over the integers and a fraction field F, absNorm I equals the rational finite-support product of Ideal.absNorm p.asIdeal raised to FractionalIdeal.count F p I, over height-one primes p, provided I is nonzero. No NumberField F, Q-algebra structure on F or integral basis is required. At the zero ideal all counts vanish, giving product one rather than norm zero.
NumberField.FinitePlace.absNorm_eq_finprod_count	theorem	DedekindIdealArithmetic/NumberField/FinitePlaceHeight.lean, line 44	For a number field K and a nonzero fractional ideal I, the real cast of absNorm I is the finite-support product over finite places w of q_w raised to FractionalIdeal.count K w.maximalIdeal I, where q_w = Ideal.absNorm w.maximalIdeal.asIdeal is the residue cardinality. The signed exponents use no extra finite-place weights.
NumberField.ArchimedeanNorms.height_eq_finitePlace	theorem	DedekindIdealArithmetic/NumberField/FinitePlaceHeight.lean, line 72	For a number field K, Module.Invertible (O_K) M, archimedean norms P and any rational frame e, P.height equals the finite-support product of residue cardinalities raised to the negatives of the counts of e.coefficientIdeal, divided by the product of P.rationalEval v (e.symm 1) raised to v.mult over infinite places v. Nonzeroness of the coefficient ideal follows from the frame. No integral section, integral basis, new height or further metric data are required. The denominator has weights one at real places and two at complex places; multiplicative height has no degree root.
LinearEquiv.cardQuot_span_singleton_mul_absNorm_coefficientIdeal	theorem	DedekindIdealArithmetic/Module/CoefficientIdealNorm.lean, line 35	A supplied rational frame for a finite torsion-free module over a Dedekind domain finite free over the integers gives, for every section, its span index times the coefficient-ideal norm equal to the principal fractional norm of its coefficient. No invertibility or freeness over the Dedekind domain is assumed.
NumberField.ArchimedeanNorms.normProduct_eq_rationalFrame	theorem	DedekindIdealArithmetic/NumberField/RationalFrameHeight.lean, line 49	In any supplied rational frame, the weighted norm product of every integral section equals the absolute field norm of its coefficient times the weighted rational norm product of the frame unit vector. This needs no finiteness, torsion-freeness or invertibility of the integral module and includes zero sections.
NumberField.ArchimedeanNorms.height_eq_rationalFrame	theorem	DedekindIdealArithmetic/NumberField/RationalFrameHeight.lean, line 74	For a number field and an invertible module over its ring of integers, every supplied rational frame evaluates the existing intrinsic height as the reciprocal of the product of the coefficient-ideal norm and the weighted archimedean norm product of its rational unit vector. No integral basis or second height definition is introduced.
NumberField.ArchimedeanNorms.normalizedLogHeight_eq_rationalFrame	theorem	DedekindIdealArithmetic/NumberField/RationalFrameHeight.lean, line 100	Under the same height hypotheses, normalized logarithmic height is minus the logarithm of the coefficient-ideal norm and the weighted archimedean logarithmic sum, divided by [K:Q]. There is no degree root in multiplicative height and no nonnegativity assertion.
LinearEquiv.coefficientIdeal	def	DedekindIdealArithmetic/Module/CoefficientIdeal.lean, line 251	For a commutative ring R, a fraction field F, a finitely generated R-module M and a supplied frame e : F ⊗[R] M ≃ₗ[F] F, the coefficient ideal is the nonzero fractional ideal whose elements are exactly e (1 tensor m) for m in M. The scalar module in its multiplication frame gives the unit ideal. Neither injectivity of M into its rational fibre nor integral freeness is assumed; this construction does not define a frame-independent height.
Seminorm.extendScalarsRankOne	def	DedekindIdealArithmetic/Module/RankOneSeminorm.lean, line 72	For normed fields k and l with NormedAlgebra k l and an invertible k-vector space V, any seminorm p, possibly degenerate, extends uniquely to l tensor_k V with value norm(a) * p(x) on a tensor x. Restriction along 1 tensor x recovers p, definiteness is preserved when p is definite, and the unit line recovers the norm of l. No completeness or finite-extension hypothesis is imposed; this is not a height law.
NumberField.InfinitePlace.Completion.isometry_completionMap	theorem	DedekindIdealArithmetic/NumberField/Completion/Extension.lean, line 59	For fields K and L with Algebra K L and infinite places v and w satisfying w.LiesOver v, Mathlib's completionMap extends the field algebra map and preserves the ordinary norm. The identity field map gives the identity on the completion. No number-field, finite-extension or real-place hypothesis is needed; no extension-height law is asserted.

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

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.