trouble in `shift_functor` land

Stream: maths

[Scott Morrison]

I think we have an overlapping ...cluster... of problems, centred around docs#category_theory.shift_functor. I've made several recent attempts to clean this up, and always found myself dealing with trying to solve multiple problems at once, and getting frustrated. This is an attempt to list all the problems I've noticed, in the hope that this helps me understand what order they should be fixed in!

I think these problems are important to solve, as shift_functor is used all over the homological algebra in LTE, and at the moment I can't bring myself to work on things in LTE that involve it, not wanting to build on shaky foundations.

To recall, a shift_functor A C is currently defined as a monoidal functor from a monoid A (thought of as a discrete monoidal category) to the endofunctors of C.

Although this sounds complicated, I think it is fundamentally sound: equations in the monoid A are going to be reflected by something "equational" (i.e. equations, or natural isomorphisms) between the corresponding endofunctors, and it is better and saner to handle this explicitly as part of the structure of a monoidal functor, rather than risking dealing with eq.rec.

This version of shift_functor was introduced in #10573 by @Johan Commelin and @Andrew Yang. Previous to that, we described shift functors just by a single auto-equivalence of the category, corresponding to shift-by-one.

Okay, so what is currently wrong?

1. docs#category_theory.endofunctor_monoidal_category and docs#category_theory.discrete.monoidal are presumably missing @[simp] lemmas, because there are places where we are compelled to write local attribute [reducible] on them; to me this is a bad code smell.
2. There is some unfortunate tension between different simp lemmas involving inverses, sometimes pushing inverses down and sometimes pulling them up. There's no well-defined simp normal form, and so we're often left with nasty goals where manual rewriting is needed to cancel inverses. As an example, we distribute inv over ≫, but pull inv out from inside F.map, so the simplifier can't cope with inv (F.map (inv f ≫ inv g)).
3. In docs#category_theory.shift_mk_core, we provide a helper lemma for constructing a shift functor, but really it should be generalised to construct a lax monoidal functor from a ->+. (EDIT: maybe not.)
4. category_theory.opaque_eq_to_isois a weird hack, that ideally we could avoid, because it is a weird hack?
5. monoidal_functor contains an is_iso field for both μ and ε, the tensorator and unitor of the underlying lax monoidal functor. However we're then erratic about whether we refer to the inverse via something like inv μ, or via something like μ_iso.inv, where μ_iso := as_iso μ. This results in some unnecessary and painful rewriting, and bad simp normal forms.
6. In category_theory.triangulated.rotate, we show that rotating triangles is an equivalence of categories. A while back, the proofs here were short and sensible. Now they are big and fragile. (See e.g. this sort of diff.) Most of my attempts to fix problems above have foundered on not being able to get these proofs to work again. Hopefully the explanation for this change is that previously they were solely in terms of the shift-by-one equivalence, and now are exposed to the full complexity of the monoidal functor. It doesn't seem impossible that we could recover the previous clean situation.

[Scott Morrison]

Problem 6. feels like the fundamental one to me, and it prevents me from making progress on the others, it seems. Any attempt to fix other problems results in these fragile proofs breaking, and then I can't fix them. So far my best idea is do revert #10573 and try again, this time with the requirement that we don't ever write local reducible, and that one-liner proofs stay that way. This would cast LTE adrift for a while, but I'm running out of ideas. I just spent another hour on this with nothing to show for it. Help, or alternatively saying that reverting #10573 is not insane, very much appreciated.

[Adam Topaz]

How reliable are the simp lemmas around pseudofunctors? I haven't been following these recent developments around bicategories too closely, but IIRC there was some PR recently adjusting some simp lemmas for the better (I assume...). Would changing has_shift to use pseudofunctors as opposed to a monoidal functor help at all?

[Scott Morrison]

Hmm, I don't know there's much difference on the monoida functor / pseudofunctor front, although I will have a think about this. The formalisation of bicategory we have in mathlib has a nice advantage over monoidal_category because it doesn't allow horizontal composition (corresponding to tensor product) as an elementary operation, only whiskering. This seems to have a nice juicy payoff in better simp lemmas.

[Scott Morrison]

But that's all at the category level, not the functor level.

[Kevin Buzzard]

Scott, thanks a lot for this very coherent summary of the situation.

Trying to understand what's going on here (not that I'm convinced I can help much, but I'm obviously interested). I don't have a good understanding of simp normal form. We spent a long time in the past trying to make simp do the job of both norm_cast and push_cast despite @Mario Carneiro being adamant that it wasn't the tool for the job, and ultimately this was fixed by writing norm_cast and push_cast instead. One of the issues is that sometimes the user wants to push one way and sometimes the other; neither is "simpler". I've seen other situations where I've been confused about whether to make something into a simp lemma: it seems like a good idea for when you're making some basic API but then when that's made you don't want the lemma to be simp any more. As a result I always feel a bit confused about simp and simp normal form. Is the issue here that no global coherent decision has been made about a simp normal form or that there is no "best" normal form and that one sometimes wants to push and sometimes pull? I appreciate that this seems not to be the main issue but I thought I'd start somewhere.

[Kevin Buzzard]

push_inv and pull_inv?

[Scott Morrison]

I'm pretty sure there's just no plausible normal form that will make everyone happy.

[Scott Morrison]

I think some generic push and pull tactics would be amazing.

[Scott Morrison]

I'm imagining some lookup table (controllable by attributes?) that informs the tactic "if the user has asked you to push the symbol ◫, perhaps try these lemmas", and then it just blindly rewrites by those lemmas, accepting any successful rewrites that increase/decrease the depth of ◫.

[Kevin Buzzard]

So your opinion seems to be consistent with what we've seen with nat/int/real, where sometimes you just want all the coercions to go away but at other times you want them to happen as soon as they can ie every natural immediately gets coerced to a real

[Scott Morrison]

Yes. The category theory library is full of these: do we want functors in or out, natural transformations to the left or right, inverses in or out? There's no hope of consistently deciding all of these. (That's far from saying that our current simp lemmas are optimal, or even seriously thought about...)

[Kevin Buzzard]

Right, and my understanding of Mario's point of view was that perhaps one shouldn't be using simp at all to do this job

[Kevin Buzzard]

Because we don't know what we want, we want access to both directions

[Scott Morrison]

Specifically on the subject of inverses, I have a branch (another failure because of this shift_functor problem) that introduces a has_syntactic_inv, a "syntactic typeclass" that says "this expression has an inv deep inside it, and if you want to take inv of the whole expression, I know how to make them cancel". I think it's fun, and maybe useful, and would like to return to it again later. :-)

[Scott Morrison]

This would allow simplification of expressions like inv (F.map (inv f ≫ inv g)) mentioned above, because F.map (inv f ≫ inv g) would easily acquire a has_syntactic_inv instance!

[Kevin Buzzard]

Trying to understand the meat of your post -- my first naive thought was "well maybe forget about this whole monoidal stuff and just define a has_scalar action of a monoid on a category". Are your comments about eq.rec explaining why this is a bad idea? Is this the whole "A (n-1+1) isn't A n" thing?

[Kevin Buzzard]

docs#category_theory.opaque_eq_to_iso

[Kevin Buzzard]

docs#category_theory.eq_to_iso

[Johan Commelin]

Thanks for writing down this list! Now that I read it, I recognize these pain points, but I hadn't distilled them into such an articulate form.
Concerning (2). I think we have (F.map_iso e).inv = F.map e.inv as simp-lemma for iso.inv. So it would be good to have the same direction for is_iso.inv.

[Johan Commelin]

Aaah, internet is back. I see I missed a lot of messages

[Scott Morrison]

@Kevin Buzzard, yes, this is basically the dependent type theory hell problem. Johan might have a more detailed explanation in this particular case. But the argument is that you inevitably have these "transports" either way, and it's better to have them as explicit morphisms, which are easier to keep track of (and there are fewer things to do with them) than arbitrary eq.recs.

[Yaël Dillies]

In that specific case, why can't F.map (inv f ≫ inv g) be rewritten to F.map (inv f) ≫ F.map (inv g). Distributivity simp lemmas seem to be very useful.

[Scott Morrison]

Hmm, maybe I picked a terrible example.. :-) That is just functor.map_comp, hopefully.

[Scott Morrison]

Another example of "distant invs" that I've met in the wild is inv (H.map (α.inv.app X)) = H.map (α.hom.app X).

[Scott Morrison]

Okay, hopefully #14262 deals with #4, by killing off opaque_eq_to_iso. It depends on #14260, so if review of both of those could happen, that would be lovely. :-)

[Johan Commelin]

@Scott Morrison Thanks. eq_to_hom_map is indeed a very bad lemma for the default simp-set.

[Scott Morrison]

Yes, and surely my fault that it is in the simp set. Sorry about that. :-) I do like simp to work when it can.

[Scott Morrison]

I would like to rename it to functor.map_eq_to_hom, but I'll keep that for a separate PR.

[Johan Commelin]

No worries. It's all part of the experiment. We learn as we go.

[Scott Morrison]

I am on the edge of seriously proposing that we revert #10573. I am trying to solve the problems in shift_functor, but having to make incremental changes while maintaining the proofs in pretriangulated/rotate.lean is simply too painful.

[Scott Morrison]

Could we just try again with shift_functor, next time being more careful?

[Reid Barton]

Oh no you deleted eq_to_hom_map again?

[Reid Barton]

I still don't understand why one wouldn't want it by default, and the PR gives no indication

[Reid Barton]

I realize it's biased to be looking at existing mathlib proofs but #14260 doesn't look very good to me, it broke about 30 proofs, and the ones that it fixed were mostly using nonterminal simp

[Reid Barton]

I understand in principle how there could be an issue with naturality, but isn't naturality not a simp lemma anyways?

[Reid Barton]

What about just writing local attribute [-simp] where you don't want it?

[Reid Barton]

We could also add the simp-normal-form of naturality applied to eq_to_hom of something as a new lemma

[Adam Topaz]

docs#category_theory.nat_trans.naturality

[Adam Topaz]

Yeah, it's a simp lemma.

[Adam Topaz]

I think I agree with Scott in this case. In practice, it seems that eq_to_hom is easier to work with when it's as deeply nested as possible. I.e. I would indeed prefer F.map (eq_to_hom h) as opposed to eq_to_hom (congr_arg ...) because with F.map on the outside you at least have some hope of progress if you have some other F.maps around or e.app where e is a nat trans.

[Scott Morrison]

@Reid Barton, would you be interested in

1. either removing, or finding an alternative to, opaque_eq_to_iso in shift_functor.lean, as #14262 does (but this depends on #14260)
2. restoring the proofs in pretriangulated/rotate.lean to something similar to the state they were in prior to #10573? (#14258 is a draft PR which shows what reverting #10573 does relative to current master)

Alternatively resolving points 1. or 5. in my list above would be very helpful.

The basic problem with allowing simp to use eq_to_hom_map is that afterwards you can't use naturality, functoriality, etc, because the functors have disappeared into a proof.

[Scott Morrison]

I am certainly open to attempting to restore eq_to_hom_map to the default simp later, if we can first bring shift_functor and rotate back to a maintainable state, and then restore it to the simp set without rebreaking them.

[Scott Morrison]

But to be honest at this point I am very frustrated by the issues around shift_functor, and my enthusiasm for dealing with it is vanishing, and so when I find steps that go partially towards repairing these problems, if there are problems with those steps I would like concrete (ideally in the form of PRs) alternatives.

[Johan Commelin]

I find eq_to_hom_map very dubious as simp-lemma. And get shift to work well is certainly higher on my list of "important things" than supporting this simp-lemma.

[Reid Barton]

OK, I can't really imagine why it should not be a simp lemma (and I think the PR diff speaks for itself) but if it looks like progress to you, then carry on!

[Reid Barton]

I'm mainly annoyed because we already went through one round of this with #1346 and #2713. I feel something else is wrong here.

[Johan Commelin]

Hmm, as simp-lemmas that certainly prevent other chains of simp-lemmas to fire. So it seems to me that the simp-set is not confluent.

[Johan Commelin]

Reid Barton said:

We could also add the simp-normal-form of naturality applied to eq_to_hom of something as a new lemma

I guess this would allow some progress.
Maybe the biggest show-stopper is that you have no idea what to do when you see eq_to_hom _ in the goal view. So you prefer to have that _ be as small as possible.

[Johan Commelin]

Personally I always feel some relief when I get eq_to_hom_refl to fire, so that I'm back in "honest" category theory land.

[Reid Barton]

I didn't realize naturality was a simp lemma. That means there are two non-confluent simp rewrites from whatever the left hand side of naturality is applied to eq_to_hom. The way to fix it is to add another simp lemma.

[Reid Barton]

Johan Commelin said:

Personally I always feel some relief when I get eq_to_hom_refl to fire, so that I'm back in "honest" category theory land.

Yes, that's exactly the purpose of lemmas like eq_to_hom_map--you want to compose all the eq_to_homs appearing in your expression into one place, so that if at the end of the day you are talking about the same object, they will all cancel with eq_to_hom_refl. This doesn't require looking at the proofs in any way.

[Reid Barton]

It's kind of silly to be talking about naturality--if $t_{X} : FX \to GX$ and $A = B$ then up to equalities of objects we have $t_A = t_B$, and this doesn't require any kind of functoriality or naturality assumptions.

[Scott Morrison]

Haha, I had forgotten about #1346 and #2713. Very reasonable to be annoyed. :-) I'm away from my desktop at the moment and don't have the branch, but I'll try to post some examples where eq_to_hom_map was annoying me later.

[Reid Barton]

Regarding def shift_functor (n : ℤ) : differential_object C ⥤ differential_object C--first I'll have to apologize that this is very far from the way I usually think about these things.

[Reid Barton]

Don't you want a sign in this definition?

[Reid Barton]

https://stacks.math.columbia.edu/tag/0119

[Reid Barton]

abbreviation shift_functor_comp_shift_functor_neg (i : A) :
  shift_functor C i ⋙ shift_functor C (-i) ≅ 𝟭 C :=
unit_of_tensor_iso_unit (shift_monoidal_functor C A) ⟨i⟩ ⟨(-i : A)⟩
--(opaque_eq_to_iso (add_neg_self i))
  (discrete.eq_to_iso (add_neg_self i))

I think the problem is in this definition, we should be thinking of discrete int as having an "inversor" $i \oplus (-i) \cong 0$ which should be part of its structure as a "groupoidal" category. We should not directly expose that this inversor is defined in terms of eq_to_iso (especially not in an abbreviation!)

[Reid Barton]

At a higher level, I think it is not that easy to prove that discrete nat is equivalent to the free monoidal category on one object, right? The latter would have objects like $(X \otimes 1) \otimes (1 \otimes (X \otimes X))$, and then all the maps we can build from the associators and unitors.

[Reid Barton]

If we formed the free monoidal category on an invertible object, the objects $X \otimes X^{-1}$ and $1$ wouldn't be equal. So, you shouldn't be exposing this inversor as built from eq_to_hom.

[Kevin Buzzard]

Re the sign: you're not going to have this with an arbitrary group action on a category. Or should the group come equipped with a map to Z/2?

[Reid Barton]

Well differential_object is specialized to int. A $G$-graded object can just be shifted without needing any extra data, but for a differential object you need to specify how to identify $X[n][1]$ with $X[1][n]$ in order to get the differential on the shifted object.

[Reid Barton]

I found a discussion about signs in a shifted complex from last year, but it seems LTE still uses the "non-mathsy" definition, unless I'm missing something

[Reid Barton]

If we're going to have the shift with no signs in mathlib then it would be good to find at least one source using this convention; I suspect it won't be easy.

[Johan Commelin]

This is the mathsy def, right: https://github.com/leanprover-community/lean-liquid/blob/master/src/for_mathlib/homological_complex_shift.lean#L34

[Reid Barton]

oh yes

[Reid Barton]

I was looking at the derived category or something, but I guess it unwinds to that definition

[Scott Morrison]

I would be very happy to just delete the current differential_object, particularly if it induces anyone to redo shift_functor!

[Johan Commelin]

I don't know of any uses of differential_object atm. So deleting it to aid this refactor is fine with me. It should be very easy to add it back afterwards.

[Joël Riou]

Recently, while constructing the derived category of an abelian category, I have had to develop more extensively the API for shifts. In addition to the shifts on categories, I have developed notions of functors commuting with shifts, and also natural transformations compatible with shifts, etc. The biggest problem with the current shift API I have faced is that when we have to prove a compatibility, internals of the monoidal_functor API always pop out, and this is messy...

Then, while porting some files (CategoryTheory.Shift, CategoryTheory.Triangulated.Rotate), I have tried to implement a "no MonoidalFunctor API leakage" policy: the internals of that API are almost only used in order to show some lemmas about shifts, and then in my new version of Triangulated.Rotate.lean, almost all the proofs are by aesop_cat! see !4#3039

[Joël Riou]

I have backported these improvements as #18670. The corresponding series of mathlib4 PR are !4#3039 !4#3046 !4#3047 !4#3070 !4#3072 (I guess I will have to update sha and add #align commands later).