English
If q ⊆ M satisfies a certain invariant-submodule condition across all roots and a universal subset property, then q = ⊤.
Русский
Если q ⊆ M удовлетворяет заданному условию инвариантного подпространства по всем корням и свойству полноты подмножеств, то q = ⊤.
LaTeX
$$$$ q = \top \quad \text{under invariant-submodule and universal-subset hypotheses}. $$$$
Lean4
theorem eq_top_of_mem_invtSubmodule_of_forall_eq_univ {K : Type*} [Field K] [NeZero (2 : K)] [Module K M] [Module K N]
(P : RootSystem ι K M N) (q : Submodule K M) (h₀ : q ≠ ⊥) (h₁ : ∀ i, q ∈ invtSubmodule (P.reflection i))
(h₂ : ∀ Φ, Φ.Nonempty → P.root '' Φ ⊆ q → (∀ i ∉ Φ, q ≤ ker (P.coroot' i)) → Φ = univ) : q = ⊤ :=
by
obtain ⟨Φ, b, c⟩ := P.exist_set_root_not_disjoint_and_le_ker_coroot'_of_invtSubmodule q h₁
rcases Φ.eq_empty_or_nonempty with rfl | hΦ
· replace c : q ≤ ⨅ i, LinearMap.ker (P.coroot' i) := by simpa using c
simp [h₀, ← P.corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot'] at c
· replace b : P.root '' Φ ⊆ q := by simpa [Submodule.disjoint_span_singleton' (P.ne_zero _)] using b
simpa [h₂ Φ hΦ b c, ← span_le] using b
