IntrinsicCanonicalHeight.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Canonical height without a global exponential chart

The logarithmic adjoint diagonal is projected back to the canonical linear quotient using a linear left inverse. Exponential basis products give a continuous section and prove the quotient-map property.

theorem OAI.PolycyclicRecognition.exists_intrinsic_canonical_height_with_kernel line 26

theorem OAI.PolycyclicRecognition.exists_intrinsic_canonical_height line 95

Source documentation

The canonical height and its section, without exposing the optional adjoint-kernel property used in the representation construction.

theorem exists_intrinsic_canonical_height {a : ℕ}
    (T : TriangularAdjoint (GroupLieAlgebra (𝓘(ℝ, E)) G) a)
    (q : HeightSpace T.character ≃ₗ[ℝ] W)
    {Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G} (hExp : IsGroupExponential Exp) :
    ∃ π : G →* Multiplicative W,
      Continuous (fun g => (π g).toAdd) ∧
      (∀ x, (π (Exp x)).toAdd = q (heightProjection T.character x)) ∧
      Function.Surjective π ∧ Topology.IsQuotientMap (fun g => (π g).toAdd) ∧
      ∃ s : W → G, Continuous s ∧ s 0 = 1 ∧ ∀ w, (π (s w)).toAdd = w := by
…

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

theorem OAI.PolycyclicRecognition.exists_lipschitz_intrinsic_canonical_height line 118

Source documentation

Metric compatibility of intrinsic height requires neither Dixmier nor an independent triangular representation premise.

theorem exists_lipschitz_intrinsic_canonical_height {a : ℕ}
    (T : TriangularAdjoint (GroupLieAlgebra (𝓘(ℝ, EM)) GM) a)
    (q : HeightSpace T.character ≃ₗ[ℝ] WM) (chains : LinearMetricChains GM)
    {Exp : GroupLieAlgebra (𝓘(ℝ, EM)) GM → GM} (hExp : IsGroupExponential Exp) :
    ∃ π : GM →* Multiplicative WM,
      (∀ x, (π (Exp x)).toAdd = q (heightProjection T.character x)) ∧
      Function.Surjective π ∧ Topology.IsQuotientMap (fun g => (π g).toAdd) ∧
      ∃ K : ℝ, 0 ≤ K ∧ ∀ x y, ‖(π x).toAdd - (π y).toAdd‖ ≤ K * dist x y := by
…

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