CartanRealShadow.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The real shadow Lie algebra

Removing only the imaginary semisimple Cartan action gives a genuine Lie algebra on the original vector space. Its bracket is obtained from a closed graph in the derivation semidirect sum, so the Jacobi identity is inherited.

def OAI.PolycyclicRecognition.cartanRealShadowSubalgebra line 22

Source documentation

The graph of minus the imaginary semisimple derivation.

def cartanRealShadowSubalgebra :
    LieSubalgebra ℝ (L ⋊⁅(LieHom.id : LieDerivation ℝ L L →ₗ⁅ℝ⁆ LieDerivation ℝ L L)⁆
      LieDerivation ℝ L L) where
…

abbrev OAI.PolycyclicRecognition.CartanRealShadow line 42
def OAI.PolycyclicRecognition.cartanRealShadowEquiv line 45
Source documentation
Only multiplication changes: the real vector space is unchanged.
```
def cartanRealShadowEquiv : L ≃ₗ[ℝ] CartanRealShadow T H where
…
```
Mentions: OAI.PolycyclicRecognition.CartanRealShadow
instance OAI.PolycyclicRecognition.(instance at line 68) line 68

theorem OAI.PolycyclicRecognition.cartanRealShadow_bracket line 72

Source documentation

Exact bracket after removing the imaginary semisimple action.

theorem cartanRealShadow_bracket (x y : L) :
    (cartanRealShadowEquiv T H).symm ⁅cartanRealShadowEquiv T H x,
      cartanRealShadowEquiv T H y⁆ =
      ⁅x,y⁆ - T.weightImaginaryAction H x y + T.weightImaginaryAction H y x := by
…

Mentions: OAI.PolycyclicRecognition.cartanRealShadowEquiv

theorem OAI.PolycyclicRecognition.cartanRealShadow_bracket_weight line 81
Source documentation
The weight quotient of the modified bracket remains abelian.
```
theorem cartanRealShadow_bracket_weight (x y : L) :
    T.weightMap ((cartanRealShadowEquiv T H).symm
      ⁅cartanRealShadowEquiv T H x,cartanRealShadowEquiv T H y⁆) = 0 := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanRealShadowEquiv