OAI/GroupTheory/PolycyclicRecognition/Algebra/ComplexCharacterLift.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.eq_of_continuous_complex_exp_eq line 21

   Source documentation

   Two continuous lifts through the complex exponential agree everywhere when they agree at one point of a connected domain.

   theorem eq_of_continuous_complex_exp_eq
       {X : Type*} [TopologicalSpace X] [PreconnectedSpace X]
       {f g : X → ℂ} (hf : Continuous f) (hg : Continuous g)
       (he : ∀ x, Complex.exp (f x) = Complex.exp (g x))
       (x₀ : X) (h₀ : f x₀ = g x₀) : f = g := by
   …

2. theorem OAI.PolycyclicRecognition.exists_additive_lift_complex_character line 32

   Source documentation

   A continuous character into the nonzero complex numbers has a normalized additive lift on a simply connected group.

   theorem exists_additive_lift_complex_character
       {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
       [SimplyConnectedSpace G] [LocallyPathConnectedSpace G]
       (χ : G →* ℂˣ) (hχ : Continuous (fun g => (χ g : ℂ))) :
       ∃ π : G →* Multiplicative ℂ, Continuous (fun g => (π g).toAdd) ∧
         ∀ g, Complex.exp (π g).toAdd = (χ g : ℂ) := by
   …

3. theorem OAI.PolycyclicRecognition.additive_lift_complex_character_on_curve line 59

   Source documentation

   The additive lift recovers the exact weight along a continuous one-parameter curve starting at the identity.

   theorem additive_lift_complex_character_on_curve
       {G : Type*} [Group G] [TopologicalSpace G]
       (χ : G →* ℂˣ) (π : G →* Multiplicative ℂ)
       (hπ : Continuous (fun g => (π g).toAdd))
       (he : ∀ g, Complex.exp (π g).toAdd = (χ g : ℂ))
       (γ : ℝ → G) (hγ : Continuous γ) (hγ0 : γ 0 = 1)
       (z : ℂ) (hz : ∀ t, (χ (γ t) : ℂ) = Complex.exp ((t : ℂ) * z)) :
       ∀ t, (π (γ t)).toAdd = (t : ℂ) * z := by
   …