CartanFactorModel.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Construction of the two Cartan factor models

The only existence premises are the cited Lie correspondence specialized to the actual root ideal and Cartan algebra. Integration, normality and global charts are supplied by the separately named published inputs. All assertions about the multiplication map are derived in CartanFactorization.

structure OAI.PolycyclicRecognition.CartanFactorModel line 28
Source documentation
The concrete group part of the manuscript's Cartan model. The ambient overlap is retained, and all lifting conclusions refer to the actual map.
```
structure CartanFactorModel where
…
```
theorem OAI.PolycyclicRecognition.nonempty_cartanFactorModel_of_published_inputs line 57
Source documentation
The group factors now exist from the precise published inputs; the caller does not supply arbitrary nilpotent models or a product theorem.
```
theorem nonempty_cartanFactorModel_of_published_inputs
    {a : ℕ} (T : TriangularAdjoint (GroupLieAlgebra (𝓘(ℝ, EG)) G) a)
    (hExpG : IsGroupExponential ExpG)
    (dixmier : DixmierExponentialInput (E := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.DixmierExponentialInput