Zulip Chat Archive

Stream: maths

Topic: what is an injective object


Kevin Buzzard (Feb 08 2022 at 10:24):

We could be clever and define an injective object in C to be a projective object in C^op. Is this a sensible thing to do or should we just make the API from first principles and avoid op hell?

Kevin Buzzard (Feb 08 2022 at 10:29):

It's part of #11878 and I'm thinking it should be split off but I'm wondering whether people will object to the definition.

Yaël Dillies (Feb 08 2022 at 10:30):

So a projective object in C is an injective object in Cᵒᵖ? How can you state that if you try to spare yourself the definition from first principles?

Jujian Zhang (Feb 08 2022 at 10:32):

class injective (J : C) : Prop :=
 (factors :  {X Y : C} (g : X  J) (f : X  Y) [mono f],  h : Y  J, f  h = g)

Johan Commelin (Feb 08 2022 at 10:38):

We duplicate the entire limit API into a colimit API. I would do the same here.

Kevin Buzzard (Feb 08 2022 at 10:56):

OK great; Jujian is working on it!

Jujian Zhang (Feb 15 2022 at 11:52):

In the process of translating projectiveness to injectiveness, there is docs#category_theory.exact.lift, which says
if QRSQ\rightarrow R\rightarrow S is exact and PP is projective with PRP\rightarrow R such that PRS=0P\rightarrow R\rightarrow S=0, then we can lift PRP\rightarrow R to PQP\rightarrow Q. So we need an analogous statement for injective objects. In the setting of abelian category, this is easily done, reverse arrow then use exact.lift, but that would require abelian category because we used exact g.op f.op from exact f g. To do this without abelian setting, we need the following fact (if this is true): if f:QRf : Q\rightarrow R and g:RSg:R\rightarrow S is exact then cokerfimg\mathrm{coker} f\rightarrow\mathrm{im} g is mono (dual to imfkerg\mathrm{im} f\rightarrow\mathrm{ker} g being epi).
So is this true in a general category where all relevant notion makes sense?

The reason that I don't want to assume abelianness is that the corresponding docs#category_theory.exact.lift is proved with far weaker assumption (only zero_morphisms, equalizers and images). So how much theory of injective objects and injective resolutions do we want to develop before introducing abelianness assumption?

Reid Barton (Feb 15 2022 at 12:46):

If we're trying to talk about projectives and injectives without exactness conditions on the category--I'm kind of surprised that the definition of projective object does not involve regular epimorphisms.

Johan Commelin (Feb 15 2022 at 12:46):

I think we have a pretty assymetrical notion of exactness in mathlib, and maybe that's not a good idea.

Reid Barton (Feb 15 2022 at 12:48):

I guess I would be inclined to say that you shouldn't bother worrying about the non-abelian category case until you have some use for it

Reid Barton (Feb 15 2022 at 12:53):

I see both wikipedia and nLab say a projective object is an object that lifts against all epimorphisms but I think it's the kind of definition that someone would make if they only think about cases where every epi is regular (e.g. in a topos or an abelian category).

Reid Barton (Feb 15 2022 at 12:54):

I don't know if this helps with your question, but my point is that if you want to get correct definitions without any exactness assumptions on the category then maybe you have to start earlier.

Matthew Ballard (Feb 15 2022 at 12:57):

Are there general has_lifting_property x C for an object x and a class of morphisms C?

Adam Topaz (Feb 15 2022 at 13:12):

We do have docs#category_theory.has_lifting_property but it's not used much AFAIK

Julian Külshammer (Feb 15 2022 at 13:50):

I would agree that lifting against all mono- (resp. epi-)morphisms is mostly relevant to the abelian setup. If one wants to generalise the notion of a projective object, one should probably look into an exact category and then restrict having the lifting property to admissible mono- (resp. epi-) morphisms, aka inflations and deflations.

Jujian Zhang (Feb 15 2022 at 14:22):

I found out an almost comical solution, instead of assuming exact f g, we can work with assumption exact g.op f.op, so that the corresponding statement only requires [has_zero_morphisms C] [has_images Cᵒᵖ] [has_equalizers Cᵒᵖ]

Adam Topaz (Feb 15 2022 at 14:25):

Please don't change the definition of projective. We use it in LTE to talk about projective profinite spaces, and it works just fine as is. Profinite is not an exact category.

Reid Barton (Feb 15 2022 at 14:26):

I think every epimorphism in Profinite is regular though, right?

Adam Topaz (Feb 15 2022 at 14:26):

Is it?

Jujian Zhang (Feb 15 2022 at 14:26):

Adam Topaz said:

Please don't change the definition of projective. We use it in LTE to talk about projective profinite spaces, and it works just fine as is. Profinite is not an exact category.

I won't change it.

Adam Topaz (Feb 15 2022 at 14:26):

What does regular mean again?

Reid Barton (Feb 15 2022 at 14:27):

Coequalizer of some pair (which can be taken to be the kernel pair if the category has pullbacks)

Adam Topaz (Feb 15 2022 at 14:28):

Oh, yeah that's fine.

Reid Barton (Feb 15 2022 at 14:29):

I think it's usually less work to show that this agreess with what you want (surjections) than general epis

Adam Topaz (Feb 15 2022 at 14:31):

Do we have docs#category_theory.regular_epi

Adam Topaz (Feb 15 2022 at 14:33):

Hmm... is that the right definition for regular_epi? It includes the coequalizer as data.

Reid Barton (Feb 15 2022 at 14:34):

maybe a forgotten : Prop? I also don't understand why it is a class

Reid Barton (Feb 15 2022 at 14:34):

(why is anything a class :angry:)

Julian Külshammer (Feb 15 2022 at 16:27):

nlab seems to suggest that we should have different notions of projective, the one of lifting with respect to all epimorphisms, then also something called regular_projective which I have to admit I had not heard of before. In my area of research, the more frequently appearing notion is that of projective with respect to some (Quillen) exact structure, which is yet another version of a lifting property, see e.g. Exact categories by Bühler.

Reid Barton (Feb 15 2022 at 18:03):

Regular epimorphisms are the right notion in categories of models of an algebraic theory. For example in rings, the inclusion ZQ\mathbb{Z} \to \mathbb{Q} is an epimorphism (but not surjective of course) and so the polynomial ring Z[X]\mathbb{Z}[X] isn't projective. Regular epimorphisms agree with the surjective maps.

Reid Barton (Feb 15 2022 at 18:03):

And one of the characteristic features of algebraic categories is that they have enough compact [regular] projective objects.

Reid Barton (Feb 15 2022 at 18:32):

But indeed in other situations you might want to take the "right" notion of "epimorphism" as a parameter.

Kevin Buzzard (Feb 16 2022 at 07:27):

@Jujian Zhang how about you make the basic definitions of projective objects with as few assumptions as possible but the moment it's convenient to do so, assume abelian. In contrast to what we were worried about yesterday it looks unlikely that people will be using the notion any time soon in the nonabelian setting (indeed it may not even be the right one), and the sooner we're in a position to start talking about it in the abelian setting the better.

Joël Riou (Feb 28 2022 at 19:04):

Adam Topaz said:

We do have docs#category_theory.has_lifting_property but it's not used much AFAIK

I have started attempting at formalising Quillen's model categories, and for that has_lifting_property shall be used and extended... (I guess that the first reachable example of model_category would be that of complexes (C^+) in an abelian category with enough injectives, or the dual version with enough projectives. )

Adam Topaz (Feb 28 2022 at 19:07):

That sounds great @Joël Riou ! Actually @Matthew Ballard and I were discussing just a few days ago that it would be nice to have the model category of complexes, and perhaps (re?)define derived functors using this approach.

Adam Topaz (Feb 28 2022 at 19:08):

And IIRC @Jakob Scholbach 's original motivation for defining has_lifting_property was indeed as a start toward model categories!

Matthew Ballard (Feb 28 2022 at 19:11):

The only good things in categories come from has_lifting_property

Matthew Ballard (Feb 28 2022 at 19:12):

The work on simplicial objects might make that equally accessible

Joël Riou (Feb 28 2022 at 19:13):

I am working towards the "fundamental lemma of homotopical algebra", which is that is X is cofibrant and Y fibrant, then the morphisms in the localized category (obtained by formally inverting the weak equivalences) identifies to homotopy classes of maps defined by cylinder. I have already a draft of the construction of localized categories C[W^-1] (based on the great works that are already in mathlib, like path_category of a quiver and quotient categories).

Adam Topaz (Feb 28 2022 at 19:14):

Nice! I wonder, how did you formalize the definition of (co)filbration and weak_equivalence?

Joël Riou (Feb 28 2022 at 19:15):

I believe that the model structure on simpliical sets will take more time! (I think we first need to have it for the category of topological spaces, with Serre fibrations. It would be nice if the on-going work on homotopies in topological helps there.)

Joël Riou (Feb 28 2022 at 19:15):

Adam Topaz said:

Nice! I wonder, how did you formalize the definition of (co)filbration and weak_equivalence?

abbreviation arrow_class := set (arrow C)

Reid Barton (Feb 28 2022 at 19:17):

Happy to see people working on this! you might be interested in:
https://github.com/rwbarton/lean-homotopy-theory
https://github.com/rwbarton/lean-model-categories/tree/top-dev (old WIP, but has some stuff)

Adam Topaz (Feb 28 2022 at 19:17):

Aha I see. Did you find working with arrow to be easy enough? I would have guessed that

def arrow_class (C : Type*) [category C] := Π X Y : C⦄, (X  Y)  Prop

might be easier to work with in practice.

Adam Topaz (Feb 28 2022 at 19:19):

It looks like this is what @Reid Barton chose to do in his repo:

class has_weak_equivalences (C : Type u) [category C] :=
(is_weq : Π a b : C⦄, (a  b)  Prop)

Joël Riou (Feb 28 2022 at 19:21):

That was my first idea, but it turned out to be easier to work with arrow C. One of the reasons is that has_lifting_property is defined using arrow.

Reid Barton (Feb 28 2022 at 19:22):

Is there a reason for it to be? you can just use implicits for the objects and talk about lifting conditions between two morphisms without mentioning arrow

Adam Topaz (Feb 28 2022 at 19:22):

Yes, of course, but perhaps it would be worthwhile to change the definition of has_lifting_property? (I don't remember exactly why @Jakob Scholbach decided to use arrow there.)

Joël Riou (Feb 28 2022 at 19:30):

In order to work with commutative squares (and lifting properties, etc), it is very convenient to use morphisms between objects in the category arrow C... Also, when stating some lemmas, we need only one variable for each arrow, not three!

Matthew Ballard (Feb 28 2022 at 19:34):

Progress in this direction is excellent. I've spent my time looking for appropriate emoji to express my feelings. :smile:

Jakob Scholbach (Feb 28 2022 at 19:35):

I first want to apologize for leaving this topic. I simply didn't find the time do work on lean anymore.
I thought it is a good idea to formalize lifting properties using the arrow category since for example the usual arguments involving transfinite compositions take place as colimits in the arrow category, I think. But of course, if you see any reason to undo this choice, go ahead!
On the original question: what is an injective object, I would like to briefly point out a remark / definition in "Cesnavicius, Scholze. Purity for flat cohomology" that a compact object is an object x such that Hom(x, -) commutes with sifted colimits. Does it make sense to define a projective object to be an object such that Hom(x, -) preserves reflexive coequalizers?

Adam Topaz (Feb 28 2022 at 19:37):

Perhaps something like the following would be a good compromise

import category_theory.arrow

namespace category_theory
variables (C : Type*) [category C]

abbreviation arrow_class := set (arrow C)

instance : has_coe_to_fun (arrow_class C) (λ a, (Π X Y : C⦄, (X  Y)  Prop)) :=
λ a X Y f, (arrow.mk f)  a

end category_theory

Matthew Ballard (Feb 28 2022 at 19:42):

Adam Topaz said:

That sounds great Joël Riou ! Actually Matthew Ballard and I were discussing just a few days ago that it would be nice to have the model category of complexes, and perhaps (re?)define derived functors using this approach.

After a little thought, I might temper this though. The derived functor will depend on the model structure and that seems hard to unify in a simple way. Relating Tor sheaves over a scheme and sheaf cohomology might be annoying as an example

Matthew Ballard (Feb 28 2022 at 19:45):

But bounded above chain complexes with the projective model structure is definitely a good target given the work @Adam Topaz, @Andrew Yang, and others have done for LTE.

Jakob Scholbach (Feb 28 2022 at 19:46):

Matthew Ballard said:

Adam Topaz said:

That sounds great Joël Riou ! Actually Matthew Ballard and I were discussing just a few days ago that it would be nice to have the model category of complexes, and perhaps (re?)define derived functors using this approach.

After a little thought, I might temper this though. The derived functor will depend on the model structure and that seems hard to unify in a simple way. Relating Tor sheaves over a scheme and sheaf cohomology might be annoying as an example

Yes, this is true. To get a formalism independent of choices of (co)fibrations, one can use the notion of a category with weak equivalences (as in this book https://ncatlab.org/nlab/show/Homotopy+Limit+Functors+on+Model+Categories+and+Homotopical+Categories ).

Adam Topaz (Feb 28 2022 at 19:48):

The model category structures on complexes always have quasi isos as the weak equivalences right?

Matthew Ballard (Feb 28 2022 at 19:49):

Not the pure versions if I remember correctly

Joël Riou (Feb 28 2022 at 19:54):

Actually, I think that in this context, model categories can be considered as a tool in order to study derived categories and construct derived functors. The homotopy category does not depend on the choice of cofibrations/fibrations, only on the class of weak equivalences. Similarly, the (total) left/right derived functors is defined by a universal property which depends only on the class of weak equivalences.

Adam Topaz (Feb 28 2022 at 19:57):

If we want to define derived functors as Kan extensions, then we should try to resolve this issue as well:
https://github.com/leanprover-community/mathlib/issues/7051

Matthew Ballard (Feb 28 2022 at 20:03):

True. But using adapted objects to "compute" derived functors in the linear setting seems more complicated here to me.

Adam Topaz (Feb 28 2022 at 20:06):

I think in this case having a characteristic predicate for a Kan extension would help if, for example, you want to "compute" a derived functor using projectives, i.e. you get some functor (defined in terms of projectives) which should satisfy the characteristic predicate, hence would be isomorphic to "the" derived functor defined in terms of a Kan extension.

Adam Topaz (Feb 28 2022 at 20:06):

Or maybe I am misunderstanding the issue?

Matthew Ballard (Feb 28 2022 at 20:15):

I want to compute sheaf cohomology using a cover.

Matthew Ballard (Feb 28 2022 at 20:15):

As an example

Adam Topaz (Feb 28 2022 at 20:19):

Okay, so in that case you can show that some functor you define in terms of (hyper)cover(s) of your scheme/space satisfies the characteristic predicate. I'm not saying it would be easy to show, but I don't think it's much more difficult than the proof showing that sheaf cohomology (defined in terms of injective resolutions of the sheaf) agrees with the object defined in terms of hypercovers.

Matthew Ballard (Feb 28 2022 at 20:25):

Same for sheaf Tor and a resolution by locally frees?

Reid Barton (Feb 28 2022 at 20:38):

The problem with arrow is that you cannot really compose arrows. More generally, you are forced to either introduce variables in a restricted format (which will sometimes be impossible, as in the case of composition) or just go ahead and use {X Y Z : C} (f : X -> Y) (g : Y -> Z) anyways. The latter form will be required at least some of the time. If you always use the latter form, then there is obviously no advantage to "arrow classes" since it forces you to write <f> for no reason. If you mix them, then you have to decide when to talk about arrows versus morphisms, and you're likely to have annoyances due to a lack of eta f = <f.hom>.

Reid Barton (Feb 28 2022 at 20:38):

I can't imagine there is any advantage of arrow that outweighs this problem.

Reid Barton (Feb 28 2022 at 20:40):

(Another subjective advantage is that it's nicer to talk about maps B -> X than maps f.cod -> g.dom or whatever.)

Reid Barton (Feb 28 2022 at 20:42):

It's true that at some point you'll want to say things like "weak equivalences are closed under filtered colimits in the arrow category", but this isn't made harder by working with morphism classes: use a cocone in arrow C, and then formulate the hypotheses and conclusions in terms of is_weq (F.obj i).hom or whatever.

Joël Riou (Feb 28 2022 at 20:59):

Reid Barton said:

I can't imagine there is any advantage of arrow that outweighs this problem.

Actually, when working with model categories, it is important to be able to talk about retracts of arrows, and this is a very good mathematical reason to work with the category arrow C. Anyway, I do not think this is a serious discussion, and I will refrain from fueling it more here.

Reid Barton (Feb 28 2022 at 21:00):

I'm not exactly sure what you mean by a serious discussion.

Reid Barton (Feb 28 2022 at 21:03):

It's true that retracts of arrows come up but it's not clear to me that this notion is necessarily more conveniently phrased in terms of arrow--in order to work with it you have to unwind this definition anyways.

Reid Barton (Feb 28 2022 at 21:05):

I spent a lot of time thinking specifically about formalizing model categories in Lean (as you can see from the linked repos) and my heartfelt opinion is that you will save yourself a lot of annoyance by avoiding arrow when talking about classes of morphisms. Of course you can just ignore me, if you like.

Johan Commelin (Mar 01 2022 at 09:12):

I think that Reid probably has the most experience of everyone, when it comes to formalizing model categories (and homotopy theory outside of HoTT). I would take his opinion very serious.


Last updated: Dec 20 2023 at 11:08 UTC