English
Restriction of scalars to rationals over crystallographic root pairings yields a RootSystem over Rat with span conditions preserved.
Русский
Ограничение скаляров до рациональных для кристаллографических пар корней даёт корневую систему над Rat с сохранением условий порождающих подпростраций.
LaTeX
$$$\\text{restrictScalars}_{\\text{Rat}} : \\text{RootSystem } ι \\mathbb{Q} (\\operatorname{span}_{\\mathbb{Q}}(\\operatorname{range}(P.root))) (\\operatorname{span}_{\\mathbb{Q}}(\\operatorname{range}(P.coroot)))$$$
Lean4
/-- Even though the roots may not span, coroots are distinguished by their pairing with the
roots. The proof depends crucially on the fact that there are finitely-many roots.
Modulo trivial generalisations, this statement is exactly Lemma 1.1.4 on page 87 of SGA 3 XXI. -/
theorem injOn_dualMap_subtype_span_root_coroot [NoZeroSMulDivisors ℤ M] :
InjOn ((span R (range P.root)).subtype.dualMap ∘ₗ P.toLinearMap.flip) (range P.coroot) :=
by
have :=
injOn_dualMap_subtype_span_range_range (finite_range P.root) (c := P.toLinearMap.flip ∘ P.coroot) P.root_coroot_two
P.mapsTo_reflection_root
rintro - ⟨i, rfl⟩ - ⟨j, rfl⟩ hij
exact P.flip.toPerfPair.injective <| this (mem_range_self i) (mem_range_self j) hij
