OAI/GroupTheory/PolycyclicRecognition/Lattices/UniformLatticeEmbedding.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform lattices under cocompact embeddings and finite index

  1. theorem OAI.PolycyclicRecognition.IsUniformLattice.map_of_compact_cover line 18

    Source documentation

    A topological group embedding with a compact right fundamental cover carries uniform lattices to uniform lattices.

    theorem IsUniformLattice.map_of_compact_cover [IsTopologicalGroup H]
    {Λ : Subgroup G} (hΛ : IsUniformLattice Λ) (f : G →* H)
    (hf : Topology.IsEmbedding f) (K : Set H) (hK : IsCompact K)
    (hcover : ∀ h : H, ∃ (g : G) (k : H), k ∈ K ∧ f g * k = h) :
    IsUniformLattice (Λ.map f) := by
…
  2. theorem OAI.PolycyclicRecognition.IsUniformLattice.finiteIndex line 47

    Source documentation

    A finite-index subgroup of a uniform lattice is again uniform in the same ambient group.

    theorem IsUniformLattice.finiteIndex [IsTopologicalGroup G]
    {Λ : Subgroup G} (hΛ : IsUniformLattice Λ) (J : Subgroup Λ) [J.FiniteIndex] :
    IsUniformLattice (J.map Λ.subtype) := by
…