15.2. The ring of integers
The ring of integers of K is NumberField.RingOfIntegers, defined as the
integral closure of ℤ in K.
The scoped notation 𝓞 K (type \McO) becomes available after open NumberField:
open NumberField
#check (𝓞 K : Type _)
An element of 𝓞 K is a bundled pair of an element of K together with a
proof that it is integral over ℤ; the coercion ((↑·) : 𝓞 K → K) recovers
the underlying element of K.
As an abstract structure, 𝓞 K is everything you expect.
It is a commutative ring, and also a Dedekind domain: in particular all the various properties
of ideals, like unique factorization, are known.
example : IsDedekindDomain (𝓞 K) := inferInstance
As a ℤ-module it is free of finite rank, and that rank equals the degree of the
field. The freeness and finiteness are found by instance search,
example : Module.Free ℤ (𝓞 K) := inferInstance
example : Module.Finite ℤ (𝓞 K) := inferInstance
and the equality of ranks is NumberField.RingOfIntegers.rank:
example : Module.finrank ℤ (𝓞 K) = Module.finrank ℚ K :=
RingOfIntegers.rank K
The fact that 𝓞 K is the integers of K (that an algebraic integer's
minimal polynomial over ℚ already has coefficients in ℤ) is the statement
that ℤ is integrally closed, recorded as an instance:
example : IsIntegrallyClosed ℤ := inferInstance
The general lemma turning this into a statement about minimal polynomials is
minpoly.isIntegrallyClosed_eq_field_fractions: over an integrally closed domain,
the minimal polynomial computed over the ring agrees with the one computed over its
field of fractions.