English
The finiteness dimension of the polarization image equals that of the coroot span: finrank_S(range PolarizationIn S) = finrank_S(corootSpan S).
Русский
Размерность поляризации равна размерности корневой области: finrank_S( Range(PolarizationIn S) ) = finrank_S( corootSpan S ).
LaTeX
$$$\operatorname{finrank}_S(\operatorname{range}(P.PolarizationIn S)) = \operatorname{finrank}_S(\operatorname{corootSpan} S)$$$
Lean4
theorem polarizationIn_Injective [P.IsAnisotropic] : Function.Injective (P.PolarizationIn S) :=
by
have : IsReflexive R M := .of_isPerfPair P.toLinearMap
have : NoZeroSMulDivisors S M := NoZeroSMulDivisors.trans_faithfulSMul S R M
rw [← LinearMap.ker_eq_bot, ← top_disjoint]
refine Submodule.disjoint_ker_of_finrank_le (L := ⊤) (P.PolarizationIn S) ?_
rw [finrank_top, ← finrank_corootSpan_eq, ← finrank_range_polarization_eq_finrank_span_coroot]
exact Submodule.finrank_mono <| le_of_eq <| LinearMap.range_eq_map (P.PolarizationIn S)
