English
If R is a commutative semiring with an algebra structure to K, and the R-action on K is uniformly continuous and faithful, then the induced R-action on the completion hat K is also faithful.
Русский
Если R — коммутативное полупкольцо с алгебраическим отображением в K, и скалярное действие R на K непрерывно по униформной топологии и действенно, тогда соответствующее действие на завершающей оболочке hat K тоже будет действенным.
LaTeX
$$$\\text{FaithfulSMul } R (\\hat K)$$$
Lean4
instance {R : Type*} [CommSemiring R] [Algebra R K] [UniformContinuousConstSMul R K] [FaithfulSMul R K] :
FaithfulSMul R (hat K) := by
rw [faithfulSMul_iff_algebraMap_injective R (hat K)]
exact (FaithfulSMul.algebraMap_injective K (hat K)).comp (FaithfulSMul.algebraMap_injective R K)