EnvelopingDerivation.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Extending Lie derivations to the enveloping algebra

The square-zero extension constructs the associative Leibniz extension. This will act on the finite truncated enveloping representation of the nilradical.

theorem OAI.PolycyclicRecognition.enveloping_induction line 26

Source documentation

Induction on scalar elements and Lie generators.

theorem enveloping_induction {P : U → Prop}
    (hscalar : ∀ r, P (algebraMap R U r)) (hgen : ∀ x, P (η x))
    (hadd : ∀ a b, P a → P b → P (a + b))
    (hmul : ∀ a b, P a → P b → P (a * b)) (u : U) : P u := by
…

def OAI.PolycyclicRecognition.envelopingDerivationLift line 38
theorem OAI.PolycyclicRecognition.envelopingDerivationLift_fst line 64
def OAI.PolycyclicRecognition.envelopingDerivation line 74
Source documentation
The unique associative derivation extending the given Lie derivation.
```
def envelopingDerivation (D : LieDerivation R L L) : U →ₗ[R] U :=
…
```
theorem OAI.PolycyclicRecognition.envelopingDerivation_generator line 79
theorem OAI.PolycyclicRecognition.envelopingDerivation_scalar line 87
theorem OAI.PolycyclicRecognition.envelopingDerivation_mul line 94
theorem OAI.PolycyclicRecognition.enveloping_derivation_ext line 105
theorem OAI.PolycyclicRecognition.envelopingDerivation_add line 118
theorem OAI.PolycyclicRecognition.envelopingDerivation_smul line 132
theorem OAI.PolycyclicRecognition.envelopingDerivation_lie line 146
def OAI.PolycyclicRecognition.envelopingDerivationRepresentation line 163
Source documentation
Derivations act on the enveloping algebra by a Lie representation.
```
def envelopingDerivationRepresentation : LieDerivation R L L →ₗ⁅R⁆ Module.End R U where
…
```