OAI/GroupTheory/PolycyclicRecognition/Geometry/ComplexWeightLift.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.complexMatrixDiagonalHom line 15
2. theorem OAI.PolycyclicRecognition.exists_lifted_complex_matrix_weights line 23

   Source documentation

   Simply connectedness lifts all diagonal characters, preserving the specified linear weights on exponential curves.

   theorem exists_lifted_complex_matrix_weights
       (ρ : G →* Matrix (Fin n) (Fin n) ℂ) (hρ : Continuous ρ)
       (hu : ∀ g, (ρ g).IsUpperTriangular)
       (d : V →ₗ[ℝ] (Fin n → ℂ)) (Exp : V → G)
       (hExp0 : Exp 0 = 1) (hcurve : ∀ x, Continuous (fun t : ℝ => Exp (t • x)))
       (he : ∀ x i, ρ (Exp x) i i = Complex.exp (d x i)) :
       ∃ π : G →* Multiplicative (Fin n → ℂ),
         Continuous (fun g => (π g).toAdd) ∧ ∀ x, (π (Exp x)).toAdd = d x := by
   …