InvariantTriangularBasis.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Restricting an actual triangular action

An invariant subspace of a simultaneous real triangular action again has a simultaneous triangular basis. The proof chooses the last nonzero coordinate functional and inducts on its invariant kernel. No spectral splitting or solvability hypothesis is needed.

theorem OAI.PolycyclicRecognition.exists_triangular_eigenfunctional line 28

Source documentation

The last active coordinate of a triangular representation is a common eigenfunctional on every nonzero invariant subspace.

theorem exists_triangular_eigenfunctional
    {ι W : Type*} [AddCommGroup W] [Module ℝ W] [Nontrivial W]
    {n : ℕ} (e : W →ₗ[ℝ] (Fin n → ℝ)) (he : Function.Injective e)
    (T : ι → W →ₗ[ℝ] W) (A : ι → Matrix (Fin n) (Fin n) ℝ)
    (hA : ∀ x, (A x).IsUpperTriangular)
    (hinter : ∀ x v, e (T x v) = A x *ᵥ e v) :
    ∃ (p : W →ₗ[ℝ] ℝ), p ≠ 0 ∧
      ∀ x, ∃ c : ℝ, ∀ v, p (T x v) = c * p v := by
…

theorem OAI.PolycyclicRecognition.exists_upperTriangular_basis_of_embedding line 68

Source documentation

Every action embedded into actual upper triangular matrices admits an upper triangular basis on its own finite-dimensional space.

theorem exists_upperTriangular_basis_of_embedding
    {ι W : Type*} [AddCommGroup W] [Module ℝ W] [FiniteDimensional ℝ W]
    {n : ℕ} (e : W →ₗ[ℝ] (Fin n → ℝ)) (he : Function.Injective e)
    (T : ι → W →ₗ[ℝ] W) (A : ι → Matrix (Fin n) (Fin n) ℝ)
    (hA : ∀ x, (A x).IsUpperTriangular)
    (hinter : ∀ x v, e (T x v) = A x *ᵥ e v) :
    ∃ (m : ℕ) (b : Basis (Fin m) ℝ W),
      ∀ x, (LinearMap.toMatrix b b (T x)).IsUpperTriangular := by
…