OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanBoundaryLeaf.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The nilpotent leaf bound from the actual Cartan support data

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.nilpotent_leaf_bound_from_boundary_traces line 27

    Source documentation

    The positive relation and separation are derived from the actual unimodular Cartan support datum. Boundary volume comparisons and the outside-generator quotient actions then give the whole leaf bound.

    theorem nilpotent_leaf_bound_from_boundary_traces
    (hunimod : ∀ v : GroupLieAlgebra (𝓘(ℝ, EG)) G, LinearMap.trace ℝ _ (ad ℝ _ v) = 0)
    (eW : HeightSpace T.character ≃ₗ[ℝ] W)
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.HeightSpace, OAI.PolycyclicRecognition.ExponentialLinearRealizationInput