exists_nontrivial_weightSpace_of_lieIdeal

English

If a LieModule IsTriangularizable and a LieIdeal A ⊆ L has a nontrivial weight space for some χ0 on A, then there exists χ on L with a nontrivial weight space for V.

Русский

Если модуль Ли является треугольным и существует тензорная идеал A ⊆ L с неупорядоченным весовым пространством для χ0, тогда существует χ на L с ненулевым весовым пространством для V.

LaTeX

$$$\\exists \\chi \\in \\operatorname{Dual}(k,L): \\operatorname{Nontrivial}(\\operatorname{weightSpace}(V,\\chi)).$$$

Lean4

theorem exists_nontrivial_weightSpace_of_lieIdeal [LieModule.IsTriangularizable k L V] (A : LieIdeal k L)
    (hA : IsCoatom A.toSubmodule) (χ₀ : Module.Dual k A) [Nontrivial (weightSpace V χ₀)] :
    ∃ (χ : Module.Dual k L), Nontrivial (weightSpace V χ) :=
  by
  obtain ⟨z, -, hz⟩ := SetLike.exists_of_lt (hA.lt_top)
  let e : (k ∙ z) ≃ₗ[k] k := (LinearEquiv.toSpanNonzeroSingleton k L z <| by aesop).symm
  have he : ∀ x, e x • z = x := by simp [e]
  have hA : IsCompl A.toSubmodule (k ∙ z) := isCompl_span_singleton_of_isCoatom_of_notMem hA hz
  let π₁ : L →ₗ[k] A := A.toSubmodule.linearProjOfIsCompl (k ∙ z) hA
  let π₂ : L →ₗ[k] (k ∙ z) := (k ∙ z).linearProjOfIsCompl (↑A) hA.symm
  set W : LieSubmodule k L V := weightSpaceOfIsLieTower k V χ₀
  obtain ⟨c, hc⟩ : ∃ c, (toEnd k _ W z).HasEigenvalue c :=
    by
    have : Nontrivial W := inferInstanceAs (Nontrivial (weightSpace V χ₀))
    apply Module.End.exists_hasEigenvalue_of_genEigenspace_eq_top
    exact LieModule.IsTriangularizable.maxGenEigenspace_eq_top z
  obtain ⟨⟨v, hv⟩, hvc⟩ := hc.exists_hasEigenvector
  have hv' : ∀ (x : ↥A), ⁅x, v⁆ = χ₀ x • v := by simpa [W, weightSpaceOfIsLieTower, mem_weightSpace] using hv
  use (χ₀.comp π₁) + c • (e.comp π₂)
  refine nontrivial_of_ne ⟨v, ?_⟩ 0 ?_
  · rw [mem_weightSpace]
    intro x
    have hπ : (π₁ x : L) + π₂ x = x := hA.projection_add_projection_eq_self x
    suffices ⁅hA.symm.projection x, v⁆ = (c • e (π₂ x)) • v by
      calc
        ⁅x, v⁆ = ⁅π₁ x, v⁆ + ⁅hA.symm.projection x, v⁆ := congr(⁅$hπ.symm, v⁆) ▸ add_lie _ _ _
        _ = χ₀ (π₁ x) • v + (c • e (π₂ x)) • v := by rw [hv' (π₁ x), this]
        _ = _ := by simp [add_smul]
    calc
      ⁅hA.symm.projection x, v⁆ = e (π₂ x) • ↑(c • ⟨v, hv⟩ : W) := by
        rw [IsCompl.projection_apply, ← he, smul_lie, ← hvc.apply_eq_smul]; rfl
      _ = (c • e (π₂ x)) • v := by rw [smul_assoc, smul_comm]; rfl
  · simpa [ne_eq, LieSubmodule.mk_eq_zero] using hvc.right

Похожие утверждения