15.3. Ideals🔗

Ideals of the ring of integers are values of Ideal:

variable (I : Ideal (𝓞 K))

The ideals form a commutative semiring, like the semiring of natural numbers, a ring without subtraction, under addition and multiplication. Because 𝓞 K is a Dedekind domain, this semiring is a unique factorization monoid: every nonzero ideal factors uniquely as a product of prime ideals. Both facts are available by instance search. In Lean, a UFD is called UniqueFactorizationMonoid, since its definition does not use addition:

example : CommSemiring (Ideal (𝓞 K)) := inferInstance
example : UniqueFactorizationMonoid (Ideal (𝓞 K)) :=
  inferInstance

Concretely, the prime/maximal coincidence and unique factorization let you reason about ideals through UniqueFactorizationMonoid and the prime-ideal API, rather than by choosing generators.

15.3.1. The ideal norm🔗

The absolute norm of an ideal is its index, Ideal.absNorm, the cardinality of the finite quotient 𝓞 K ⧸ I. It is bundled as a monoid-with-zero homomorphism, so multiplicativity is part of the definition:

absNorm : Ideal (𝓞 K) →*₀ ℕ#check (Ideal.absNorm : Ideal (𝓞 K) →*₀ ℕ)

example (I J : Ideal (𝓞 K)) :
    absNorm (I * J) = absNorm I * absNorm J :=
  map_mul absNorm I J

Because it is a bundled hom, apply general lemmas like map_mul and map_one to it rather than looking for absNorm-specific versions. The norm of a principal ideal is the absolute value of the element norm, Ideal.absNorm_span_singleton.

15.3.2. Splitting of primes in an extension🔗

An extension L/K of number fields is set up as:

variable {K L : Type*} [Field K] [Field L]
  [NumberField K] [NumberField L] [Algebra K L]

A prime p of 𝓞 K decomposes into primes P of 𝓞 L lying over it. Each such P carries two invariants:

the ramification index Ideal.ramificationIdx, the exponent of P in the factorization of the extended ideal;
the inertia degree Ideal.inertiaDeg, the degree of the residue field extension.

The finite set of primes lying over p is IsDedekindDomain.primesOverFinset, and the fundamental identity ∑ over P of (e P * f P) = [L : K] is sum_ramification_inertia_eq_finrank.