OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanInteriorProfileHeights.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_profile_coordinate_above_template line 14

   Source documentation

   A compact height template strictly inside the open profile domain provides the interior-switch condition in every Cartan coordinate basis.

   theorem exists_profile_coordinate_above_template
       {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)
       (b : Basis (Fin (finrank ℝ H)) ℝ H)
       (E V : Set W) (hE : IsCompact E) (hne : E.Nonempty)
       (hV : IsOpen V) (hEV : E ⊆ V) (i : Fin M.letterCount) :
       ∃ z : Fin (finrank ℝ H) → ℝ,
         eW (heightProjection T.character (b.equivFun.symm z : L)) ∈ V ∧
   …

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