range_polarization_domRestrict_le_span_coroot

English

Let P be a RootPairing. Then the range of the polarization map restricted to the root span is contained in the coroot span.

Русский

Пусть P — парировка корней. Тогда образ отображения поляризации, ограниченного на корневой охват, содержится в охвате корот.

LaTeX

$$$\\operatorname{range}\\bigl(P.Polarization.domRestrict(P.rootSpan\\ R)\\bigr) \\le P.corootSpan\\ R$$$

Lean4

theorem range_polarization_domRestrict_le_span_coroot :
    LinearMap.range (P.Polarization.domRestrict (P.rootSpan R)) ≤ P.corootSpan R :=
  by
  intro y hy
  obtain ⟨x, hx⟩ := hy
  rw [← hx, LinearMap.domRestrict_apply, Polarization_apply]
  refine (Submodule.mem_span_range_iff_exists_fun R).mpr ?_
  use fun i => P.toLinearMap x (P.coroot i)
  simp

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