CoordinateSchemeBasis.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Nondegenerate schemes in limiting coordinate groups

The preserved adjoint-conjugation identity turns the spanning adjoint orbits into actual group-word conjugates. Their polynomial endpoint map is exactly the ordered exponential product in the resulting basis.

theorem OAI.PolycyclicRecognition.exp_bilinearAdjointWord line 24

Source documentation

The coordinate adjoint word is realized by the corresponding generator word in the polynomial coordinate group.

theorem exp_bilinearAdjointWord (m : V → V → V) (hg : PolynomialGroupLaws m)
    (B : V →L[ℝ] V →L[ℝ] V) (hc : ExponentialConjugationLaw m B)
    (X : I → V) (w : List (I × ℝ)) (v : V) :
    PolynomialCoordinateGroup.exp m hg (bilinearAdjointWord B X w v) =
      generatorGroupWord X (PolynomialCoordinateGroup.exp m hg) w *
        PolynomialCoordinateGroup.exp m hg v *
        (generatorGroupWord X (PolynomialCoordinateGroup.exp m hg) w)⁻¹ := by
…

Mentions: OAI.PolycyclicRecognition.PolynomialGroupLaws, OAI.PolycyclicRecognition.ExponentialConjugationLaw, OAI.PolycyclicRecognition.PolynomialCoordinateGroup.exp, OAI.PolycyclicRecognition.bilinearAdjointWord, OAI.PolycyclicRecognition.generatorGroupWord

theorem OAI.PolycyclicRecognition.exp_polynomialEndpointScheme line 48
Source documentation
Expanding a polynomial scheme gives its actual generator word.
```
theorem exp_polynomialEndpointScheme {c n : ℕ}
    (a : DynkinCoefficients c 2) (B : V →L[ℝ] V →L[ℝ] V) (hB : IsLieBracket B)
    (hg : PolynomialGroupLaws (dynkinProduct a B)) (X : I → V)
    (w : Fin n → List (I × ℝ)) (i : Fin n → I) (t : Fin n → ℝ) :
    PolynomialCoordinateGroup.exp (dynkinProduct a B) hg
      (polynomialEndpointScheme a w i (B, X) t) =
    generatorGroupWord X (PolynomialCoordinateGroup.exp (dynkinProduct a B) hg)
      (generatorSchemeWord w i t) := by
…
```
Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.IsLieBracket, OAI.PolycyclicRecognition.PolynomialGroupLaws, OAI.PolycyclicRecognition.dynkinProduct, OAI.PolycyclicRecognition.PolynomialCoordinateGroup.exp, OAI.PolycyclicRecognition.polynomialEndpointScheme, OAI.PolycyclicRecognition.generatorGroupWord, OAI.PolycyclicRecognition.generatorSchemeWord

theorem OAI.PolycyclicRecognition.polynomialEndpointScheme_basisProduct line 79

Source documentation

The polynomial formula of a chosen conjugate scheme is the genuine ordered basis product whenever the parameters satisfy the group laws.

theorem polynomialEndpointScheme_basisProduct {c n : ℕ}
    (a : DynkinCoefficients c 2) (B : V →L[ℝ] V →L[ℝ] V) (hB : IsLieBracket B)
    (hg : PolynomialGroupLaws (dynkinProduct a B))
    (X : I → V) (b : Basis (Fin n) ℝ V)
    (w : Fin n → List (I × ℝ)) (i : Fin n → I)
    (hb : ∀ k (s : ℝ), PolynomialCoordinateGroup.exp (dynkinProduct a B) hg (s • b k) =
      generatorGroupWord X (PolynomialCoordinateGroup.exp (dynkinProduct a B) hg) (w k) *
        PolynomialCoordinateGroup.exp (dynkinProduct a B) hg (s • X (i k)) *
        (generatorGroupWord X (PolynomialCoordinateGroup.exp (dynkinProduct a B) hg) (w k))⁻¹)
    (t : Fin n → ℝ) :
    PolynomialCoordinateGroup.exp (dynkinProduct a B) hg
      (polynomialEndpointScheme a w i (B, X) t) =
…

Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.IsLieBracket, OAI.PolycyclicRecognition.PolynomialGroupLaws, OAI.PolycyclicRecognition.dynkinProduct, OAI.PolycyclicRecognition.PolynomialCoordinateGroup.exp, OAI.PolycyclicRecognition.generatorGroupWord, OAI.PolycyclicRecognition.polynomialEndpointScheme

theorem OAI.PolycyclicRecognition.exists_coordinate_basis_scheme line 111

Source documentation

Every normalized word-generated limiting law has an actual basis scheme. Its smoothness is proved independently in PolynomialEndpointSchemes.

theorem exists_coordinate_basis_scheme {J : Type*} {c : ℕ}
    (a : DynkinCoefficients c 2) (B : V →L[ℝ] V →L[ℝ] V) (hB : IsLieBracket B)
    (hg : PolynomialGroupLaws (dynkinProduct a B))
    (hc : ExponentialConjugationLaw (dynkinProduct a B) B)
    (X : I → V) (b₀ : Basis J ℝ V) (w₀ : J → FreeMagma I)
    (hw₀ : ∀ j, evalBilinearWord B X (w₀ j) = b₀ j) :
    ∃ (b : Basis (Fin (finrank ℝ V)) ℝ V)
      (w : Fin (finrank ℝ V) → List (I × ℝ)) (i : Fin (finrank ℝ V) → I),
      ∀ t, PolynomialCoordinateGroup.exp (dynkinProduct a B) hg
        (polynomialEndpointScheme a w i (B, X) t) =
          basisExponentialProduct (PolynomialCoordinateGroup.exp (dynkinProduct a B) hg) b t := by
…

Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.IsLieBracket, OAI.PolycyclicRecognition.PolynomialGroupLaws, OAI.PolycyclicRecognition.dynkinProduct, OAI.PolycyclicRecognition.ExponentialConjugationLaw, OAI.PolycyclicRecognition.evalBilinearWord, OAI.PolycyclicRecognition.PolynomialCoordinateGroup.exp, OAI.PolycyclicRecognition.polynomialEndpointScheme, OAI.PolycyclicRecognition.basisExponentialProduct