Lost instance

Stream: maths

[Patrick Massot]

@Eric Wieser the following used to be no problem:

import algebra.algebra.operations
import algebra.module.submodule


variables {ι R A : Type*} [comm_ring R] [comm_ring A] [algebra R A]

example : has_scalar A (submodule R A) :=
sorry

[Patrick Massot]

It used to be mul_action.to_has_scalar B (submodule R B) : has_scalar B (submodule R B) which used submodule.mul_action_algebra : mul_action B (submodule R B).

[Patrick Massot]

Do you know what happened to those instances?

[Patrick Massot]

Beware: when I write "used to work" I mean it worked two years ago.

[Eric Wieser]

I have no memory of docs#submodule.mul_action_algebra, but I suppose it's possible I removed it by accident

[Eric Wieser]

"Two years ago" is helpful, that's a starting point for a git blame

[Patrick Massot]

Oh I'm sorry. I followed the trail and actually ended up somewhere in the perfectoid spaces project. So it probably never was in mathlib.

[Patrick Massot]

Sorry about the noise.

[Patrick Massot]

And we should probably do it differently now.

[Eric Wieser]

I would assume it generalizes to has_scalar S (submodule R A) for some compatibility condition on R,S, A that presumably becomes obvious once you try to prove it

[Patrick Massot]

Do you know the name of the linear map given by scalar multiplication?

[Eric Wieser]

docs#linear_map.to_span_singleton?

[Eric Wieser]

Or do you mean one of the other ones?

[Patrick Massot]

One of the other ones

[Eric Wieser]

docs#linear_map.lsmul?

[Eric Wieser]

I think there's a less bundled version but I don't remember where it is

[Patrick Massot]

I can now use:

instance toto : has_scalar A (submodule R A) :=
⟨λ a S, submodule.map ((linear_map.lsmul A A a).restrict_scalars R) S⟩

[Patrick Massot]

I'll let you the pleasure to find the generalization you want.

[Eric Wieser]

This looks like a suitable generalization:

variables {R S M : Type*} [semiring R] [add_comm_monoid M] [module R M]
variables [monoid S] [distrib_mul_action S M] [smul_comm_class S R M]

/-- I have no idea how to name this -/
def another_smul_hom (s : S) : M →ₗ[R] M :=
{ to_fun := has_scalar.smul s,
  map_add' := smul_add s,
  map_smul' := λ a b, smul_comm _ _ _ }

instance toto : has_scalar S (submodule R M) :=
⟨λ s p, p.map (another_smul_hom s)⟩

-- works
example {R A : Type*} [comm_ring R] [comm_ring A] [algebra R A] : has_scalar A (submodule R A) :=
by apply_instance

[Eric Wieser]

I was hoping that would be enough to get has_scalar (opposite A) (submodule R A) too, but we're missing some pieces

[Kevin Buzzard]

It's crazy how we don't assume commutativity of R or S or anything -- the ingredient needed to make it work is that multiplication by s : S is R-linear, and whilst in practice this will usually be because R and S are subtypes of some bigger commutative structure, these crazy smul_comm_class typeclasses are somehow the precise fact we need from the set-up to make the construction work.

[Eric Wieser]

PR'd as #8945

[Eric Wieser]

submodule.mul_action_algebra now exists as submodule.pointwise_distrib_mul_action