OAI/GroupTheory/PolycyclicRecognition/Algebra/CoordinateBilinearExpansion.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite-coordinate expansion of the transported Lie bracket

  1. def OAI.PolycyclicRecognition.coordinateBilinearUnit line 15

    Source documentation

    A single elementary coordinate bilinear map.

    def coordinateBilinearUnit {n : ℕ} (i j k : Fin n) :
    (Fin n → ℝ) →L[ℝ] (Fin n → ℝ) →L[ℝ] (Fin n → ℝ) :=
…
  2. theorem OAI.PolycyclicRecognition.coordinateBilinearUnit_apply line 20
  3. theorem OAI.PolycyclicRecognition.basisBracket_eq_coordinate_sum line 26

    Source documentation

    Every coordinate bracket is the finite linear combination of its structure constants and elementary bilinear maps.

    theorem basisBracket_eq_coordinate_sum
    {L : Type*} [LieRing L] [LieAlgebra ℝ L] {n : ℕ}
    (b : Basis (Fin n) ℝ L) :
    basisBracket b = ∑ i, ∑ j, ∑ k,
      b.repr ⁅b i, b j⁆ k • coordinateBilinearUnit i j k := by
…

    Mentions: OAI.PolycyclicRecognition.basisBracket, OAI.PolycyclicRecognition.coordinateBilinearUnit