What is `DFinsupp`?

Stream: mathlib4

[Luna]

I'm trying to find the definition of the internal DirectSum for modules. This led me to DFinsupp and I'm trying to parse exactly what it means.

The definition in mathlib is below:

structure DFinsupp [∀ i, Zero (β i)] : Type max u v where mk' ::
  /-- The underlying function of a dependent function with finite support (aka `DFinsupp`). -/
  toFun : ∀ i, β i
  /-- The support of a dependent function with finite support (aka `DFinsupp`). -/
  support' : Trunc { s : Multiset ι // ∀ i, i ∈ s ∨ toFun i = 0 }

From the vibes I'm getting, I think it says that finitely many β i are non-zero, but I'm confused on how support' enforces this. I also don't understand what Trunc is?

And if I'm correct in the above, does that mean that a DirectSum of module is just an (arbitrarily large) product of modules with finite non-zero entries?

[Ruben Van de Velde]

It basically says there exists a multiset, and each i is either in that (finite) multiset or maps to zero

[Ruben Van de Velde]

I have only the vaguest idea of what Trunc is, though

[Weiyi Wang]

DFinsupp.support (without ') probably explains more

[Ruben Van de Velde]

docs#DFinsupp.support

[Weiyi Wang]

sorry I misremembered how the doc was structured

[Weiyi Wang]

The main explanation is in the header of that page

[Eric Wieser]

@Luna, is there something we could add to the docstring of docs#DFinsupp itself to make this more obvious? Ideally the docstring should be enough to tell you what DFinsupp means without you having to dig into how it's implemented.

[Alfredo Moreira-Rosa]

@Eric Wieser i think a link to wikipedia would be good. When you pointed out to me to use DFinsupp, the docs where obscur to me, but when reading the wikipedia page, it all became clear :
https://en.wikipedia.org/wiki/Support_(mathematics)

And in general, i think mathlib should point whenever possible to wikipedia or another math source to expand on the mathematics behind some mathlib definitions

[Violeta Hernández]

Ruben Van de Velde said:

I have only the vaguest idea of what Trunc is, though

It's the quotient by the always true relationship

[Violeta Hernández]

The idea with DFinsupp is that it's often computationally expensive/and or requires extra decidability assumptions to compute the exact support of a function (e.g. the support of f + g might be an arbitrary subset of the union of both supports), so you instead compute some superset. What Trunc does is ensure that even if two finsupps have different support supersets, they remain propositionally equal.

[Violeta Hernández]

(My question is, what stops us from copying this design to Finsupp?)

[Ruben Van de Velde]

Oh right, the clever thing is that the multiset can still include elements that map to zero, but nothing outside it can map to something nonzero

[Eric Wieser]

Violeta Hernández said:

(My question is, what stops us from copying this design to Finsupp?)

There'd be little point, we might as well just make Finsupp an abbrev for DFinsupp if we're going to use the same design

[Violeta Hernández]

Well, what stops us from doing that?

[Violeta Hernández]

Is it just "no one has wanted to do it yet", or are there other considerations?

[Eric Wieser]

It's too big a thing to do / review in one go

[Eric Wieser]

@Yaël Dillies is working on adding some abstraction barriers which will make it easier to do piecewise

[Eric Wieser]

#25324 also works in that direction

[Luna]

Eric Wieser said:

Luna, is there something we could add to the docstring of docs#DFinsupp itself to make this more obvious? Ideally the docstring should be enough to tell you what DFinsupp means without you having to dig into how it's implemented.

Ah the above makes sense. I think it was just the combination of seeing Trunc and Multiset that through me for a loop.

Also is there a reason why its defined with Multiset instead of Finset? Could support equally be defined like support' : {s : Finset ι // ∀ i, i ∉ s → β i = 0}?

[Eric Wieser]

Finset would require decidable equality for adding the functions

[Luna]

Oh ok! To compute a Finset, you need to remove duplicates which means that equality needs to be decidable. So the solution is to use a Multiset and just don't remove duplicates.

[Luna]

A tangential question, why does Mathlib care about computability? Are there efforts to create algorithms from various theorems?

[Eric Wieser]

Computability is a property of definitions not theorems

[Luna]

Or maybe I'm using the wrong word. Why is decidability important for Mathlib?

[Aaron Liu]

Luna said:

Or maybe I'm using the wrong word. Why is decidability important for Mathlib?

it means you can #eval your definitions

[Aaron Liu]

usually it also means you can #reduce your definitions

[Ruben Van de Velde]

It's not considered particularly important in mathlib, but sometimes it can be helpful to be able to tell the computer "just run the algorithm"

[Violeta Hernández]

Decidability is one of those things that's great when it works and a total pain point when it doesn't

[Luna]

I have another related question, what is the conceptual definition of DFinsupp.sumAddHom? I'm having a lot of trouble parsing/following along its definition. Can someone write out in standard mathematical notation what the function is supposed to be?

[Luna]

And thanks for the responses all. @Aaron Liu I'm still on chapter 10 for MIL but it hasn't talked much about decidability and its uses with #eval. When is it used in mathlib? Off the top of my head, I'm imagining it can be used for not just knowing a matrix can be put into RREF but actually compute the entries of the matrix when its reduced to RREF?

[Ruben Van de Velde]

Given a iota-indexed dfinsupp f and a iota-indexed collection of functions φ that preserve addition (i.e. g (x + y) = g x + g y), sumAddHom φ is another function that preserves addition, and sumAddHom φ f is the sum of φ i (f i) for all i in the support of f

[Ruben Van de Velde]

So if iota is {0, 1} and \phi 0 (f 0) = 3, \phi 1 (f 0) = 5, then sumAddHom \phi f = 3 + 5

[Ruben Van de Velde]

I think I got that right, at least

[Luna]

Ah! Ok so putting it into my own words, its doing the following:

Given $\Phi = (\phi_0, \phi_1, \ldots)$ and $X = (x_0, x_1, \ldots)$, where $\phi_i : M_i \rightarrow N$ is a module homomorphism and $x_i \in M_i$ s.t. finitely many $x_i$ are non-zero. Then sumAddHom Φ X is

$$\sum_{i} \phi_i(x_i)$$

And this is well-defined because there is finitely non-zero $x_i$ (e.g. a finite support).

Is that correct?

[Kevin Buzzard]

Yes that looks right. The input is additive group homs $M_i\to N$ for all $i$ and the output is an additive group hom $\bigoplus_i M_i \to N$ defined as the sum of the $\phi_i$ (i.e. how you said it was defined).

[Kevin Buzzard]

I agree that the docstring is useless. Please make a PR changing it! The docstring seems to be assuming that you've read some of the docstrings above it, which IMO a docstring should never do.

[Eric Wieser]

Note that using $\bigoplus$ in the docstring would be wrong, since that docs#DirectSum.toModule instead!

[Kevin Buzzard]

Bleurgh so we have two ways of saying the same thing?

[Eric Wieser]

One has convolutive multiplication, the other doesn't (and should have pointwise)

[Eric Wieser]

DFinsupp is to DirectSum as Finsupp is to AddMonoidAlgebra