CartanConeIdeal.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The mixed-word ideal contains every outside generalized weight space

theorem OAI.PolycyclicRecognition.bracketWordWeight_mem_of_pure line 16

Source documentation

A pure word has weight in any additively closed set containing all of its letter weights.

theorem bracketWordWeight_mem_of_pure
    {I H : Type*} [AddCommGroup H] [Module ℝ H]
    (α : I → H →ₗ[ℝ] ℝ) (C : Set (H →ₗ[ℝ] ℝ))
    (hadd : ∀ x ∈ C, ∀ y ∈ C, x + y ∈ C)
    (w : FreeMagma I) (hw : ¬IsMixedWord (fun i => α i ∉ C) w) :
    bracketWordWeight α w ∈ C := by
…

Mentions: OAI.PolycyclicRecognition.IsMixedWord, OAI.PolycyclicRecognition.bracketWordWeight

def OAI.PolycyclicRecognition.CartanWordModel.coneWordIdeal line 33
Source documentation
The ideal generated by the letters outside the allowed cone of weights.
```
def coneWordIdeal (C : Set (H →ₗ[ℝ] ℝ)) : LieIdeal ℝ (cartanRootIdeal H) :=
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal
theorem OAI.PolycyclicRecognition.CartanWordModel.outside_genWeightSpace_le_coneWordIdeal line 38
Source documentation
Homogeneous word bases show that every generalized weight space outside an additively closed cone is contained in the mixed-word ideal.
```
theorem outside_genWeightSpace_le_coneWordIdeal
    (C : Set (H →ₗ[ℝ] ℝ)) (hadd : ∀ x ∈ C, ∀ y ∈ C, x + y ∈ C)
    (φ : H →ₗ[ℝ] ℝ) (hφ : φ ∉ C) :
    (genWeightSpace (cartanRootIdeal H) φ).toSubmodule ≤ (M.coneWordIdeal C).toSubmodule := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal
theorem OAI.PolycyclicRecognition.CartanWordModel.coneWordIdeal_cartan_invariant line 77
Source documentation
The mixed ideal is invariant under the full Cartan action, including its generalized-eigenvector corrections.
```
theorem coneWordIdeal_cartan_invariant
    (C : Set (H →ₗ[ℝ] ℝ)) (hadd : ∀ x ∈ C, ∀ y ∈ C, x + y ∈ C)
    (h : H) (v : cartanRootIdeal H) (hv : v ∈ M.coneWordIdeal C) :
    ⁅h, v⁆ ∈ M.coneWordIdeal C := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal
theorem OAI.PolycyclicRecognition.CartanWordModel.zero_genWeightSpace_le_coneWordIdeal line 97
Source documentation
For a pointed positive cone, the zero generalized weight space is removed in the quotient. Here the allowed set omits the cone vertex.
```
theorem zero_genWeightSpace_le_coneWordIdeal
    (C : Set (H →ₗ[ℝ] ℝ)) (hadd : ∀ x ∈ C, ∀ y ∈ C, x + y ∈ C)
    (hzero : (0 : H →ₗ[ℝ] ℝ) ∉ C) :
    (genWeightSpace (cartanRootIdeal H) (0 : H → ℝ)).toSubmodule ≤
      (M.coneWordIdeal C).toSubmodule :=
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal
theorem OAI.PolycyclicRecognition.CartanWordModel.cartan_intersection_mem_coneWordIdeal line 106
Source documentation
In particular the Cartan/root intersection is killed by the cone quotient, so the later action can descend through the factorization of G.
```
theorem cartan_intersection_mem_coneWordIdeal
    (C : Set (H →ₗ[ℝ] ℝ)) (hadd : ∀ x ∈ C, ∀ y ∈ C, x + y ∈ C)
    (hzero : (0 : H →ₗ[ℝ] ℝ) ∉ C) (v : cartanRootIdeal H) (hv : (v : L) ∈ H) :
    v ∈ M.coneWordIdeal C := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal