AB4 and AB5 categories

Stream: mathlib4

[Jakob von Raumer]

In #6504, we have to decide whether to have the HasCoproducts assumption as a type class argument or as a field. I guess the preference depends on whether instances will rather have a HasCoproducts instance that's already defined prior to a AB4 instance? Any opinions? /cc @Joël Riou @Markus Himmel @Adam Topaz

[Joël Riou]

I would probably make this assumption a field, but this is not a strong preference.

[Adam Topaz]

I think it should remain a mixin.

[Adam Topaz]

If you do make it a field, then it would probably be better to use HasColimits (note that when you have cokernels, hence coequalizers, and all coproducts, that implies you have all colimits)

[Adam Topaz]

But if you keep it a mixin, then just using HasCoproducts works perfectly fine

[Dagur Asgeirsson]

I've generalized some of the file GrothendieckAxioms.lean in #19200. It defines a new class ABOfShape and redefines AB4 and AB5 in terms of that. Reviews welcome

@Jakob von Raumer @Isaac Hernando @Coleton Kotch

[Joël Riou]

How does this interact with #18510 by @Paul Reichert ?

[Markus Himmel]

As mentioned in https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/How.20to.20define.20.60GrothendieckCategory.60/near/481753810 I would be interested to hear what people think of making AbOfShape/AB4/AB5 into Prop-valued typeclasses.

[Paul Reichert]

Regarding the interactions of our PRs, no worries! I just rehearsed the merging of mine into @Dagur Asgeirsson's and there are no substantial merge conflicts; all proofs still typecheck. Only the @[stacks] attributes I added cause a few easy syntactical conflicts.

[Dagur Asgeirsson]

Markus Himmel said:

As mentioned in https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/How.20to.20define.20.60GrothendieckCategory.60/near/481753810 I would be interested to hear what people think of making AbOfShape/AB4/AB5 into Prop-valued typeclasses.

Ah, I hadn't seen that thread. I agree with Joël's comment there

[Paul Reichert]

Oh, I made a mistake and there actually is a small interaction of our PRs.
I have this variable declaration in GrothendieckCategory.lean:

variable [HasFilteredColimits C] [AB5 C] [Abelian C] [HasSeparator C] [GrothendieckCategory C]

After merging #19200, Lean complains on GrothendieckCategory C that it cannot synthesize an AB5 instance. The following works but is ugly:

variable [HasFilteredColimits C] [h : AB5 C] [Abelian C] [HasSeparator C] [@GrothendieckCategory C _ _ _ h _]

I suspect this has to do with the fact that AB5 is now just an abbrev and not a class itself.

[Paul Reichert]

I created a separate thread for this phenomenon.

[Dagur Asgeirsson]

Does it work if you change AB5 to

class AB5 [HasFilteredColimits C] where
  abOfShape (J : Type v) [SmallCategory J] [IsFiltered J] : ABOfShape J C

?

[Dagur Asgeirsson]

I mean without the "ugly" fix

[Paul Reichert]

That helps, provided I add `attribute [instance] AB5.abOfShape, too.
Actually, as discussed in https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/How.20to.20define.20.60GrothendieckCategory.60/near/481753810, I either way plan to make the AB5 instance into a field of GrothendieckCategory, so I guess this concrete situation is not a problem right now, but other people might stumble into similar problems. I have no idea why this happens here, I've never had the same problems with HasLimits.

[Dagur Asgeirsson]

Ok, I will change AB4 and AB5 etc to classes instead of abbrevs in #19200

[Dagur Asgeirsson]

#19912 proves AB4* for abelian groups and #19914 adds a bunch of new API which results in proofs of AB5 and AB4* for categories of R-modules and condensed R-modules in #19892. Reviews welcome!

#19914 slightly interferes with #18510 in that it proves a more general version of hasExactColimitsOfShape_obj_of_equiv. It's hasExactColimitsOfShape_transport, which takes a functor which preserves colimits of the given shape and finite limits, instead of an equivalence.

[Johan Commelin]

One downside of the new emoji-bot is that I have no idea which of the PRs was merged...

[Johan Commelin]

Turns out it is #19912

So the following are open. (But atm have merge conflicts or are blocked for other reasons.)

[Johan Commelin]

• #19914 adds a bunch of new API

[Johan Commelin]

• which results in proofs of AB5 and AB4* for categories of R-modules and condensed R-modules in #19892

[Dagur Asgeirsson]

I've solved the merge conflicts

[Dagur Asgeirsson]

#19939: AB5 and AB4* for categories of modules now follow easily.

[Dagur Asgeirsson]

The condensed version further depends on #19913 about colimits in sheaf categories

[Paul Reichert]

Dagur Asgeirsson said:

#19914 slightly interferes with #18510 in that it proves a more general version of hasExactColimitsOfShape_obj_of_equiv. It's hasExactColimitsOfShape_transport, which takes a functor which preserves colimits of the given shape and finite limits, instead of an equivalence.

Actually, HasExactColimitsOfShape.domain_of_functor (as I think it's called now) doesn't fully generalize hasExactColimitsOfShape_obj_of_equiv because the former requires an additional HasFiniteLimits instance. Would it be worth, then, to preserve the latter, perhaps giving it a name that is more consistent with the former?

[Paul Reichert]

Oh, there's also Adjunction.hasColimitsOfShape_of_equivalence which seems to prove exactly the same statement as my hasExactColimitsOfShape_obj_of_equiv, so it's definitely redundant. (Misread hasColimits for hasExactColimits)

[Dagur Asgeirsson]

Paul Reichert said:

Actually, HasExactColimitsOfShape.domain_of_functor (as I think it's called now) doesn't fully generalize hasExactColimitsOfShape_obj_of_equiv because the former requires an additional HasFiniteLimits instance. Would it be worth, then, to preserve the latter, perhaps giving it a name that is more consistent with the former?

Ah yes, of course. It is worth having both. We have a similar situation for equivalences/functors between the shapes