English
If two crystallographic root pairings agree on the coroot data after restriction, their restricted scalar maps agree and their base data coincide.
Русский
Если два кристаллографических парора корней совпадают по данным короута после ограничения, то их ограниченные скаляры совпадают и их базовые данные совпадают.
LaTeX
$$$((P.restrictScalars' K hP).coroot i) = P.coroot i$ and $((P.restrictScalars' K hP).root i) = P.root i$ for all i$$
Lean4
/-- In characteristic zero if there is no torsion, to check that two finite families of roots and
coroots form a root pairing, it is sufficient to check that they are stable under reflections. -/
def mk' [CharZero R] [NoZeroSMulDivisors R M] (p : M →ₗ[R] N →ₗ[R] R) [p.IsPerfPair] (root : ι ↪ M) (coroot : ι ↪ N)
(hp : ∀ i, p (root i) (coroot i) = 2)
(hr : ∀ i, MapsTo (preReflection (root i) (p.flip (coroot i))) (range root) (range root))
(hc : ∀ i, MapsTo (preReflection (coroot i) (p (root i))) (range coroot) (range coroot)) : RootPairing ι R M N
where
toLinearMap := p
root := root
coroot := coroot
root_coroot_two := hp
reflectionPerm i := RootPairing.equiv_of_mapsTo p root coroot i hr hp
reflectionPerm_root i
j := by simp [(exist_eq_reflection_of_mapsTo p root coroot i j hr).choose_spec, preReflection_apply]
reflectionPerm_coroot i
j := by
refine (coroot_eq_coreflection_of_root_eq' p root coroot hp hr hc ?_).symm
rw [equiv_of_mapsTo_apply, (exist_eq_reflection_of_mapsTo p root coroot i j hr).choose_spec]
