DirectSum defeqs

Stream: mathlib4

[Johan Commelin]

DirectSum is defined to be DFinsupp, and this defeq is used a lot, for example to write x.sum when x is a term of a direct sum, but the .sum refers to DFinsupp.sum.
However, this leads to proofs like

theorem mul_eq_dfinsupp_sum [∀ (i : ι) (x : A i), Decidable (x ≠ 0)] (a a' : ⨁ i, A i) :
    a * a'
      = a.sum fun _ ai => a'.sum fun _ aj => DirectSum.of _ _ <| GradedMonoid.GMul.mul ai aj := by
  change mulHom _ a a' = _
  -- Porting note: I have no idea how the proof from ml3 worked it used to be
  -- simpa only [mul_hom, to_add_monoid, dfinsupp.lift_add_hom_apply, dfinsupp.sum_add_hom_apply,
  -- add_monoid_hom.dfinsupp_sum_apply, flip_apply, add_monoid_hom.dfinsupp_sum_add_hom_apply],
  rw [mulHom, toAddMonoid, DFinsupp.liftAddHom_apply]
  dsimp only [DirectSum]
  rw [DFinsupp.sumAddHom_apply, AddMonoidHom.dfinsupp_sum_apply]
  apply congrArg _
  simp_rw [flip_apply]
  funext x
  -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
  erw [DFinsupp.sumAddHom_apply]
  simp only [gMulHom, AddMonoidHom.dfinsupp_sum_apply, flip_apply, coe_comp, AddMonoidHom.coe_mk,
    ZeroHom.coe_mk, Function.comp_apply, AddMonoidHom.compHom_apply_apply]

Should DirectSum be an abbrev? Or a 1-field structure?
It seems to me that at the moment it is trying to act a bit like both.

[Eric Wieser]

I tried to set things up such that DFinsupp : DirectSum :: Finsupp : AddMonoidAlgebra

[Eric Wieser]

Which in theory would include one using pointwise multiplication and the other using convolutive multiplication, which rules out an abbrev

[Eric Wieser]

As an aside, docs#mul_eq_dfinsupp_sum looks like it should be true by definition, at least if the RHS is adjusted to use DirectSum APIs

[Eric Wieser]

I think a one-field structure (with name coeff or component) would be sensible here. That could also remove the coercion to function, which is maybe desirable.

[Riccardo Brasca]

It looks a good idea to me.

[Eric Wieser]

@Damiano Testa and I talked about doing the same thing for MonoidAlgebra two years ago

[Eric Wieser]

docs#SkewMonoidAlgebra got the right treatment at least

[Damiano Testa]

I remember the conversation and I also started to refactor, but as I was doing it, it became apparent that untangling MonoidAlgebra and AddMonoidAlgebra was a very useful preliminary step, but I did not have the capacity to do that!

[Matthew Ballard]

I think an abbrev is a bad idea. I started a refactor via a structure wrapper a while back but got led off into the sorry state of deriving handlers which never produced anything.

[Eric Wieser]

I think more automation for single-field structures is perhaps a better investment than doing this refactor

[Eric Wieser]

(in that we need it anyway, and it will make the refactor easier)

[Matthew Ballard]

It would be nice not to make life harder when doing the prudent thing.