Bundling docs#submodule.restrict_scalars?

Stream: general

[Anne Baanen]

I would like to turn docs#submodule.restrict_scalars into an order embedding:

def restrict_scalars : submodule R M ↪o submodule S M :=
{ to_fun := λ V, { carrier := V.carrier,
    zero_mem' := V.zero_mem,
    smul_mem' := λ c m h, V.smul_of_tower_mem c h,
    add_mem' := λ x y hx hy, V.add_mem hx hy },
  inj' := λ p q h, set_like.ext (by simpa using set_like.ext_iff.mp h),
  map_rel_iff' := λ p q, by simpa [set_like.le_def] }

However, this breaks dot notation: if you write (p : submodule R M).restrict_scalars S, you get an error invalid field notation, function 'submodule.restrict_scalars' does not have explicit argument with type (submodule ...) because the elaborator doesn't turn ↪o into → when elaborating dot notation. So I think I'll just add a new bundled version and simp it to restrict_scalars when it gets applied, or does someone want to help replacing all the dots?

[Anne Baanen]

Another argument against bundling: restrict_scalars is also a monoid_with_zero_hom (or at least it preserves some subset of those operations).

[Anne Baanen]

I'll just go with the separate definition. Thanks for the rubber duck debugging.

[Eric Wieser]

Dot notation would work if you made S implicit, but that's also annoying