PolynomialCoordinateGroup.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The group carried by a polynomial coordinate law

This type keeps the group multiplication distinct from vector addition. The exponential-coordinate bijection is the identity on underlying points.

def OAI.PolycyclicRecognition.PolynomialCoordinateGroup line 19
Source documentation
A separate type for the group structure supplied by a coordinate law.
```
def PolynomialCoordinateGroup (m : V → V → V) (_h : PolynomialGroupLaws m) := V
…
```
Mentions: OAI.PolycyclicRecognition.PolynomialGroupLaws
instance OAI.PolycyclicRecognition.PolynomialCoordinateGroup.(instance at line 25) line 25
def OAI.PolycyclicRecognition.PolynomialCoordinateGroup.exp line 35
Source documentation
Exponential coordinates identify the underlying sets bijectively.
```
def exp : V ≃ PolynomialCoordinateGroup m h := Equiv.refl _
```
Mentions: OAI.PolycyclicRecognition.PolynomialCoordinateGroup
theorem OAI.PolycyclicRecognition.PolynomialCoordinateGroup.exp_zero line 37
theorem OAI.PolycyclicRecognition.PolynomialCoordinateGroup.exp_neg line 39
theorem OAI.PolycyclicRecognition.PolynomialCoordinateGroup.exp_add_smul line 41
theorem OAI.PolycyclicRecognition.PolynomialCoordinateGroup.exp_mul line 45

def OAI.PolycyclicRecognition.polynomialWord line 50

Source documentation

A word evaluated directly by the polynomial multiplication.

def polynomialWord (m : V → V → V) (X : I → V) : List (I × ℝ) → V
  | [] => 0
  | (i, t) :: w => m (t • X i) (polynomialWord m X w)

/-- The direct polynomial evaluation is exactly the generator group word. -/

theorem OAI.PolycyclicRecognition.exp_polynomialWord line 55
Source documentation
The direct polynomial evaluation is exactly the generator group word.
```
theorem exp_polynomialWord (m : V → V → V) (h : PolynomialGroupLaws m)
    (X : I → V) (w : List (I × ℝ)) :
    PolynomialCoordinateGroup.exp m h (polynomialWord m X w) =
      generatorGroupWord X (PolynomialCoordinateGroup.exp m h) w := by
…
```
Mentions: OAI.PolycyclicRecognition.PolynomialGroupLaws, OAI.PolycyclicRecognition.PolynomialCoordinateGroup.exp, OAI.PolycyclicRecognition.polynomialWord, OAI.PolycyclicRecognition.generatorGroupWord