HeightFactorization.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Factoring matrix height through the canonical quotient

A continuous vector-valued homomorphism killing the kernel of an open quotient homomorphism factors continuously, hence real-linearly, through that quotient. For triangular representations, unipotence on the kernel supplies this condition.

theorem OAI.PolycyclicRecognition.exists_continuousLinearMap_of_quotient_kernel line 26

Source documentation

Quotient factorization is linear, not only an abstract additive map.

theorem exists_continuousLinearMap_of_quotient_kernel
    (π : G →* Multiplicative W) (τ : G →* Multiplicative V)
    (hπ : Function.Surjective π)
    (hquot : Topology.IsQuotientMap (fun g => (π g).toAdd))
    (hτ : Continuous (fun g => (τ g).toAdd)) (hker : π.ker ≤ τ.ker) :
    ∃ T : W →L[ℝ] V, ∀ g, T (π g).toAdd = (τ g).toAdd := by
…

theorem OAI.PolycyclicRecognition.continuous_triangular_height line 58
Source documentation
Continuity of the matrix representation gives continuity of logarithmic height, since the diagonal entries remain positive.
```
theorem continuous_triangular_height {n : ℕ} (ρ : G →* positiveTriangular n)
    (hρ : Continuous (fun g => matrix (ρ g))) :
    Continuous (fun g => (height (ρ g)).toAdd) := by
…
```
Mentions: OAI.PolycyclicRecognition.positiveTriangular

theorem OAI.PolycyclicRecognition.exists_linear_height_factor_of_kernel_unipotent line 69

Source documentation

A representation unipotent on the height kernel has diagonal height factoring through the height quotient by a continuous linear map.

theorem exists_linear_height_factor_of_kernel_unipotent
    {n : ℕ} (π : G →* Multiplicative W) (ρ : G →* positiveTriangular n)
    (hπ : Function.Surjective π)
    (hquot : Topology.IsQuotientMap (fun g => (π g).toAdd))
    (hρheight : Continuous (fun g => (height (ρ g)).toAdd))
    (hker : ∀ g, π g = 1 → StrictUpper (matrix (ρ g) - 1)) :
    ∃ T : W →L[ℝ] (Fin n → ℝ), ∀ g, (height (ρ g)).toAdd = T (π g).toAdd := by
…

Mentions: OAI.PolycyclicRecognition.positiveTriangular, OAI.PolycyclicRecognition.StrictUpper

theorem OAI.PolycyclicRecognition.polynomialBoundedChainPacking_of_unipotent_kernel line 92

Source documentation

The complete packing bridge needs only an open height quotient and a compatible triangular representation unipotent on its kernel.

theorem polynomialBoundedChainPacking_of_unipotent_kernel
    {G W : Type*} [Group G] [NormedAddCommGroup W] [NormedSpace ℝ W]
    [MetricSpace G] [IsIsometricSMul G G] [ProperSpace G] [DecidableEq G]
    {n : ℕ} [NeZero n]
    (π : G →* Multiplicative W) (ρ : G →* positiveTriangular n)
    (hπ : Function.Surjective π)
    (hquot : Topology.IsQuotientMap (fun g => (π g).toAdd))
    (hρ : Topology.IsInducing (fun g => matrix (ρ g)))
    (hker : ∀ g, π g = 1 → StrictUpper (matrix (ρ g) - 1)) :
    PolynomialBoundedChainPacking (fun g => (π g).toAdd) := by
…

Mentions: OAI.PolycyclicRecognition.positiveTriangular, OAI.PolycyclicRecognition.StrictUpper, OAI.PolycyclicRecognition.PolynomialBoundedChainPacking