endomorphisms

Stream: condensed mathematics

[Johan Commelin]

Is there anyone who would like to work on src/for_mathlib/endomorphisms/? If you want to play around with a bit of category theory, I think this can be fun.

[Kevin Buzzard]

You should advertise in #maths ;-)

[Kevin Buzzard]

So here is an update on for_mathlib/endomorphisms/. There is basically one sorry in it, here, and it's going to be some work to remove.

Here's some of the mathematics behind the statement of the sorry. If A is an abelian category then one can make a new abelian category endomorphisms A whose objects are pairs (Y,f) with Y an object of A and f an endomorphism of Y. Morphisms are maps intertwining the endomorphisms, and there's a forgetful functor back down to A. If Y is an object and X is a complex of objects in endomorphism A, then both the endomorphism of Y and the endomorphisms of the objects of X induce endomorphisms of Ext^i(X,Y) (Ext group computed in the category of complexes of objects of A up to homotopy). Let e_i denote the difference of these two endomorphisms. The claim is that e_i is an isomorphism for all i iff Ext_{end}^j(X,Y)=0 for all j, where here Ext_{end} means computing ext groups in the category of complexes of objects of endomorphism A, so in particular you probably get different answers in this category than when just considering everything as objects of A.

The proof looks like this: @Andrew Yang developed a theory of projective replacements, but unfortunately we seem to need to develop a parallel theory of projective replacements in endomorphism categories with extra properties. If P is a suitable complex of projective objects with endomorphisms and P is quasi-isomorphic to X (apparently these are called "replacements" now), then one can consider the complex (with morphisms going the other way) C_i := Hom(P^i,Y) with differentials coming from P^i, and one checks that the homology of the complex C_i is the Ext group. If instead you do homomophisms intertwining the endomorphisms then the homology of the resulting complex is the endomorphism Ext group. So it just comes down to checking that e_i : C_i -> C_i (the difference of the endomorphisms) is surjective and its kernel is the equivariant endomorphisms; this gives a short exact sequence of complexes, and it's easily checked that the associated long exact sequence of homology has the property that every third term is 0 iff all the maps in the long exact sequence which have source and target one of the other terms, are isomorphisms:

$\to\mathrm{Ext}_{end}^i(X,Y)\to\mathrm{Ext}^i(X,Y)\to\mathrm{Ext}^i(X,Y)\to\mathrm{Ext}_{end}^{i\pm1}(X,Y)\to\cdots$

All those middle maps are isomorphisms iff all those Ext_{end} terms are 0.

Right now I'm trying to write down a Lean sketch of this in the file src/for_mathlib/endomorphisms/Ext.lean. It's a shame but it seems (unless I'm missing a trick) that we'll have to redo a lot of the projective replacement stuff, because to ensure that the $e_i:C_i\to C_i$ are surjective we seem to need to ensure that the objects-with-endomorphisms $P^i$ are of the form free Q, i.e., $Q\otimes_{\Z}\Z[T]$ for some projective $Q$, with the endomorphism being multiplication by $T$.

Random thought that might save a lot of work: is it likely to be true that every projective object in endomorphisms A is of the form free Q for some object Q which is projective in A?

[Adam Topaz]

Unfortunately, that random thought is probably not true, as you can take direct summands of a projective which will again be projective (although I don't have an explicit example at hand).

[Adam Topaz]

But I think that such projectives are "dense" in the sense that any object can be resolved by a projective of that form.

[Kevin Buzzard]

If it's not true then it probably means we have to redo a bunch of the projective replacement stuff so that it works in this context (I should also say that this is actually an observation of Adam, we've exchanged many direct messages about the situation and the reason I'm posting publically was just to sort out my thoughts a bit)

[Kevin Buzzard]

Yes I believe you that they're dense: take a random object Y in endomorphisms A, imagine it in A, take a projective Q which maps onto it, and now by a universal property free Q will surject onto it in endomorphisms A.

[Johan Commelin]

Maybe the construction of projective replacements can take an extra argument that returns a preferred projective cover for every object?

[Johan Commelin]

Then you don't have to redo it, but only generalize/refactor.

[Kevin Buzzard]

Interesting idea! The only extra thing I need, according to my paper argument, is that each object in the endomorphism-replacement P is (isomorphic to something) of the form free Q with Q projective in A.

[Johan Commelin]

Yep, that sounds right to me

[Julian Külshammer]

Random observations that most likely doesn't buy you anything currently: Your category endomorphisms A is in mathlib as docs#category_theory.endofunctor.algebra for the identity endofunctor.

[Adam Topaz]

They're even essentially defeq

[Adam Topaz]

Here's a fun one: CompHaus is the category of algebras of the codensity monad of the inclusion of Fintype into Type ;)

[Joël Riou]

I may have a solution. The free projective objects surjects onto any object, and in particular any projective object P. By the projective condition of P, P is actually a direct factor of some of these Q := free ?. Then, any condition formulated as the surjectivity of a natural map is satisfied by any projective P if it is satisfied by the free objects.

[Adam Topaz]

@Joël Riou interesting idea. The actual argument we had in mind is a bit more complicated, but in principle this has to work because things must be unique up to homotopy. The question is whether it would be less work to deal with all the homotopies, or just to construct things in a more explicit way as Kevin indicated. I'll have to think about this more carefully.

[Adam Topaz]

The reason we want free ? is because we want to map out of it eventually, but if we have some non-free but projective thing P, then we can resolve by a free, split the epi, and map out of the free to get a map out of the P. This may be enough, I'm not sure.

[Johan Commelin]

Yes, I've convinced myself that this should work.

[Johan Commelin]

So now we only need to get a complex of projective objects in endomorphisms A that is a replacement for X, and such that endomorphism.forget maps all those projective objects to projective objects in A.

[Johan Commelin]

But afaict, that's true in general.

[Johan Commelin]

No wait, it looks like an actual condition.

[Joël Riou]

Johan Commelin said:

No wait, it looks like an actual condition.

SImilarly as above, to show that the forgetful functor preserves projectives, it suffices to check it for the free functor applied to projectives. In that case, this is stability of projectives by direct sums. (Alternatively, if we have exact infinite products, one may use the exactness of the right adjoint of the forgetful functor, which is the dual construction to free, more into power series than polynomials...)

[Adam Topaz]

Yeah we have the cofree construction already ;)

[Johan Commelin]

Aah, of course. I pushed a proof of

instance projective_X [enough_projectives C] (P : endomorphisms C) [projective P] :
  projective P.X :=

[Johan Commelin]

So now we can just work with X.replace for X : endomorphisms A. Because by definition that is a complex with projective objects as components.

[Julian Külshammer]

For porting to mathlib, would it be of interest to generalise most of the things you have to the endofunctor.algebra setting mentioned earlier? Pretty sure this is possible, assuming the appropriate endofunctor right exact, additive, etc. (as one of my latest papers deals with this set-up)

[Johan Commelin]

Yeah, I guess that makes sense

[Julian Külshammer]

Wait a minute, wouldn't it have been easier to realise the category endomorphisms A as the functor_category from the free category on one morphism (aka N as a 1-object category) to A? In this case most of the basic instances should already be in mathlib?

[Adam Topaz]

The defeqs of the current def are much nicer than the functor from the free category approach, IMO.

[Kevin Buzzard]

So the surjectivity proof we need is the following. If $P$ and $Y$ are objects of an abelian category, equipped with endomorphisms $e:P\to P$ and $f:Y\to Y$, and if $\phi:P\to Y$ is a morphism in the category (not necessarily intertwining the endomorphisms), then we want $\psi:P\to Y$ such that $\phi=\psi\circ e - f \circ \psi$. In general we can't have such $\psi$. If $P$ is of the form free Q i.e. $P=\oplus_{n\in\N}Q$ with $e(q_n)=q_{n+1}$ then we can make $\psi$, it's of the form $\oplus \psi_n$ with $\psi_0=0$ and $\psi_{n+1}=\phi_n+f\circ\psi_n$. The question is whether we can make $\psi$ knowing only that $(P,e)$ is projective in the endomorphism category.

[Johan Commelin]

Yes, see Joël's argument above

[Johan Commelin]

https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/endomorphisms/near/288276488

[Kevin Buzzard]

Another way of saying what I'm saying above is "I don't understand Joël's argument yet". I thought it was worth writing down precisely the statement we needed.

[Kevin Buzzard]

Once I understand this, I am ready to get started formalising the argument.

[Kevin Buzzard]

So, say $(P,e)$ is projective. Choose $Q$ as above. Say $\phi:P\to Y$. Extend to $Free(Q)\to Y$. Now we get $\psi:Free(Q)\to Y$. Now restrict back down to $P$. Oh it's as easy as that? :D

[Adam Topaz]

P=Q?

[Kevin Buzzard]

Sorry, let me try again. Let $(P,e)$ be projective. Choose $Q$ such that $P$ is a direct summand of $Free(Q)$. Then continue as above. Is that OK?

[Kevin Buzzard]

Oh, you're saying $P=Q$ works! Yes, I guess it does.

[Kevin Buzzard]

The delicate part of the argument is that the splitting $P\to Free(P)$ will not be the "obvious" map.

[Adam Topaz]

Right!

[Adam Topaz]

It’s just the one you get from projectivity

[Johan Commelin]

the short-exactness is done

[Kevin Buzzard]

The argument that's worrying me in the endomorphisms directory is this hideous diagram chase. I'll have a look at it this evening.

[Johan Commelin]

Can you already state it? Or do you need more setup?

[Kevin Buzzard]

I've stated it, it's the bottom sorry.

[Kevin Buzzard]

There's an isomorphism called j which is a composite of about three isomorphisms and is supposed to intertwine two maps of the form $\psi\mapsto f\psi-\psi g$.

[Johan Commelin]

Yep, I see it.

[Joël Riou]

Kevin Buzzard said:

There's an isomorphism called j which is a composite of about three isomorphisms and is supposed to intertwine two maps of the form $\psi\mapsto f\psi-\psi g$.

I do not have much time today to work on this, but if dsimp/simp does not work well, I would suggest getting rid of convert on the line convert iso.app this _ in the definition of j. There is an annoying single 𝓐 (0 - -i). It you introduce an eq_to_iso isomorphism (single 𝓐 p).obj Y ≅ (single 𝓐 q).obj Y when p=q, it may dsimp/simp better.

[Johan Commelin]

There are also a bunch of haves for data. I'm fixing those now.

[Kevin Buzzard]

Thanks. I defined the map late last night!

[Johan Commelin]

I split the goal into two pieces, as you suggested.

[Johan Commelin]

I just added

lemma hom_single_iso_naturality'
  (P₁ P₂ : bounded_homotopy_category C) (B : C) (i : ℤ)
  (f : P₁.val.as ⟶ P₂.val.as) :
  (preadditive_yoneda.obj ((single C i).obj B)).map (of_hom f).op ≫ (hom_single_iso P₁ B i).hom =
  (hom_single_iso P₂ B i).hom ≫
  (((preadditive_yoneda.obj B).right_op.map_homological_complex _ ⋙
      homological_complex.unop_functor.right_op ⋙
      (_root_.homology_functor _ _ _).op).map f).unop :=

with a minor sorry.

[Johan Commelin]

Compiling :fencing: to see if I didn't break the build

[Johan Commelin]

j is mostly built from preadditive_yoneda stuff. So maybe your goal isn't too bad.

[Johan Commelin]

I pushed to branch jmcwip because I need to run

[Joël Riou]

I have just removed the minor sorry in this lemma hom_single_iso_naturality'.

[Joël Riou]

Today, I have worked on one of the two compatibilities in Ext_is_zero_iff. I have struggled very much because of op/unop intricacies with homological_complex/homotopy_category. Modulo two more sorried basic statements, this should be ok soon, but I have to stop for today. I may have some time tomorrow morning only.

[Joël Riou]

If anyone sees how to fill these sorries in for_mathlib/endomorphisms/Ext.lean, feel free to do so.

[Johan Commelin]

Thanks for your work!

[Johan Commelin]

I closed the compatibility sorry.

[Johan Commelin]

Other one is done as well

[Joël Riou]

I have almost finished proving the last compatibility in for_mathlib/endomorphisms/Ext.lean. The only left sorry is a basic naturality statement that I have moved to hom_single_iso.lean. It is the naturality with respect to the other variable. In principle, I would think that it should be easier than the naturality on the first variable, but I have no idea about the internals of the definitions in this file and I have no more Lean time today (dance again...). Maybe @Adam Topaz this could be for you?

[Johan Commelin]

The sorries are now done.

[Joël Riou]

I have just finished the other naturality sorry that was left for the presheaf iso eval_freeFunc_homology_zero.