OAI/GroupTheory/PolycyclicRecognition/Geometry/IntegralSemidirectEmbedding.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Cocompact embeddings of integral semidirect groups

A uniform lattice in the integral semidirect group may have translated kernel fibers. No product-lattice assumption is required.

  1. theorem OAI.PolycyclicRecognition.integerVectorHom_isEmbedding line 20
  2. def OAI.PolycyclicRecognition.integralSemidirectEmbedding line 34
  3. theorem OAI.PolycyclicRecognition.integralSemidirectEmbedding_isEmbedding line 39
  4. theorem OAI.PolycyclicRecognition.integralSemidirectEmbedding_compact_cover line 49
  5. theorem OAI.PolycyclicRecognition.uniformLattice_integralSemidirect_image line 69

    Source documentation

    The image of any uniform lattice remains uniform in the real extension.

    theorem uniformLattice_integralSemidirect_image
    [IsTopologicalGroup L]
    (hcont : Continuous (fun p : Multiplicative (Fin n → ℝ) × L => φ p.1 p.2))
    {Γ : Subgroup (L ⋊[ρ] IntegralLatticeGroup n)} (hΓ : IsUniformLattice Γ) :
    IsUniformLattice (Γ.map (integralSemidirectEmbedding ρ φ hφ)) := by
…

    Mentions: OAI.PolycyclicRecognition.IntegralLatticeGroup, OAI.PolycyclicRecognition.integralSemidirectEmbedding