Move lemma from concrete class to mixin or duplicate?

Stream: new members

[Calvin Lee]

Hello! I'm currently working with docs#localized_module and its mixin class docs#is_localized_module. I've decided I need localized_module.is_module' and localized_module.is_scalar_tower to hold for is_localized_module instead of localized_module.
Should I move it to the mixin class and hope that class inference picks up on this for existing use-cases? Or should I duplicate the instances for the mixin class so that it holds for both?

[Anne Baanen]

Unfortunately is_localized_module S f doesn't have the right structure to work for is_module' or is_scalar_tower:

[Anne Baanen]

First of all, is_module' would take is_localized_module S (f : M →[R] N) and return module R N. But the type of f already assumes N is an R-module. So I don't see why you need it :/

[Anne Baanen]

For is_scalar_tower the issue is as follows: suppose we want an instance of is_scalar_tower R (localization (S : submonoid R)) N. Lean searches through the candidate instances and tries to apply is_localized_module.is_scalar_tower ?S (?f : ?M →[?R] ?N) : is_scalar_tower ?R (localization ?S) ?N (the question marks represent metavariables to be filled by unification). It figures out ?R = R, ?S = S and ?N = N, but there is no way for it to figure out which ?f to use.

[Anne Baanen]

In general the rule is that all parameters to an instance inst should be able to be automatically figured out either through unification (i.e. appear in the result type) or through instance synthesis. A good test is that apply inst should never produce any new goals.

[Calvin Lee]

oh oops, I meant docs#localized_module.is_module which would provide module (localization S) N instead.
the unification problem is exactly what I'm asking about!
Wouldn't [is_localized_module.is_scalar_tower take an implicit argument of [is_localized_module S f] which could be filled in by localized_module.is_localized_module? or is this too difficult to infer

[Anne Baanen]

So yes, f can be filled in in the end if we continue synthesizing instances. However, this has two big disadvantages: First is that I'm pretty sure Lean won't start looking for instances until all parameters have been filled. Second is that there is no guarantee that we'll find the instance for the right f: a priori there could be many f : M →[R] N with the right properties. I'm pretty sure we can prove those are all equal, but Lean doesn't know this by definition. So you're somewhat likely to have to use congr and convert and etc. to get your lemmas to apply when they pick up the wrong f.

[Anne Baanen]

It seems like making these instances do all the work on localized_module would be a good idea, and I can think of two ways we can go about it:

[Anne Baanen]

• If for fixed values of S M N there is a canonical f, then we should redefine the is_localized_module to instead have type is_localized_module (S : submonoid R) (M N : Type*) (f : out_param (M →[R] N)). In exchange for promising never to have an instance with the same values for S M N and different values for f, Lean will allow (force!) f to be a free variable that is found alongside the proof that f is indeed a localized module.

[Anne Baanen]

• We copy the approach used by ring localizations (docs#is_localization): we pass in f through another typeclass, providing a canonical map f : M →[R] N given values for R M N. I expect this will be more convenient in practice since algebra is very convenient. In fact, I was already trying to implement classes for doing this. However, due to many details changing between Lean 3 and Lean 4, we'll probably have to wait for the mathlib4 port to finish before we can implement something complicated along these lines.