OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanBoundaryLeafTemplate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The template label supplies every generator action needed for the leaf bound

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.nilpotent_leaf_bound_of_template_boundary_traces line 33

    Source documentation

    Equal-set volume traces for the constructed ray actions imply the whole nilpotent-leaf bound; the exceptional-ray choices are derived from preservation of the actual support templates.

    theorem nilpotent_leaf_bound_of_template_boundary_traces
    {P : Type*} [SimplyConnectedSpace G]
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput