Abelian TopCat.Sheaf not synthesizing

Stream: mathlib4

[Brian Nugent]

I am currently working with sheaves of abelian groups on a topological space and would like to use the fact that they form an abelian category.

import Mathlib

open CategoryTheory

variable (X : TopCat)

#synth Abelian (Sheaf (Opens.grothendieckTopology X) AddCommGrpCat)

#synth Abelian (TopCat.Sheaf AddCommGrpCat X)

Currently the first #synth works but the second does not, even though they are the same by definition. I changed the definition of TopCat.Sheaf from a def to an abbrev in mathlib and it fixed this issue and I was still able to build mathlib. Is this a reasonable change? I know I can just write an instance of

Abelian (TopCat.Sheaf AddCommGrpCat X)

but I figure this change might help with other type inferences.

[Aaron Liu]

I think docs#TopCat.Sheaf.presheaf shouldn't be an abbrev if docs#TopCat.Sheaf is a def

[Aaron Liu]

so making TopCat.Sheaf also an abbrev would fix this

[Joël Riou]

I would think that most of the API about sheaves on topological spaces should be abbreviations referring to the more general notions for sites. However, there is still one aspect of the formalization of sheaves on topological spaces for which we do not have a complete general API yet: this is the functor of stalks and its properties (even though I have recently introduced the notion of point of a site https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Sites/Point/Basic.html).

[Brian Nugent]

Ok, I've opened a PR to change some of them. #34094

[Christian Merten]

Sorry, a bit late to the party. There is value in preserving an API barrier between sheaves on a topological space and the general notion. It allows users to use the docs#TopCat.Sheaf API without knowing about Grothendieck topologies. Making it an abbrev means that the site API will leak through more easily.