module from semimodule over a ring

Stream: general

[Scott Morrison]

Am I allowed to ask for

import algebra.module.basic

variables (R : Type) [ring R]

instance foo (M : Type) [add_comm_monoid M] [semimodule R M] : add_comm_group M :=
by sorry

example (M : Type) [add_comm_monoid M] [semimodule R M] : module R M :=
by sorry

these days, or is that verboten?

[Scott Morrison]

I'm trying to match up the abstract and concrete definitions of projective that we now have. The problem is that Module R is the category of modules over R (so R must be a ring, not a semiring), while in is_projective.of_lifting_property, we quantify over semimodules. So in order to show that an X : Module R with projective X also has is_projective X, I need to know those semimodules are actually modules.

[Scott Morrison]

So I'm happy if these are evil instances: I promise not to ever release them from a Prop-valued goal. :-)

[Kevin Buzzard]

Another alternative is to give up on this silly semimodule nonsense completely. I'm well aware that you can have semimodules over a semiring but honestly, do semimodule theorists (if such people actually exist) really study projective semimodules?

[Scott Morrison]

I would support not caring about whether semimodules are projective. :-)

[Kevin Buzzard]

What I'm saying is that I was just conforming to mathlib principles when I defined projective semimodules, and have 0 applications in mind

[Scott Morrison]

src#semimodule.add_comm_monoid_to_add_comm_group

[Scott Morrison]

found it!

[Scott Morrison]

Oh, but #7255 is about to change all this.

[Scott Morrison]

maybe not.

[Sebastien Gouezel]

Scott Morrison said:

Am I allowed to ask for

import algebra.module.basic

variables (R : Type) [ring R]

instance foo (M : Type) [add_comm_monoid M] [semimodule R M] : add_comm_group M :=
by sorry

example (M : Type) [add_comm_monoid M] [semimodule R M] : module R M :=
by sorry

these days, or is that verboten?

The first one can not be a global instance, as R is not determined from the target, so there would be some unknown metavariable in the instance search, which is very bad. But you can use it in proofs with explicit declarations as you like. The second one is already an instance, since semimodule and module are the same thing.

[Scott Morrison]

I'm still not getting this to work.

import algebra.module.basic

local attribute [instance] semimodule.add_comm_monoid_to_add_comm_group

example (R : Type) [ring R] (M : Type) [mM: add_comm_monoid M] [sM : semimodule R M] : module R M :=
???

[Scott Morrison]

(This is post #7255.)

[Oliver Nash]

How about:

example (R : Type) [ring R] (M : Type) [mM: add_comm_monoid M] [sM : semimodule R M] : module R M :=
{..sM} -- (or `{..(infer_instance : semimodule R M)}` or even `{..‹semimodule R M›}`)

[Anne Baanen]

Wouldn't it be a nicer solution to just get rid of module altogether and rename semimodule to module? Whenever you need a - on R or M you can add it back in through the other typeclasses.

[Sebastien Gouezel]

Abbreviations are really weird. As Anne suggests, I would just ditch semimodule and rename it to module, since as far as I can see the abbreviation we currently have doesn't buy us anything, and is creating problems sometimes.

[Anne Baanen]

Shall I make a PR to try it out (and do the same for vector_space)?

[Anne Baanen]

I ran sed -i s/semimodule/module/g s/vector_space/module/g **/*.lean, see #7322 for the result.

[Anne Baanen]

I went through all changes. My main question: it would be okay to keep dim in the vector_space namespace, even though there is no definition called vector_space?

[Anne Baanen]

(Or should I just go ahead and move it to the free_module namespace, in anticipation of a free_module typeclass?)

[Johan Commelin]

My guess is that the typeclass would be called module.free

[Johan Commelin]

We could just have module.rank and never use dim?

[Eric Wieser]

I'm not sure the abbreviation is a problem here - Scott's example just seems like a weird thing to want to do

[Mario Carneiro]

Anne Baanen said:

Shall I make a PR to try it out (and do the same for vector_space)?

Heh, we're coming full circle

[Anne Baanen]

@Johan Commelin's suggestion sounds good. I'll see if calling it rank works, and then add a TODO that this should be defined for modules that are not over a field.

[Anne Baanen]

One drawback: _root_.rank already exists, the rank of a linear map. So module.rank will have to be a protected definition (until we rename _root_.rank to linear_map.rank).

[Anne Baanen]

By the way, I found an example of the instance : module := {.. infer_instance : semimodule} pattern at docs#triv_sq_zero_ext.module

[Eric Wieser]

Does that instance break if you change it to := infer_instance?

[Anne Baanen]

I'm currently compiling mathlib with (among others) that entire instance removed, so could you check that yourself? :)

[Anne Baanen]

On the semimodule_to_module branch, I'm getting a timeout in Module.limit_module (src/algebra/category/Module/limits.lean):

instance limit_module (F : J ⥤ Module R) :
  module R (types.limit_cone (F ⋙ forget (Module.{v} R))).X :=
begin
  change module R (sections_submodule F),
  apply_instance,
end

Doing this in term mode makes it almost instant (60ms elaboration time):

instance limit_module (F : J ⥤ Module R) :
  module R (types.limit_cone (F ⋙ forget (Module.{v} R))).X :=
(infer_instance : module R (sections_submodule F))
-- or:
instance limit_module (F : J ⥤ Module R) :
  module R (types.limit_cone (F ⋙ forget (Module.{v} R))).X :=
show module R (sections_submodule F), by apply_instance

[Johan Commelin]

And if you change change to show in tactic mode?

[Anne Baanen]

Also times out.

[Yakov Pechersky]

I've found, in my large refactors like the nat-mul one, or trying things with the nsmul and gsmul ones, that change tactic proofs are often a troublemaker.

[Yakov Pechersky]

They're good at getting the goal to be something human readable, and perhaps rwable, but really they usually hide heavy-rfl steps.

[Yakov Pechersky]

And are particularly brittle to changes in defeq

[Anne Baanen]

I tried using rw (rfl : ... = ...) instead, but that gives an incorrect motive error.

[Anne Baanen]

Looking at the is_def_eq_detail trace, looks like it really is the limit_add_comm_group that is being unified badly.

[Anne Baanen]

Aha, defining limit_add_comm_monoid analogous to limit_add_comm_group solves the timeout almost instantly.