PR summary fe23b837f9

Import changes for modified files

No significant changes to the import graph

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

./scripts/technical-debt-metrics.sh pr_summary

@j-loreaux Do I understand correctly that removing the awaiting author label will draw your attention to these files again?
I've made quite a few changes, but the file now also starts to grow a bit...

Yes, generally, although it is also possible to request review.

I see that you now also consider semigroups, which has led to a proliferation of classes. I think there is yet another possibility to consider here: make the algebraic structure an argument to the class rather than extending it.

So you would write

class Quantale (\a : Type*) [Semigroup \a] extends CompleteLattice \a where ...`

The downside is that you have to write two things to get a quantale, but the upside is that you can easily change the underlying algebraic structure without defining all new classes.

So, to get a bare bones quantale, you just write: but to get a commutative unital one, you simply change this to: [CommMonoid \a] [Quantale \a].

After that, you could potentially make IsIdem or IsIntegral mixin classes. It depends on how often they come up, and whether they come up in conjunction with each other. This is hard for me to say with my limited knowledge of quantales.

So you would write

class Quantale (\a : Type*) [Semigroup \a] extends CompleteLattice \a where ...`

The downside is that you have to write two things to get a quantale, but the upside is that you can easily change the underlying algebraic structure without defining all new classes.

That does not seem the best way to go to me. I think the definition I have now for quantales fits best.
As I explain in the preceding comments, the term is not completely consistent within literature, with some authors
using it for a semigroup and others using it for a monoid, so we have to decide on which stance Mathlib will take on it.
But in many papers I actually see it acknowledged that the original is without assuming the unit element, to subsequently
say: but in this paper we use the term to mean a unital quantale. Therefore, from a Mathlib point of view, I guess it is okay
to drag along the OneQuantale whenever a paper you are formalizing says Quantale.

The construct you are proposing would make sense if the general way of looking at it is that "you turn a semigroup into a quantale", but (just like with a ring consisting of two semigroups) that is not the way quantales are being used imo.

Thanks for thinking along though! It really helps to have someone giving feedback :-)

I've decided to remove the variable_alias for the time being, awaiting the PR by Julian on VectorSpaces and having the discussion on how to use it there.

This lead to a small change again regarding namespaces in the Quantale file.
I would like the main namespaces to be Quantale and AddQuantale, not IsQuantale and IsAddQuantale.

When I introduced the variable alias for AddQuantale, this also introduced its namespace, so the definition of addLeftResidual could be done through to_additive. Now, however, the AddQuantale namespace is not implicitly introduced anymore, which meant I had to pull the introduction of those definitions forward.

Do you agree that using the namespace Quantale is better than IsQuantale?
Especially with an eye on the future introduction of the variable_alias, I think it is more natural, but at the moment it has a small cost involved in not being able to use to_additive for the introduction of leftAddResidual.

I would personally stick to the IsQuantale and IsAddQuantale namespaces, with a view towards renaming if ever Quantale and AddQuantale become a thing

What I think is happening, is that to_additive needs to have made the connection between the Quantale namespace and the AddQuantale namespace, before it can transfer between the two. But there is no way to put the @[to_additive] before a namespace declaration, you can only do that in front of a structure or class definition. So only after you've defined a class or structure with the name of the namespace, to_additive can do its job.

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style