SemidirectPrefixTuples.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Exact accumulated lifts of a finite tuple of transitions

theorem OAI.PolycyclicRecognition.wordPrefix_succ_left line 12
theorem OAI.PolycyclicRecognition.wordPrefix_relative_transitions line 18
theorem OAI.PolycyclicRecognition.wordPrefix_height_bound line 24
def OAI.PolycyclicRecognition.basedTuplePosition line 41
Source documentation
The tuple positions with the identity adjoined at time zero.
```
def basedTuplePosition {G : Type*} [One G] {h : ℕ} (x : Fin h → G) (j : ℕ) : G :=
…
```
theorem OAI.PolycyclicRecognition.basedTuplePosition_zero line 44
theorem OAI.PolycyclicRecognition.basedTuplePosition_succ line 47
theorem OAI.PolycyclicRecognition.cartan_word_prefix_identity line 53
theorem OAI.PolycyclicRecognition.prefixCoordinateEquiv_eq_wordPrefix line 68
theorem OAI.PolycyclicRecognition.prefixCoordinateEquiv_symm_wordPrefix line 81
theorem OAI.PolycyclicRecognition.tuple_accumulated_cartan_lifts line 88

theorem OAI.PolycyclicRecognition.tuple_accumulated_lifts_eq line 101

Source documentation

Individual lifts of the successive relative transitions reproduce the entire tuple, with the required conjugations by preceding Cartan prefixes.

theorem tuple_accumulated_lifts_eq (ι : N →* G) (κ : D →* G) (φ : D →* MulAut N)
    (hc : ∀ d n, ι (φ d n) = κ d * ι n * (κ d)⁻¹)
    {h : ℕ} (x : Fin h → G) (u : ℕ → N) (d : ℕ → D)
    (hprod : ∀ j < h, ι (u j) * κ (d j) =
      (basedTuplePosition x j)⁻¹ * basedTuplePosition x (j + 1)) :
    ∀ i : Fin h,
      ι (prefixCoordinateEquiv h (fun j => φ (wordPrefix d j.val) (u j.val)) i) *
        κ (wordPrefix d (i.val + 1)) = x i := by
…

Mentions: OAI.PolycyclicRecognition.basedTuplePosition, OAI.PolycyclicRecognition.prefixCoordinateEquiv, OAI.PolycyclicRecognition.wordPrefix