English
The completion of a ring A over R inherits a natural R-algebra structure; the algebraMap to the completion is the composite of the algebraMap from R to A with the completion embedding A → Completion A.
Русский
Завершение кольца A над R наследует естественную структуру R-алгебры; алгебраическое отображение в завершение есть композиция алгебраMap_R→A с встраиванием A → Completion A.
LaTeX
$$$$ \mathrm{algebraMap}_{R,\widehat{A}} = (\mathrm{coeRingHom}: A \to \widehat{A}) \circ \mathrm{algebraMap}_{R,A}. $$$$
Lean4
@[simp]
theorem map_smul_eq_mul_coe (r : R) : Completion.map (r • ·) = ((algebraMap R A r : Completion A) * ·) :=
by
ext x
refine Completion.induction_on x ?_ fun a => ?_
· exact isClosed_eq Completion.continuous_map (continuous_mul_left _)
· simp_rw [map_coe (uniformContinuous_const_smul r) a, Algebra.smul_def, coe_mul]
