English
If for a nonempty set s of indices, whenever a root P.root j is not in the span of P.root '' s, then every i in s is orthogonal to j, then the span of P.root '' s equals the top subspace.
Русский
Если для ненулевого множества индексов s выполняется: если корень P.root j не лежит в порождении P.root''s, то для каждого i ∈ s мы имеем ортогональность с j, то порождение P.root '' s равно верхнему подпространству.
LaTeX
$$$$ \operatorname{span}_R(P.root''s) = \top \quad \text{при условии } (\forall j, P.root_j \not\in \operatorname{span}_R(P.root''s) \Rightarrow \forall i \in s, P.IsOrthogonal j i). $$$$
Lean4
theorem span_root_image_eq_top_of_forall_orthogonal (s : Set ι) (hne : s.Nonempty)
(h : ∀ j, P.root j ∉ span R (P.root '' s) → ∀ i ∈ s, P.IsOrthogonal j i) : span R (P.root '' s) = ⊤ :=
by
have hq (j : ι) : span R (P.root '' s) ∈ Module.End.invtSubmodule (P.reflection j) :=
by
by_cases hj : P.root j ∈ span R (P.root '' s)
· exact Submodule.mem_invtSubmodule_reflection_of_mem _ _ hj
· refine (Module.End.mem_invtSubmodule _).mpr fun x hx ↦ ?_
rwa [Submodule.mem_comap, LinearEquiv.coe_coe, (isFixedPt_reflection_of_isOrthogonal (h _ hj) hx).eq]
apply IsIrreducible.eq_top_of_invtSubmodule_reflection _ hq
simpa using ⟨hne.choose, hne.choose_spec, P.ne_zero _⟩
