DiscreteLinearNilpotentKernel.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Lattice finiteness from a nilpotent linear kernel

The quotient may include lifted rotational characters. Discrete subgroups of its kernel lift to the constructed simply connected nilpotent Lie model. For a finitely generated ambient discrete subgroup the remaining quotient is finitely generated abelian, giving polycyclicity.

theorem OAI.PolycyclicRecognition.isPolycyclic_discrete_linear_nilpotent_kernel line 26

Source documentation

No finite-generation premise is needed for a discrete subgroup of the constructed nilpotent kernel.

theorem isPolycyclic_discrete_linear_nilpotent_kernel
    (I : LieIdeal ℝ (GroupLieAlgebra (𝓘(ℝ, E)) G)) (hI : LieRing.IsNilpotent I)
    (d : E →ₗ[ℝ] W) (hd : Function.Surjective d)
    (hker : LinearMap.ker d = I.toSubmodule)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (π : G →* Multiplicative W) (hπ : Continuous π)
    (he : ∀ x, (π (Exp x)).toAdd = d x)
    (Γ : Subgroup G) [DiscreteTopology Γ] (hΓ : Γ ≤ π.ker) : IsPolycyclic Γ := by
…

Mentions: OAI.PolycyclicRecognition.IsPolycyclic

theorem OAI.PolycyclicRecognition.isPolycyclic_finitelyGenerated_discrete_of_linear_nilpotent_kernel line 54

Source documentation

A finitely generated discrete subgroup is polycyclic whenever the ambient additive quotient has nilpotent Lie kernel.

theorem isPolycyclic_finitelyGenerated_discrete_of_linear_nilpotent_kernel
    (I : LieIdeal ℝ (GroupLieAlgebra (𝓘(ℝ, E)) G)) (hI : LieRing.IsNilpotent I)
    (d : E →ₗ[ℝ] W) (hd : Function.Surjective d)
    (hker : LinearMap.ker d = I.toSubmodule)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (π : G →* Multiplicative W) (hπ : Continuous π)
    (he : ∀ x, (π (Exp x)).toAdd = d x)
    (Γ : Subgroup G) [DiscreteTopology Γ] [Group.FG Γ] : IsPolycyclic Γ := by
…

Mentions: OAI.PolycyclicRecognition.IsPolycyclic