OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanTemplateSupports.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_cartan_template_supports line 15

   Source documentation

   All the independently supported generator exponents are realized by actual Cartan vectors whose heights stay in the given compact template.

   theorem exists_cartan_template_supports
       {L W : Type*} [LieRing L] [LieAlgebra ℝ L] [FiniteDimensional ℝ L]
       [NormedAddCommGroup W] [NormedSpace ℝ W] [FiniteDimensional ℝ W]
       {H : LieSubalgebra ℝ L} [H.IsCartanSubalgebra]
       (M : CartanWordModel H) {n : ℕ} (T : TriangularAdjoint L n)
       (hunimod : ∀ x : L, LinearMap.trace ℝ L (LieAlgebra.ad ℝ L x) = 0)
       (eW : HeightSpace T.character ≃ₗ[ℝ] W)
       (E : Set W) (hE : IsCompact E) (hne : E.Nonempty) :
       ∃ v : Fin M.letterCount → H,
         (∀ i, eW (heightProjection T.character (v i : L)) ∈ E) ∧
         M.templateSupportExponent v = (M.supportIn T hunimod eW).weightSupport E := by
   …

   Mentions: OAI.PolycyclicRecognition.CartanWordModel, OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.HeightSpace, OAI.PolycyclicRecognition.heightProjection