OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanFullCellAffinity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.cartan_neighbor_profiles_affine_on_contracted_cell line 39

   Source documentation

   Both supported profiles are affine on the full inverse image of the open contracted cell. Openness, convexity, and nonemptiness of that domain are proved here from the surjective Cartan height map.

   theorem cartan_neighbor_profiles_affine_on_contracted_cell
       [IsTopologicalGroup F.N.carrier]
       [Nonempty (Fin (finrank ℝ (cartanRootIdeal H)))]
       (hExp : IsGroupExponential Exp)
       (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
   …

   Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.ExponentialLinearRealizationInput