English
For any i, if x lies in the span of the roots (the root span), then P.coroot' i applied to x lies in the image of algebraMap S R.
Русский
Пусть x лежит в области, образованной линейной комбинацией корней; тогда P.coroot' i применительно к x лежит в образе algebraMap S R.
LaTeX
$$$x\in\operatorname{span}_S(\operatorname{range}(P.root)) \Rightarrow P.coroot' i\,x \in \operatorname{range}(\operatorname{algebraMap}_{S\to R})$$$
Lean4
theorem coroot'_apply_apply_mem_of_mem_span [Module S M] [IsScalarTower S R M] [P.IsValuedIn S] {x : M}
(hx : x ∈ span S (range P.root)) (i : ι) : P.coroot' i x ∈ range (algebraMap S R) :=
by
rw [show range (algebraMap S R) = LinearMap.range (Algebra.linearMap S R) by ext; simp]
induction hx using Submodule.span_induction with
| mem x hx =>
obtain ⟨k, rfl⟩ := hx
simpa using RootPairing.exists_value k i
| zero => simp
| add x y _ _ hx hy => simpa only [map_add] using add_mem hx hy
| smul t x _ hx => simpa only [LinearMap.map_smul_of_tower] using Submodule.smul_mem _ t hx
