OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanBoundaryGeneratorAction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.outside_generator_boundary_action_eq_one line 22

   Source documentation

   A generator outside the retained ray acts trivially on the actual quotient, for every real flow parameter.

   theorem outside_generator_boundary_action_eq_one
       (α₀ : H →ₗ[ℝ] ℝ)
       (Q : NilpotentLieModel ((cartanRootIdeal H) ⧸ M.coneWordIdeal (positiveWeightRay α₀)))
       (ExpQ : GroupLieAlgebra (𝓘(ℝ, Q.modelSpace)) Q.carrier → Q.carrier)
       (hExpQ : IsGroupExponential ExpQ)
       (π : F.N.carrier →* Q.carrier)
       (hπ : ∀ x : cartanRootIdeal H, π (F.ExpN (F.N.equiv x)) =
         ExpQ (Q.equiv (M.coneProjection (positiveWeightRay α₀) x)))
       (α : F.D.carrier →* MulAut Q.carrier) (act : G →* Equiv.Perm Q.carrier)
       (hact : ∀ u d q, act (F.inclusionN u * F.inclusionD d) q = π u * α d q)
       (i : Fin M.letterCount) (hi : (M.weight i : H →ₗ[ℝ] ℝ) ∉ positiveWeightRay α₀)
       (t : ℝ) : act (ExpG (t • (M.letter i : GroupLieAlgebra (𝓘(ℝ, EG)) G))) = 1 := by
   …

   Mentions: OAI.PolycyclicRecognition.NilpotentLieModel, OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.positiveWeightRay