is_scalar_tower for morprhisms

Stream: maths

[Kevin Buzzard]

I've never used is_scalar_tower seriously until today, and I've had a great time with it, it worked like a dream. Except for here:

import ring_theory.algebra_tower

variables (R₀ R N P : Type*)

variables [comm_semiring R₀] [comm_semiring R] [algebra R₀ R]
  [add_comm_monoid N] [semimodule R₀ N] [semimodule R N] [is_scalar_tower R₀ R N]
  [add_comm_monoid P] [semimodule R₀ P] [semimodule R P] [is_scalar_tower R₀ R P]

example : add_comm_monoid (N →ₗ[R] P) := infer_instance
example : semimodule R (N →ₗ[R] P) := infer_instance
example : has_scalar R₀ (N →ₗ[R] P) := infer_instance
example : is_scalar_tower R₀ R (N →ₗ[R] P) := infer_instance -- fails

Is this a missing instance? I'm not quite confident enough to start adding things, but mathematically it looks OK. Am I missing an import?

[Kevin Buzzard]

example : is_scalar_tower R₀ R (N →ₗ[R] P) :=
{ smul_assoc := λ _ _ _, linear_map.ext $ by simp }

[Kevin Buzzard]

@Damiano Testa this was why simp was failing -- linear_map.map_smul_of_tower is a simp lemma and should have been making our lives easier but it wasn't firing for this reason.

[Eric Wieser]

I assume there is no docs#linear_map.is_scalar_tower or docs#linear_map.smul_comm_class?

[Eric Wieser]

I'd expect to find them next to each other, and the latter exists

[Kevin Buzzard]

OK thanks, I'll add the former. It's solved the problems we were having earlier.

[Eric Wieser]

What lemmas does simp use in your example?

[Eric Wieser]

I'd kind of expect the instance to involve three rings not two

[Kevin Buzzard]

It's the toric branch of lean-liquid. The lemma which wasn't firing was linear_map.map_smul_of_tower.

[Kevin Buzzard]

docs#linear_map.map_smul_of_tower

[Kevin Buzzard]

compatible_smul wasn't firing.

[Eric Wieser]

Since docs#linear_map.semimodule involves two rings

[Kevin Buzzard]

M_2 in our case was (N ->_l[S] P) in the notation of map_smul_of_tower

[Kevin Buzzard]

so we had two rings and three modules

[Kevin Buzzard]

It all works fine with the instance added.

[Eric Wieser]

Sure, but my point is that the missing instance you suggest upthread is not the most general one

[Eric Wieser]

It's definitely better than no instance though

[Kevin Buzzard]

I'll make the PR and we can continue the discussion there.

[Kevin Buzzard]

#6331. I managed to remove the assumption that the "bottom" semiring was a semiring, instead its now a monoid with a smul_comm_class instance and a mul_action.

[Damiano Testa]

This is all great: thank you for taking the time to solve this!

I will now look at the file!