OAI/GroupTheory/PolycyclicRecognition/Geometry/ConjugateCartanWeights.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Conjugation of the complex Cartan weight spaces

  1. def OAI.PolycyclicRecognition.cartanConjugation line 18

    Source documentation

    The conjugation induced on the actual complexified Cartan subalgebra.

    def cartanConjugation (h : complexifiedSubalgebra L H) : complexifiedSubalgebra L H :=
…

    Mentions: OAI.PolycyclicRecognition.complexifiedSubalgebra

  2. theorem OAI.PolycyclicRecognition.cartanConjugation_involutive line 22
  3. def OAI.PolycyclicRecognition.conjugateCartanWeight line 29

    Source documentation

    Complex conjugation sends a weight to its conjugate after conjugating its Cartan argument.

    def conjugateCartanWeight (χ : complexifiedSubalgebra L H → ℂ) :
    complexifiedSubalgebra L H → ℂ := fun h => star (χ (cartanConjugation L H h))
…

    Mentions: OAI.PolycyclicRecognition.complexifiedSubalgebra, OAI.PolycyclicRecognition.cartanConjugation

  4. theorem OAI.PolycyclicRecognition.conjugation_ad_sub_pow line 33
  5. theorem OAI.PolycyclicRecognition.conjugation_mem_genWeightSpace line 60