AmplitudeWordRank.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Full rank of one fixed independent generator word

theorem OAI.PolycyclicRecognition.exists_submersive_amplitudeWord line 16

Source documentation

The rank belongs to the full word, before any successful-parameter restriction.

theorem exists_submersive_amplitudeWord {I J : Type*} [Fintype I] {n c : ℕ}
    (a : DynkinCoefficients c 2)
    (B : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ) →L[ℝ] (Fin n → ℝ))
    (hB : IsLieBracket B) (hg : PolynomialGroupLaws (dynkinProduct a B))
    (hc : ExponentialConjugationLaw (dynkinProduct a B) B)
    (X : I → Fin n → ℝ) (b₀ : Basis J ℝ (Fin n → ℝ)) (w₀ : J → FreeMagma I)
    (hw₀ : ∀ j, evalBilinearWord B X (w₀ j) = b₀ j) :
    ∃ (m : ℕ) (letters : Fin m → I) (t₀ : Fin m → ℝ),
      amplitudeWordEndpoint a letters (B, X) t₀ = 0 ∧
      Function.Surjective (fderiv ℝ (amplitudeWordEndpoint a letters (B, X)) t₀) := by
…

Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.IsLieBracket, OAI.PolycyclicRecognition.PolynomialGroupLaws, OAI.PolycyclicRecognition.dynkinProduct, OAI.PolycyclicRecognition.ExponentialConjugationLaw, OAI.PolycyclicRecognition.evalBilinearWord, OAI.PolycyclicRecognition.amplitudeWordEndpoint

theorem OAI.PolycyclicRecognition.exists_amplitudeWord_nonsingular_minor line 59

Source documentation

Select a nonzero square minor of that same fixed word.

theorem exists_amplitudeWord_nonsingular_minor {I J : Type*} [Fintype I] {n c : ℕ}
    (a : DynkinCoefficients c 2)
    (B : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ) →L[ℝ] (Fin n → ℝ))
    (hB : IsLieBracket B) (hg : PolynomialGroupLaws (dynkinProduct a B))
    (hc : ExponentialConjugationLaw (dynkinProduct a B) B)
    (X : I → Fin n → ℝ) (b₀ : Basis J ℝ (Fin n → ℝ)) (w₀ : J → FreeMagma I)
    (hw₀ : ∀ j, evalBilinearWord B X (w₀ j) = b₀ j) :
    ∃ (m : ℕ) (letters : Fin m → I) (t₀ : Fin m → ℝ) (j : Fin n → Fin m),
      Function.Injective j ∧ amplitudeWordEndpoint a letters (B, X) t₀ = 0 ∧
      (Matrix.of fun i k =>
        fderiv ℝ (amplitudeWordEndpoint a letters (B, X)) t₀ (Pi.single (j k) 1) i).det ≠ 0 := by
…