PolynomialGroupLaws.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Polynomial group laws in a fixed coordinate space

The binary Dynkin coefficients are fixed once in the original nilpotent group. Changing its basis changes only the bracket. The group identities and the straight-line one-parameter identities are closed conditions on this finite-dimensional bracket parameter.

def OAI.PolycyclicRecognition.bilinearDynkinPolynomial line 25
Source documentation
The finite Dynkin expression evaluated with a variable bilinear law.
```
def bilinearDynkinPolynomial {c n : ℕ} (a : DynkinCoefficients c n)
    (B : V →L[ℝ] V →L[ℝ] V) (X : Fin n → V) : V :=
…
```
Mentions: OAI.PolycyclicRecognition.DynkinCoefficients
def OAI.PolycyclicRecognition.dynkinProduct line 31
Source documentation
The binary multiplication polynomial, with fixed coefficients.
```
def dynkinProduct {c : ℕ} (a : DynkinCoefficients c 2)
    (B : V →L[ℝ] V →L[ℝ] V) (x y : V) : V :=
…
```
Mentions: OAI.PolycyclicRecognition.DynkinCoefficients
theorem OAI.PolycyclicRecognition.contDiff_bilinearDynkinPolynomial line 35
theorem OAI.PolycyclicRecognition.contDiff_dynkinProduct line 46
theorem OAI.PolycyclicRecognition.continuous_dynkinProduct line 57
def OAI.PolycyclicRecognition.PolynomialGroupLaws line 66
Source documentation
Identities obeyed by a group in exponential coordinates, including its actual straight-line one-parameter subgroups.
```
def PolynomialGroupLaws (m : V → V → V) : Prop :=
…
```

theorem OAI.PolycyclicRecognition.polynomialGroupLaws_of_exp line 74

Source documentation

Exponential coordinates transfer the genuine group axioms, rather than postulating them for a limiting polynomial.

theorem polynomialGroupLaws_of_exp {G : Type*} [Group G]
    (m : V → V → V) (Exp : V → G) (hinj : Function.Injective Exp)
    (hzero : Exp 0 = 1) (hneg : ∀ x, Exp (-x) = (Exp x)⁻¹)
    (hadd : ∀ x (s t : ℝ), Exp ((s + t) • x) = Exp (s • x) * Exp (t • x))
    (hm : ∀ x y, Exp (m x y) = Exp x * Exp y) : PolynomialGroupLaws m := by
…

Mentions: OAI.PolycyclicRecognition.PolynomialGroupLaws

theorem OAI.PolycyclicRecognition.isClosed_dynkinGroupLaws line 97
Source documentation
These group identities persist under convergence of the bracket data.
```
theorem isClosed_dynkinGroupLaws {c : ℕ} (a : DynkinCoefficients c 2) :
    IsClosed {B : V →L[ℝ] V →L[ℝ] V | PolynomialGroupLaws (dynkinProduct a B)} := by
…
```
Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.PolynomialGroupLaws, OAI.PolycyclicRecognition.dynkinProduct
theorem OAI.PolycyclicRecognition.basis_dynkinProduct line 123
Source documentation
Exact coordinate transport of the fixed binary polynomial.
```
theorem basis_dynkinProduct (b : Module.Basis (Fin n) ℝ L)
    {c : ℕ} (a : DynkinCoefficients c 2) (x y : L) :
    dynkinProduct a (basisBracket b) (b.equivFun x) (b.equivFun y) =
      b.equivFun (finiteDynkinPolynomial a ![x, y]) := by
…
```
Mentions: OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.dynkinProduct, OAI.PolycyclicRecognition.basisBracket, OAI.PolycyclicRecognition.finiteDynkinPolynomial