The category of sheaves is balanced.

Stream: maths

[Andrew Yang]

Is it true that if C is a balanced category, then the category of C-valued sheaves over a site is balanced? Is there an easy proof?
Actually I only care about when C is Type or Module R, and mathlib already know that the latter is abelian.
For the former, to show that every mono is regular, I could either show that there exists a subobject classifier, or show that functors that creates pushouts and pullbacks reflects regular monos and do the heavy-lifting in the category of presheaves. However, both approaches seem to have constraints on the universe and seems to be quite some work, and I am wondering if there is a better way forward.

[Reid Barton]

I'm not sure what is in mathlib already, but I would suggest first proving that in a sheaf category, a pushout of a mono is also a pullback square. You can prove it in a somewhat long-winded way from the Giraud axioms, or by checking it in Set and using that sheaves form a left-exact localization.

[Andrew Yang]

Thanks for the reply! I think we are quite far from Giraud's axioms, so I'll look into the second approach. If I understand it correctly, I should first check in Type u and then Cᵒᵖ ⥤ Type u and then Sheaf J (Type u)? And I guess this only holds over small sites?

[Reid Barton]

Andrew Yang said:

If I understand it correctly, I should first check in Type u and then Cᵒᵖ ⥤ Type u and then Sheaf J (Type u)?

Yes exactly.

And I guess this only holds over small sites?

I don't know what happens if you take sheaves (of small sets) on a large site (usually it is not a very useful thing to do).

[Kevin Buzzard]

Sheaves on a large site are scary, this is exactly why Scholze spends several of the first few pages of his course on condensed sets going on about strong limit cardinals and concludes that the definition of condensed set is not your first guess.