MultiplierOrder.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Multiplier orders and the saturation index

The initial arithmetic reduction in Section 2 of paper 031-01. A lattice is represented by its actual integer submodule of a number field, not by an abstract label. The two inclusions proved here are the algebraic input to the discriminant bound D(M) ≤ D(K) q^(2*n).

def OAI.DukePrimeDegree.multiplierOrder line 24
Source documentation
Elements of the field preserving the given integer lattice.
```
def multiplierOrder (M : Submodule ℤ K) : Subalgebra ℤ K where
…
```
theorem OAI.DukePrimeDegree.mem_multiplierOrder line 38
theorem OAI.DukePrimeDegree.multiplierOrder_le_integralClosure line 44
Source documentation
A multiplier of a nonzero finitely generated lattice is integral. This proves the upper inclusion in the manuscript's discriminant-scale reduction directly from the library's determinant trick.
```
theorem multiplierOrder_le_integralClosure (M : Submodule ℤ K)
    (hne : M ≠ ⊥) (hfg : M.FG) :
    multiplierOrder M ≤ integralClosure ℤ K := by
…
```
Mentions: OAI.DukePrimeDegree.multiplierOrder
def OAI.DukePrimeDegree.maximalOrderSpan line 51
Source documentation
The maximal-order span of an integer lattice.
```
def maximalOrderSpan (M : Submodule ℤ K) : Submodule (𝓞 K) K :=
…
```
def OAI.DukePrimeDegree.saturationLattice line 55
Source documentation
The maximal-order span, viewed again as an integer lattice.
```
def saturationLattice (M : Submodule ℤ K) : Submodule ℤ K :=
…
```
lemma OAI.DukePrimeDegree.le_saturationLattice line 58
def OAI.DukePrimeDegree.latticeInSaturation line 63
Source documentation
The original lattice inside its maximal-order span.
```
def latticeInSaturation (M : Submodule ℤ K) : Submodule ℤ (saturationLattice M) :=
…
```
Mentions: OAI.DukePrimeDegree.saturationLattice
def OAI.DukePrimeDegree.saturationIndex line 68
Source documentation
The additive index [O_K M : M]. For a full lattice this is finite. As usual, the index is zero if the quotient is infinite.
```
noncomputable def saturationIndex (M : Submodule ℤ K) : ℕ :=
…
```
lemma OAI.DukePrimeDegree.saturationIndex_nsmul_mem line 72
Source documentation
Multiplication by the index sends the saturation into the lattice.
```
lemma saturationIndex_nsmul_mem (M : Submodule ℤ K) {x : K}
    (hx : x ∈ saturationLattice M) : saturationIndex M • x ∈ M := by
…
```
Mentions: OAI.DukePrimeDegree.saturationLattice, OAI.DukePrimeDegree.saturationIndex
theorem OAI.DukePrimeDegree.saturationIndex_mul_integer_mem_multiplierOrder line 80
Source documentation
The conductor inclusion q O_K ⊆ O(M) with q = [O_K M : M]. Together with integrality of multipliers, this gives the two order inclusions used in the manuscript.
```
theorem saturationIndex_mul_integer_mem_multiplierOrder
    (M : Submodule ℤ K) (r : 𝓞 K) :
    (saturationIndex M : K) * (r : K) ∈ multiplierOrder M := by
…
```
Mentions: OAI.DukePrimeDegree.saturationIndex, OAI.DukePrimeDegree.multiplierOrder