OAI/GroupTheory/PolycyclicRecognition/Lattices/NilpotentKernelCompletion.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Induction data for completing a nilpotent group with a real kernel

The integer grid is required only to lie in the embedded group. The kernel may already contain real one-parameter groups, so discreteness is not assumed.

  1. structure OAI.PolycyclicRecognition.NilpotentKernelCompletion line 19
  2. def OAI.PolycyclicRecognition.NilpotentKernelCompletion.of_polynomial_kernel line 47
  3. theorem OAI.PolycyclicRecognition.NilpotentKernelCompletion.hom_ext line 64

    Source documentation

    The polynomial integer grid determines every smooth homomorphism.

    theorem hom_ext (M : Type) [RealNormedLieAlgebra M] [FiniteDimensional ℝ M]
    [PM : PolynomialExponentialCoordinates M]
    (φ ψ : C.carrier →* M)
    (hφ : ContMDiff (𝓘(ℝ, C.carrier)) (𝓘(ℝ, M)) ∞ φ)
    (hψ : ContMDiff (𝓘(ℝ, C.carrier)) (𝓘(ℝ, M)) ∞ ψ)
    (h : ∀ a, φ (C.embed a) = ψ (C.embed a)) : φ = ψ := by
…

    Mentions: OAI.PolycyclicRecognition.RealNormedLieAlgebra, OAI.PolycyclicRecognition.PolynomialExponentialCoordinates

  4. theorem OAI.PolycyclicRecognition.NilpotentKernelCompletion.automorphism_extension line 93

    Source documentation

    Compatible automorphisms of the original group extend with their inverse.

    theorem automorphism_extension (a : MulAut H)
    (ha : ContMDiff (𝓘(ℝ, K)) (𝓘(ℝ, C.carrier)) ∞
      ((C.embed.comp a.toMonoidHom).comp i))
    (hai : ContMDiff (𝓘(ℝ, K)) (𝓘(ℝ, C.carrier)) ∞
      ((C.embed.comp a.symm.toMonoidHom).comp i)) :
    ∃ A : MulAut C.carrier, ContMDiff (𝓘(ℝ, C.carrier)) (𝓘(ℝ, C.carrier)) ∞ A ∧
      ContMDiff (𝓘(ℝ, C.carrier)) (𝓘(ℝ, C.carrier)) ∞ A.symm ∧
      ∀ h, A (C.embed h) = C.embed (a h) := by
…