what is an injective object

Stream: maths

[Kevin Buzzard]

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]

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]

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]

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]

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

[Kevin Buzzard]

OK great; Jujian is working on it!

[Jujian Zhang]

In the process of translating projectiveness to injectiveness, there is docs#category_theory.exact.lift, which says
if $Q\rightarrow R\rightarrow S$ is exact and $P$ is projective with $P\rightarrow R$ such that $P\rightarrow R\rightarrow S=0$, then we can lift $P\rightarrow R$ to $P\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 : Q\rightarrow R$ and $g:R\rightarrow S$ is exact then $\mathrm{coker} f\rightarrow\mathrm{im} g$ is mono (dual to $\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]

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]

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

[Reid Barton]

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]

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]

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]

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

[Adam Topaz]

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

[Julian Külshammer]

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]

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]

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]

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

[Adam Topaz]

Is it?

[Jujian Zhang]

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]

What does regular mean again?

[Reid Barton]

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

[Adam Topaz]

Oh, yeah that's fine.

[Reid Barton]

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

[Adam Topaz]

Do we have docs#category_theory.regular_epi

[Adam Topaz]

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

[Reid Barton]

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

[Reid Barton]

(why is anything a class :angry:)

[Julian Külshammer]

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]

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

[Reid Barton]

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

[Reid Barton]

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

[Kevin Buzzard]

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

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]

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]

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

[Matthew Ballard]

The only good things in categories come from has_lifting_property

[Matthew Ballard]

The work on simplicial objects might make that equally accessible

[Joël Riou]

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]

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

[Joël Riou]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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

[Jakob Scholbach]

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]

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]

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]

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]

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]

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

[Matthew Ballard]

Not the pure versions if I remember correctly

[Joël Riou]

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]

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]

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

[Adam Topaz]

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]

Or maybe I am misunderstanding the issue?

[Matthew Ballard]

I want to compute sheaf cohomology using a cover.

[Matthew Ballard]

As an example

[Adam Topaz]

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]

Same for sheaf Tor and a resolution by locally frees?

[Reid Barton]

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]

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

[Reid Barton]

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

[Reid Barton]

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]

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]

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

[Reid Barton]

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]

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]

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.