Transporting along is_scalar_tower

Stream: maths

[Yaël Dillies]

Yesterday, I finally understood what all the fuss around scalar actions was about (thanks Eric for your talk!) and I'm now having thinking about them.
Right now I'm wondering whether we can think of is_scalar_tower as saying "here is a scalar action of α on β and another one of β on γ, please make the scalar action of α on γ that associates" and how far that leads.
For example, [is_scalar_tower α β γ] [smul_with_zero α β] [smul_with_zero β γ]and "every c : γ can be written as b • c'" gives smul_with_zero α γ because (0 : α) • c = 0 • b • c' = (0 • b) • c' = 0 • c = 0 and a • (0 : γ) = a • (0 • 0) = (a • 0) • 0 = 0 • 0 = 0.
What instances can we get like that, and what's the canonical way to express "every c : γ can be written as b • c'"?

[Anne Baanen]

I think you're confusing the typeclass docs#is_scalar_tower with the type synonym docs#restrict_scalars. The latter has a new scalar action, which is more like your description, while the former takes three scalar actions and asserts they commute.

[Johan Commelin]

Yaël Dillies said:

For example, [is_scalar_tower α β γ] [smul_with_zero α β] [smul_with_zero β γ]

This doesn't type check, right? You first need 3 has_scalar instances, before you can talk about a is_scalar_tower X Y Z

[Yaël Dillies]

Nono, I did mean is_scalar_tower (although maybe restrict_scalars is what I'm after. I can't tell). I meant to have scalar action instances on α β and β γ, has_scalar α γ and then use is_scalar_tower α β γ to populate the naked has_scalar α γ.

[Johan Commelin]

No, that doesn't work.

[Johan Commelin]

structure is_scalar_tower (M : Type u_9) (N : Type u_10) (α : Type u_11)
  [has_scalar M N] [has_scalar N α] [has_scalar M α] : Prop

[Anne Baanen]

How would the typeclass system figure out which β to fill into is_scalar_tower α β γ?

[Johan Commelin]

is_scalar_tower is a Prop that asserts that 3 scalar actions are compatible.

[Anne Baanen]

So for example, you're asking: "if I have algebra α β, algebra β γ and a bare has_scalar α γ such that is_scalar_tower α β γ, can I automatically derive algebra α γ?", right?

[Yaël Dillies]

Yeah exactly

[Eric Wieser]

The point of is_scalar_tower α β γ is not to populate has_scalar α γ, it's to indicate that an existing instance is propositionally equal to the obvious population

[Anne Baanen]

It would be a nice trick, but the answer is not really. Because there is no automatic way for the typeclass system to choose the β for which it works. I guess the closest you could come is have a tactic figure it out based on what is in the context.

[Yaël Dillies]

or even just an instance as a def?

[Eric Wieser]

docs#restrict_scalars.is_scalar_tower says "The populated algebra R (restrict_scalars R S A) you're asking for is compatible with algebra R S and algebra S A"

[Yaël Dillies]

Ah so yeah, that's kind of what I was thinking about.

[Anne Baanen]

There are a few defs, like docs#is_integral_of_is_scalar_tower, that do something similar.

[Anne Baanen]

But they all have to work manually

[Eric Wieser]

It's usually a bad idea to actually put the instance on γ as in your example, because frequently there will already be an instance on γ elsewhere and your new instance will form a diamond

[Eric Wieser]

Which is why we use the type synonym restrict_scalars

[Yaël Dillies]

So when I have a lemma that requires the 3 instances, and the first two allow to derive the last and the last doesn't appear in the statement, should I still ask for the 3?

[Yaël Dillies]

I understand that if it did appear then yes, definitely, for defeqness issues.

[Johan Commelin]

@Yaël Dillies We used to have algebra.comp R A B which was a type alias that made B into an R algebra. It created all sorts of defeq problems, and very ugly code.

[Johan Commelin]

So, given the current state of lean and mathlib, I'm very much in favour of: add all the (redundant) data by hand, and on top of that, ask for compatibilities using classes like is_scalar_tower

[Yaël Dillies]

And then the burden of proving them is left on the end user who is working with concrete structures?

[Anne Baanen]

In principle you could try deriving it in the body, but why not make a separate global instance? Then it would be less risk of accidentally ending up in the lemma statement, and available to further developments.

[Anne Baanen]

E.g. #8761 was originally an inline letI : algebra _ _ := _ which I later put into its own instance.

[Yaël Dillies]

I see I see. Thanks for the explanations!

[Eric Wieser]

Yaël Dillies said:

So when I have a lemma that requires the 3 instances, and the first two allow to derive the last and the last doesn't appear in the statement, should I still ask for the 3?

If the lemma statement only requires 2 of them and the third is only needed by the proof, then arguably constructing it with restrict_scalars inside the lemma proof is sometimes the right thing to do

[Eric Wieser]

Indeed, this is quite common for downgrading complex-modules to real-modules I think

[Eric Wieser]

But usually, you'll end up also wanting a lemma that _does_ need all three instances in the statement, and for that one you should _not_ use restrict_scalars and will need the appropriate global instance like in @Anne Baanen's linked PR.