OAI/GroupTheory/PolycyclicRecognition/Geometry/ComplexCartanJordan.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The semisimple Cartan operator preserves the original triangular flag

  1. def OAI.PolycyclicRecognition.ComplexCartan.semisimpleOperator line 17

    Source documentation

    The full semisimple part, before its imaginary part is removed.

    def semisimpleOperator (h : H) : Module.End ℂ L := weightOperator H (fun χ => χ h)

    Mentions: OAI.PolycyclicRecognition.ComplexCartan.weightOperator

  2. theorem OAI.PolycyclicRecognition.ComplexCartan.semisimpleOperator_apply line 19
  3. theorem OAI.PolycyclicRecognition.ComplexCartan.semisimpleOperator_jordan line 24

    Source documentation

    The root-space scalar operator is precisely the Jordan semisimple part.

    theorem semisimpleOperator_jordan (h : H) :
    semisimpleOperator H h ∈ Algebra.adjoin ℂ {ad ℂ L (h : L)} ∧
      IsNilpotent (ad ℂ L (h : L) - semisimpleOperator H h) := by
…

    Mentions: OAI.PolycyclicRecognition.ComplexCartan.semisimpleOperator

  4. theorem OAI.PolycyclicRecognition.ComplexCartan.semisimpleOperator_upper line 48

    Source documentation

    The semisimple part preserves every upper triangular flag for the original adjoint operator.

    theorem semisimpleOperator_upper {n : ℕ} (b : Basis (Fin n) ℂ L) (h : H)
    (hh : (LinearMap.toMatrix b b (ad ℂ L (h : L))).IsUpperTriangular) :
    (LinearMap.toMatrix b b (semisimpleOperator H h)).IsUpperTriangular := by
…

    Mentions: OAI.PolycyclicRecognition.ComplexCartan.semisimpleOperator