DiscreteHeightKernel.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Discrete subgroups of the intrinsic height kernel

The actual closed nilpotent kernel supplies exponential preimages. The intrinsic faithful triangular representation is upper unipotent on those preimages, so its discrete subgroups are polycyclic.

theorem OAI.PolycyclicRecognition.exists_faithful_unipotent_representation_on_height_kernel line 26

Source documentation

One faithful inducing representation is unipotent on every element of the actual height kernel.

theorem exists_faithful_unipotent_representation_on_height_kernel
    {a : ℕ} (T : TriangularAdjoint (GroupLieAlgebra (𝓘(ℝ, E)) G) a)
    (q : HeightSpace T.character ≃ₗ[ℝ] W)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (π : G →* Multiplicative W)
    (he : ∀ x, (π (Exp x)).toAdd = q (heightProjection T.character x)) :
    ∃ m : ℕ, ∃ ρ : G →* (Matrix (Fin m) (Fin m) ℝ)ˣ,
      Function.Injective ρ ∧
      Topology.IsInducing (fun g => (ρ g : Matrix (Fin m) (Fin m) ℝ)) ∧
      ∀ g ∈ π.ker, StrictUpper ((ρ g : Matrix (Fin m) (Fin m) ℝ) - 1) := by
…

Mentions: OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.HeightSpace, OAI.PolycyclicRecognition.heightProjection, OAI.PolycyclicRecognition.StrictUpper

theorem OAI.PolycyclicRecognition.isPolycyclic_discrete_height_kernel line 62

Source documentation

A discrete subgroup of the height kernel is polycyclic, without an initial finite-generation assumption.

theorem isPolycyclic_discrete_height_kernel
    {a : ℕ} (T : TriangularAdjoint (GroupLieAlgebra (𝓘(ℝ, E)) G) a)
    (q : HeightSpace T.character ≃ₗ[ℝ] W)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (π : G →* Multiplicative W)
    (he : ∀ x, (π (Exp x)).toAdd = q (heightProjection T.character x))
    (Γ : Subgroup G) [DiscreteTopology Γ] (hΓ : Γ ≤ π.ker) : IsPolycyclic Γ := by
…

Mentions: OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.HeightSpace, OAI.PolycyclicRecognition.heightProjection, OAI.PolycyclicRecognition.IsPolycyclic

theorem OAI.PolycyclicRecognition.isPolycyclic_finitelyGenerated_discrete_height_extension line 77

Source documentation

The ambient discrete group is a polycyclic extension of its intersection with the height kernel by its finitely generated abelian height image.

theorem isPolycyclic_finitelyGenerated_discrete_height_extension
    {a : ℕ} (T : TriangularAdjoint (GroupLieAlgebra (𝓘(ℝ, E)) G) a)
    (q : HeightSpace T.character ≃ₗ[ℝ] W)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (π : G →* Multiplicative W)
    (he : ∀ x, (π (Exp x)).toAdd = q (heightProjection T.character x))
    (Γ : Subgroup G) [DiscreteTopology Γ] [Group.FG Γ] : IsPolycyclic Γ := by
…

Mentions: OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.HeightSpace, OAI.PolycyclicRecognition.heightProjection, OAI.PolycyclicRecognition.IsPolycyclic

theorem OAI.PolycyclicRecognition.isPolycyclic_finitelyGenerated_discrete_of_triangularAdjoint line 101
Source documentation
The needed lattice-polycyclicity specialization for an ambient group whose actual adjoint Lie representation is real triangular.
```
theorem isPolycyclic_finitelyGenerated_discrete_of_triangularAdjoint
    {a : ℕ} (T : TriangularAdjoint (GroupLieAlgebra (𝓘(ℝ, E)) G) a)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G) (hExp : IsGroupExponential Exp)
    (Γ : Subgroup G) [DiscreteTopology Γ] [Group.FG Γ] : IsPolycyclic Γ := by
…
```
Mentions: OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.IsPolycyclic