OAI/GroupTheory/PolycyclicRecognition/Algebra/CollinearDynkin.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Collinear restrictions of the finite BCH formula

All nonlinear bracket terms vanish on a line. The derivative of a genuine one-parameter subgroup then determines the remaining linear term, without assuming injectivity of the exponential.

  1. theorem OAI.PolycyclicRecognition.finiteDynkinPolynomial_zero line 19
  2. theorem OAI.PolycyclicRecognition.eval_rightNestedWord_succ_collinear line 27
  3. theorem OAI.PolycyclicRecognition.finiteDynkinPolynomial_collinear_smul line 37
  4. theorem OAI.PolycyclicRecognition.finiteDynkinPolynomial_single_of_product line 62

    Source documentation

    A single nonzero logarithm is fixed by the BCH polynomial, as follows from the actual derivative of its exponential curve.

    theorem finiteDynkinPolynomial_single_of_product
    {Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G} (hExp : IsGroupExponential Exp)
    {c n : ℕ} (coeff : DynkinCoefficients c n)
    (hprod : ∀ X : Fin n → GroupLieAlgebra (𝓘(ℝ, E)) G,
      (List.ofFn (fun i => Exp (X i))).prod = Exp (finiteDynkinPolynomial coeff X))
    (i : Fin n) (v : GroupLieAlgebra (𝓘(ℝ, E)) G) :
    finiteDynkinPolynomial coeff (Pi.single i v) = v := by
…

    Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial