NormalizedLattice.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Normalized embedded lattices

Changing the sign of the first basis vector makes an invertible real basis matrix positively oriented without changing its integer lattice. Its transpose, scaled by the inverse positive root of its determinant, then gives a point of the column-lattice homogeneous space.

def OAI.DukePrimeDegree.orientBasis line 23
Source documentation
Reorient a row basis by changing one sign when necessary.
```
noncomputable def orientBasis (B : Matrix (Fin n) (Fin n) ℝ) :
    Matrix (Fin n) (Fin n) ℝ :=
…
```
lemma OAI.DukePrimeDegree.det_orientBasis line 27
lemma OAI.DukePrimeDegree.span_orientBasis line 37
Source documentation
Reorientation preserves the integer span of the rows.
```
lemma span_orientBasis (B : Matrix (Fin n) (Fin n) ℝ) :
    Submodule.span ℤ (Set.range (orientBasis B)) = Submodule.span ℤ (Set.range B) := by
…
```
Mentions: OAI.DukePrimeDegree.orientBasis
def OAI.DukePrimeDegree.normalizationFactor line 63
Source documentation
The positive covolume-normalizing scalar.
```
noncomputable def normalizationFactor (B : Matrix (Fin n) (Fin n) ℝ) : ℝ :=
…
```
lemma OAI.DukePrimeDegree.normalizationFactor_pos line 67
lemma OAI.DukePrimeDegree.det_normalizedBasis line 72
def OAI.DukePrimeDegree.normalizedBasis line 80
Source documentation
The special-linear matrix of the normalized column lattice.
```
noncomputable def normalizedBasis (B : Matrix (Fin n) (Fin n) ℝ) (hB : B.det ≠ 0) :
    RealSL n := ⟨normalizationFactor B • (orientBasis B)ᵀ, det_normalizedBasis B hB⟩
```
Mentions: OAI.DukePrimeDegree.RealSL, OAI.DukePrimeDegree.normalizationFactor, OAI.DukePrimeDegree.orientBasis, OAI.DukePrimeDegree.det_normalizedBasis
def OAI.DukePrimeDegree.latticePoint line 84
Source documentation
An invertible row basis determines a covolume-one lattice.
```
noncomputable def latticePoint (B : Matrix (Fin n) (Fin n) ℝ) (hB : B.det ≠ 0) :
    LatticeSpace n := QuotientGroup.mk (normalizedBasis B hB)
…
```
Mentions: OAI.DukePrimeDegree.LatticeSpace, OAI.DukePrimeDegree.normalizedBasis
def OAI.DukePrimeDegree.realEmbeddingLinear line 90
Source documentation
The ordered real embedding, regarded as an integer-linear map.
```
noncomputable def realEmbeddingLinear (σ : EmbeddingOrder K n) :
    K →ₗ[ℤ] (Fin n → ℝ) :=
…
```
Mentions: OAI.DukePrimeDegree.EmbeddingOrder
lemma OAI.DukePrimeDegree.FullLattice.span_embeddingMatrix line 94
def OAI.DukePrimeDegree.FullLattice.point line 118
Source documentation
The normalized embedded lattice attached to a full lattice and an ordering of the real embeddings.
```
noncomputable def FullLattice.point (M : FullLattice K)
    (σ : EmbeddingOrder K (Module.finrank ℚ K)) :
    LatticeSpace (Module.finrank ℚ K) := by
…
```
Mentions: OAI.DukePrimeDegree.FullLattice, OAI.DukePrimeDegree.EmbeddingOrder, OAI.DukePrimeDegree.LatticeSpace