OAI/GroupTheory/PolycyclicRecognition/Algebra/GradedHorizontalStructure.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.gradedGeneratorLinearMap line 17

   Source documentation

   The degree-one part of exponential coordinates is linear in the original horizontal vector.

   def gradedGeneratorLinearMap
       {L : Type*} [LieRing L] [LieAlgebra ℝ L] {n : ℕ}
       (b : Basis (Fin n) ℝ L) (cost : Fin n → ℝ) (s : ℝ) :
       L →ₗ[ℝ] (Fin n → ℝ) where
   …

2. def OAI.PolycyclicRecognition.gradedGeneratorMap line 31
3. theorem OAI.PolycyclicRecognition.gradedGeneratorMap_apply line 38
4. theorem OAI.PolycyclicRecognition.gradedGenerator_word_height line 46

   Source documentation

   A height that vanishes on brackets is unchanged by the horizontal projection in a basis made of unit-cost words.

   theorem gradedGenerator_word_height
       {L W I : Type*} [LieRing L] [LieAlgebra ℝ L]
       [AddCommGroup W] [Module ℝ W] [Fintype I] [DecidableEq I]
       (X : I → L) (S : Finset (FreeMagma I)) (β : WordBasisSelections X S)
       (h : L →ₗ[ℝ] W) (hh : ∀ x y : L, h ⁅x, y⁆ = 0) (v : L) :
       let b := WordBasisSelections.basis X S β
   …

   Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.WordBasisSelections.basis

5. theorem OAI.PolycyclicRecognition.graded_exponentialConjugationLaw line 77

   Source documentation

   The actual representation-derived conjugation identity is closed under the graded rescaling.

   theorem graded_exponentialConjugationLaw
       {L G A : Type*} [LieRing L] [LieAlgebra ℝ L] [FiniteDimensional ℝ L]
       [Group G] [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A]
       {n c : ℕ} (b : Basis (Fin n) ℝ L) (cost : Fin n → ℝ)
       (hweight : ∀ i j k, b.repr ⁅b i, b j⁆ k ≠ 0 → cost i + cost j ≤ cost k)
       (Exp : L → G) (hinj : Function.Injective Exp)
       (hneg : ∀ x, Exp (-x) = (Exp x)⁻¹)
       (a : DynkinCoefficients c 2)
       (hm : ∀ x y, Exp (finiteDynkinPolynomial a ![x, y]) = Exp x * Exp y)
       (j : L →ₗ⁅ℝ⁆ A) (ρ : G →* Aˣ) (hρ : Function.Injective ρ)
       (hmatch : ∀ x, ρ (Exp x) = algebraExpUnit (j x)) :
       ExponentialConjugationLaw (dynkinProduct a (gradedCoordinateBracket b cost))
   …

   Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial, OAI.PolycyclicRecognition.algebraExpUnit, OAI.PolycyclicRecognition.ExponentialConjugationLaw, OAI.PolycyclicRecognition.dynkinProduct, OAI.PolycyclicRecognition.gradedCoordinateBracket