OAI/GroupTheory/PolycyclicRecognition/Geometry/ComplexWeightRange.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_range_restricted_complex_weights line 18

   Source documentation

   Exponential generation ensures the lifted character takes values in the real linear image of its derivative.

   theorem exists_range_restricted_complex_weights
       {Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G} (hExp : IsGroupExponential Exp)
       (d : E →ₗ[ℝ] (Fin n → ℂ)) (π : G →* Multiplicative (Fin n → ℂ))
       (hπ : Continuous (fun g => (π g).toAdd))
       (he : ∀ x, (π (Exp x)).toAdd = d x) :
       ∃ q : G →* Multiplicative d.range, Continuous (fun g => (q g).toAdd) ∧
         ∀ x, (q (Exp x)).toAdd = d.rangeRestrict x := by
   …