CanonicalHeight.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The linear canonical height quotient

The height space is the quotient by the common kernel of the diagonal adjoint characters. The induced characters on this quotient separate points.

def OAI.PolycyclicRecognition.heightKernel line 23
Source documentation
The common kernel of the diagonal characters. Empty families give ⊤.
Also declared: ComparatorChallenges/PolycyclicRecognition.lean:142 (same declaration text).
```
def heightKernel (χ : I → L →ₗ[ℝ] ℝ) : Submodule ℝ L := ⨅ i, (χ i).ker
```
abbrev OAI.PolycyclicRecognition.HeightSpace line 26
Source documentation
The canonical linear height space.
Also declared: ComparatorChallenges/PolycyclicRecognition.lean:145 (same declaration text).
```
abbrev HeightSpace (χ : I → L →ₗ[ℝ] ℝ) := L ⧸ heightKernel χ
```
Mentions: OAI.PolycyclicRecognition.heightKernel
def OAI.PolycyclicRecognition.heightProjection line 29
Source documentation
The quotient map defining infinitesimal height.
Also declared: ComparatorChallenges/PolycyclicRecognition.lean:148 (same declaration text).
```
def heightProjection (χ : I → L →ₗ[ℝ] ℝ) : L →ₗ[ℝ] HeightSpace χ :=
…
```
Mentions: OAI.PolycyclicRecognition.HeightSpace
def OAI.PolycyclicRecognition.heightCharacter line 33
Source documentation
Each character descends to the height quotient.
```
def heightCharacter (χ : I → L →ₗ[ℝ] ℝ) (i : I) : HeightSpace χ →ₗ[ℝ] ℝ :=
…
```
Mentions: OAI.PolycyclicRecognition.HeightSpace
theorem OAI.PolycyclicRecognition.heightCharacter_projection line 36
theorem OAI.PolycyclicRecognition.heightProjection_surjective line 39
theorem OAI.PolycyclicRecognition.mem_heightKernel line 42
theorem OAI.PolycyclicRecognition.heightCharacters_separate line 48
Source documentation
The common kernel has been removed: all induced character values vanish only at the zero height.
```
theorem heightCharacters_separate (χ : I → L →ₗ[ℝ] ℝ) (w : HeightSpace χ)
    (hw : ∀ i, heightCharacter χ i w = 0) : w = 0 := by
…
```
Mentions: OAI.PolycyclicRecognition.HeightSpace, OAI.PolycyclicRecognition.heightCharacter
theorem OAI.PolycyclicRecognition.heightCharacter_relation line 56
Source documentation
A relation among the original characters descends without changing its coefficients. This is used with the trace-zero, positive-multiplicity relation.
```
theorem heightCharacter_relation [Fintype I]
    (χ : I → L →ₗ[ℝ] ℝ) (c : I → ℝ)
    (h : ∀ x : L, ∑ i, c i * χ i x = 0) (w : HeightSpace χ) :
    ∑ i, c i * heightCharacter χ i w = 0 := by
…
```
Mentions: OAI.PolycyclicRecognition.HeightSpace, OAI.PolycyclicRecognition.heightCharacter
theorem OAI.PolycyclicRecognition.heightSpace_subsingleton_of_characters_zero line 64
Source documentation
Vanishing diagonal characters give a zero-dimensional height quotient.
```
theorem heightSpace_subsingleton_of_characters_zero
    (χ : I → L →ₗ[ℝ] ℝ) (hχ : ∀ i, χ i = 0) : Subsingleton (HeightSpace χ) := by
…
```
Mentions: OAI.PolycyclicRecognition.HeightSpace
theorem OAI.PolycyclicRecognition.characters_zero_of_heightSpace_subsingleton line 75
Source documentation
Conversely, a trivial height quotient forces all the diagonal characters to vanish.
```
theorem characters_zero_of_heightSpace_subsingleton
    (χ : I → L →ₗ[ℝ] ℝ) [Subsingleton (HeightSpace χ)] : ∀ i, χ i = 0 := by
…
```
Mentions: OAI.PolycyclicRecognition.HeightSpace
theorem OAI.PolycyclicRecognition.heightProjection_lie_eq_zero line 87
Source documentation
Characters vanishing on brackets make every bracket have zero height.
```
theorem heightProjection_lie_eq_zero
    (χ : I → L →ₗ[ℝ] ℝ) (hχ : ∀ i (x y : L), χ i ⁅x, y⁆ = 0) (x y : L) :
    heightProjection χ ⁅x, y⁆ = 0 := by
…
```
Mentions: OAI.PolycyclicRecognition.heightProjection