withAbs and defeq abuse

Stream: mathlib4

[Kevin Buzzard]

I need results about adeles, and hence infinite adeles, for FLT. These are defined as products of infinite completions of number fields, and Mathlib.NumberTheory.NumberField.Completion uses docs#WithAbs, a type synonym for a field (or semiring) which gives it a canonical normed structure for typeclass inference.

Sometimes these type synonyms are defined as one-field structures in mathlib (e.g. Opposite, MulOpposite etc) but here this is not the case; WithAbs (v : AbsoluteValue K ℝ) is just defined to be K and we have the principled WithAbs.equiv v : WithAbs v ≃+* K (which is rfl) to move between the object with the canonical norm and the object without it.

So now I want to develop theory so for example if L is a K-algebra and I have valuations w and v on them I want WithAbs w to be a WithAbs v-algebra, so it's tempting to write

instance {v : AbsoluteValue K ℝ} {w : AbsoluteValue L ℝ} :
    Algebra (WithAbs v) (WithAbs w) :=
  ‹Algebra K L›

but should I really be writing

noncomputable instance {v : AbsoluteValue K ℝ} {w : AbsoluteValue L ℝ} :
    Algebra (WithAbs v) (WithAbs w) :=
  RingHom.toAlgebra <| (WithAbs.equiv w).symm.toRingHom.comp <| ‹Algebra K L›.algebraMap.comp (WithAbs.equiv v).toRingHom

? The latter seems like such a mess; but I'm just unclear about whether the former will cause me problems later or whether I'm fussing about nothing.

[Andrew Yang]

I believe the former would be fine if you add the proper smul_def and algebraMap_eq lemmas.

[Michael Stoll]

There is an open PR (#20642) that adds docs#Module and docs#Algebra instances for docs#WithAbs (using essentially the first approach).