English
The invariant form derived from the posRootForm is anisotropic, i.e., its quadratic map is anisotropic.
Русский
Инвариантная форма, полученная из posRootForm, анизотропна, то есть её квадратичная форма анизотропна.
LaTeX
$$$(P\,\posRootForm\, S).posForm.Anisotropic$$
Lean4
theorem finrank_range_polarization_eq_finrank_span_coroot [P.IsAnisotropic] :
finrank S (LinearMap.range (P.PolarizationIn S)) = finrank S (P.corootSpan S) :=
by
apply (Submodule.finrank_mono (P.range_polarizationIn_le_span_coroot S)).antisymm
have : IsReflexive R N := .of_isPerfPair P.flip.toLinearMap
have : NoZeroSMulDivisors S N := NoZeroSMulDivisors.trans_faithfulSMul S R N
have h_ne : ∏ i, (P.RootFormIn S (P.rootSpanMem S i) (P.rootSpanMem S i)) ≠ 0 :=
by
refine Finset.prod_ne_zero_iff.mpr fun i _ h ↦ ?_
have := (FaithfulSMul.algebraMap_eq_zero_iff S R).mpr h
rw [algebraMap_rootFormIn] at this
apply IsAnisotropic.rootForm_root_ne_zero i this
refine
LinearMap.finrank_le_of_isSMulRegular (P.corootSpan S) (LinearMap.range (M₂ := N) (P.PolarizationIn S))
(smul_right_injective N h_ne) ?_
intro _ hx
obtain ⟨c, hc⟩ := (Submodule.mem_span_range_iff_exists_fun S).mp hx
rw [← hc, Finset.smul_sum]
simp_rw [smul_smul, mul_comm, ← smul_smul]
exact
Submodule.sum_smul_mem (LinearMap.range (P.PolarizationIn S)) c fun j _ ↦
prod_rootFormIn_smul_coroot_mem_range_PolarizationIn P S j
