product of modules over product of rings

Stream: mathlib4

[Kevin Buzzard]

I was surprised that we didn't have this:

import Mathlib

-- variable (R S M N : Type*) [CommRing R] [CommRing S]
--     [AddCommGroup M] [Module R M] [AddCommGroup N] [Module S N] in
-- #synth Module (R × S) (M × N)-- fails

variable (R S M N : Type*) [CommRing R] [CommRing S]
    [AddCommGroup M] [Module R M] [AddCommGroup N] [Module S N] in
instance : Module (R × S) (M × N) where
  smul rs mn := (rs.1 • mn.1, rs.2 • mn.2)
  one_smul mn := by cases mn; ext; exacts [one_smul R _, one_smul S _]
  mul_smul rs rs' mn := by
    cases rs; cases rs'; cases mn
    ext <;>
    exact mul_smul _ _ _
  smul_zero rs := by cases rs; ext <;> exact smul_zero _
  smul_add rs mn mn' := by
    cases rs; cases mn; cases mn'
    ext <;>
    exact smul_add _ _ _
  add_smul rs rs' mn := by
    cases rs; cases rs'; cases mn
    ext <;>
    exact add_smul _ _ _
  zero_smul mn := by cases mn; ext <;> exact zero_smul _ _

Is it not there for a reason?

[Aaron Liu]

You get a diamond when R = S and M = N = R × S, which could be a problem

[Kevin Buzzard]

yeah this was exactly the sort of reason I was expecting :-/

[Kenny Lau]

Note that Prod.instModule (Module R (M × N)) is already a thing

[Kenny Lau]

so what's missing is actually the "projection" instances

[Eric Wieser]

The general rule is that SMul X Y -> SMul (F X) (F Y) is almost always a bad idea

[Kenny Lau]

which cause diamond with each other

[Kevin Buzzard]

Eric Wieser said:

The general rule is that SMul X Y -> SMul (F X) (F Y) is almost always a bad idea

In FLT we have an instance [NumberField K] [NumberField L] [Algebra K L] -> [Algebra (AdeleRing (𝓞 K) K) (AdeleRing (𝓞 L) L)]. Would this be an exception to the general rule? Because here the arguments of the form "what if X = F Z" can't apply, as X is always a number field and F X never is.

[Eric Wieser]

Yes, that's the kind of exception I had in mind; those are still "bad" in that they encourage people to write similar instances which could satisfy X = F Z, especially if type-classes are weakened

[Antoine Chambert-Loir]

Aaron Liu said:

You get a diamond when R = S and M = N = R × S, which could be a problem

Then I'm puzzled, because it seems that the case of arbitrary products exists as docs#Pi.module', so that instance would probably make a diamond as well.

[Anatole Dedecker]

It does indeed: there are two natural actions of X → R on X → X → R. I don't think this is fixable without a convenient way to refer to module structures, but this has been discussed before (e.g in the context of representation theory).

[Kevin Buzzard]

Hmm. There is still a diamond problem with the instance [Algebra K L] -> [Algebra (𝔸 K) (𝔸 L)] in FLT, namely that if L = K this gives two non-defeq instances of [Algebra (𝔸 K) (𝔸 L)] (here 𝔸 K := AdeleRing (𝓞 K) K)). Should I be (a) striving to make them defeq or (b) giving up on the idea of being able to write this very natural-looking mathematics in Mathlib at all or (c) doing instance priority hacks to get around it (basically ensuring that Lean tries identity stuff before this stuff)?

Interestingly this issue even propogates to Prop-valued instances. For example we have an instance IsModuleTopology (𝔸 K) (𝔸 L) and my instinct would be that this couldn't cause diamonds because it's a Prop, but it instead causes typeclass timeouts because it's necessarily defined using the more general [Algebra (𝔸 K) (𝔸 L)] so won't fire when L = K.

[Kevin Buzzard]

What do people think of #29315 ? This ensures that synthesizing IsModuleTopology (𝔸 K) (𝔸 K) does not time out in FLT.

[Eric Wieser]

I think in general it's impossible to make them defeq unless you have some kind of X.map id = X := by rfl lemma, which is very rarely true by definition.

[Eric Wieser]

So yes, defeq of SMul (F X) (F X) via the SMul X Y -> SMul (F X) (F Y) instance vs the Mul X -> SMul X X one is another reason that this pattern is really not a good one

[Kevin Buzzard]

I understand what you're saying but it's hard not to read it as "Mathlib's setup makes it not very good for doing some parts of number theory".

[Kevin Buzzard]

Let me go through this again to make sure I've got my argument straight. 𝔸 (pronounced "adeles of") is a function which eats a (number) field and spits out a commutative topological ring (which is never a field). Objections are being raised above to the instance Algebra K L -> Algebra (𝔸 K) (𝔸 L) so that's fine, this doesn't have to an instance, it can be something which can be switched on manually.

A nontrivial and interesting theorem which we're working towards in FLT is that if Algebra K L then the topology on 𝔸 L is the 𝔸 K-module topology. This is stated as a typeclass IsModuleTopology R M in Mathlib, where M is an R-module. So to even state the theorem we're going for in mathlib we need an instance Module (𝔸 K) (𝔸 L) so this instance needs to be inserted into the system somehow, and it has to come from Algebra K L. In particular, when we ask typeclass inference to find IsModuleTopology (𝔸 K) (𝔸 L), the instance it finds must use an instance of Module (𝔸 K) (𝔸 L) so it must use an instance of Algebra K L, so the proof must use the construction Algebra K L -> Algebra (𝔸 K) (𝔸 L) (whether or not this construction itself is an instance). However when K = L this construction which will necessarily be used does not (and probably cannot) give us something defeq to Algebra.id (𝔸 K) for Algebra (𝔸 K) (𝔸 K). This is likely to manifest itself in typeclass inference timing out.

My proposal in #29315 is simply to slightly raise the priority of IsTopologicalSemiring.toIsModuleTopology R : IsModuleTopology R R so that IsModuleTopology (𝔸 K) (𝔸 K) is solved by this instance before it finds the K = L case of the path Algebra K L -> Algebra (𝔸 K) (𝔸 L) -> IsModuleTopology (𝔸 K) (𝔸 L) (which won't unify because the algebra instance is wrong).

I dug into the history of why Algebra.id managed to get a priority of 1100 (so higher than default). It was done in #13032 which was itself inspired by a far more technical discussion about adeles (which I'm about to link to). I didn't understand most of the things said about discriminant trees but I'd like to highlight this comment by @Jovan Gerbscheid which argued that Algebra.id should be tried last because of something to do with discrimination trees which I have no understanding of (indeed I'm still looking for the basic reference on discrimination trees which would tell me what they are -- blog post anyone?). People can just read Jovan's explanation so I won't attempt to copy-paste and possibly butcher it here. Is this an argument against #29315 ? Note that just as #13032 did, #29315 makes mathlib slightly quicker.

[Sébastien Gouëzel]

What about scoping all the instances you need (including Algebra K L -> Algebra (𝔸 K) (𝔸 L)) and opening them in sections where you will never use K = L?

[Kevin Buzzard]

The problem is that the proof of IsModuleTopology (𝔸 K) (𝔸 L) uses along the way the fact that 𝔸 L is homeomorphic to Fin n -> 𝔸 K where $n=[L:K]$ and then uses IsModuleTopology R M -> IsModuleTopology R (Fin n -> M) so in particular it uses IsModuleTopology (𝔸 K) (𝔸 K) :-) Indeed formalising this argument is exactly how we discovered the problem.

[Eric Wieser]

In Lean 3 we often used a pattern along the lines of

attribute [local instance] someBadDataCarryingInstance in
instance : SomePropInstanceThatNeedsIt := sorry

though I seem to recall that this was very rarely unsafe in some versions of Lean 4 (maybe @Anne Baanen remembers), as some unwanted unification sometimes happened in typeclass search.

[Eric Wieser]

Maybe that's orthogonal to your point though

[Eric Wieser]

I don't see anything wrong with #29315; in general I think we're not very principled with priority changes, and so ultimately determining if a priority change is a good idea is just a matter of measuring if the things you care about got faster without other things getting too much slower

[Eric Wieser]

Kevin Buzzard said:

I'd like to highlight this comment by @Jovan Gerbscheid which argued that Algebra.id should be tried last because of something to do with discrimination trees which I have no understanding of

My reading of this was not "it should be tried last", but "it will be tried last and there's nothing you can do about it"

[Eric Wieser]

Mathematically, is Algebra (𝔸 K) (𝔸 L) subsingleton? If so you could assume that in your theorem instead and maybe the problem would go away.

[Kevin Buzzard]

No it's not, unfortunately; if K has automorphisms then so does 𝔸 K; for example complex conjuation on $K:=\mathbb{Q}(i)$ will induce a nontrivial topological ring automorphism of 𝔸 K and precomposing with this will give you another algebra instance.

[Sébastien Gouëzel]

If you just need IsModuleTopology (𝔸 K) (𝔸 K) in a proof, can't you just put a line have : IsModuleTopology (𝔸 K) (𝔸 K) := instIdOrWhatever to override what typeclass inference would do?

[Kevin Buzzard]

Yes absolutely. The only reason I was looking into this was that the person who was writing the PR (not me) couldn't understand why typeclass inference was not doing all the work for them, because all the issues are there. I checked that their sorry could be replaced by inferInstance after #29315 .

[Kevin Buzzard]

If the community doesn't like that PR though, then probably either I will do this or I will lower the priority of Algebra (\A K) (\A L) to slightly less than 1000, which will have the same effect in practice.