English
If P is valued in T, and T → S and T → R are ring homomorphisms in an algebra tower, then P is valued in S by setting pairingIn S i j = algebraMap_T_S (P.pairingIn_T i j).
Русский
Если P ценовано в T, и через цепочку гомоморфизмов T → S → R образуется тождество, то P ценовано в S задавая pairingIn_S i j = algebraMap_T_S (P.pairingIn_T i j).
LaTeX
$$$\exists\,\mathrm{exists\_value}\;i\,j := algebraMap_T_S\bigl(P.pairingIn_T\;i\;j\bigr) \;\Rightarrow\; P.IsValuedIn\;S$$$
Lean4
theorem trans (T : Type*) [CommRing T] [Algebra T S] [Algebra T R] [IsScalarTower T S R] [P.IsValuedIn T] :
P.IsValuedIn S where
exists_value i
j := by
use algebraMap T S (P.pairingIn T i j)
simp [← RingHom.comp_apply, ← IsScalarTower.algebraMap_eq T S R]
