OAI/GroupTheory/PolycyclicRecognition/Geometry/SequenceCartanTupleLifts.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Controlled transition lifts give compatible lifts of target tuples

The previous Cartan prefixes act on the nilpotent transitions. Their logarithmic size remains subexponential, and their height tends to zero on the scale, so these actions preserve each specified template box.

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_sequence_accumulated_tuple_lifts line 37

    Source documentation

    Single-transition decompositions determine compatible tuple lifts. No compatibility of independently chosen decompositions is assumed.

    theorem exists_sequence_accumulated_tuple_lifts
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput