rootForm_self_smul_coroot — Mathlib

English

The product over all roots of RootForm times coroot, acting on i, lies in the range of Polarization.domRestrict(rootSpan).

Русский

Произведение RootForm по всем корням, умноженное на короот, действует на i и лежит в диапазоне Polarization.domRestrict(rootSpan).

LaTeX

$$$(\\prod_{a \\in ι} P.RootForm (P.root a) (P.root a)) \\cdot P.coroot i \\in \\operatorname{range}(P.Polarization.domRestrict (P.rootSpan R))$$$

Lean4

/-- A version of SGA3 XXI Lemma 1.2.1 (10). -/
theorem rootForm_self_smul_coroot (i : ι) :
    (P.RootForm (P.root i) (P.root i)) • P.coroot i = 2 • P.Polarization (P.root i) :=
  by
  have :
    (algebraMap R R) ((P.RootFormIn R) (P.rootSpanMem R i) (P.rootSpanMem R i)) • P.coroot i =
      2 • P.Polarization (P.root i) :=
    by rw [Algebra.algebraMap_self_apply, P.rootFormIn_self_smul_coroot R i, PolarizationIn_eq]
  rw [← this, algebraMap_rootFormIn]

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