OAI/GroupTheory/PolycyclicRecognition/Lattices/NilpotentExtensionLattice.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

A uniform lattice after completing only the nilpotent kernel

The quotient is still discrete. This is an intermediate construction, not a claim that the resulting group is connected.

  1. def OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.completedExtensionLattice line 22
  2. theorem OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.completedExtensionLattice_discrete line 25
  3. theorem OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.extension_action_lattice line 43
  4. theorem OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.completedExtensionLattice_uniform line 53

    Source documentation

    Compactness of the original kernel fundamental cover is retained by the completed extension, even though its quotient may be infinite and nonsplit.

    theorem completedExtensionLattice_uniform :
    IsUniformLattice (C.completedExtensionLattice S σ hσ) := by
…
  5. def OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.completedExtensionLatticeEquiv line 73

    Source documentation

    The lattice is isomorphic to the original group, not a quotient by its center.

    def completedExtensionLatticeEquiv : G ≃* C.completedExtensionLattice S σ hσ :=
…
  6. theorem OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.completedExtension_topologicalGroup line 76