beef up smul on completion to algebra instance

Stream: mathlib4

[Kevin Buzzard]

I was just bitten by a diamond of my own making (in FLT, not mathlib), and I traced the issue back to this. docs#UniformSpace.Completion.instSMul says that if M acts on a uniform space then it acts on the completion. I have a K-algebra L with a uniform space structure and want to put a K-algebra structure on the completion of L, so I need to tread carefully to ensure that the SMul which we already have is compatible and I got stuck trying to make it work (my first attempt created a diamond; I'm hoping the below is the right approach but I can't fill in the sorry):

import Mathlib
set_option autoImplicit false

open IsDedekindDomain HeightOneSpectrum

-- Let L/K be an extension of fields (number fields in the application)
variable (K : Type*) [Field K] (L : Type*) [Field L] [Algebra K L]

-- and ensure L is the field of fractions of a Dedekind domain B (the ring of integers in the application)
variable (B : Type*) [CommRing B] [IsDedekindDomain B] [Algebra B L] [IsFractionRing B L]

-- We're going to complete L at a finite place w
variable  (w : HeightOneSpectrum B)

-- The completion L_w is an L-algebra
#synth Algebra L (adicCompletion L w)

-- And L is a K-algebra by assumption above.
#synth Algebra K L

-- So we can (and I want to) think of L_w as a K-algebra.
-- But here's the catch: there's already a SMul K L_w. In particular this works

#synth SMul K (adicCompletion L w) -- UniformSpace.Completion.instSMul K L

-- But this doesn't (yet):
-- #synth Algebra K (HeightOneSpectrum.adicCompletion L w)

-- So we have to be careful

open UniformSpace.Completion

noncomputable instance : Algebra K (HeightOneSpectrum.adicCompletion L w) where
  toFun k := algebraMap L (adicCompletion L w) (algebraMap K L k)
  map_one' := by simp only [map_one]
  map_mul' k₁ k₂ := by simp only [map_mul]
  map_zero' := by simp only [map_zero]
  map_add' k₁ k₂ := by simp only [map_add]
  commutes' k lhat := mul_comm _ _
  smul_def' k lhat := by
    simp only [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk]
    rw [UniformSpace.Completion.smul_def] -- not sure if this is the right move
    /-
    ⊢ UniformSpace.Completion.map (fun x => k • x) lhat =
        (algebraMap L (adicCompletion L w)) ((algebraMap K L) k) * lhat
    -/
    sorry

-- guess I need this too
instance : IsScalarTower K L (adicCompletion L w) := IsScalarTower.of_algebraMap_eq fun _ => rfl

[Eric Wieser]

This looks like the right approach to me, though I have some memory of finding a troublesome and possibly unresolvable diamond here before

[Eric Wieser]

I also think there was a PR that tried to redefine the Mul structure, and perhaps the analogous change for SMul would make your goal easier

[Yaël Dillies]

I've opened #19466 for this

[Salvatore Mercuri]

I've just run into this exact issue for infinite completions of number fields. Will try the above also.

[Salvatore Mercuri]

The above approach fixed my diamonds! Btw I closed off the sorry in the infinite case via the following:

variable (K : Type*) [Field K] (v : InfinitePlace K)
variable variable (L : Type*) [Field L] [Algebra K L] (w : InfinitePlace L)

instance : Algebra K (WithAbs w.1) := ‹Algebra K L›

instance : UniformContinuousConstSMul K (WithAbs w.1) :=
  uniformContinuousConstSMul_of_continuousConstSMul _ _

instance : IsScalarTower K L (WithAbs w.1) := inferInstanceAs (IsScalarTower K L L)

noncomputable instance : Algebra K (w.completion) where
  toFun k := algebraMap L w.completion (algebraMap K L k)
  map_one' := by simp only [map_one]
  map_mul' k₁ k₂ := by simp only [map_mul]
  map_zero' := by simp only [map_zero]
  map_add' k₁ k₂ := by simp only [map_add]
  commutes' k lhat := mul_comm _ _
  smul_def' k lhat := by
    rw [RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, UniformSpace.Completion.smul_def,
    ← RingHom.comp_apply, ← IsScalarTower.algebraMap_eq,
    UniformSpace.Completion.map_smul_eq_mul_coe, UniformSpace.Completion.algebraMap_def]