IntrinsicTriangularRepresentation.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A faithful triangular group representation without Dixmier

The intrinsic height kernel makes the Cartan construction and its overlap faithful. A kernel element of the resulting representation acts trivially on the Lie algebra, hence has zero intrinsic height and lies in the known nilpotent kernel, where faithfulness follows from the finite logarithm.

theorem OAI.PolycyclicRecognition.exists_intrinsic_faithful_triangular_representation line 29
theorem OAI.PolycyclicRecognition.intrinsic_exponential_injective line 101
Source documentation
The real triangular exponential and the faithful group representation make the intrinsic exponential injective, without assuming a global chart.
```
theorem intrinsic_exponential_injective
    {a : ℕ} (T : TriangularAdjoint (GroupLieAlgebra (𝓘(ℝ, E)) G) a)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp) :
    Function.Injective Exp := by
…
```
Mentions: OAI.PolycyclicRecognition.TriangularAdjoint