HomogeneousGenerators.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Choosing generators and their positive word multiplicities

A basis of the abelianization can be selected from any homogeneous spanning pool. Its lifts generate the nilpotent algebra. Every bracket-word basis then uses every selected generator, which is the positivity needed in the support-volume formula.

theorem OAI.PolycyclicRecognition.exists_quotient_basis_lifts line 23

theorem OAI.PolycyclicRecognition.abelian_coordinate_eval_eq_zero_of_count_zero line 54

Source documentation

An abelian coordinate of a word without the corresponding letter is zero.

theorem abelian_coordinate_eval_eq_zero_of_count_zero
    (X : I → L) (f : L →ₗ[ℝ] ℝ) (i : I)
    (hbracket : ∀ x y : L, f ⁅x, y⁆ = 0)
    (hX : ∀ j, j ≠ i → f (X j) = 0)
    (w : FreeMagma I) (hw : bracketWordCount w i = 0) :
    f (evalBracketWord X w) = 0 := by
…

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

theorem OAI.PolycyclicRecognition.mandatory_letter_of_abelianization line 70

Source documentation

Every abelianization-basis letter occurs as an actual one-letter word in every word basis, since all longer words vanish in the abelian quotient.

theorem mandatory_letter_of_abelianization
    {J Q : Type*} [Fintype J] [AddCommGroup Q] [Module ℝ Q]
    (q : L →ₗ[ℝ] Q) (hq : ∀ x y : L, q ⁅x, y⁆ = 0)
    (X : I → L) (bq : Basis I ℝ Q) (hX : ∀ i, q (X i) = bq i)
    (b : Basis J ℝ L) (words : J → FreeMagma I)
    (hwords : ∀ j, evalBracketWord X (words j) = b j) (i : I) :
    ∃ j, words j = .of i := by
…

Mentions: OAI.PolycyclicRecognition.evalBracketWord

theorem OAI.PolycyclicRecognition.positive_bracketWord_multiplicities line 94

Source documentation

Every word basis uses every generator whose images are a basis in an abelian quotient. In particular its total letter count is strictly positive.

theorem positive_bracketWord_multiplicities
    [Fintype I] {J Q : Type*} [Fintype J]
    [AddCommGroup Q] [Module ℝ Q]
    (q : L →ₗ[ℝ] Q) (hq : ∀ x y : L, q ⁅x, y⁆ = 0)
    (X : I → L) (bq : Basis I ℝ Q) (hX : ∀ i, q (X i) = bq i)
    (b : Basis J ℝ L) (words : J → FreeMagma I)
    (hwords : ∀ j, evalBracketWord X (words j) = b j) :
    ∀ i, 0 < ∑ j, bracketWordCount (words j) i := by
…

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

theorem OAI.PolycyclicRecognition.exists_positive_word_basis line 122

Source documentation

Extract the finite word data needed by the box construction from a generating pool, retaining membership in that pool for every chosen letter.

theorem exists_positive_word_basis [FiniteDimensional ℝ L] [LieRing.IsNilpotent L]
    (S : Set L) (hS : LieSubalgebra.lieSpan ℝ L S = ⊤) :
    ∃ (m : ℕ) (X : Fin m → L)
      (b : Basis (Fin (Module.finrank ℝ L)) ℝ L)
      (words : Fin (Module.finrank ℝ L) → FreeMagma (Fin m)),
      (∀ i, X i ∈ S) ∧ (∀ j, evalBracketWord X (words j) = b j) ∧
      (∀ i, 0 < ∑ j, bracketWordCount (words j) i) := by
…

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