OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteProductPolynomialCoordinates.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Polynomial exponential coordinates from a finite product law

A concrete representation may provide a polynomial law with a degree larger than the Lie nilpotency class. That is enough for the global coordinate construction.

  1. theorem OAI.PolycyclicRecognition.polynomialExponentialCoordinates_equiv_of_finite_products line 24
  2. theorem OAI.PolycyclicRecognition.polynomialExponentialCoordinates_of_finite_products line 134

    Source documentation

    Forgetting the exponential chart recovers the original existence result.

    theorem polynomialExponentialCoordinates_of_finite_products
    (N : NilpotentLieModel L) (hnil : LieRing.IsNilpotent L)
    {c : ℕ} (coefficients : (n : ℕ) → DynkinCoefficients c n)
    (products : ∀ n (X : Fin n → GroupLieAlgebra (𝓘(ℝ, N.modelSpace)) N.carrier),
      (List.ofFn (fun i => groupExponential (X i))).prod =
        groupExponential (finiteDynkinPolynomial (coefficients n) X)) :
    Nonempty (PolynomialExponentialCoordinates L) := by
…

    Mentions: OAI.PolycyclicRecognition.NilpotentLieModel, OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.groupExponential, OAI.PolycyclicRecognition.finiteDynkinPolynomial, OAI.PolycyclicRecognition.PolynomialExponentialCoordinates