EmbeddingMatrix.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Ordered real embeddings and lattice basis matrices

An ordering of the complex embeddings of a totally real field gives the ordered real embeddings used in the manuscript. The matrix of any full lattice basis under these embeddings has nonzero determinant.

abbrev OAI.DukePrimeDegree.EmbeddingOrder line 21
Source documentation
An ordering of all embeddings; total reality makes their values real.
```
abbrev EmbeddingOrder (K : Type*) [Field K] [NumberField K] (n : ℕ) :=
…
```
def OAI.DukePrimeDegree.orderedRealEmbedding line 25
Source documentation
The real ring embedding at one place of the ordering.
```
noncomputable def orderedRealEmbedding (σ : EmbeddingOrder K n) (j : Fin n) : K →+* ℝ :=
…
```
Mentions: OAI.DukePrimeDegree.EmbeddingOrder
lemma OAI.DukePrimeDegree.orderedRealEmbedding_complex line 28
def OAI.DukePrimeDegree.realEmbeddingMatrix line 33
Source documentation
Rows are basis vectors and columns are ordered real embeddings.
```
noncomputable def realEmbeddingMatrix (b : Fin n → K) (σ : EmbeddingOrder K n) :
    Matrix (Fin n) (Fin n) ℝ := fun i j => orderedRealEmbedding σ j (b i)
```
Mentions: OAI.DukePrimeDegree.EmbeddingOrder, OAI.DukePrimeDegree.orderedRealEmbedding
lemma OAI.DukePrimeDegree.realEmbeddingMatrix_complex line 36
theorem OAI.DukePrimeDegree.det_realEmbeddingMatrix_ne_zero line 44
Source documentation
The field trace discriminant proves the embedded lattice basis is linearly independent over the real numbers.
```
theorem det_realEmbeddingMatrix_ne_zero (b : Module.Basis (Fin n) ℚ K)
    (σ : EmbeddingOrder K n) : (realEmbeddingMatrix b σ).det ≠ 0 := by
…
```
Mentions: OAI.DukePrimeDegree.EmbeddingOrder, OAI.DukePrimeDegree.realEmbeddingMatrix
theorem OAI.DukePrimeDegree.FullLattice.det_embeddingMatrix_ne_zero line 63
Source documentation
In particular this applies to the chosen integer basis of a full lattice.
```
theorem FullLattice.det_embeddingMatrix_ne_zero (M : FullLattice K)
    (σ : EmbeddingOrder K (Module.finrank ℚ K)) :
    (realEmbeddingMatrix (fun i => (M.integralBasis i : K)) σ).det ≠ 0 := by
…
```
Mentions: OAI.DukePrimeDegree.FullLattice, OAI.DukePrimeDegree.EmbeddingOrder, OAI.DukePrimeDegree.realEmbeddingMatrix