English
There is a canonical Algebra structure on Completion A making it an Algebra over R, built from the existing structures on A and the completion map.
Русский
Существует каноническая структура алгебры на Completion A, делающая его алгеброй над R и вытекающую из существующих структур на A и завершения.
LaTeX
$$$$ \text{Algebra } R (\mathrm{Completion} A) $$$$
Lean4
instance algebra : Algebra R (Completion A)
where
algebraMap := (UniformSpace.Completion.coeRingHom : A →+* Completion A).comp (algebraMap R A)
commutes' := fun r x =>
Completion.induction_on x (isClosed_eq (continuous_mul_left _) (continuous_mul_right _)) fun a => by
simpa only [coe_mul] using congr_arg ((↑) : A → Completion A) (Algebra.commutes r a)
smul_def' := fun r x => congr_fun (map_smul_eq_mul_coe A R r) x
