CartanConeTrace.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The positive trace character of a Cartan cone quotient

The coefficients come from an actual pure-word basis of the quotient. The abelianization coordinates prove strict positivity for every inside generator, including the extremal generators of a ray or a two-ray cone.

theorem OAI.PolycyclicRecognition.bracketWordCount_eq_zero_of_pure line 19
def OAI.PolycyclicRecognition.CartanWordModel.coneCartanSubmodule line 36
Source documentation
The same mixed ideal, viewed as a submodule for the actual Cartan action.
```
def coneCartanSubmodule (C : Set (H →ₗ[ℝ] ℝ))
    (hadd : ∀ x ∈ C, ∀ y ∈ C, x + y ∈ C) : LieSubmodule ℝ H (cartanRootIdeal H) :=
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal

theorem OAI.PolycyclicRecognition.CartanWordModel.trace_cone_word_basis line 43

Source documentation

Trace on a pure-word quotient basis is the sum of the actual word weights; generalized eigenspaces retain the nilpotent parts of the action.

theorem trace_cone_word_basis
    (C : Set (H →ₗ[ℝ] ℝ)) (hadd : ∀ x ∈ C, ∀ y ∈ C, x + y ∈ C)
    {J : Type*} [Fintype J]
    (b : Basis J ℝ ((cartanRootIdeal H) ⧸ M.coneCartanSubmodule C hadd))
    (words : J → FreeMagma (Fin M.letterCount))
    (hwords : ∀ j, (M.coneWordIdeal C).toSubmodule.mkQ
      (evalBracketWord M.letter (words j)) = b j) (h : H) :
    LinearMap.trace ℝ ((cartanRootIdeal H) ⧸ M.coneCartanSubmodule C hadd)
      (toEnd ℝ H _ h) =
        ∑ i, ((∑ j, bracketWordCount (words j) i : ℕ) : ℝ) * M.weight i h := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.evalBracketWord, OAI.PolycyclicRecognition.bracketWordCount

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_positive_cone_trace_coefficients line 77

Source documentation

The quotient trace is an integral combination of inside generator weights, with strictly positive coefficients for every inside generator.

theorem exists_positive_cone_trace_coefficients
    (C : Set (H →ₗ[ℝ] ℝ)) (hadd : ∀ x ∈ C, ∀ y ∈ C, x + y ∈ C) :
    ∃ c : Fin M.letterCount → ℕ,
      (∀ i, (M.weight i : H →ₗ[ℝ] ℝ) ∉ C → c i = 0) ∧
      (∀ i, (M.weight i : H →ₗ[ℝ] ℝ) ∈ C → 0 < c i) ∧
      ∀ h : H, LinearMap.trace ℝ
        ((cartanRootIdeal H) ⧸ M.coneCartanSubmodule C hadd) (toEnd ℝ H _ h) =
          ∑ i, (c i : ℝ) * M.weight i h := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_positive_cone_height_character line 104

Source documentation

The trace character descends to the canonical height space.

theorem exists_positive_cone_height_character {n : ℕ} (T : TriangularAdjoint L n)
    (C : Set (H →ₗ[ℝ] ℝ)) (hadd : ∀ x ∈ C, ∀ y ∈ C, x + y ∈ C) :
    ∃ (ℓ : HeightSpace T.character →ₗ[ℝ] ℝ) (c : Fin M.letterCount → ℕ),
      (∀ i, (M.weight i : H →ₗ[ℝ] ℝ) ∉ C → c i = 0) ∧
      (∀ i, (M.weight i : H →ₗ[ℝ] ℝ) ∈ C → 0 < c i) ∧
      ℓ = ∑ i, (c i : ℝ) • cartanHeightWeight T H (M.weight i) ∧
      ∀ h : H, LinearMap.trace ℝ
        ((cartanRootIdeal H) ⧸ M.coneCartanSubmodule C hadd) (toEnd ℝ H _ h) =
          ℓ (heightProjection T.character (h : L)) := by
…

Mentions: OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.HeightSpace, OAI.PolycyclicRecognition.cartanHeightWeight, OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.heightProjection