defeq abuse: monoid_algebra → finsupp

Stream: general

[Anne Baanen]

Is there any plan to make monoid_algebra less dependent on its unfolding to finsupp? I have had to fix a number of places in #16123 and #16132 where there are two defeq instances on monoid_algebra but there's a finsupp in the expression somewhere causing unification to fail.

[Antoine Labelle]

I agree that this would be a good thing, I also had issues with that in representation theory.

[Adam Topaz]

IMO the monoid_algebra (and other similar constructions) should be defined using the usual quotient-inductive definition, and the comparison with finsupp should be a separate algebra equiv.

[Eric Wieser]

and the comparison with finsupp should be a separate algebra equiv.

We can't state this equivalence without the docs#add_monoid_algebra.algebra that you seem to be suggesting we remove along with the current definition of add_monoid_algebra?

[Eric Wieser]

@Anne Baanen, can you point to the specific location where unification is failing?

[Anne Baanen]

See e.g. this commit: we are assuming an instance on monoid_algebra. Since we have finsupp.single in the goal, monoid_algebra gets unfolded to finsupp and suddenly the monoid_algebra instance does not get applied.

[Eric Wieser]

I think this would be less painful if either:

• We had a separate monoid_algebra.monomial instead of mixing in finsupp.single
• We had a finsupp.to_monoid_algebra casting function to keep the types straight, along the lines of to_multiplicative etc

[Adam Topaz]

I'm not suggesting that we don't introduce instances on finsupp. Rather that there should be some separation between finsupp and monoid_algebra via some algebra isomorphism. Making monoid_algebra irreducible (is it not right now?) could do the same thing.

[Eric Wieser]

Rather that there should be some separation between finsupp and monoid_algebra via some algebra isomorphism.

But we can't put the algebra structure on finsupp, because finsupp has pointwise multiplication; so this isomorphism becomes impossible to state

[Adam Topaz]

Oh I see. Ugh! So why is finsupp used for the monoid algebra in the first place!?

[Eric Wieser]

Because it has all the right additive structure already

[Eric Wieser]

So we make a type alias to copy across all that, and then use a different multiplication

[Eric Wieser]

Just like what we do for mul_opposite

[Adam Topaz]

Ok so let's make monoid_algebra irreducible

[Adam Topaz]

docs#monoid_algebra since I'm on mobile

[Eric Wieser]

The main difference is that we're more hygienic with mul_opposite as we use mul_opposite.of_add and mul_opposite.to_add to swap back and forth

[Adam Topaz]

What's the issue with making it irreducible?

[Eric Wieser]

My experience is that irreducible is usually a bad idea; it breaks a bunch of places where you actually need it to be semireducible (such as when trying to unify typeclass diamonds)

[Adam Topaz]

Another option is to put it in a structure with one projection to finsupp

[Damiano Testa]

Is this a similar discussion to what happened when polynomial was sealed off from finsupp? Could a similar approach be used with (add_)monoid_algebra? I remember that for polynomials it was a lot of work (not by me!).

[Eric Wieser]

The main advantage of irreducible is that it forces us to use functions like mul_opposite.of_add and mul_opposite.to_add; but review is reasonably good at enforcing that too

[Adam Topaz]

PR review requires work by humans...

[Eric Wieser]

Damiano Testa said:

Is this a similar discussion to what happened when polynomial was sealed off from finsupp? Could a similar approach be used with (add_)monoid_algebra? I remember that for polynomials it was a lot of work (not by me!).

Perhaps the lesson here is that we put the structure barrier in the wrong place, and should have left polynomial as defeq to monoid_algebra, and made monoid_algebra the structure instead

[Damiano Testa]

Eric, I think that I agree. I am now wishing that all the API that we have for polynomials were actually for (add_)monoid_algebras.

[Yaël Dillies]

That makes a lot of sense, actually.

[Eric Wieser]

But we still end up in the mess where we have multiple names for the same thing; how do you avoid ending up with an expression like add_monoid_algebra.of 1 + polynomial.X? Even though all the instances agree, we now are trying to keep two separate sets of names for exactly the same construction.

[Adam Topaz]

But polynomials are more special... they're monoid algebras on free (comm) monoids. And their universal properties combine the universal prop of the algebra and the free monoid

[Yaël Dillies]

Have simp lemmas that go back through the API barrier?

[Eric Wieser]

simp can't always tell the difference between two defeq types; see the pain with have with with_bot and option lemmas interfering

[Eric Wieser]

At least in that case it's possible to index by the different instances, but for polynomial vs add_monoid_algebra all the instances would be exactly the same

[Adam Topaz]

Yes that's exactly the issue that my approach was trying to address

[Damiano Testa]

There is also the possibility of porting as much as possible to monoid algebras, and seal off monoid algebras from finsupp and polynomials from monoid algebras...

[Damiano Testa]

It would likely be a lot of work, though.

[Eric Wieser]

Sealing off monoid_algebra from finsupp seems reasonable because it avoids typeclass issues, but sealing off polynomials from monoid algebras is a massive amount of work just to get some different names (as the instances already agree)

[Eric Wieser]

And the worst bit is, after giving the mathematicians these nice names about polynomials, we have to tell them "oh, if you're going to PR this for mathlib you have to write your proof using the ugly names about monoid_algebras and then transfer the results to polynomials", otherwise the two sides of the seal diverge and now we have to do all the work again to get them back in sync

[Damiano Testa]

Would this procedure also split off naturally the monster file algebra.monoid_algebra.basic? I am always worried when I do something that might have to modify that file...

[Eric Wieser]

Sort of like how we have docs#vector_space but no-one uses it

[Damiano Testa]

I think that if monoid_algebras received some more love, they would be much nicer to use.

[Damiano Testa]

Currently, I find navigating monoid algebras tricky and I always feel that I should know more programming, rather than more maths.

[Damiano Testa]

(Well, being a mathematician, I'm used to the "needing to know more programming than maths", but it seems more extreme for monoid algebras.)

[Yaël Dillies]

Is that not just because Kenny used the free monoid as an exercise for himself to learn monads? :laughing:

[Adam Topaz]

That's cute, but I think that was a mistake.

[Adam Topaz]

And I'm fairly comfortable with monads

[Damiano Testa]

For a recent example, it took me what I consider too long to first state and then prove that X - 1 ≠ 0 in add_monoid_algebra ℤ (zmod 2). I could not even find the notation for something resembling X!

[Damiano Testa]

At some point, the goal passed through being ⇑↑↑a 1 = 0.

[Damiano Testa]

Ultimately, the proof was a single application of simp [carefully chosen lemmas], which means that the lemmas are probably mostly there, but I found it hard.

[Adam Topaz]

For similar reasons, I don't think the goal should end up loking like f >>= g <$> t = X <| h when dealing with monoid algebras no matter how nice ascii art might be

[Damiano Testa]

Adam, this can happen?!?! :fear:

[Adam Topaz]

I've had it happen with docs#free_abelian_group for example (not to that extreme though)

[Damiano Testa]

I'm glad that I was not there to see it! :smile:

[Adam Topaz]

I tend to use dsimp fairly indiscriminately though