RealCartanQuotient.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Real Cartan representatives of the complex adjoint-weight quotient

theorem OAI.PolycyclicRecognition.complexification_add_conjugate line 16
Source documentation
Taking real parts is averaging with the canonical conjugation.
```
theorem complexification_add_conjugate (x : ℂ ⊗[ℝ] L) :
    x + complexificationConjugation L x =
      (complexificationLieHom L) ((2 : ℝ) • complexificationRealPart L x) := by
…
```
Mentions: OAI.PolycyclicRecognition.complexificationConjugation, OAI.PolycyclicRecognition.complexificationLieHom, OAI.PolycyclicRecognition.complexificationRealPart
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.complexWeightMap_conjugate_zero line 37
Source documentation
Conjugation preserves the common complex weight kernel.
```
theorem complexWeightMap_conjugate_zero {x : ℂ ⊗[ℝ] L}
    (hx : T.complexWeightMap x = 0) :
    T.complexWeightMap (complexificationConjugation L x) = 0 := by
…
```
Mentions: OAI.PolycyclicRecognition.complexificationConjugation
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.weightMap_realPart_zero line 61
Source documentation
The real part of a vector in the complex weight kernel is in the original real weight kernel.
```
theorem weightMap_realPart_zero {x : ℂ ⊗[ℝ] L}
    (hx : T.complexWeightMap x = 0) :
    T.weightMap (complexificationRealPart L x) = 0 := by
…
```
Mentions: OAI.PolycyclicRecognition.complexificationRealPart
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.exists_real_cartan_representative line 75
Source documentation
Every real adjoint-weight vector has a real Cartan representative.
```
theorem exists_real_cartan_representative (x : L) :
    ∃ h : H, T.weightMap h = T.weightMap x := by
…
```
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.cartan_weightRange_surjective line 89
Source documentation
Surjectivity is onto the actual linear image of the adjoint weights.
```
theorem cartan_weightRange_surjective :
    Function.Surjective (fun h : H => T.weightMap.rangeRestrict (h : L)) := by
…
```
def OAI.PolycyclicRecognition.ComplexTriangularAdjoint.cartanWeightSection line 96
Source documentation
A linear choice of real Cartan representative for each weight vector.
```
def cartanWeightSection : T.weightMap.range →ₗ[ℝ] H :=
…
```
theorem OAI.PolycyclicRecognition.ComplexTriangularAdjoint.cartanWeightSection_weight line 100