TriangularLieDifferential.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The differential of a triangular Lie-group realization

The differential of a continuous injective matrix-group homomorphism is a Lie algebra homomorphism. Precisely, John M. Lee, Introduction to Smooth Manifolds, second edition, GTM 218 (2013), Problem 20-11(b), pp.537–538, gives automatic smoothness; Theorem 8.44, p.195, gives the induced Lie algebra homomorphism; Proposition 8.41, pp.193–195, identifies the matrix-group Lie algebra with the matrix commutator algebra. Its injectivity follows from Proposition 7.17, pp.157–158 (see its proof using Theorem 7.5 and the Global Rank Theorem 4.14(b)).

The input retains only the Lie homomorphism and its equality to the matrix-valued derivative. Its injectivity is proved using faithful one-parameter subgroups. The derivative is upper triangular and solvable, and admits a simultaneous adjoint basis.

def OAI.PolycyclicRecognition.MatrixLieDifferentialInput line 52
Source documentation
The matrix derivative supplied by the precisely cited Lee results. No injectivity, triangularity or spectral consequence is assumed.
```
def MatrixLieDifferentialInput : Prop :=
…
```

theorem OAI.PolycyclicRecognition.matrixLieDifferential_injective line 66

Source documentation

Faithfulness of the actual derivative follows from faithfulness of the group map, without an immersion theorem.

theorem matrixLieDifferential_injective
    (S : SimplyConnectedSolvableLieModel) (n : ℕ)
    (ρ : S.carrier →* Matrix.GeneralLinearGroup (Fin n) ℝ)
    (hi : Function.Injective ρ)
    (d : GroupLieAlgebra (𝓘(ℝ, S.modelSpace)) S.carrier →ₗ⁅ℝ⁆
      Matrix (Fin n) (Fin n) ℝ)
    (hd : HasMFDerivAt (𝓘(ℝ, S.modelSpace))
      (𝓘(ℝ, Matrix (Fin n) (Fin n) ℝ))
      (fun g => (ρ g : Matrix (Fin n) (Fin n) ℝ)) 1
      d.toLinearMap.toContinuousLinearMap) : Function.Injective d :=
…

Mentions: OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel

theorem OAI.PolycyclicRecognition.hasMFDerivAt_upperTriangular line 81

Source documentation

Differentiating the identically zero entries below the diagonal preserves upper triangularity.

theorem hasMFDerivAt_upperTriangular
    {E G : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [TopologicalSpace G] [ChartedSpace E G] {n : ℕ}
    {f : G → Matrix (Fin n) (Fin n) ℝ} {a : G}
    {d : TangentSpace (𝓘(ℝ, E)) a →L[ℝ] Matrix (Fin n) (Fin n) ℝ}
    (hd : HasMFDerivAt (𝓘(ℝ, E)) (𝓘(ℝ, Matrix (Fin n) (Fin n) ℝ)) f a d)
    (hf : ∀ g, (f g).IsUpperTriangular) (v : TangentSpace (𝓘(ℝ, E)) a) :
    (d v).IsUpperTriangular := by
…

theorem OAI.PolycyclicRecognition.IsRealTriangulable.exists_triangularAdjoint line 110
Source documentation
CT's actual closed triangular matrix realization supplies a simultaneous adjoint basis once the narrow matrix-differential input is given. The algebraic conclusions come from the proved matrix lemmas.
```
theorem IsRealTriangulable.exists_triangularAdjoint
    (differential : MatrixLieDifferentialInput)
    (S : SimplyConnectedSolvableLieModel) (hS : IsRealTriangulable S) :
    ∃ m : ℕ, Nonempty (TriangularAdjoint
      (GroupLieAlgebra (𝓘(ℝ, S.modelSpace)) S.carrier) m) := by
…
```
Mentions: OAI.PolycyclicRecognition.MatrixLieDifferentialInput, OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel, OAI.PolycyclicRecognition.IsRealTriangulable, OAI.PolycyclicRecognition.TriangularAdjoint
theorem OAI.PolycyclicRecognition.IsRealTriangulable.lieAlgebra_isSolvable line 122
theorem OAI.PolycyclicRecognition.exists_triangularAdjoint_metric_model line 136
Source documentation
The published CT reduction and faithful differential give the actual adjoint-basis model, with the metric comparison proved from the three proper cocompact arrows.
```
theorem exists_triangularAdjoint_metric_model
    (ct : CornulierTesseraModelInput) (metricInput : GeodesicMetricExistenceInput)
    (differential : MatrixLieDifferentialInput) (S : SimplyConnectedSolvableLieModel) :
    ∃ T : SimplyConnectedSolvableLieModel, ∃ m : ℕ,
      Nonempty (TriangularAdjoint
        (GroupLieAlgebra (𝓘(ℝ, T.modelSpace)) T.carrier) m) ∧
      ∃ (dS : ProperChainMetric S.carrier) (dT : ProperChainMetric T.carrier),
        letI := dS.compatibleMetric
…
```
Mentions: OAI.PolycyclicRecognition.CornulierTesseraModelInput, OAI.PolycyclicRecognition.GeodesicMetricExistenceInput, OAI.PolycyclicRecognition.MatrixLieDifferentialInput, OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel, OAI.PolycyclicRecognition.TriangularAdjoint, OAI.PolycyclicRecognition.ProperChainMetric