OAI/GroupTheory/PolycyclicRecognition/Lattices/UniformLatticeFiniteIndexEmbedding.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.IsUniformLattice.comap_of_le_range line 13

   Source documentation

   If a closed subgroup contains the lattice, its induced lattice is uniform.

   theorem IsUniformLattice.comap_of_le_range
       {Γ : Subgroup G} (hΓ : IsUniformLattice Γ) (f : H →* G)
       (hf : Topology.IsClosedEmbedding f) (hle : Γ ≤ f.range) :
       IsUniformLattice (Γ.comap f) := by
   …

2. theorem OAI.PolycyclicRecognition.IsUniformLattice.comap_finiteIndex line 38

   Source documentation

   Restriction to a closed finite-index subgroup preserves a uniform lattice.

   theorem IsUniformLattice.comap_finiteIndex [IsTopologicalGroup G]
       {Γ : Subgroup G} (hΓ : IsUniformLattice Γ) (f : H →* G)
       (hf : Topology.IsClosedEmbedding f) [f.range.FiniteIndex] :
       IsUniformLattice (Γ.comap f) := by
   …