TriangularHeight.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Diagonal adjoint characters and the zero-height case

Starting from an actual simultaneous upper triangular basis for the adjoint action, the diagonal entries are linear characters and kill every bracket. The resulting canonical height space is zero exactly when the Lie algebra is nilpotent. This proves the algebraic zero-height branch used in the manuscript; it does not assume nilpotence from vanishing height.

theorem OAI.PolycyclicRecognition.upperTriangular_mul_diag line 21
theorem OAI.PolycyclicRecognition.upperTriangular_pow_diag line 32
theorem OAI.PolycyclicRecognition.upperTriangular_nilpotent_diag line 39
theorem OAI.PolycyclicRecognition.upperTriangular_nilpotent_of_diag_zero line 47
structure OAI.PolycyclicRecognition.TriangularAdjoint line 59
Source documentation
A simultaneous real upper triangular adjoint basis, including its actual matrix inequalities. This is the linear-algebra meaning of real triangulability.
Also declared: ComparatorChallenges/PolycyclicRecognition.lean:154 (same declaration text).
```
structure TriangularAdjoint (L : Type*) [LieRing L] [LieAlgebra ℝ L] (n : ℕ) where
…
```
def OAI.PolycyclicRecognition.TriangularAdjoint.character line 69
Source documentation
The diagonal entries of the adjoint representation are linear forms.
Distinct definitions of this name: ComparatorChallenges/PolycyclicRecognition.lean:164 (same statement text; different proof or body). Qualify references as OAI.PolycyclicRecognition.TriangularAdjoint.character@path.
```
noncomputable def character (i : Fin n) : L →ₗ[ℝ] ℝ where
…
```
theorem OAI.PolycyclicRecognition.TriangularAdjoint.character_eq_diag line 74
theorem OAI.PolycyclicRecognition.TriangularAdjoint.character_lie line 79
Source documentation
The diagonal of a commutator of upper triangular matrices vanishes.
```
theorem character_lie (i : Fin n) (x y : L) : T.character i ⁅x, y⁆ = 0 := by
…
```
theorem OAI.PolycyclicRecognition.TriangularAdjoint.height_lie line 92
Source documentation
The canonical height map kills the Lie bracket, so its quotient is abelian.
```
theorem height_lie (x y : L) : heightProjection T.character ⁅x, y⁆ = 0 :=
…
```
Mentions: OAI.PolycyclicRecognition.heightProjection
def OAI.PolycyclicRecognition.TriangularAdjoint.kernelIdeal line 96
Source documentation
The common character kernel is a Lie ideal, not just a linear subspace.
```
noncomputable def kernelIdeal : LieIdeal ℝ L where
…
```
theorem OAI.PolycyclicRecognition.TriangularAdjoint.mem_kernelIdeal line 102
theorem OAI.PolycyclicRecognition.TriangularAdjoint.ad_nilpotent_of_mem_kernel line 106
Source documentation
Every element of the height kernel acts nilpotently on the entire Lie algebra.
```
theorem ad_nilpotent_of_mem_kernel (x : L) (hx : x ∈ T.kernelIdeal) :
    IsNilpotent (LieAlgebra.ad ℝ L x) := by
…
```
theorem OAI.PolycyclicRecognition.TriangularAdjoint.mem_kernelIdeal_of_ad_nilpotent line 118
Source documentation
Conversely, a nilpotent adjoint operator has zero diagonal characters.
```
theorem mem_kernelIdeal_of_ad_nilpotent (x : L)
    (hx : IsNilpotent (LieAlgebra.ad ℝ L x)) : x ∈ T.kernelIdeal := by
…
```
theorem OAI.PolycyclicRecognition.TriangularAdjoint.kernelIdeal_nilpotent line 130
Source documentation
Engel's theorem applied to the faithful restricted adjoint module proves nilpotence of the common character kernel.
```
theorem kernelIdeal_nilpotent : LieRing.IsNilpotent T.kernelIdeal := by
…
```
theorem OAI.PolycyclicRecognition.TriangularAdjoint.nilpotent_of_height_zero line 139
Source documentation
The zero-height case really is nilpotent, by the triangular adjoint matrices and Engel's theorem.
```
theorem nilpotent_of_height_zero [Subsingleton (HeightSpace T.character)] :
    LieRing.IsNilpotent L := by
…
```
Mentions: OAI.PolycyclicRecognition.HeightSpace
theorem OAI.PolycyclicRecognition.TriangularAdjoint.height_zero_of_nilpotent line 152
theorem OAI.PolycyclicRecognition.TriangularAdjoint.ad_nilpotent_of_mem_nilpotent_ideal line 165
Source documentation
An element of a nilpotent ideal acts nilpotently on the whole algebra: its first adjoint image lies in the ideal, where subsequent powers vanish.
```
theorem ad_nilpotent_of_mem_nilpotent_ideal
    (I : LieIdeal ℝ L) [LieRing.IsNilpotent I] (x : L) (hx : x ∈ I) :
    IsNilpotent (LieAlgebra.ad ℝ L x) := by
…
```
theorem OAI.PolycyclicRecognition.TriangularAdjoint.nilpotent_ideal_le_kernelIdeal line 188
Source documentation
The canonical character kernel contains every nilpotent Lie ideal. Together with kernelIdeal_nilpotent, this identifies it as the nilradical.
```
theorem nilpotent_ideal_le_kernelIdeal
    (I : LieIdeal ℝ L) [LieRing.IsNilpotent I] : I ≤ T.kernelIdeal := by
…
```