instFaithfulSMulCompletionOfUniformContinuousConstSMul

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)

Похожие утверждения