OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanBoxSchemes.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed submersive words in the actual Cartan box coordinates

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_box_normalized_bound line 34

    Source documentation

    The endpoint word is fixed from the limiting genuine Cartan box law. The only external inputs are the stated exponential realization and Haar chart, which provide the faithful realization and injective exponential.

    theorem exists_box_normalized_bound
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput

  2. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_box_submersive_scheme line 79

    Source documentation

    The endpoint word is fixed from the limiting genuine Cartan box law. The only external inputs are the stated exponential realization and Haar chart, which provide the faithful realization and injective exponential.

    theorem exists_box_submersive_scheme
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput