English
Two RootPairings are equal if their linear maps, roots, and coroot ranges coincide; ext is established via root and coroot data.
Русский
Две RootPairings равны, если их линейные отображения, корни и диапазоны коротов совпадают; экстензия строится по данным корней и коротов.
LaTeX
$$$P_1.toLinearMap = P_2.toLinearMap\\;\\&\\; P_1.root = P_2.root\\;\\&\\; \\operatorname{range} P_1.coroot = \\operatorname{range} P_2.coroot \\Rightarrow P_1 = P_2$$$
Lean4
/-- Over a field of characteristic zero, to check that a finite family of roots form a
crystallographic root system, we do not need to check that the coroots are stable under reflections
since this follows from the corresponding property for the roots. Likewise, we do not need to
check that the coroots span. -/
def mk' {k : Type*} [Field k] [CharZero k] [Module k M] [Module k N] (p : M →ₗ[k] N →ₗ[k] k) [p.IsPerfPair]
(root : ι ↪ M) (coroot : ι ↪ N) (hp : ∀ i, p (root i) (coroot i) = 2)
(hs : ∀ i, MapsTo (preReflection (root i) (p.flip (coroot i))) (range root) (range root))
(hsp : span k (range root) = ⊤) (h_int : ∀ i j, ∃ z : ℤ, z = p (root i) (coroot j)) : RootSystem ι k M N :=
let P :=
RootPairing.mk' p root coroot hp hs <| by
rintro i - ⟨j, rfl⟩
use RootPairing.equiv_of_mapsTo p root coroot i hs hp j
refine (coroot_eq_coreflection_of_root_eq_of_span_eq_top p root coroot hp hs hsp ?_)
rw [equiv_of_mapsTo_apply, (exist_eq_reflection_of_mapsTo p root coroot i j hs).choose_spec]
have _i : P.IsCrystallographic := ⟨h_int⟩
have _i : Fintype ι := Fintype.ofFinite ι
{ toRootPairing := P, span_root_eq_top := hsp, span_coroot_eq_top := P.rootSpan_eq_top_iff.mp hsp }
