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

[Kenny Lau]

@Junyan Xu how much of this thread made it into mathlib and how much are in PR?

[Junyan Xu]

Everything done so far is basically contained in #21776 (a draft PR). I'll try to do some cleanup and extract some reviewable bits to a PR tonight.

[Kenny Lau]

@Junyan Xu i just had a quick read of that file, i'm not sure if i understand correctly, it seems like the universe issue hasn't been solved yet?

[Junyan Xu]

What universe issue do you have in mind? Do you want a definition of the Picard group that lies in the same universe as the ring?

[Kenny Lau]

@Junyan Xu yes

[Junyan Xu]

It wouldn't be hard to make such a definition, with the benefit of avoiding category theory in the file.

[Kenny Lau]

I'll try to cook up something locally with a bunch of sorrys and with your definitions in mind

[Kenny Lau]

why do i get strange error when i try to checkout your branch

[Kenny Lau]

✖ [30/1984] Building Mathlib.Data.Nat.BinaryRec

BinaryRec.lean:6:0
object file '.\.\.lake/packages\Cli\.lake\build\lib\Lean\Elab\Command.olean' of module Lean.Elab.Command does not exist

[Junyan Xu]

Not sure; it's an old branch so shouldn't be affected by #general > Cache acting weird @ 💬 ? Cleaning the .lake directory would be a first attempt.
I can open the PicardGroup file in Gitpod, by the way.

[Damiano Testa]

There is a weird "slash" between .lake and packages, unlike the others in the path.

[Kenny Lau]

@Junyan Xu ok i made this with a ton of sorrys. If you are happy with this infrastructure, I'll go on and prove more of the sorrys:

import Mathlib

open Classical TensorProduct

namespace Module

variable (R : Type u) (M : Type v) (N P Q : Type*) [CommRing R]
variable [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [AddCommGroup Q]
variable [Module R M] [Module R N] [Module R P] [Module R Q]

class Invertible : Prop where
  bijective : Function.Bijective (lift <| dualPairing R M)

instance invertible_tensor [Invertible R M] [Invertible R N] :
    Invertible R (M ⊗[R] N) :=
  sorry

theorem exists_iso_of_invertible [Invertible R M] :
    ∃ (n : ℕ) (M₀ : Submodule R (Fin n → R)), Nonempty ((_ ⧸ M₀) ≃ₗ[R] M) :=
  sorry

theorem invertible_of_iso [Invertible R M] (e : M ≃ₗ[R] N) : Invertible R N :=
  sorry

structure Pic.Carrier : Type u where
  (n : ℕ)
  (S : Submodule R (Fin n → R))
  (invertible : Invertible R (_ ⧸ S))

instance Pic.carrier_invertible (C : Pic.Carrier R) : Invertible R (_ ⧸ C.S) :=
  C.invertible

instance Pic.setoid : Setoid (Pic.Carrier R) where
  r C₁ C₂ := Nonempty ((_ ⧸ C₁.S) ≃ₗ[R] (_ ⧸ C₂.S))
  iseqv := ⟨fun _ ↦ ⟨1⟩, fun ⟨i⟩ ↦ ⟨i.symm⟩, fun ⟨i₁⟩ ⟨i₂⟩ ↦ ⟨i₁.trans i₂⟩⟩

def Pic : Type u :=
  Quotient (Pic.setoid R)

variable {R} in
@[coe] noncomputable def Pic.repr (x : Pic R) : Type u :=
  _ ⧸ x.out.S

-- It prints as ↑x but I can't type it myself.
noncomputable instance (x : Pic R) : AddCommGroup x.repr := by
  unfold Pic.repr; exact inferInstance

noncomputable instance (x : Pic R) : Module R x.repr := by
  unfold Pic.repr; exact inferInstance

instance : One (Pic R) where
  one := ⟦⟨1, ⊥, sorry⟩⟧

/-- The element of `Pic R` that corresponds to the given invertible `R`-module `M`. -/
noncomputable def Pic.of_invertible [Invertible R M] : Pic R :=
  have := exists_iso_of_invertible R M;
  ⟦⟨choose this, choose (choose_spec this),
    let ⟨e⟩ := choose_spec (choose_spec this);
    invertible_of_iso R _ _ e.symm⟩⟧

noncomputable def Pic.iso_of_invertible [Invertible R M] : (of_invertible R M).repr ≃ₗ[R] M :=
  sorry

/-- Can be made "computable" in a future PR. -/
private noncomputable def Pic.mul : Pic R → Pic R → Pic R :=
  Quotient.lift₂ (fun C₁ C₂ ↦ Pic.of_invertible R ((_ ⧸ C₁.S) ⊗[R] (_ ⧸ (C₂.S))))
    (fun _ _ _ _ ⟨e₁⟩ ⟨e₂⟩ ↦ Quotient.sound ⟨sorry⟩)

noncomputable instance : Mul (Pic R) where
  mul := Pic.mul R

noncomputable instance : CommGroup (Pic R) where
  inv := sorry
  zpow := sorry -- TensorPower
  mul_assoc := sorry
  mul_one := sorry
  one_mul := sorry
  mul_comm := sorry
  inv_mul_cancel := sorry
  zpow_zero' := sorry
  zpow_succ' := sorry
  zpow_neg' := sorry

end Module

[Kenny Lau]

@Junyan Xu i feel like there's one "intermediate" step we can extract; as I was reading your PR I saw you talk about how this can be generalised to finitely generated modules, and I think this might indeed be a useful middle step. We can build a small category (still "computable") that is equivalent to the full subcategory of finitely generated R-modules

[Kenny Lau]

and then... actually and then I would need less infrastructure here, because then we can use the same skeleton trick you initially used

[Kenny Lau]

I think this is actually worth doing; what do you think?

[Andrew Yang]

We do have docs#FGModuleCat. I claim we just show that it is docs#CategoryTheory.EssentiallySmall and it should be enough.

[Kenny Lau]

@Andrew Yang thanks for the helpful pointer; we still need to explicitly construct the category, right?

[Andrew Yang]

I think we in general don't care that the category lives in a larger category and we would rather have it being a large category for defeq reasons. And for the group itself you could do docs#Shrink

[Kenny Lau]

that is once again very useful!

[Kenny Lau]

@Andrew Yang what is the precise roadmap you have in mind, if you have one?

[Kenny Lau]

just to make sure that i'm following the most efficient path

[Kenny Lau]

Andrew Yang said:

I think we in general don't care that the category lives in a larger category

I'm a bit lost here; what are you referring to?

[Kenny Lau]

I was saying that to use CategoryTheory.EssentiallySmall, we still need to construct the SmallCategory explicitly

[Andrew Yang]

Oh I thought you want to replace FGModuleCat with a small category of representations.
Yes you are right then. Another option is to use docs#CategoryTheory.essentiallySmall_iff but I think both approaches are probably identical in terms of difficulty in lean.

[Kenny Lau]

I now came up with a second intermediate step (R : Type u)

1. ModuleCat R : Type u+1
2. FGModuleCat R : Type u+1
3. FGModuleRepr R : Type u (new construction)
4. FGModuleRepr R ≌ FGModuleCat (I think having this explicit isomorphism basically sidesteps the destructive CategoryTheory.EssentiallySmall, which seems to be a technically weaker version?)
5. InvertibleRepr R : Type u (the new step; this is mathematically a groupoid and is technically computable)
6. Then we can just use the skeleton of 5

[Kenny Lau]

@Andrew Yang does this make sense?

[Kenny Lau]

The philosophy here seems to be that in Category Theory, the bad step is "taking the skeleton", and as long as we don't do that, everything will still be technically computable (hmm maybe except the inverse?), so we should delay the bad step and postpone it to the end as much as possible?

[Andrew Yang]

I personally prefer if we do things under the docs#CategoryTheory.essentiallySmall framework. I don't think they are "computable" in any useful way except that lean doesn't force you to slap on noncomputable

[Kenny Lau]

@Andrew Yang I agree with that; but do you think maybe we should change SmallModel to be non-canonical (so that we can use the "essentiallySmall framework" with my customly defined representative)? This is like how we switched from a canonical model of localisation of a ring to docs#IsLocalization ; do you see any bad outcomes this might lead to?

[Kenny Lau]

actually upon further thought even my "equivalence" is noncomputable (only one direction is computable)

[Andrew Yang]

I don't think this is necessary. If we have two categories that we both care about and they are isomorphic we use the Equivalence framework. EssentiallySmall is for when you know there is a small model but you don't care about what the model actually is (which is exactly the situation here).

[Kenny Lau]

made #25249 to prove that cat. of f.g. module is ess. small

[Kenny Lau]

@Andrew Yang @Junyan Xu

[Kenny Lau]

i just had the terrifying realisation that even though it makes sense for R : Type u ring to have a M : Type v module, ModuleCat.{v} R does not form a monoid when v < u

[Andrew Yang]

I wonder what is endomorphism ring of 𝟭 _ : ModuleCat.{v} R ⥤ ModuleCat.{v} R is if R is large.

[Kevin Buzzard]

Toy example: $R=\Z[X_i]$ the where the $X_i$ are indexed by J : Type 1 (and J is not 0-small i.e. really not a Type). Then a term of type ModuleCat.{0} R is I think an additive abelian group in Type equipped with commuting endomorphisms indexed by J so it's easy to write down examples. Seems to me that the endomorphism ring might just be R again?

[Kevin Buzzard]

I guess the point is here that the intersection of the kernels of all the ring homomorphisms from R to S : Type is trivial. On the other hand if R is a field in Type 1 whose underlying type is genuinely big to descend to Type (e.g. the field of fractions of the previous R) then ModuleCat.{0} R is I think just {0} so now the endomorphisms are tiny.

Maybe in general there's some concept of "largest u-quotient of R which is v-small"?

[Kenny Lau]

it's not just a quotient, the point here is that we can build R up from smaller parts, which is one of the key differences between the two cases

[Kenny Lau]

on the topic of Picard group, I think it's safe to always assume that the invertible module lives in Type max u v?

[Kevin Buzzard]

I think it's safe to assume that both the ring and the module live in Type for all concievable applications :-)

[Kevin Buzzard]

I think that the fact that Lean has universes just makes us philosophise about universes but it's not clear that we ever actually need them for anything other than keeping track of whether we are a set or a class.

[Kenny Lau]

Kevin Buzzard said:

I think it's safe to assume that both the ring and the module live in Type for all concievable applications :-)

i've heard that condensed sets use universes

[Junyan Xu]

The Picard group shouldn't have any universe parameter other than the ring's. The definition of invertible module we are using is universe agnostic as it doesn't use category theory.
P.S. if you haven't seen it it has been shown above that an invertible module always has the same cardinality as the ring.

[Kenny Lau]

@Junyan Xu yes, the Picard group of R : Type u lives in Type u in my file. What I'm referring to is the operation of taking an invertible module : Type ?? and outputing the corresponding element of Pic R

[Kenny Lau]

it's this ?? that is the problem, that i'm proposing should be max u v

[Junyan Xu]

With my original definition of Pic this operation is implemented here and ?? can be arbitrary. It uses a representative in Type u obtained as a quotient of some Fin _ → R.

[Kenny Lau]

that is indeed simpler; i just wanted to use the structures available but i suppose there is no need for that

[Kenny Lau]

import Mathlib

open TensorProduct CategoryTheory

namespace Module

variable (R : Type u) (M N P Q: Type*) [CommRing R]
variable [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [AddCommGroup Q]
variable [Module R M] [Module R N] [Module R P] [Module R Q]

class Invertible : Prop where
  bijective : Function.Bijective (lift <| dualPairing R M)

namespace Invertible

variable [Invertible R M]

instance finite : Module.Finite R M :=
  sorry

instance dual : Invertible R (Dual R M) :=
  sorry

instance tensor [Invertible R N] : Invertible R (M ⊗[R] N) :=
  sorry

theorem of_iso (e : M ≃ₗ[R] N) : Invertible R N :=
  sorry

protected abbrev repr : Type u :=
  FGModuleRepr.ofFinite R M

noncomputable def reprEquiv : Invertible.repr R M ≃ₗ[R] M :=
  Classical.choice (Finite.exists_fin_quot_equiv R M).choose_spec.choose_spec

instance : Module.Invertible R (Invertible.repr R M) :=
  of_iso R _ _ <| (reprEquiv R M).symm

end Invertible

-- generalise for SmallModel?
noncomputable instance : MonoidalCategory (SmallModel.{u} <| FGModuleCat.{u} R) :=
  Monoidal.transport <| equivSmallModel _

noncomputable instance : BraidedCategory (SmallModel.{u} <| FGModuleCat.{u} R) where
  braiding M N := (equivSmallModel _).functor.mapIso (β_ _ _)
  braiding_naturality_right := sorry
  braiding_naturality_left := sorry
  hexagon_forward := sorry
  hexagon_reverse := sorry

instance : CoeSort (SmallModel <| FGModuleCat R) (Type u) :=
  ⟨fun x ↦ (equivSmallModel <| FGModuleCat R).inverse.obj x⟩

def Pic : Type u :=
  (Skeleton <| SmallModel <| FGModuleCat.{u} R)ˣ

namespace Pic

variable {R} in
@[coe] def repr (x : Pic R) : Type u :=
  x.val

instance : CoeSort (Pic R) (Type u) :=
  ⟨Pic.repr⟩

-- It prints as ↑x but I can't type it myself.
noncomputable instance (x : Pic R) : AddCommGroup x := by
  unfold Pic.repr; infer_instance

noncomputable instance (x : Pic R) : Module R x := by
  unfold Pic.repr; infer_instance

noncomputable instance : CommGroup (Pic R) := by
  unfold Pic; infer_instance

-- set_option pp.universes true
/-- The element of `Pic R` that corresponds to the given invertible `R`-module `M`. -/
noncomputable def of_invertible [Invertible R M] : Pic R :=
  ⟨toSkeleton <| (equivSmallModel _).functor.obj <| .of R <| Invertible.repr R M,
    toSkeleton <| (equivSmallModel _).functor.obj <| .of R <| Dual R <| Invertible.repr R M,
    sorry,
    sorry⟩

noncomputable def iso_of_invertible [Invertible R M] : of_invertible R M ≃ₗ[R] M :=
  (FGModuleCat.isoToLinearEquiv <| ((equivSmallModel (FGModuleCat.{u} R)).inverse.mapIso
    (preCounitIso <| (equivSmallModel _).functor.obj <| FGModuleCat.of R <|
      Invertible.repr R M)).trans
    ((equivSmallModel _).unitIso.app _).symm).trans
  (Invertible.reprEquiv R M)

end Pic

end Module

[Kenny Lau]

@Junyan Xu I've updated my sorry-filled skeleton based on the PR #25249 which proves that FGModuleCat.{v} is essentially small

[Kenny Lau]

Please let me know your thoughts

[Junyan Xu]

The design looks solid to me. For CategoryTheory.Skeleton.instMonoid you only need MonoidalCategory though, so BraidedCategory is probably stronger than what you need.

[Kenny Lau]

@Junyan Xu monoid <=> group; braided <=> commgroup

[Kenny Lau]

i mean i guess i could also prove the commgroup directly

[Junyan Xu]

I see, CategoryTheory.Skeleton.instCommMonoid is the relevant instance

[Andrew Yang]

instance (C : Type u) [Category.{v} C] [EssentiallySmall.{w} C] : Small.{w} (Skeleton C) :=
  ((essentiallySmall_iff C).mp ‹_›).1

def Pic : Type u := (Shrink <| Skeleton <| FGModuleCat.{u} R)ˣ

You should just do this (or shrink outside of Units)

[Junyan Xu]

Why not just Shrink (Skeleton <| ModuleCat.{u} R)ˣ then

[Andrew Yang]

Because we don't have the instance [Small M] : Small Mˣ (yet)

[Junyan Xu]

Skeleton <| ModuleCat.{u} R is not small, but its group of units is.

[Andrew Yang]

Oh you mean removing FG. Yeah sure (though you need some more instances).

[Junyan Xu]

Not sure about that ... I'd prove Small.{u} (Skeleton <| ModuleCat.{u} R)ˣ by constructing a surjective function from Σ n, Submodule (Fin n → R).

[Kenny Lau]

Small.{u} (Skeleton <| ModuleCat.{u} R) is not true

[Kenny Lau]

unless R is trivial

[Andrew Yang]

(and I though you (Junyan) just said that some lines above)

[Junyan Xu]

Forgot to add the ˣ; corrected

[Kenny Lau]

i see, with that edit it's certainly an interesting approach

[Kenny Lau]

but ultimately i think the philosophy is that the definition doesn't really matter as long as you have the API right

[Junyan Xu]

Yeah, working with Pic in Type (u+1) is also feasible if the library is sufficiently universe polymorphic ... but maybe we want it in Type u for philosophical rather than practical reasons.

[Kenny Lau]

i definitely want Pic R to be in Type u

[Kenny Lau]

and i'm sure Kevin Buzzard can give you more good reasons XD

[Junyan Xu]

I think if you want a construction that doesn't mention Type (u + 1), you probably want to define FGModuleCat using Σ n, Submodule (Fin n → R) rather than just prove a Small.{u} instance. With such a definition then what @Mario Carneiro said here probably works: "count up the Type levels directly used in the proof and you will get a number like 4 or something and this can indeed be used to prove that you can establish the theorem using 4 universes", e.g. you may be able to mechanically translate proofs into ZFC if u = 0. With this half-baked Shrink approach I think you're not really achieving much.

[Andrew Yang]

Unfortunately the category theory library isn't really universe polymorphic enough. In particular we probably want Pic and other cohomology groups to live in the same universe.

[Kevin Buzzard]

Etale cohomology is another example where if we follow our nose we'll have $H^{42}_{et}(\mathbb{P}^{2025}_{\mathbb{C}},\Z/37\Z)$ in Type 1. This will certainly get the set theorists excited because it means we're using universes, and in fact here's something I'm not clear about: we could use the standard techniques of restricting what we take a limit over to get it back down to Type, or we could just prove it's finite and deduce it descends to Type as a consequence :-) I wonder whether the latter approach is "using universes"?

[Joël Riou]

The étale cohomology of any X : Scheme.{0} is going to be in Type 0. The reason is that even though the category AbÉtaleSheaf X of étale abelian sheaves (with values in abelian groups in Type 0) has hom types in Type 1, these hom sets are small (morphisms of étale sheaves are determined by their values on a suitable small family of étale schemes over X), and we shall show that it satisfies IsGrothendieckAbelian.{0} (AbÉtaleSheaf X) (all of this is related to the very draft PR #19462). Then, the Ext groups in AbÉtaleSheaf X shall be in Type 0. (In a more remote future, all the hom types in DerivedCategory (AbÉtaleSheaf X) can be made to be in Type 0.) There is no reason to worry about this.

[Kevin Buzzard]

The étale cohomology of any X : Scheme.{0} is going to be in Type 0.

But will it be in Type 1 first? :-)

[Joël Riou]

The end user will see Ext F G n : Type 0.

[Kevin Buzzard]

This is a very clever trick!

[Kenny Lau]

@Junyan Xu again, many thanks for making #25337 ; I do have an API question: should we split this into Pic and IsPic, just like how we split localization into Localization and IsLocalization? More concretely, this would allow us to supply custom "models" of the Picard group, say (ok this is the wrong thing because it's not affine) in the future, where P^1 would have a model of the Picard group using Int?

[Junyan Xu]

We can construct an isomorphism between Pic P^1 and Multiplicative Int, but I don't see the point of having a IsPic class. If we add IsPic do we also want IsGaloisGroup, IsCohomologyGroup, IsKGroup etc.?

[Andrew Yang]

(we actually want IsGaloisGroup)
But I agree that we don’t want IsPic

[Junyan Xu]

we actually want IsGaloisGroup

I'd like to hear about the use case(s) and design proposal(s)

[Kenny Lau]

Junyan Xu said:

We can construct an isomorphism between Pic P^1 and Multiplicative Int, but I don't see the point of having a IsPic class. If we add IsPic do we also want IsGaloisGroup, IsCohomologyGroup, IsKGroup etc.?

on second thought, I guess we can just have 𝒪 : ℤ → Pic (P^1) lol

[Kenny Lau]

it would indeed be mathematically valid :melt:

[Thomas Browning]

One option would be to have IsGaloisGroup build off of docs#Algebra.IsInvariant

[Junyan Xu]

#30736 shows that the Picard group of a domain is isomorphic to the class group, as a consequence of the exact sequence 1 → Rˣ → Aˣ → (Submodule R A)ˣ → Pic R → Pic A (assuming R → A is injective) due to Roberts and Singh (1993), which appears as an exercise in Weibel's K-book. For A := FractionRing R, (Submodule R A)ˣ consists of the invertible fractional ideals, the image of Aˣ consists of the principal fractional ideals, so the quotient, ClassGroup R, is isomorphic to the relative Picard group Pic(A/R), the kernel of the last map, and since Pic A is trivial, the kernel is the whole group Pic R.

[Junyan Xu]

#30837 proves that any Noetherian total ring of fractions is semilocal, as a step towards showing invertible modules over Noetherian (comm.) rings are isomorphic to ideals (see my answer on MO). The argument is due to Gemini, and Grok can independently reproduce. Has any one seen this fact before? I'm surprised such a simple fact isn't more widely known. If the ring is moreover reduced, then it's more well known that it must be Artinian, therefore semilocal.

[Junyan Xu]

Reading Lemma 4.1 in this paper I realized that puzzle 1 (swapping the two factors in $M\otimes_R M$ equals identity for invertible $M$) is the crucial input to show the (Nat- or Int-graded) tensor algebra $\bigoplus_n M^{\otimes n}$ is commutative (it "is" the symmetric algebra). The Int-graded algebra is apparently associated to notions like $\mathbb{G}_\mathrm{m}$-bundle or torsor associated to $M$, and base changing to it trivializes $M$.

[Kenny Lau]

@Junyan Xu I recall that we already have the result that Hom(M⊗M1,M⊗M2) = Hom(M1,M2) or something like that, or at least we do know that Hom(M⊗M,M⊗M) = Hom(M,M) = Hom(R,R) = R, i.e. we know that every linear map is a scalar multiplication, and the only scalar that makes sense is 1

[Junyan Xu]

Yeah, we further know the scalar is a unit of order 2, see my comment about the natural transformation from Pic to $\mu_2$ at the very top of the thread #maths > Puzzles around Picard group @ 💬. I've now solved puzzle 1 following Andrew's proof in #31308 (for rings, not semirings for now). There's an MO question asking for an explanation why this NatTrans is trivial: https://mathoverflow.net/questions/38759/why-is-the-symmetric-monoidal-structure-on-invertible-modules-strict (I guess if the brading were -1 we'd get a superalgebra ...)

[Junyan Xu]

The simplest way I can think of to construct $A:=\bigoplus_{n\in\mathbb{Z}}M^{\otimes n}$ is to take the docs#TensorAlgebra of $M$ and $M^\vee$, tensor them together, then quotient out by the congruence identifying $\varphi\otimes m$ with $\varphi(m)$ for $f\in M$. Not sure how difficult it would be to show $A\otimes_R M\cong_A A$ and $A\otimes_R A\cong_A A[X,X^{-1}]$ (i.e. LaurentPolynomial A) ... (btw mathlib doesn't have LaurentPolynomial is localization of Polynomial, though it has the analogue for PowerSeries)