DiscreteUnipotentGroup.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Polycyclicity of discrete upper-unipotent groups

An inducing representation turns the polynomial logarithm of every abelian subgroup into a discrete integral submodule. Matrix nilpotence and the abelian-subgroup criterion then supply a finite cyclic series.

theorem OAI.PolycyclicRecognition.isPolycyclic_of_discrete_strictUpper_representation line 22

Source documentation

Every discrete faithfully represented upper-unipotent real matrix group is polycyclic. No finite-generation assumption is needed.

theorem isPolycyclic_of_discrete_strictUpper_representation
    {n : ℕ} (ρ : H →* (Matrix (Fin n) (Fin n) ℝ)ˣ)
    (hρ : Topology.IsInducing (fun h => (ρ h : Matrix (Fin n) (Fin n) ℝ)))
    (hinj : Function.Injective ρ)
    (hu : ∀ h, StrictUpper ((ρ h : Matrix (Fin n) (Fin n) ℝ) - 1)) :
    IsPolycyclic H := by
…

Mentions: OAI.PolycyclicRecognition.StrictUpper, OAI.PolycyclicRecognition.IsPolycyclic