Zulip Chat Archive

Stream: maths

Topic: is_scalar_tower for morprhisms


view this post on Zulip Kevin Buzzard (Feb 20 2021 at 22:27):

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?

view this post on Zulip Kevin Buzzard (Feb 20 2021 at 22:30):

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

view this post on Zulip Kevin Buzzard (Feb 20 2021 at 22:31):

@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.

view this post on Zulip Eric Wieser (Feb 20 2021 at 22:47):

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

view this post on Zulip Eric Wieser (Feb 20 2021 at 22:47):

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

view this post on Zulip Kevin Buzzard (Feb 20 2021 at 22:48):

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

view this post on Zulip Eric Wieser (Feb 20 2021 at 22:54):

What lemmas does simp use in your example?

view this post on Zulip Eric Wieser (Feb 20 2021 at 22:55):

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

view this post on Zulip Kevin Buzzard (Feb 20 2021 at 22:55):

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

view this post on Zulip Kevin Buzzard (Feb 20 2021 at 22:55):

docs#linear_map.map_smul_of_tower

view this post on Zulip Kevin Buzzard (Feb 20 2021 at 22:56):

compatible_smul wasn't firing.

view this post on Zulip Eric Wieser (Feb 20 2021 at 22:56):

Since docs#linear_map.semimodule involves two rings

view this post on Zulip Kevin Buzzard (Feb 20 2021 at 22:56):

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

view this post on Zulip Kevin Buzzard (Feb 20 2021 at 22:56):

so we had two rings and three modules

view this post on Zulip Kevin Buzzard (Feb 20 2021 at 22:57):

It all works fine with the instance added.

view this post on Zulip Eric Wieser (Feb 20 2021 at 22:57):

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

view this post on Zulip Eric Wieser (Feb 20 2021 at 22:57):

It's definitely better than no instance though

view this post on Zulip Kevin Buzzard (Feb 20 2021 at 22:57):

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

view this post on Zulip Kevin Buzzard (Feb 20 2021 at 23:58):

#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.

view this post on Zulip Damiano Testa (Feb 21 2021 at 05:43):

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

I will now look at the file!


Last updated: May 10 2021 at 08:14 UTC