ComplexificationRealForm.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

The real form inside a complexified Lie algebra

Real and imaginary tensor coordinates detect membership in a complexified subalgebra. In particular the complexification of the chosen real Cartan subalgebra is again Cartan; it is preserved by the canonical conjugation.

def OAI.PolycyclicRecognition.complexificationRealPart line 21
def OAI.PolycyclicRecognition.complexificationImagPart line 25
theorem OAI.PolycyclicRecognition.complexificationRealPart_tmul line 29
theorem OAI.PolycyclicRecognition.complexificationImagPart_tmul line 32
theorem OAI.PolycyclicRecognition.complexification_decompose line 35
def OAI.PolycyclicRecognition.complexificationConjugation line 50
Source documentation
Conjugation on the complexification as a real Lie automorphism.
```
def complexificationConjugation : (ℂ ⊗[ℝ] L) ≃ₗ⁅ℝ⁆ (ℂ ⊗[ℝ] L) := by
…
```
theorem OAI.PolycyclicRecognition.complexificationConjugation_tmul line 59
theorem OAI.PolycyclicRecognition.complexification_conjugation_fixed_iff line 62
def OAI.PolycyclicRecognition.complexifiedInclusion line 84
Source documentation
Complexification of the inclusion of a real Lie subalgebra.
```
def complexifiedInclusion (H : LieSubalgebra ℝ L) :
    (ℂ ⊗[ℝ] H) →ₗ⁅ℂ⁆ (ℂ ⊗[ℝ] L) where
…
```
theorem OAI.PolycyclicRecognition.complexifiedInclusion_tmul line 90
def OAI.PolycyclicRecognition.complexifiedSubalgebra line 94
Source documentation
The actual complex Lie subalgebra generated by the real subalgebra.
```
def complexifiedSubalgebra (H : LieSubalgebra ℝ L) : LieSubalgebra ℂ (ℂ ⊗[ℝ] L) :=
…
```
theorem OAI.PolycyclicRecognition.mem_complexifiedSubalgebra_iff line 97
theorem OAI.PolycyclicRecognition.complexificationConjugation_smul line 121
Source documentation
Scalar conjugation is the only failure of complex linearity.
```
theorem complexificationConjugation_smul (z : ℂ) (x : ℂ ⊗[ℝ] L) :
    complexificationConjugation L (z • x) = star z • complexificationConjugation L x := by
…
```
Mentions: OAI.PolycyclicRecognition.complexificationConjugation
theorem OAI.PolycyclicRecognition.complexificationConjugation_involutive line 127
theorem OAI.PolycyclicRecognition.complexificationConjugation_inclusion line 131
theorem OAI.PolycyclicRecognition.complexifiedSubalgebra_conjugation line 138