English
Let P be a RootPairing valued in a smaller coefficient ring S. For every indices i, j from the index set, there exists an element in S, denoted pairingIn S i j, such that algebraMap S R (pairingIn S i j) equals the original pairing P.pairing i j. This value is unique if the map S → R is injective.
Русский
Пусть P — корневое парирование, ценностное в меньшей кольцевой оболочке S. Для любых i, j из множества индексов существует элемент в S, обозначаемый pairingIn S i j, такой что algebraMap S R (pairingIn S i j) = P.pairing i j. Это значение является единственным, если отображение S → R инъективно.
LaTeX
$$$\exists f\colon ι \to ι \to S\quad\text{such that}\quad \forall i,j,\; \operatorname{algebraMap}_{S\to R}(f(i,j)) = P.pairing i j.$$$$
Lean4
/-- A variant of `RootPairing.pairing` for root pairings which are valued in a smaller set of
coefficients.
Note that it is uniquely-defined only when the map `S → R` is injective, i.e., when we have
`[FaithfulSMul S R]`. -/
def pairingIn [P.IsValuedIn S] (i j : ι) : S :=
(P.exists_value i j).choose
