invertible modules are f.g.

Stream: Is there code for X?

[Kevin Buzzard]

Picard groups are really intereting.

I think this is a theorem. Do we have this in Lean?

If $R$ is a commutative ring, and $M$ and $N$ are $R$==-modules such that $N\otimes_RN\cong R$, then $M$ is finitely-generated. Furthermore $M$ is projective.

Handwavy maths proof: if $i;R\to M\otimes N$ is the iso and $i(1)=\sum_{i:F} m^in_i$ then the map from $R^F$ to $M$ defined by $(m^i)$ canonically induces a map $N^F\to M\otimes N$ which is surjective because it sends $(n_i)$ to a generator. This morphism then splits. Because the transition from the $R^F,M$ world to the $N^F,R$ world was in some sense canonical we deduce that $R^F\to M$ splits and hence $M$ is projective and finitely generated. Checking that the diagrams commute is what I would call an "exercise for the reader".

The reason this theorem is interesting is that I think it implies that you can do universe bumping. Mathematicians work in ZFC. All the prizes are for ZFC stuff. Brian Conrad told me that Fermat's Last Theorem can be proved in ZFC and I believe him, Deligne went out of his way with SGA4.5 to prove that Grothendieck's zany topos proof of the Weil conjectures could be done in ZFC, and Scholze explicitly takes time out in his etale cohomology of diamonds paper to show that his results can be formalised in ZFC. Who knows how long the resistance will last though.

I'd be really interested in seeing a Lean proof of this invertible module thing. I will see if I can make any sense of my universe-bumping assertion.

[Kevin Buzzard]

Here's what I was thinking about. You end up with two groups, one in Type (a quotient) and one in Type 1 (a much bigger quotient) but they're isomorphic by the first isomorphism theorem.

import tactic
import algebra.module
import linear_algebra.tensor_product
import ring_theory.noetherian
import algebra.category.Module.abelian
import algebra.category.Module.monoidal
import category_theory.isomorphism_classes


--open_locale tensor_product

variables (R M N : Type) [comm_ring R] [add_comm_group M] [module R M]
[add_comm_group N] [module R N]

-- sketchy proof in the chat
theorem fg_of_pseudoinvertible :
  nonempty (linear_equiv R (tensor_product R M N) R) →
  submodule.fg (⊤ : submodule R M) :=
sorry

def is_pseudoinvertible (A : Module R) : Prop :=
∃ B, nonempty (A ⊗ B ≅ 𝟙_ (Module R))

instance : has_mul (Module R) := ⟨λ A B, A ⊗ B⟩

example (A B : Module R) : Module R := A * B

local attribute [instance] category_theory.is_isomorphic_setoid

def isom_con : con (Module R) :=
{ mul' := λ A B C D hAB hCD,
  ⟨{ hom := Module.monoidal_category.tensor_hom
    (category_theory.iso.hom (@classical.choice (A ≅ B) hAB))
    (category_theory.iso.hom (@classical.choice (C ≅ D) hCD)),
  inv := Module.monoidal_category.tensor_hom
    (category_theory.iso.inv (@classical.choice (A ≅ B) hAB))
    (category_theory.iso.inv (@classical.choice (C ≅ D) hCD)),
  -- left as an exercise for the reader
  hom_inv_id' := sorry,
  inv_hom_id' := sorry }⟩,
 ..(category_theory.is_isomorphic_setoid (Module R))
}

example : has_mul $ (isom_con R).quotient :=
-- (category_theory.is_isomorphic_setoid (Module R)) :=
by apply_instance

def Isom_classes := (isom_con R).quotient

instance : has_mul (Isom_classes R) := by unfold Isom_classes; apply_instance

instance : has_one (Isom_classes R) := ⟨⟦𝟙_ (Module R)⟧⟩

-- possibly all tricky theorems in category theory
instance Picard_Monoid : monoid (Isom_classes R) :=
{ mul := (*),
  mul_assoc := sorry,
  one := 1,
  one_mul := sorry,
  mul_one := sorry }

def Picard_Group := units (Isom_classes R)
#check Picard_Group ℚ -- Type 1!!

-- set of quotients of R^n
structure finitely_generated_module (R : Type) [comm_ring R] :=
(n : ℕ)
(quotient_by_me : submodule R ((fin n) → R))

#check finitely_generated_module R -- still in Type!

-- surjects onto the pseudoinvertible ones
def forget : finitely_generated_module R → Module R :=
λ nQ, Module.of R nQ.quotient_by_me.quotient

def fgmod_equiv (L M : finitely_generated_module R) : Prop
:= nonempty (L.quotient_by_me.quotient ≅
M.quotient_by_me.quotient)

def Picard_Group2 := quot (fgmod_equiv R)

#check Picard_Group2 -- still in Type

-- now define the forgetful morphism from this category
-- to Module R, observe that is maximally well-behaved
-- with respect to isomorphisms and hence gives us
-- a map from the quotient of `finitely_generated_module R`
-- by the isomorphism equivalence relation to the Picard Group.
-- It's a surjection by the ring theory theorem, so
-- by the first isomorphism theorem we have an isomorphism
-- between a Picard Group in Type (invertible fractional ideals
-- modulo principal ones) to a Picard Group in Type 1 (iso
-- classes of invertible modules). We want the one in Type
-- because its existence is a stronger statement but note
-- that we will have to make the Type 1 quotient property
-- even though there is a lot of AC about here