CartanJacobian.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The Jacobian of actual Cartan conjugation

The nilpotent residual exponential has determinant one. The scalar weight factors multiply to one by the already proved trace balance. Consequently conjugation on the nilpotent Cartan ideal preserves coordinate volume.

theorem OAI.PolycyclicRecognition.det_eq_one_of_sub_one_nilpotent line 22
Source documentation
A unipotent real endomorphism has determinant one, including in dimension zero. This uses its actual characteristic polynomial.
```
theorem det_eq_one_of_sub_one_nilpotent
    {V : Type*} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V]
    (F : Module.End ℝ V) (hF : _root_.IsNilpotent (F - 1)) : F.det = 1 := by
…
```

theorem OAI.PolycyclicRecognition.det_nilpotent_exp line 34

Source documentation

Finite nilpotent exponential has unit determinant.

theorem det_nilpotent_exp
    {V : Type*} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V]
    [Module ℚ V] [IsScalarTower ℚ ℝ V]
    (A : Module.End ℝ V) (hA : _root_.IsNilpotent A) :
    LinearMap.det (_root_.IsNilpotent.exp A) = 1 :=
…

theorem OAI.PolycyclicRecognition.det_cartanIdealResidualAutomorphism line 46
Source documentation
The nonsemisimple part of the actual Cartan action has Jacobian one.
```
theorem det_cartanIdealResidualAutomorphism (h : H) :
    LinearMap.det (cartanIdealResidualAutomorphism T H h).toLinearEquiv.toLinearMap = 1 := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanIdealResidualAutomorphism
theorem OAI.PolycyclicRecognition.CartanWordModel.det_idealWeightDilation line 57
Source documentation
The diagonal scalar action has Jacobian given by the total word weight.
```
theorem det_idealWeightDilation (β : M.Bases) (h : H) :
    LinearMap.det (cartanIdealWeightDilation T H h).toLinearEquiv.toLinearMap =
      Real.exp (∑ j, bracketWordExponent (fun i => M.weight i h) (β.val j)) := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanIdealWeightDilation, OAI.PolycyclicRecognition.bracketWordExponent
theorem OAI.PolycyclicRecognition.CartanWordModel.det_idealWeightDilation_eq_one line 78
Source documentation
Unimodularity makes all word-basis scalar Jacobians equal to one.
```
theorem det_idealWeightDilation_eq_one
    (hunimod : ∀ x : L, LinearMap.trace ℝ L (ad ℝ L x) = 0) (h : H) :
    LinearMap.det (cartanIdealWeightDilation T H h).toLinearEquiv.toLinearMap = 1 := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanIdealWeightDilation
theorem OAI.PolycyclicRecognition.CartanWordModel.det_idealAdjointAutomorphism_eq_one line 98
Source documentation
The full actual Cartan action, rather than only its scalar part, has Jacobian one on the nilpotent ideal.
```
theorem det_idealAdjointAutomorphism_eq_one
    (hunimod : ∀ x : L, LinearMap.trace ℝ L (ad ℝ L x) = 0) (h : H) :
    LinearMap.det (cartanIdealAdjointAutomorphism T H h).toLinearEquiv.toLinearMap = 1 := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanIdealAdjointAutomorphism