FullLattice.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Full lattices in number fields

A full lattice is a finitely generated integer submodule spanning the number field over the rationals. In a characteristic-zero field it is free; the span condition forces its rank to be the field degree.

structure OAI.DukePrimeDegree.FullLattice line 23
Source documentation
The lattice data appearing in Theorem 1.1, before choosing an ordering of the real embeddings.
```
structure FullLattice where
…
```
lemma OAI.DukePrimeDegree.FullLattice.ne_bot line 30
lemma OAI.DukePrimeDegree.FullLattice.multiplierOrder_le line 39
Source documentation
The multiplier order of a full lattice consists of algebraic integers.
```
lemma FullLattice.multiplierOrder_le (M : FullLattice K) :
    multiplierOrder M.toSubmodule ≤ integralClosure ℤ K :=
…
```
Mentions: OAI.DukePrimeDegree.FullLattice, OAI.DukePrimeDegree.multiplierOrder
lemma OAI.DukePrimeDegree.FullLattice.exists_integer_multiple line 45
Source documentation
Every field element has an integer denominator relative to a full lattice. This is a direct application of localization of spans.
```
lemma FullLattice.exists_integer_multiple (M : FullLattice K) (x : K) :
    ∃ q : ℤ, q ≠ 0 ∧ q • x ∈ M.toSubmodule := by
…
```
Mentions: OAI.DukePrimeDegree.FullLattice
lemma OAI.DukePrimeDegree.FullLattice.saturation_fg line 56
Source documentation
The maximal-order saturation is again finitely generated over the integers.
```
lemma FullLattice.saturation_fg (M : FullLattice K) :
    (saturationLattice M.toSubmodule).FG := by
…
```
Mentions: OAI.DukePrimeDegree.FullLattice, OAI.DukePrimeDegree.saturationLattice
lemma OAI.DukePrimeDegree.FullLattice.saturationIndex_pos line 61
Source documentation
A full lattice has finite, nonzero index in its maximal-order saturation.
```
lemma FullLattice.saturationIndex_pos (M : FullLattice K) :
    0 < saturationIndex M.toSubmodule := by
…
```
Mentions: OAI.DukePrimeDegree.FullLattice, OAI.DukePrimeDegree.saturationIndex