Zulip Chat Archive

Stream: Is there code for X?

Topic: Projective R-modules.


view this post on Zulip Kevin Buzzard (Mar 16 2021 at 08:52):

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?

view this post on Zulip Eric Wieser (Mar 16 2021 at 09:00):

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

view this post on Zulip Eric Wieser (Mar 16 2021 at 09:03):

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

view this post on Zulip Kenny Lau (Mar 16 2021 at 09:10):

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

view this post on Zulip Scott Morrison (Mar 16 2021 at 09:35):

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

view this post on Zulip Scott Morrison (Mar 16 2021 at 09:38):

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

view this post on Zulip Scott Morrison (Mar 16 2021 at 09:39):

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

view this post on Zulip Scott Morrison (Mar 16 2021 at 09:41):

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

view this post on Zulip Yury G. Kudryashov (Mar 16 2021 at 17:08):

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

view this post on Zulip Julian Külshammer (Mar 16 2021 at 17:20):

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

view this post on Zulip Adam Topaz (Mar 16 2021 at 17:29):

What's the analogue of this for injective semimodules?

view this post on Zulip Julian Külshammer (Mar 16 2021 at 17:29):

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'.

view this post on Zulip Yury G. Kudryashov (Mar 16 2021 at 22:30):

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

view this post on Zulip Julian Külshammer (Mar 16 2021 at 22:38):

Thanks.

view this post on Zulip Markus Himmel (Mar 17 2021 at 07:36):

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.

view this post on Zulip Scott Morrison (Mar 17 2021 at 09:11):

:fingers_crossed:

view this post on Zulip Kevin Buzzard (Mar 17 2021 at 10:08):

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).

view this post on Zulip Scott Morrison (Mar 17 2021 at 10:42):

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.

view this post on Zulip Kevin Buzzard (Mar 17 2021 at 10:48):

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.

view this post on Zulip Kevin Buzzard (Mar 17 2021 at 10:50):

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".

view this post on Zulip Johan Commelin (Mar 17 2021 at 10:51):

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

view this post on Zulip Johan Commelin (Mar 17 2021 at 10:52):

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

view this post on Zulip Kevin Buzzard (Mar 17 2021 at 10:52):

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

view this post on Zulip Kevin Buzzard (Mar 17 2021 at 10:57):

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.

view this post on Zulip Kevin Buzzard (Mar 17 2021 at 11:08):

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

view this post on Zulip Scott Morrison (Mar 17 2021 at 11:19):

(deleted)

view this post on Zulip Scott Morrison (Mar 17 2021 at 11:19):

(deleted)

view this post on Zulip Scott Morrison (Mar 17 2021 at 11:20):

(deleted)

view this post on Zulip Scott Morrison (Mar 17 2021 at 11:20):

oh, this is all garbage, sorry

view this post on Zulip Scott Morrison (Mar 17 2021 at 11:22):

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....

view this post on Zulip Scott Morrison (Mar 17 2021 at 11:26):

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

view this post on Zulip Scott Morrison (Mar 17 2021 at 11:27):

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.

view this post on Zulip Johan Commelin (Mar 17 2021 at 11:58):

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

view this post on Zulip Johan Commelin (Mar 17 2021 at 12:00):

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

view this post on Zulip Kevin Buzzard (Mar 17 2021 at 12:05):

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

view this post on Zulip Kevin Buzzard (Mar 17 2021 at 12:25):

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".

view this post on Zulip Kevin Buzzard (Mar 17 2021 at 12:26):

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

view this post on Zulip Johan Commelin (Mar 17 2021 at 12:28):

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.

view this post on Zulip Johan Commelin (Mar 17 2021 at 12:38):

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

view this post on Zulip Kevin Buzzard (Mar 17 2021 at 12:42):

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

view this post on Zulip Kevin Buzzard (Mar 17 2021 at 13:38):

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

view this post on Zulip Scott Morrison (Mar 17 2021 at 22:42):

@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.

view this post on Zulip Scott Morrison (Mar 17 2021 at 22:45):

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

view this post on Zulip Markus Himmel (Mar 17 2021 at 23:19):

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


Last updated: May 07 2021 at 22:14 UTC