OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentCoordinatesInput.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Removing exponential existence from the nilpotent coordinate input

The global intrinsic exponential identifies a simply connected nilpotent Lie group with its Lie algebra and transports coordinate volume to Haar measure.

  1. def OAI.PolycyclicRecognition.NilpotentGlobalExponentialChartInput line 23

    Source documentation

    Only the global topological chart, with no measure compatibility.

    def NilpotentGlobalExponentialChartInput [T2Space G] [SimplyConnectedSpace G] : Prop :=
…
  2. def OAI.PolycyclicRecognition.NilpotentExponentialCoordinatesInput line 28
  3. theorem OAI.PolycyclicRecognition.NilpotentExponentialCoordinatesInput.toGlobalCharts line 38
  4. theorem OAI.PolycyclicRecognition.NilpotentExponentialCoordinatesInput.toHaar line 42
  5. theorem OAI.PolycyclicRecognition.nilpotentExponentialHaarInput_iff_coordinates line 46