# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Projective R-modules.

#### 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?

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

#### Eric Wieser (Mar 16 2021 at 09:03):

`finsupp.total M M R id (s m) = m`

I guess

#### Kenny Lau (Mar 16 2021 at 09:10):

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

#### Scott Morrison (Mar 16 2021 at 09:35):

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

#### 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,

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

#### Scott Morrison (Mar 16 2021 at 09:41):

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

#### Yury G. Kudryashov (Mar 16 2021 at 17:08):

(and probably should use different universes for `R`

and `M`

)

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

#### Adam Topaz (Mar 16 2021 at 17:29):

What's the analogue of this for injective semimodules?

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

#### Yury G. Kudryashov (Mar 16 2021 at 22:30):

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

#### Julian Külshammer (Mar 16 2021 at 22:38):

Thanks.

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

#### Scott Morrison (Mar 17 2021 at 09:11):

:fingers_crossed:

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

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

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

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

#### Johan Commelin (Mar 17 2021 at 10:51):

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

branch

#### Johan Commelin (Mar 17 2021 at 10:52):

Maybe they should be backported to `master`

, because they are independent of any other experiments.

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

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

#### 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`

#### Scott Morrison (Mar 17 2021 at 11:19):

(deleted)

#### Scott Morrison (Mar 17 2021 at 11:19):

(deleted)

#### Scott Morrison (Mar 17 2021 at 11:20):

(deleted)

#### Scott Morrison (Mar 17 2021 at 11:20):

oh, this is all garbage, sorry

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

#### 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`

.

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

#### Johan Commelin (Mar 17 2021 at 11:58):

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

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

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

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

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

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

#### Johan Commelin (Mar 17 2021 at 12:38):

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

#### Kevin Buzzard (Mar 17 2021 at 12:42):

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

#### Kevin Buzzard (Mar 17 2021 at 13:38):

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

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

#### Scott Morrison (Mar 17 2021 at 22:45):

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

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