GradedHeight.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The original height is a homomorphism on the graded group

theorem OAI.PolycyclicRecognition.rescaledWordChartProduct_height line 20

Source documentation

Exact height additivity survives in every rescaled word chart.

theorem rescaledWordChartProduct_height
    (X : I → L) (S : Finset (FreeMagma I)) (β : WordBasisSelections X S)
    (h : L →ₗ[ℝ] W) (hh : ∀ x y : L, h ⁅x, y⁆ = 0)
    (Exp : L → G) (π : G →* Multiplicative W)
    (hπ : ∀ x, (π (Exp x)).toAdd = h x)
    {c : ℕ} (a : DynkinCoefficients c 2)
    (hm : ∀ x y, Exp (finiteDynkinPolynomial a ![x, y]) = Exp x * Exp y)
    (r : ℝ) (x y : Fin (finrank ℝ L) → ℝ) :
    let b := WordBasisSelections.basis X S β
…

Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial, OAI.PolycyclicRecognition.WordBasisSelections.basis

theorem OAI.PolycyclicRecognition.word_length_chart_pivot_height line 47

Source documentation

The rescaled coordinates of a scaled pivot retain exactly its height.

theorem word_length_chart_pivot_height
    (X : I → L) (S : Finset (FreeMagma I)) (β : WordBasisSelections X S)
    (height : L →ₗ[ℝ] W) (hkill : ∀ x y : L, height ⁅x, y⁆ = 0)
    {r : ℝ} (hr : 0 < r) (pivot : L) :
    let b := WordBasisSelections.basis X S β
…

Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.WordBasisSelections.basis

theorem OAI.PolycyclicRecognition.gradedWordChartProduct_height line 68

Source documentation

Passing the finite-scale identity to the limiting polynomial product gives the actual height homomorphism, without a new input on the limit.

theorem gradedWordChartProduct_height
    (X : I → L) (S : Finset (FreeMagma I)) (β : WordBasisSelections X S)
    (h : L →ₗ[ℝ] W) (hh : ∀ x y : L, h ⁅x, y⁆ = 0)
    (Exp : L → G) (π : G →* Multiplicative W)
    (hπ : ∀ x, (π (Exp x)).toAdd = h x)
    {c : ℕ} (a : DynkinCoefficients c 2)
    (hm : ∀ x y, Exp (finiteDynkinPolynomial a ![x, y]) = Exp x * Exp y)
    (hweight : ∀ i j k,
      (WordBasisSelections.basis X S β).repr
        ⁅(WordBasisSelections.basis X S β) i, (WordBasisSelections.basis X S β) j⁆ k ≠ 0 →
      bracketWordExponent (fun _ : I => 1) (β.val i) +
        bracketWordExponent (fun _ : I => 1) (β.val j) ≤
…

def OAI.PolycyclicRecognition.polynomialCoordinateHeightHom line 106
Source documentation
Regard an additive coordinate height as a homomorphism on the polynomial group. Its additivity is supplied by the preceding limit proof.
```
def polynomialCoordinateHeightHom
    {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
    (m : V → V → V) (hg : PolynomialGroupLaws m) (p : V →L[ℝ] W)
    (hp : ∀ x y, p (m x y) = p x + p y) :
    PolynomialCoordinateGroup m hg →* Multiplicative W where
…
```
Mentions: OAI.PolycyclicRecognition.PolynomialGroupLaws, OAI.PolycyclicRecognition.PolynomialCoordinateGroup

theorem OAI.PolycyclicRecognition.surjective_word_height_on_horizontal line 116

Source documentation

Surjectivity of the original height persists on the horizontal layer.

theorem surjective_word_height_on_horizontal
    [TopologicalSpace L] [IsTopologicalAddGroup L] [ContinuousSMul ℝ L] [T2Space L]
    [FiniteDimensional ℝ L]
    (X : I → L) (S : Finset (FreeMagma I)) (β : WordBasisSelections X S)
    (h : L →ₗ[ℝ] W) (hh : ∀ x y : L, h ⁅x, y⁆ = 0)
    (hsurj : Function.Surjective h) :
    let b := WordBasisSelections.basis X S β
…

Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.WordBasisSelections.basis