English
The swap identity for the invariant form holds: P.pairing j i · B.form (P.root i) (P.root i) = P.pairing i j · B.form (P.root j) (P.root j).
Русский
Сохранение пары при перестановке индексов: pairing j i · B.form (P.root i) (P.root i) = pairing i j · B.form (P.root j) (P.root j).
LaTeX
$$$ P.pairing j i \\cdot B.form\\bigl(P.root i\\bigr)\\bigl(P.root i\\bigr) = P.pairing i j \\cdot B.form\\bigl(P.root j\\bigr)\\bigl(P.root j\\bigr) $$$
Lean4
/-- Given a root-positive form associated to a root pairing with coefficients in `R` but taking
values in `S`, this is the associated `S`-bilinear form on the `S`-span of the roots. -/
def posForm : LinearMap.BilinForm S (span S (range P.root)) :=
LinearMap.restrictScalarsRange₂ (span S (range P.root)).subtype (span S (range P.root)).subtype
(Algebra.linearMap S R) (FaithfulSMul.algebraMap_injective S R) B.form
(fun ⟨x, hx⟩ ⟨y, hy⟩ ↦
by
apply
LinearMap.BilinMap.apply_apply_mem_of_mem_span (s := range P.root) (t := range P.root) (B :=
(LinearMap.restrictScalarsₗ S R _ _ _).comp (B.form.restrictScalars S))
· rintro - ⟨i, rfl⟩ - ⟨j, rfl⟩
simpa using B.exists_eq i j
· simpa
· simpa)
