QuotientWordBasis.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Pure word bases of the mixed-word quotient

An inside generator is retained in every pure word basis. The proof uses its actual coordinate in the original abelianization, descended through the mixed-word ideal.

theorem OAI.PolycyclicRecognition.exists_pure_quotient_word_basis line 21

theorem OAI.PolycyclicRecognition.inside_abelian_coordinate_kills_mixed line 52

Source documentation

An inside abelian coordinate vanishes on the entire mixed-word ideal.

theorem inside_abelian_coordinate_kills_mixed
    {Q : Type*} [AddCommGroup Q] [Module ℝ Q]
    (X : I → L) (outside : I → Prop)
    (q : L →ₗ[ℝ] Q) (hq : ∀ x y : L, q ⁅x, y⁆ = 0)
    (bq : Basis I ℝ Q) (hX : ∀ i, q (X i) = bq i)
    (i : I) (hi : ¬outside i) :
    mixedWordSpan X outside ≤ LinearMap.ker ((bq.coord i).comp q) := by
…

Mentions: OAI.PolycyclicRecognition.mixedWordSpan

theorem OAI.PolycyclicRecognition.mandatory_inside_letter_in_quotient line 71

Source documentation

Every retained generator occurs as a one-letter word in any pure word basis of the quotient.

theorem mandatory_inside_letter_in_quotient
    {Q K : Type*} [AddCommGroup Q] [Module ℝ Q]
    (X : I → L) (outside : I → Prop)
    (hgen : LieSubalgebra.lieSpan ℝ L (range X) = ⊤)
    (q : L →ₗ[ℝ] Q) (hq : ∀ x y : L, q ⁅x, y⁆ = 0)
    (bq : Basis I ℝ Q) (hX : ∀ i, q (X i) = bq i)
    (b : Basis K ℝ (L ⧸ (mixedWordIdeal X outside hgen).toSubmodule))
    (words : K → FreeMagma I)
    (hwords : ∀ j, (mixedWordIdeal X outside hgen).toSubmodule.mkQ
      (evalBracketWord X (words j)) = b j)
    (i : I) (hi : ¬outside i) : ∃ j, words j = .of i := by
…

Mentions: OAI.PolycyclicRecognition.mixedWordIdeal, OAI.PolycyclicRecognition.evalBracketWord

theorem OAI.PolycyclicRecognition.positive_inside_quotient_word_counts line 99