English
Equality of expressions for PolarizationIn on a root span element.
Русский
Согласование выражений для PolarizationIn на элементе корневого охвата.
LaTeX
$$$P.PolarizationIn S x = P.Polarization x$$$
Lean4
/-- A version of SGA3 XXI Lemma 1.2.1 (10), adapted to change of rings. -/
theorem rootFormIn_self_smul_coroot (i : ι) :
P.RootFormIn S (P.rootSpanMem S i) (P.rootSpanMem S i) • P.coroot i = 2 • P.PolarizationIn S (P.rootSpanMem S i) :=
by
have hP :
P.PolarizationIn S (P.rootSpanMem S i) =
∑ j : ι, P.pairingIn S i (P.reflectionPerm i j) • P.coroot (P.reflectionPerm i j) :=
by
simp_rw [PolarizationIn_apply, coroot'In_rootSpanMem_eq_pairingIn]
exact
(Fintype.sum_equiv (P.reflectionPerm i)
(fun j ↦ P.pairingIn S i (P.reflectionPerm i j) • P.coroot (P.reflectionPerm i j))
(fun j ↦ P.pairingIn S i j • P.coroot j) (congrFun rfl)).symm
rw [two_nsmul]
nth_rw 2 [hP]
rw [PolarizationIn_apply]
simp only [coroot'In_rootSpanMem_eq_pairingIn, pairingIn_reflectionPerm, pairingIn_reflectionPerm_self_left,
← reflectionPerm_coroot, neg_smul, smul_sub, sub_neg_eq_add]
rw [Finset.sum_add_distrib, ← add_assoc, ← sub_eq_iff_eq_add, RootFormIn]
simp only [LinearMap.coeFn_sum, LinearMap.coe_smulRight, Finset.sum_apply, coroot'In_rootSpanMem_eq_pairingIn,
LinearMap.smul_apply, smul_eq_mul, Finset.sum_smul, root_coroot_eq_pairing, Finset.sum_neg_distrib, add_neg_cancel,
sub_eq_zero]
refine Finset.sum_congr rfl ?_
intro j hj
rw [← P.algebraMap_pairingIn S, IsScalarTower.algebraMap_smul, ← mul_smul]
