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.

[Sophie Morel]

Speaking of DirectSum, my student recently ran into the following issue. Consider the code:

theorem DirectSum_eq_sum_direct (ι : Type*) [hi : Fintype ι] (β : ι → Type*)
    [(i : ι) → AddCommMonoid (β i)] [DecidableEq ι] (x : (i : ι) → β i) (j : ι) :
    (∑ (i : ι), (DirectSum.of β i) (x i)) j = ∑ (i : ι), ((DirectSum.of β i) (x i) j) := by
  exact DFinsupp.finset_sum_apply _ _ _
  --simp [DirectSum]

The proof is a single application of DFinsupp.finset_sum_apply, but neither exact? nor apply? finds this lemma, and simp also does not call DFinsupp.finset_sum_apply to close the goal (even though DFinsupp.finset_sum_applyis tagged simp). We finally realized after some playing around that simp [DirectSum] was able to call DFinsupp.finset_sum_apply and to close the goal.

In his actual code, the goal was something more complicated, and proving the equality I wrote above is only the first step. I was able to do it because I knew DFinsupp.finset_sum_apply, my student was stuck because he didn't. Given that DFinsupp.finset_sum_apply is tagged simp, I feel that it is the kind of lemma that we want to be called automatically and the current implementation of DirectSum is not optimal.

[Edward van de Meent]

since DirectSum is a type alias, this just means that there is missing API here

[Edward van de Meent]

although to be honest, i'm not sure why DirectSum is a type alias... it looks to me like a lot of its instances are directly inherited from DFinsupp?

[Jireh Loreaux]

See above:
Eric Wieser said:

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

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

[Jireh Loreaux]

But yes, the answer is that this is just missing API.

[Eric Wieser]

I think in both cases we're missing the "coefficient" function, probably we shouldn't be using coeFn at all

[Yaël Dillies]

It's the summer soon and I have big plans to clean up this mess. It's been an annoying slowdown in Toric

[Sophie Morel]

I temporarily solved the problem for my student by telling him to systematically try simp [DirectSum].

[Eric Wieser]

That's a pretty reasonable workaround (at least, once simp by itself is stuck)

[Eric Wieser]

Another way out of the pain is to use DFinsupp as much as possible, and then prove your DirectSum result in one line using it