AddMonoidHomClass confusion

Stream: mathlib4

[Kevin Buzzard]

Here is what I want (and I can't find it for finsums although we have docs#LinearMap.sum_apply for finset sums):

import Mathlib

theorem LinearMap.finsum_apply {R : Type*} [Semiring R]
    {A : Type*} [AddCommMonoid A] [Module R A]
    {B : Type*} [AddCommMonoid B] [Module R B]
    (ι : Type*) [Finite ι]
    (φ : ∀ _ : ι, A →ₗ[R] B) (a : A) :
    (∑ᶠ i, φ i) a = ∑ᶠ i, φ i a := by
  induction ι using Finite.induction_empty_option
  · case of_equiv _ _ e h =>
    specialize h (φ ∘ e)
    simpa [← finsum_comp_equiv e]
  · simp [finsum_of_isEmpty]
  · case h_option _ _ h =>
    simp [finsum_option (Set.toFinite _), h]

And then I was looking at it thinking "wait a minute, this is a theorem about AddMonoidHoms not linear maps" so I deleted R and changed A →ₗ[R] B to A →+ B and the proof goes through unchanged. And then I was thinking "but wait a minute, this will now not apply to my use case, aah, but this problem is solved by AddMonoidHomClass, so I changed it again to

theorem AddMonoidHomClass.finsum_apply {A B : Type*} [AddCommMonoid A] [AddCommMonoid B]
    (ι : Type*) [Finite ι]
    {F : Type*} [FunLike F A B] [AddMonoidHomClass F A B]
    (φ : ∀ _ : ι, F) (a : A) :
    (∑ᶠ i, φ i) a = ∑ᶠ i, φ i a := by

and now the statement doesn't compile :-( because ∑ᶠ i, φ i needs [AddCommMonoid F] which I can't supply (and rightly so, because what if F were in fact algebra maps?).

Is the solution to just stick to linear maps and AddMonoidHoms (or more precisely MonoidHoms and then toadditivise)?

[Michael Stoll]

If ι is Finite, what is the point of using docs#finsum instead of docs#Finset.sum ? So you can avoid Fintype in place of Finite?

[Aaron Liu]

docs#finsum_apply

[Aaron Liu]

Ahh, you need the coercions to line up

[Aaron Liu]

This works

import Mathlib

variable {R A B : Type*} [Semiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B]

def LinearMap.coeAddHom  : (A →ₗ[R] B) →+ (A → B) where
  toFun φ := φ
  map_zero' := funext fun a ↦ by simp
  map_add' x y := funext fun a ↦ by simp

theorem LinearMap.finsum_apply (ι : Type*) [Finite ι] (φ : ∀ _ : ι, A →ₗ[R] B) (a : A) :
    (∑ᶠ i, φ i) a = ∑ᶠ i, φ i a := by
  conv_lhs =>
    apply congrFun
    exact LinearMap.coeAddHom.map_finsum (f := φ) (Set.toFinite _)
  exact _root_.finsum_apply (f := fun i a ↦ φ i a) (Set.toFinite _) a

The important part was seeing DFunLike.coe as an AddMonoidHom (why don't we have this yet?)

[Kevin Buzzard]

Michael Stoll said:

If ι is Finite, what is the point of using docs#finsum instead of docs#Finset.sum ? So you can avoid Fintype in place of Finite?

Yeah, my preference is to use finsum always and if there's missing API then to add it. Do you think this is crazy?

[Kevin Buzzard]

@Aaron Liu yeah that's a neat proof but my question is whether we should be proving both this and AddMonoidHom.finsum_applyor whether there is some clever way of using AddMonoidHomClass so that we only have to prove the lemma once and it applies in both cases.

[Kevin Buzzard]

theorem AddMonoidHom.finsum_apply {A B : Type*} [AddCommMonoid A] [AddCommMonoid B]
    (ι : Type*) [Finite ι]
    (φ : ∀ _ : ι, A →+ B) (a : A) :
    (∑ᶠ i, φ i) a = ∑ᶠ i, φ i a := by
  induction ι using Finite.induction_empty_option
  · case of_equiv _ _ e h =>
    specialize h (φ ∘ e)
    simpa [← finsum_comp_equiv e]
  · simp [finsum_of_isEmpty]
  · case h_option _ _ h =>
    simp [finsum_option (Set.toFinite _), h]

(same proof works). But if we had AddMonoidHomClass.finsum_apply then it could be applied to prove both theorems directly. The problem is that I can't formalise the statement of the hypothetical result.

[Michael Stoll]

Kevin Buzzard said:

Do you think this is crazy?

No; I was just wondering. I imagine always having to prove (although this can be done trivially when summing over a finite type) that your functions are finitely supported might be a bit annoying.

[Aaron Liu]

AddMonoidHomClass does not come with an AddCommMonoid instance, and we don't have a typeclass that says "I am a DFunLike F α β closed under addition", so I don't think we can have something like what you want right now. I imagine we could either prove it individually for all the different cases or introduce such a typeclass (and a multiplicative version) and then just prove it once.

[Kevin Buzzard]

Yeah I might just add both versions. It's not possible to put an AddCommMonoid instance on AddMonoidHomClass because ring homomorphisms are a counterexample.

[Eric Wieser]

@Yury G. Kudryashov has thought about generalizing "morphisms which form an additive monoid" in the past

[Eric Wieser]

Kevin Buzzard said:

Yeah, my preference is to use finsum always and if there's missing API then to add it. Do you think this is crazy?

My subjective opinion is "yes", but I guess if your craziness results in more api being written then there's no need to try to persuade you to stop

[Yury G. Kudryashov]

We don't have typeclasses for equalities like DFunLike.coe (f + g) x = f x + g x.

[Yury G. Kudryashov]

There are 2 ways to add them: (a) as Prop-valued mixins; (b) by making homs use the same structure.

[Yury G. Kudryashov]

I failed to do it either way, because it's hard to address all the special cases.

[Aaron Liu]

Yury G. Kudryashov said:

I failed to do it either way, because it's hard to address all the special cases.

What specifically was difficult?