Linear Instance about ModuleCat

Stream: mathlib4

[Nailin Guan]

Hello, I met a problem about conflict of instance.
For a R-algebra S, we have ModuleCat S is R-linear, together with module instance on element of ModuleCat S.
However if the element is of the form ModuleCat.of S Mand M come with a R-module instance already, there is also an instance straight from Module R M.
I tried to set the former one a higher priority, but it still end up with the later instance, how can I resolve this?

[Nailin Guan]

They are actually the same, however currently I can only use @ and fill it in manually.

[Riccardo Brasca]

In a given file you can deactivate one instance writing

attribute [-instance] foo

[Riccardo Brasca]

But of course the point is that we have a diamond here, and we should think about it.

[Nailin Guan]

The problem here is a bit more complicated here, the other instance is needed in the same statement, as we have Ext(M,N), M need the module instance from inside, N need it from outside...
As we are considering Ext commute with localization, we need to consider the R-linear structure on ModuleCat R_p, so this need the module instance from outside.

[Riccardo Brasca]

Can you write precisely which are the two instances?

[Riccardo Brasca]

In your first message it is not clear if you are speaking about an R-module instance or an S-module instance

[Nailin Guan]

Sorry, I'll make it clear here. For R-algebra S and M equiped with [inst1 : Module R M] [Module S M] [IsScalarTower R S M], for ModuleCat.of S M, the first Module R (ModuleCat.of S M) instance come from ModuleCat.Algebra.instModuleCarrier, the second come from inst1

[Riccardo Brasca]

Well, I think that ModuleCat.Algebra.instModuleCarrier is not an instance for this precise reason.

[Riccardo Brasca]

Anyway there is now to make the two action defeq, you literally assume they're equal

[Riccardo Brasca]

Maybe you can play with restric scalars?

[Nailin Guan]

Howevr to deal with R-linear structure on ModuleCat S I need this definitely.

[Nailin Guan]

Riccardo Brasca 說：

Anyway there is now to make the two action defeq, you literally assume they're equal

Sorry what do you mean by this? I know they both form scalar tower with the same S action, what can I do with this?

[Riccardo Brasca]

Just that you cannot expect rfl to be able to prove

import Mathlib

variable {R S M : Type*} [CommRing R] [CommRing S] [Algebra R S] [AddCommGroup M] [Module S M] [h : Module R M]
  (H : IsScalarTower R S M)

example : (ModuleCat.Algebra.instModuleCarrier : Module R (ModuleCat.of S M)) = h := by
  sorry

[Nailin Guan]

One more question, how can I use this equation?

[Riccardo Brasca]

We probably need to see a #mwe to completely understand your problem.

[Kenny Lau]

I suspect the answer is you shouldn't use that equation at all

[Riccardo Brasca]

I agree, we need to see the whole code.

[Aaron Liu]

I'm thinking it might be coming from a functor

[Aaron Liu]

I guess there's no way to tell without seeing the code

[Nailin Guan]

I have a mwe.

import Mathlib.Algebra.Category.ModuleCat.Basic
import Mathlib.Algebra.Module.Shrink

universe v

namespace ModuleCat

variable {R S M : Type*} [CommRing R] [CommRing S] [Algebra R S]

open Algebra in
noncomputable local instance (N : ModuleCat.{v} S) : Module R N := inferInstance

lemma foo {M : ModuleCat.{v} R} {N : ModuleCat.{v} S} (f : M →ₗ[R] N) : f = f := rfl

open Algebra in
lemma foo1 (M : ModuleCat.{v} R) (N : Type*) [AddCommGroup N] [Module R N] [Module S N]
    [IsScalarTower R S N] [Small.{v} N] : 1 = 1 := by
  let f : M →ₗ[R] (ModuleCat.of.{v} S (Shrink.{v} N)) := sorry
  let f' : @LinearMap R R _ _ (RingHom.id R) M (ModuleCat.of.{v} S (Shrink.{v} N)) _ _
      _ instModuleCarrier := sorry
  --#check foo f
  #check foo f'
  sorry

end ModuleCat

as we can see foo f' work but foo f fail

[Nailin Guan]

Aaron Liu 說：

I'm thinking it might be coming from a functor

Yes, my problem originate from a need of extend scalars is linear, the foo here is the thing needing it (I wrote it in some separate place, so a bit hard to show here).

[Kenny Lau]

Nailin Guan said:

noncomputable local instance (N : ModuleCat.{v} S) : Module R N := inferInstance

this line is bad, i think, you should use a functor and not abuse defeq, you should treat them as different objects

[Nailin Guan]

So where can the functor come form? I didn't see how it can be there.

[Nailin Guan]

Also without this foo is not even able to state, how should I resolve this?

[Kenny Lau]

ModuleCat.restrictScalars is the functor

[Riccardo Brasca]

What we are saying is that you should think that N as S-module and N as R-module are two (related but) different objects. In particular, don't put an R-structure on N, use RestrictScalars R S N.

[Nailin Guan]

Maybe there is a deeper problem for me, how do you expect me to fix this statement?

theorem Ext.isLocalizedModule [IsNoetherianRing R] {M N : ModuleCat.{v} R}
    [Module.Finite R M] [Module.Finite R N] {MS NS : ModuleCat.{v'} A}
    (f : M →ₗ[R] MS) (isl1 : IsLocalizedModule S f) (g : N →ₗ[R] NS)
    (isl2 : IsLocalizedModule S g) (n : ℕ) :
    IsLocalizedModule S (Ext.isLocalizedModule_map.{v, v'} S A f isl1 g isl2 n)

[Kenny Lau]

f and g are wrong, see above comment

[Nailin Guan]

OK, this problem here is solved, I'll have a try.

[Nailin Guan]

Sorry, two more question.
1: is it safe to open ModuleCat.Algebra to use the scoped inctance inside?
2: if not, how should I obtain the R-linear structure on ModuleCat S when S is R-algebra?

[Kenny Lau]

1: no; 2: use the functor I linked, or the spelling Riccardo suggested

[Riccardo Brasca]

Really, just think like this: if N is a S-module there is no R-module structure on N (you can write this using category theory, it's the same). The R-module that on paper is again denoted N is RestrictScalar R S N.

[Riccardo Brasca]

Of course under the wood RestricScalar R S N is defined to be N, but this is an implementation detail that should be ignored. If you use it you are "abusing defeq", and 99% of the time it's a bad idea.

[Nailin Guan]

OK, I know what is correct, but the problem is here: I want a R-linear map between Ext over different R-linear category C and D (see #30676), when applied to extend scalars how can I get the R-linear structure? Or is this a bad idea from the start?

[Kenny Lau]

i'm a bit confused, R-linear category means that the homs are R-modules right, so where does this problem come from, could you please specify everything precisely, what categories, what extend scalars, what R-linear structure

[Nailin Guan]

At the beginning, for an additive exact functor F : C => D we have

noncomputable def Functor.mapExtAddHom [HasExt.{w} C] [HasExt.{w'} D] (X Y : C) (n : ℕ) :
    Ext.{w} X Y n →+ Ext.{w'} (F.obj X) (F.obj Y) n

Then if C and D is R-linear, we have.

noncomputable def Functor.mapExtLinearMap [HasExt.{w} C] [HasExt.{w'} D] (X Y : C) (n : ℕ) :
    Ext.{w} X Y n →ₗ[R] Ext.{w'} (F.obj X) (F.obj Y) n

Then I would like to apply this map to ModuleCat.extendScalars (algebraMap R S) when S is flat over R, then we need ModuleCat Sis R-linear, but it is stored in ModuleCat.Algebra namespace as a def ModuleCat.Algebra.instLinear

[Andrew Yang]

This is indeed quite tricky. I think here is it reasonable to turn on ModuleCat.Algebra.instLinear because there usually will not be a better SMul R (Ext.{w'} (F.obj X) (F.obj Y) n) instance.

[Andrew Yang]

But you need to have a good control (or at least a good idea) about where has been contaminated by this instance. For example a choice would be do have an

instance : Module R (Ext.{w'} ((extendScalars _).obj M) ((extendScalars _).obj N) n)

globally, and have a def

attribute [local instance] ... in
noncomputable def extMapExtendScalars :
    Ext.{w} X Y n →ₗ[R] Ext.{w'} ((extendScalars _).obj X) ((extendScalars _).obj Y) n :=
  Functor.mapExtLinearMap ..

and not turn it on anywhere else.

[Nailin Guan]

You mean only open it locally unless unsed? I'll have a try.

[Nailin Guan]

I think I am still needing the module structure on hom as proof of 0 passes through it.

[Kenny Lau]

but 0 is from the add group structure not the module structure

[Nailin Guan]

Sorry I didn't make it clear, I when considering Ext _ _ 0

[Nailin Guan]

The proof is already reaching maximal heartbeat so I want to separarte it out, but need module instance to state.

[Kenny Lau]

it's still a separate question, the hom stuff is not from "ModuleCat.of" etc, so it should be safe

[Kenny Lau]

or you mean the hom itself needs R-module

[Kenny Lau]

nope I don't see it, it's S-hom on the RHS

[Kenny Lau]

to be clearer what i mean, i mean that Module S M -> Module R M is not safe, but Module R (M →ₗ[S] N) is safe

[Nailin Guan]

Kenny Lau 說：

it's still a separate question, the hom stuff is not from "ModuleCat.of" etc, so it should be safe

I know this is a different problem. You are right, I think ofHom will stop the bad things.

[Nailin Guan]

Kenny Lau 說：

to be clearer what i mean, i mean that Module S M -> Module R M is not safe, but Module R (M →ₗ[S] N) is safe

I am exacty needing a similar Module R (M \hom N) for M and N ModuleCat S

[Kenny Lau]

yes, and the point is that this is different from a general rule of "S-module produces R-module"

[Kenny Lau]

in fact M →ₗ[S] N counts as a specific module

[Nailin Guan]

I haven't fully understood yet, but as you say it is OK I'll use it for now. There are enough time for me to figure it out after fixing all the stuffs.

[Nailin Guan]

Another question, is it safe to unfold these kind of definitions in proof? Or better not?

Andrew Yang 說：

But you need to have a good control (or at least a good idea) about where has been contaminated by this instance. For example a choice would be do have an

instance : Module R (Ext.{w'} ((extendScalars _).obj M) ((extendScalars _).obj N) n)

globally, and have a def

attribute [local instance] ... in
noncomputable def extMapExtendScalars :
    Ext.{w} X Y n →ₗ[R] Ext.{w'} ((extendScalars _).obj X) ((extendScalars _).obj Y) n :=
  Functor.mapExtLinearMap ..

and not turn it on anywhere else.

[Kenny Lau]

yes

[Nailin Guan]

Sorry, back to a problem far high up : I want to state the following fact: for R-algebra S, M is ModuleCat R and N is ModuleCat S, I want a linear map f : M =>[R] N to state IsBaseChange S f, how should I use RestrictScalars in this particulat place?

[Kenny Lau]

change the type of f to M \rl[R] RestrictScalars R N

[Nailin Guan]

then how should I obtain Module S and IsScalarTower R S? (i.e. should I turn on RestrictScalars.moduleOrig?)

[Kenny Lau]

hmm, i suppose you would do that, but i'm not sure

[Andrew Yang]

Nailin Guan said:

Another question, is it safe to unfold these kind of definitions in proof? Or better not?

I don't think it is too safe. Do you really need to do this if you add the lemma that it coerced to an addmonoidhom is Functor.mapExtAddHom?

[Andrew Yang]

Nailin Guan said:

Sorry, back to a problem far high up : I want to state the following fact: for R-algebra S, M is ModuleCat R and N is ModuleCat S, I want a linear map f : M =>[R] N to state IsBaseChange S f, how should I use RestrictScalars in this particulat place?

I think this depends on what f you want to apply to. Another choice is unbundle things more, e.g. assume [Module R N] [IsScalarTower R S N] directly in your statement.

[Kevin Buzzard]

I second Andrew's last comment: this [Module R N] [IsScalarTower R S N] trick is a great trick (i.e. add more data into the typeclass system and then claim that the data is uniquely determined so you didn't really make any new assumptions at all).

[Nailin Guan]

Andrew Yang 說：

Nailin Guan said:

Another question, is it safe to unfold these kind of definitions in proof? Or better not?

I don't think it is too safe. Do you really need to do this if you add the lemma that it coerced to an addmonoidhom is Functor.mapExtAddHom?

I this coercion would fix all the things, thanks for this idea.

[Nailin Guan]

Andrew Yang 說：

Nailin Guan said:

Sorry, back to a problem far high up : I want to state the following fact: for R-algebra S, M is ModuleCat R and N is ModuleCat S, I want a linear map f : M =>[R] N to state IsBaseChange S f, how should I use RestrictScalars in this particulat place?

I think this depends on what f you want to apply to. Another choice is unbundle things more, e.g. assume [Module R N] [IsScalarTower R S N] directly in your statement.

I have both version now for the commute of flat base change and Ext when ring noetherian and module fg, it seems your suggestions to unbundle work perfectly for my applications. Thank you very much.

[Nailin Guan]

And thanks for all the helps!

[Nick_adfor]

I would like to introduce cszcsz123@outlook.com, who has thoroughly understood this proof and is currently learning Lean under the guidance of Jujian Zhang.