Puzzles around Picard group

Stream: maths

[Junyan Xu]

The Picard group of a (commutative) ring R is the type of all invertible R-modules M (in the sense that there exists N such that $M\otimes_R N \cong R$) up to isomorphism, with tensor product as multiplication.

abbrev Pic : Type (u + 1) := (Skeleton <| ModuleCat.{u} R)ˣ

I almost finished formalizing an isomorphism between the Picard group of a domain with docs#ClassGroup, but there are several side questions bugging me:

1. If M is an invertible R-module, then the ring homomorphism $R\to\text{End}_R(M\otimes_R M)$ is an isomorphism. The involutive R-automorphism of $M\otimes_R M$ that swaps the two factors (docs#TensorProduct.comm) gives an element of R whose square is 1, and this gives rise to a natural transformation from Pic to $\mu_2$. I'd think this invariant must have been studied if it's not always trivial, but I haven't come up with a proof that it's always trivial. If every ring embeds into some ring with trivial Picard group, that would give a proof.

2. Must an invertible R-module M have the same cardinality as R? Since invertible implies finite (and projective), if R is infinite then #M is bounded by #R, but it seems tricky to establish the reverse inequality. (Note that R is a projective (R x S)-module for any ring S, so projective+nontrivial is not enough, and it doesn't seem that playing with $M\otimes_R\text{Hom}_R(M,R)\cong R$ easily leads to a proof.)

3. When R is finite (or just Artinian), it turns out the Picard group is always trivial: the Picard group of a ring remains the same after quotienting out the nilradical (to obtain a reduced ring), and an Artinian reduced ring is a finite product of fields, which have trivial Picard groups. But is there an easier way to see triviality of Pic / equality of cardinality in the finite case?

[Junyan Xu]

I just found that @Kevin Buzzard wrote about the isomorphism $M=M\otimes_RR=M\otimes_R(N\otimes_R M)=(M\otimes_R N)\otimes_R M=R\otimes_R M=M$ 3+ years ago. I think this isomorphism is the identity iff the swapping map on $M\otimes_R M$ is the identity. However I didn't need this to show M is finite (and projective), which I already formalized. Stacks Project says "is an automorphism of M" without claiming it's the identity.

[Andrew Yang]

Can you just check locally where $M$ is trivial?

[Junyan Xu]

Great idea! I think this works (for problem 1), and probably there's no simpler proof.
I think I hadn't internalized the fact that the Picard group of a local ring is trivial. For Problem 3 one can decompose an Artinian ring into a finite product of local rings, so we no longer need to reduce to the reduced case.

[Junyan Xu]

If every ring embeds into some ring with trivial Picard group, that would give a proof.

So this is true as well: it embeds into the product of localizations (at primes/maximals), which has trivial Picard group according to this (though I don't completely understand the argument) ...

[Yaël Dillies]

Junyan Xu said:

I just found that Kevin Buzzard wrote about the isomorphism $M=M⊗ M)=(M⊗ N)⊗ M=R⊗ M=M$ 3+ years ago. I think this isomorphism is the identity iff the swapping map on $M⊗ M$ is the identity. However I didn't need this to show M is finite (and projective), which I already formalized. Stacks Project says "is an automorphism of M" without claiming it's the identity.

Some rings $R$ have nontrivial automorphisms as $R$-modules, right? If so, there is no chance that this automorphism of $M$ is always the identity because you can take $M = R$, $N = 1$, $M ⊗_R N = R$ the identity, $N ⊗_R M = R$ a nontrivial automorphism.

[Junyan Xu]

The nontrivial automorphisms of R as an R-module correspond bijectively to units in R (even for noncommutative R). But I think in Kevin's post $N\otimes_R M=R$ is supposed to be the swap map composed with $M\otimes_R N = R$. And what do you mean by $N=1$ here? Is it different from $R$?

[Junyan Xu]

I'm a bit surprised this isn't in Mathlib yet:

import Mathlib
theorem IsLocalization.flat (R S) [CommRing R] [CommRing S] [Algebra R S]
    (M : Submonoid R) [IsLocalization M S] : Module.Flat R S := by
  exact?

It should follow easily from @Andrew Yang's work on localization of submodules. It's great that we have equational criterion of flatness, but we still need to implement this proof (or else (1)->(4) here) to implement Andrew's solution to my question 1. Another option is to prove Kaplansky's theorem ...

[Andrew Yang]

We have docs#Module.free_of_flat_of_localRing. Is this enough?

[Junyan Xu]

Good! By coincidence I've formalized an easy proof that a finite projective module is finitely presented.

[Junyan Xu]

It generalizes docs#Module.finitePresentation_of_free but do we want to import Projective into that file? I've actually opened another file dedicated to finite projective modules (stacks#00NX).

[Jz Pan]

Is this docs#Module.Flat.localizedModule enough to prove IsLocalization.flat?

[Junyan Xu]

I don't think so, it's a generic fact that applies to the base change to any algebra (not necessarily flat), just specialized to the case that the algebra is a localization.

[Andrew Yang]

If @Christian Merten can PR smooth => flat into mathlib then we will have this for free :)
But it should be easy to prove directly.

[Andrew Yang]

About stacks#00NX: We are very close to having this.
We have (3) <=> (2) => (1) => (4) => (5). (modulo finite projective => finite presentation)
#18131 gives (5) => (2).
#18536 gives (5) <=> (6) and the most part of (5) <=> (8)
Don't know how (6) and (7) are different but we do have the locality of finiteness.

[Junyan Xu]

Apparently an arbitrary localization is only formally smooth docs#Algebra.FormallySmooth.of_isLocalization, not necessarily smooth (it can even not be finite), and I don't think formally smooth implies flat in general. Anyway, flatness of localization is contained in docs#Submodule.isLocalizedModule; we just need to show some diagram commutes.

[Junyan Xu]

I have a proof now and #find_home suggests Mathlib itself, so I'll probably import Flat into Mathlib.Algebra.Module.Submodule.Localization:

import Mathlib

theorem IsLocalization.flat (R S) [CommRing R] [CommRing S] [Algebra R S]
    (M : Submonoid R) [IsLocalization M S] : Module.Flat R S :=
  (Module.Flat.iff_lTensor_injective' _ _).mpr fun I ↦ by
    have := (isLocalizedModule_iff_isLocalization' M S).mpr ‹_›
    have h := (I.isLocalizedModule S M (Algebra.ofId R S).toLinearMap).isBaseChange _ S _ -- change to Algebra.linearMap
    have : I.subtype.lTensor S = (TensorProduct.rid R S).symm.comp ((Submodule.subtype _ ∘ₗ h.equiv.toLinearMap).restrictScalars R) := by
      rw [LinearEquiv.eq_toLinearMap_symm_comp]; ext
      simp [h.equiv_tmul, Algebra.smul_def, mul_comm, Algebra.ofId_apply]
    simpa [this] using Subtype.val_injective

[Yaël Dillies]

Junyan Xu said:

The nontrivial automorphisms of R as an R-module correspond bijectively to units in R (even for noncommutative R). But I think in Kevin's post $N⊗ M=R$ is supposed to be the swap map composed with $M⊗ N = R$. And what do you mean by $N=1$ here? Is it different from $R$?

I guess I mean $R$ :sweat_smile:

[Junyan Xu]

Hmm the file doesn't have IsLocalizedModule.isBaseChange available, so the current plan is to import Algebra.Module.Submodule.Localization into RingTheory.Flat.Stability ... (changed my mind again: let me import that file into Submodule.Localization as well)
By the way I'm gonna rename Module.Flat.comp to Module.Flat.trans (cc @Christian Merten: any other such lemmas are currently named comp?).

[Junyan Xu]

Found another file: I think the name RingHom.Flat.comp is okay, but ScalarTower lemmas like Algebra.Flat.comp should be named trans. What's the reasoning for introducing Algebra.Flat when Module.Flat is already a class? And why not just make it an abbrev? There's currently no instance from Module.Flat to Algebra.Flat so Lean can't synthesize Algebra.Flat instances from Module.Flat instances. Is such separation wanted?

[Andrew Yang]

Yes I agree we don't need/want Algebra.Flat.

[Junyan Xu]

I've now solved puzzle 2, namely that #R is bounded above by #M when R is infinite. Observe that $R\cong\text{Hom}_R(M,M)$ when M is invertible. If M is finite then the RHS is finite, so M must be infinite. Since M is finitely generated over R, an R-linear map out of M is determined by its value on finitely many (say n) elements, so the right hand side has cardinality bounded by $\#M^n=\#M$.

[Junyan Xu]

New puzzle: does taking dual always preserve the cardinality of a finite projective module? By the above we know it's true for an invertible module, and for finite free modules the dual is isomorphic.

[Scott Carnahan]

Does it help that any finite projective module is a direct summand of a finite free module?

[Andrew Yang]

Junyan Xu said:

I have a proof now and #find_home suggests Mathlib itself, so I'll probably import Flat into Mathlib.Algebra.Module.Submodule.Localization:

import Mathlib

theorem IsLocalization.flat (R S) [CommRing R] [CommRing S] [Algebra R S]
    (M : Submonoid R) [IsLocalization M S] : Module.Flat R S :=
  (Module.Flat.iff_lTensor_injective' _ _).mpr fun I ↦ by
    have := (isLocalizedModule_iff_isLocalization' M S).mpr ‹_›
    have h := (I.isLocalizedModule S M (Algebra.ofId R S).toLinearMap).isBaseChange _ S _ -- change to Algebra.linearMap
    have : I.subtype.lTensor S = (TensorProduct.rid R S).symm.comp ((Submodule.subtype _ ∘ₗ h.equiv.toLinearMap).restrictScalars R) := by
      rw [LinearEquiv.eq_toLinearMap_symm_comp]; ext
      simp [h.equiv_tmul, Algebra.smul_def, mul_comm, Algebra.ofId_apply]
    simpa [this] using Subtype.val_injective

Can you PR this? Turns out I need it too :)

[Junyan Xu]

I discussed with @Judith Ludwig and she would like to formalize a proof that flatness can be checked locally (at maximal ideals) which uses this. I'll probably PR it with that proof, but if you need it earlier, feel free to PR. It will use your work in #18131 (specifically this file) (I wonder why you didn't choose to use a fixed construction of Localization/LocalizedModule existing in mathlib?), but we need that the injectivity can be checked locally (by considering the kernel, again using exactness of localization). (It would be nice to add surjectivity/bijectivity as well; your proof of puzzle 1 uses that equality of linear maps can be checked locally, which can be reduced to equalizer = ⊤.)

[Christian Merten]

Note that a group around @Yongle Hu has formalized things around locality of flatness which they plan to PR soon.

[Junyan Xu]

Scott Carnahan said:

Does it help that any finite projective module is a direct summand of a finite free module?

This can be used to show finite projective modules are reflexive (side comment: working with two linear maps that compose to id is easier than with two submodules that are complement to each other in Lean), so if you prove one direction (#M ≤ #Mⱽ or #Mᵛ ≤ #M) then the equality immediately follows, but hardly anything more that I can think about.

A new puzzle is whether the dual of a non-finite projective module could be finite. For free module the impossibility is in docs#Module.finite_dual_iff. I've generalized almost everything in this file from Free to Projective (cc @Kyle Miller), but this and docs#Module.dual_rank_eq I cannot generalize.

[Junyan Xu]

Christian Merten said:

Note that a group around Yongle Hu has formalized things around locality of flatness which they plan to PR soon.

Thanks! I found the repo https://github.com/mbkybky/module_localProperties

[Junyan Xu]

Apparently flat_of_localization was done ~ 1 month ago, and a more lengthy proof of IsLocalization.flat was added 3 weeks ago.

[Andrew Yang]

I think it’s easier and faster if you can PR the nicer proof. I’ll give you a quick review if you add the LocalizedModule version too as an instance.

[Junyan Xu]

What's the LocalizedModule version?

[Andrew Yang]

Sorry, I meant the Localization version -- the one without IsLocalization so that we can make it an instance.

[Junyan Xu]

#18683 (merged )

[Junyan Xu]

#18686 generalizes some results from Free to Projective, including Finite->FinitePresentation and Finite->Reflexive.

[Junyan Xu]

Junyan Xu said:

New puzzle: does taking dual always preserve the cardinality of a finite projective module? By the above we know it's true for an invertible module, and for finite free modules the dual is isomorphic.

I posted this on StackExchange 4 days ago and received a positive solution yesterday: https://math.stackexchange.com/questions/5017812/cardinality-of-dual-of-finite-projective-module