SolvableLatticePolycyclic.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Polycyclicity of lattices in simply connected solvable Lie groups

Complex adjoint weights include rotations. Their normalized additive lifts have nilpotent Lie kernel and a real vector-space quotient. Discrete subgroups of the kernel are polycyclic, and finite generation controls the abelian image.

theorem OAI.PolycyclicRecognition.isPolycyclic_finitelyGenerated_discrete_solvableLieGroup line 21

Source documentation

Every finitely generated discrete subgroup of a connected simply connected finite-dimensional real solvable Lie group is polycyclic.

theorem isPolycyclic_finitelyGenerated_discrete_solvableLieGroup
    {E G : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    [MetricSpace G] [ChartedSpace E G] [Group G] [LieGroup (𝓘(ℝ, E)) ⊤ G]
    [SimplyConnectedSpace G] [Group.IsSolvable G]
    (Γ : Subgroup G) [DiscreteTopology Γ] [Group.FG Γ] : IsPolycyclic Γ := by
…

Mentions: OAI.PolycyclicRecognition.IsPolycyclic

theorem OAI.PolycyclicRecognition.isPolycyclic_uniformLattice_solvableLieGroup line 42
Source documentation
The full solvable lattice theorem used by the recognition argument.
```
theorem isPolycyclic_uniformLattice_solvableLieGroup
    (S : SimplyConnectedSolvableLieModel) (Λ : Subgroup S.carrier)
    (hΛ : IsUniformLattice Λ) : IsPolycyclic Λ := by
…
```
Mentions: OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel, OAI.PolycyclicRecognition.IsPolycyclic