Projective R-modules.

Stream: Is there code for X?

[Kevin Buzzard]

Am I right in thinking that we don't have the predicate that an R-module (R a ring) is projective? This works really nicely as a definition:

import linear_algebra.basic

universe u

def is_projective
  (R : Type u) [ring R] (M : Type u) [add_comm_group M] [module R M] : Prop :=
∃ s : M →ₗ[R] (M →₀ R), ∀ m, (s m).sum (λ m r, r • m) = m

I've managed to prove it's equivalent to the universal property (maps from M lift along surjections) (I was lazy with universes as you can see, but this is still the right definition I think even in a more universe-polymorphic setting). Mathematically the definition says that the obvious R-linear map from (free R-module on M) to M splits, and what's nice about it is that it doesn't quantify over any other types.

Now I'm going to show my ignorance of mathlib: where does this definition go? Is this the kind of predicate one wants on R-modules? My guess is yes. Or should this go in some category file dealing with R-modules where I then prove some statement about lifting epimorphisms in the category of R-modules? Should I be proving the universal property as an "explicit" statement about lifting along surjections or as some kind of category theoretical statement about projective objects in categories?

[Eric Wieser]

It doesn't answer any of your questions, but your sum expression looks like it would have API somewhere in linear_algebra, and reminds me a little of docs#finsupp.total

[Eric Wieser]

finsupp.total M M R id (s m) = m I guess

[Kenny Lau]

I think this should go to a new folder about homological algebra

[Scott Morrison]

@Kevin Buzzard, I think my answer to your main question is "both".

[Scott Morrison]

I mean, there should be a file projective_object (perhaps under category_theory/abelian) giving the general definition in any category,

[Scott Morrison]

and then in algebra/category/Module/??? there should be the lemma that this agrees with your characterisation when in the category of R-modules.

[Scott Morrison]

and your characterisation above should be in algebra/module/projective.lean

[Yury G. Kudryashov]

(and probably should use different universes for R and M)

[Julian Külshammer]

Apparently, this "dual basis lemna" also holds for semimodules: https://www.google.com/url?sa=t&source=web&rct=j&url=https://www.anubih.ba/Journals/vol-1,no-2,y05/03revdeore.pdf&ved=2ahUKEwirvOCaqLXvAhVHmYsKHUclDh4QFjADegQICRAC&usg=AOvVaw3kkdmXsDcjIB1-z070daQY

[Adam Topaz]

What's the analogue of this for injective semimodules?

[Julian Külshammer]

I wonder whether the following equivalent characterization is helpful: A (right) module $P$ is projective if and only if $P \otimes_R Hom(P, R) \to End(P), p \otimes f\mapsto (q \mapsto p f(q))$ is an isomorphism. One disadvantage at the moment is that there are no bimodules yet and tensor products are only defined for commutative rings. I don't know whether it is an advantage that you don't need to talk about 'elements'.

[Yury G. Kudryashov]

It seems that Zulip uses double dollars for math: e.g., $P \otimes_R Hom(P, R) \to End(P)$.

[Julian Külshammer]

Thanks.

[Markus Himmel]

Scott Morrison said:

I mean, there should be a file projective_object (perhaps under category_theory/abelian) giving the general definition in any category,

I got started on this last year (see here and here). I then tried to prove that in a category with enough projectives every object has a projective resolution, but the then-current definition of chain complex in mathlib made this very difficult (and then Part III happened and I didn't have time to work on it). Hopefully the improved chain complexes from LTE will make this less painful.

[Scott Morrison]

:fingers_crossed:

[Kevin Buzzard]

I'm engaging with chain complexes in LTE but right now I'm still doing the groundwork (if V has equalisers then so does complexes over V etc).

[Scott Morrison]

Kevin Buzzard said:

I'm engaging with chain complexes in LTE but right now I'm still doing the groundwork (if V has equalisers then so does complexes over V etc).

Oh, that sounds fun. Can I help with something there? I need something to play with to try out the new chain complex design.

[Kevin Buzzard]

Feel free to play with the mess in the file src/system_of_complexes/complex.lean in the branch ses_to_les. Because I am trying to set things up for general categories rather than just R-modules I am forced to use the category theory library. We have these "lawless complexes" -- a new differential_object I V definition (which clashes with mathlib I think? I'm using the local one) and in order to state that exact sequences make sense I need to prove that if V has zero morphisms, equalizers and images then so does differential_object I V. My proof for equalizers is timing out and I'm stuck on the proof for images :-) Bhavik helpfully suggested that I also assume has_image_maps which definitely helped.

[Kevin Buzzard]

Mathematically here is the sort of thing which is going on. A term of type differential_object I V is a map I -> V (the objects, indexed by I) and then d i j : X_i -> X_j for all i,j. Morphisms have to preserve d, so e.g. you can make a "single object" X_j in one degree with 0's everywhere, but if you have a lawless complex Y and a map X_j -> Y_j then you might not get a map (single X_i) -> Y_j because d j j might not be zero on Y_j. This is a mild stumbling block in the way of "proving things for the product by deducing them from the factors".

[Johan Commelin]

Note that Kevin wrote a fair amount of docs on that ses_to_les branch

[Johan Commelin]

Maybe they should be backported to master, because they are independent of any other experiments.

[Kevin Buzzard]

They are a bit incoherent, they are more like notes. But I can definitely expand them into docs

[Kevin Buzzard]

Once the sorried instances are there (V has images -> lawless complex I V has images, and same for equalizers) one can then say that if V is an abelian category then there is a notion of short exact sequence for the complexes. The reason this is so slow-going is that instead of just "cheating" and using some concrete category I'm following Markus' example -- he defined exact sequences for any category with zero morphisms, images and equalizers, so I have defined short exact sequences in the same generality.

[Kevin Buzzard]

Oh and the reason has_image_maps comes into things is that if you are trying to factor f:X -> Y (a morphism of complexes) through a monic, and you can factor each f_i:X_i -> Y_i, and if I_i is the image of f_i, then you need to come up with d maps which commute with everything in order to make the I_i into an object of the complex category, so you need a machine which maps images to images, and it's has_image_maps

[Scott Morrison]

(deleted)

[Scott Morrison]

(deleted)

[Scott Morrison]

(deleted)

[Scott Morrison]

oh, this is all garbage, sorry

[Scott Morrison]

I think I am still very confused by this lawless chain complex business, and don't understand at what point we're going to restrict to something equivalent to the real definition....

[Scott Morrison]

and I don't quite understand why we're trying to construct has_equalizers and similar things on differential_object.

[Scott Morrison]

Once we pass to the subcategory that actually models chain complexes, we'll lose the has_equalizers instance, and I don't really understand why we expect it to be any less work to reconstruct than to build it on the subcategory in the first place.

[Johan Commelin]

This is something that I don't have a good feeling for yet.

[Johan Commelin]

The transition between complex_like and differential_object is not completely transparent. E.g., lifting the shift functor was more work than I hoped.

[Kevin Buzzard]

Oh I had just assumed that putting all the structure on the differential object was the "natural next step".

[Kevin Buzzard]

I should perhaps add that I am still not at all sold on this bool parameter. Perhaps we should just have a predicate on I x I saying "this one can be nonzero".

[Kevin Buzzard]

so for a succ_str you get maps from X(i) to X(j) iff either r i j or r j i depending on what your convention is

[Johan Commelin]

If we want to use this also for modeling double complexes, then we should also have a predicate on $\iota \times \iota \times \iota$ saying which compositions should be zero.

[Johan Commelin]

But I'm not sure if we should want to reuse this for double complexes

[Kevin Buzzard]

How about this: a double complex is two commuting d's both satisfying d^2=0

[Kevin Buzzard]

I'm moving to #maths to continue the discussion about long exact sequences.

[Scott Morrison]

@Markus Himmel, could we PR the stuff from your branch#projective outside of the work in src/algebra/homology/? I agree that we should use projective resolutions as yet another test case for good chain complex designs, but that is going to be easier if we have the uncontroversial parts of this branch already in mathlib.

[Scott Morrison]

(I can also try this sometime if you're busy with other things.)

[Markus Himmel]

I probably won't get around to making a PR soon, so feel free to have a go