OAI/GroupTheory/PolycyclicRecognition/Geometry/TriangularRealizationConstruction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Constructing the full triangular realization from the exponential chart

The representation is obtained from the nilshadow and the two Cartan factors. The topology is recovered from the unique local logarithm in the real upper triangular algebra. Thus Onshuus–Post is no longer an independent input once the separately named Dixmier exponential chart is available.

  1. theorem OAI.PolycyclicRecognition.onshuusPostRealizationInput_of_dixmier line 25