English
There is a canonical algebra structure on the adic completion compatible with the base algebra.
Русский
Существует каноническая структура алгебры на адик завершении, совместимая с базовой алгеброй.
LaTeX
$$instAlgebraAdicCompletion$$
Lean4
instance : Algebra S (v.adicCompletion K)
where
toSMul := Completion.instSMul _ _
algebraMap := Completion.coeRingHom.comp (algebraMap _ _)
commutes' r
x := by
induction x using Completion.induction_on with
| hp => exact isClosed_eq (continuous_mul_left _) (continuous_mul_right _)
| ih
x =>
change
(↑(algebraMap S (WithVal <| v.valuation K) r) : v.adicCompletion K) * x =
x * (↑(algebraMap S (WithVal <| v.valuation K) r) : v.adicCompletion K)
norm_cast
rw [Algebra.commutes]
smul_def' r
x := by
induction x using Completion.induction_on with
| hp => exact isClosed_eq (continuous_const_smul _) (continuous_mul_left _)
| ih x =>
change _ = (↑(algebraMap S (WithVal <| v.valuation K) r) : v.adicCompletion K) * x
norm_cast
rw [← Algebra.smul_def]
