OAI/GroupTheory/PolycyclicRecognition/Geometry/RealShadowRepresentation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_realShadow_triangularRepresentation line 19

   Source documentation

   The nilpotent weight kernel acts by nilpotent matrices in a faithful real triangular representation of the modified algebra.

   theorem exists_realShadow_triangularRepresentation :
       ∃ m : ℕ, 0 < m ∧
         ∃ j : CartanRealShadow T H →ₗ⁅ℝ⁆ Matrix (Fin m) (Fin m) ℝ,
           Function.Injective j ∧ (∀ x, (j x).IsUpperTriangular) ∧
           ∀ x ∈ realShadowKernel T H, IsNilpotent (j x) := by
   …

   Mentions: OAI.PolycyclicRecognition.CartanRealShadow, OAI.PolycyclicRecognition.realShadowKernel