aargh dfinsupp is constructive

Stream: Is there code for X?

[Kevin Buzzard]

Everybody knows that I don't like finset. If you're not using set.finite, which is just bundled finiteness (like we have bundled subgroups etc which everyone loves) then I sometimes feel like you deserve all the trouble you get. Bhavik tells me that he never gets trouble now and I do believe him because I know that people like him and Chris are really really good at this stuff.

I was just placating the linter in the undeprecate branch and I noticed there was no dfinsupp documentation. I started writing some in a way which I hoped would make sense to mathematicians. On the way I realised it was just constructive finite support Pi. Is there a nonconstructive version of this in Lean? It far better models the way I think about arbitrary direct sums personally.

import data.set.finite

variables {ι : Type} (A : ι → Type) [Π (i : ι), has_zero (A i)]

def is_finitely_supported (f : Π i, A i) : Prop :=
∃ S : set ι, S.finite ∧ ∀ i, i ∉ S → f i = 0

Do we have this? Does it deserve an API? Oh I guess it is like an unbundled pi type, whereas you can think of dfinsupp as a bundled pi type. Why do we prefer bundled group homs to unbundled ones? Maybe typeclass inference would struggle with it. If we found no use for is_group_hom then does that mean there's no use for this?

[Eric Wieser]

Arguably finsupp is constructive too (in that it holds the support as data), it just throws it away at the last moment by not using decidable arguments.

[Reid Barton]

The best part is dfinsupp is not the correct way to define the direct sum constructively either

[Eric Wieser]

What would the best way be to do so in your opinion, Reid?

[Reid Barton]

Well the best way is of course the classical one, but the correct constructive way is as (inductively generated term algebra)/(inductively generated relations)

[Eric Wieser]

I think the downside of that approach is that you no longer have definitional control of coefficient extraction, right?

[Reid Barton]

but that's the incorrect thing to want

[Reid Barton]

the direct sum is a coproduct, it's naturally equipped with maps from the components

[Reid Barton]

and you can't extract coefficients without having decidable equality

[Reid Barton]

The current definition is some weird neither-fish-nor-fowl thing.

[Eric Wieser]

it's naturally equipped with maps from the components

Right, but it's not clear that the naturalness of those maps is something lean can exploit in the way it can exploit the current definition reduction of coe_fn, even if mathematically they're the more interesting maps.

[Mario Carneiro]

I thought the whole point of the API is so that none of these differences matter

[Eric Wieser]

Except sometimes APIs include "this definitional reduction is deliberate"

[Reid Barton]

Well they do matter from a constructive perspective, and from a classical perspective the API is littered with unnecessary decidable_eq constraints

[Reid Barton]

but maybe Kevin had something different in mind?

[Eric Wieser]

Ah, is your point Reid that direct_sum.of / docs#dfinsupp.single would not need decidable_eq if it were implemented the way you describe?

[Mario Carneiro]

but getting the coefficient would

[Reid Barton]

I think my main point is that constructively there is a single thing (up to isomorphism) which can be called the "direct sum of a family of groups" and dfinsupp is not (isomorphic to) that thing at all

[Mario Carneiro]

it's kind of like using multiset as an implementation of finsupp A nat

[Eric Wieser]

dfinsupp is isomorphic to that thing in all ways that we can express in lean though, right?

[Mario Carneiro]

assuming decidable_eq, yes

[Reid Barton]

I don't really know what that means. In principle you could inspect the definitions/proof and replay them in another topos (e.g. condensed sets, where this free abelian group construction on an object without decidable equality is really important!). If by "in Lean" you mean assuming classical everything, then yes that's true which is why I included the other part of my previous sentence.

[Eric Wieser]

Presumably you'd apply the same argument against the current construction of docs#monoid_algebra, and the idea of using finsupp for a free module, as opposed to another generator / relations construction?

[David Wärn]

Yes, monoid algebras etc are based on coproducts of comm monoids so should constructively be defined as Reid says

[David Wärn]

Sorry, I don't mean to suggest that we'd need a new definition of monoid_algebra, just that it should (from a constructive perspective) be based on the constructive counterpart of finsupp rather than on finsupp

[David Wärn]

Basically, in any use case of finsupp / dfinsupp (e.g. free modules, direct sums of modules, monoid algebras, polynomial algebras), you need the underlying type to be a coproduct in the category of commutative monoids (otherwise your polynomial algebra or whatever won't get its universal property). Luckily, if you have some decidable_eq instance (which you do if you're working classically) then finsupp / dfinsupp is such a coproduct, but if you don't have these instances then it's just ... not. It's like how the box topology is just not the corrrect topology on an infinite product of topological space, if that means anything to you. However you can still define a coproduct in this case (e.g. take the abelianisation of docs#free_product).

[David Wärn]

The only downside to this constructive coproduct afaics is that unlike finsupp it doesn't really have any extensionality principle, and you can potentially get performance issues if you try to compute with it (imagine computing the polynomial $(1+x)^{10}$ without collecting like terms -- instead of 11 terms you get 1024).