MixedWordIdeal.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

The mixed-word ideal used by the cone quotients

def OAI.PolycyclicRecognition.IsMixedWord line 17
Source documentation
A bracket word is mixed when at least one of its letters is outside the chosen cone. No property of that cone is needed for the ideal calculation.
```
def IsMixedWord (outside : I → Prop) : FreeMagma I → Prop
  | .of i => outside i
  | .mul u v => IsMixedWord outside u ∨ IsMixedWord outside v
```
def OAI.PolycyclicRecognition.mixedWordSpan line 21
theorem OAI.PolycyclicRecognition.eval_mixed_mem_span line 24
theorem OAI.PolycyclicRecognition.mixedWordSpan_lie line 31
Source documentation
Bracketing a mixed word with an arbitrary word still gives a mixed word; linearity extends this to the full generated algebra.
```
theorem mixedWordSpan_lie (X : I → L) (outside : I → Prop)
    (hgen : LieSubalgebra.lieSpan ℝ L (range X) = ⊤)
    (x y : L) (hy : y ∈ mixedWordSpan X outside) :
    ⁅x, y⁆ ∈ mixedWordSpan X outside := by
…
```
Mentions: OAI.PolycyclicRecognition.mixedWordSpan
def OAI.PolycyclicRecognition.mixedWordIdeal line 58
Source documentation
The span of mixed words is an actual Lie ideal, rather than an assumed quotient datum.
```
def mixedWordIdeal (X : I → L) (outside : I → Prop)
    (hgen : LieSubalgebra.lieSpan ℝ L (range X) = ⊤) : LieIdeal ℝ L :=
…
```
theorem OAI.PolycyclicRecognition.eval_mixed_mem_ideal line 64
Source documentation
Every ideal containing the outside letters contains every mixed word.
```
theorem eval_mixed_mem_ideal (X : I → L) (outside : I → Prop)
    (J : LieIdeal ℝ L) (hJ : ∀ i, outside i → X i ∈ J)
    (w : FreeMagma I) (hw : IsMixedWord outside w) : evalBracketWord X w ∈ J := by
…
```
Mentions: OAI.PolycyclicRecognition.IsMixedWord, OAI.PolycyclicRecognition.evalBracketWord

theorem OAI.PolycyclicRecognition.mixedWordIdeal_le_iff line 75

Source documentation

This is precisely the ideal generated by the outside letters.

theorem mixedWordIdeal_le_iff (X : I → L) (outside : I → Prop)
    (hgen : LieSubalgebra.lieSpan ℝ L (range X) = ⊤) (J : LieIdeal ℝ L) :
    mixedWordIdeal X outside hgen ≤ J ↔ ∀ i, outside i → X i ∈ J := by
…

Mentions: OAI.PolycyclicRecognition.mixedWordIdeal

theorem OAI.PolycyclicRecognition.quotient_mixedWordIdeal_span_pure line 87
Source documentation
The quotient by the mixed-word ideal is spanned by pure words.
```
theorem quotient_mixedWordIdeal_span_pure (X : I → L) (outside : I → Prop)
    (hgen : LieSubalgebra.lieSpan ℝ L (range X) = ⊤) :
    let J := (mixedWordIdeal X outside hgen).toSubmodule
…
```
Mentions: OAI.PolycyclicRecognition.mixedWordIdeal

theorem OAI.PolycyclicRecognition.map_mixedWordSpan_of_kills_brackets line 117

Source documentation

In the abelianization, the mixed-word ideal is exactly the span of the outside generator images. Higher bracket words contribute zero.

theorem map_mixedWordSpan_of_kills_brackets
    {V : Type*} [AddCommGroup V] [Module ℝ V]
    (X : I → L) (outside : I → Prop) (q : L →ₗ[ℝ] V)
    (hq : ∀ x y : L, q ⁅x, y⁆ = 0) :
    (mixedWordSpan X outside).map q = Submodule.span ℝ (q '' (X '' {i | outside i})) := by
…

Mentions: OAI.PolycyclicRecognition.mixedWordSpan

theorem OAI.PolycyclicRecognition.derivation_preserves_mixedWordIdeal line 138

Source documentation

A derivation preserves the mixed-word ideal as soon as it sends each outside generator into that ideal. This is the Cartan-invariance reduction.

theorem derivation_preserves_mixedWordIdeal
    (X : I → L) (outside : I → Prop)
    (hgen : LieSubalgebra.lieSpan ℝ L (range X) = ⊤)
    (D : L →ₗ[ℝ] L)
    (hD : ∀ x y, D ⁅x, y⁆ = ⁅D x, y⁆ + ⁅x, D y⁆)
    (hout : ∀ i, outside i → D (X i) ∈ mixedWordIdeal X outside hgen)
    (v : L) (hv : v ∈ mixedWordIdeal X outside hgen) :
    D v ∈ mixedWordIdeal X outside hgen := by
…

Mentions: OAI.PolycyclicRecognition.mixedWordIdeal