English
There is a duality-compatible equivalence of index maps that preserves dual pairing data under reflection and coroot relations.
Русский
Существует эквивалентность отображения двойственных индексов, сохраняющая данные двойственного спаривания при отражении и отношениях коротов.
LaTeX
$$$\\text{equiv\_of\_mapsTo}$ respects the dual maps and reflections between root and coroot data.$$
Lean4
theorem cartanMatrixIn_nondegenerate [IsDomain R] [NeZero (2 : R)] [FaithfulSMul S R] [IsDomain S]
{P : RootSystem ι R M N} [P.IsValuedIn S] [Fintype ι] [P.IsAnisotropic] (b : P.Base) :
(b.cartanMatrixIn S).Nondegenerate := by
classical
obtain ⟨B, hB⟩ : ∃ B : P.InvariantForm, B.form.Nondegenerate := ⟨P.toInvariantForm, P.rootForm_nondegenerate⟩
replace hB : ((2 : R) • BilinForm.toMatrix b.toWeightBasis B.form).Nondegenerate := by
rwa [Matrix.Nondegenerate.smul_iff two_ne_zero, LinearMap.BilinForm.nondegenerate_toMatrix_iff]
have aux : (Matrix.diagonal fun i : b.support ↦ B.form (P.root i) (P.root i)).Nondegenerate :=
by
rw [Matrix.nondegenerate_iff_det_ne_zero, Matrix.det_diagonal, Finset.prod_ne_zero_iff]
aesop
rw [← cartanMatrixIn_mul_diagonal_eq (S := S), Matrix.Nondegenerate.mul_iff_right aux,
Matrix.nondegenerate_iff_det_ne_zero, ← (algebraMap S R).mapMatrix_apply, ← RingHom.map_det, ne_eq,
FaithfulSMul.algebraMap_eq_zero_iff] at hB
rwa [Matrix.nondegenerate_iff_det_ne_zero]
