English
Base change preserves integrality: if a ring homomorphism f: R → S is integral, then for any base change R → R′ and S → S′ giving S′ ≅ S ⊗_R R′, the induced map R′ → S′ is again integral.
Русский
При базовом изменении сохраняется интегральность: если кольцо-гомоморфизм f: R → S является интегральным, то для любого базового изменения R → R′ и S → S′, дающего S′ ≅ S ⊗_R R′, индуцированный переход R′ → S′ также интегрален.
LaTeX
$$$\forall \text{rings }R,S,R',S' ,\ \text{algebras }R\to S,\ R\to R',\ S\to S',\text{IsScalarTower},\text{IsPushout},\ (IsIntegral( algebraMap R S)) \Rightarrow IsIntegral( algebraMap R' S'),$$$
Lean4
theorem isIntegral_isStableUnderBaseChange : IsStableUnderBaseChange fun f => f.IsIntegral :=
by
refine IsStableUnderBaseChange.mk isIntegral_respectsIso ?_
introv int
rw [algebraMap_isIntegral_iff] at int ⊢
infer_instance
