[Merged by Bors] - refactor(topology/sheaves/*): Make sheaf condition a Prop

[justus-springer]

Make sheaf_condition into a Prop and redefine the type of sheaves on a topological space X as a subtype of (opens X)ᵒᵖ ⥤ C.

---

Previously, sheaves on a topological space were defined as a structure with a Type-valued field sheaf_condition. Meanwhile, the sheaf condition for sheaves on sites is defined as a Prop. I don't have a strong preference towards either design, but for the purpose of connecting the two theories, the design should be consistent on both sides.

That said, changing the sheaf condition to a Prop does seem to simplify things a little, as indicated by the net negative diff. The most changes are in unique_gluing, where some definitions have become no longer necessary.

[jcommelin]

I think the net size of the diff is a convincing argument for this PR. But I haven't done much with sheaves yet myself (besides reviewing). So I would like to hear from @b-mehta and/or @semorrison as well.

[jcommelin]

Is there a reason for this change? I find it less readable.
Idem in several other places.

[justus-springer]

Thanks for bringing this up. sheaf C X is now a subtype of presheaf C X, hence the projection sheaf.presheaf no longer exists. I was considering adding it back in as an alias for subtype.val, but then you'd have to change quite a few rws to erws, for example when applying naturality of a sheaf homomorphism. This is essentially because the type of sheaf homomorphisms F ⟶ G is now defined as F.val ⟶ G.val, not F.presheaf ⟶ G.presheaf.

I guess you could make sheaf.presheaf an abbreviation for subtype.val, but this felt a little weird to me as the former is longer than the latter.

[semorrison]

I haven't read this carefully yet, but I'm also concerned here.

1. I don't think .presheaf being longer than .1 is a problem; it's a good thing!
2. What is the motivation for changing sheaf to a subtype, anyway? You lose the meaningful names, and gain ... what?

[justus-springer]

You gain consistency in the library: Sheaves on sites are already defined as a subtype: docs#category_theory.Sheaf. As I wrote above, I don't have a preference towards either design, but for the purpose of connecting the theories, I need consistency between them.

Personally, I think the mental jump between a sheaf and a presheaf isn't that high, so I'd say it's fine writing .1 or .val everywhere. I see that opinions can differ on that. All I can say is that #9609 would be a lot uglier if the design on both sides is not consistent.

[justus-springer]

As far as I can see, it all depends on whether you want the sheaf condition to be a Prop or a Type. If you want it to be a Prop, then defining sheaf as a subtype is the most natural choice. Then I don't really see the point of introducing the alias sheaf.presheaf, as it's just an extra layer of definition that needs to be unfolded and that makes everything longer. And I don't think writing F.val or F.1 instead of F.presheaf is that bad, it's done all the time for sheaves on sites. Of course, the alternative would be to make the sheaf condition a Type everywhere, but then the library of sheaves on sites had to be changed. And there are some formulations of the sheaf condition (e.g. unique gluings, amalgamations) which are clearly stated easier as a Prop instead of a Type.

[semorrison]

Okay, I will accept the consistency argument. :-) (That said, maybe the sheaves on sites development should have used a structure with named fields rather than relying on subtype, but that question need not be addressed today!)

[semorrison]

I've marked as approved, but will wait a moment to hit merge in case @b-mehta or @jcommelin have further comments.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests

[b-mehta]

Apologies for not taking a closer look at this - I'm on board with making the sheaf condition a Prop: the question of whether Sheaf should be a subtype or structure is one I'm ambivalent on, so I have no objections to this PR!

[alreadydone]

The only changes I needed to make to an existing file is adding .some when extracting the is_limit condition; just a slight inconvenience!

[alreadydone]

Some comments have not been edited accordingly and still refers to names involving sheaf_condition instead of is_sheaf and equiv instead of iff, for example

mathlib/src/topology/sheaves/sheaf_condition/opens_le_cover.lean

Line 90 in c1f754b

`sheaf_condition_equiv_sheaf_condition_opens_le_cover`).

I've noticed this elsewhere in mathlib so am not sure if it's a priority to fix.

[justus-springer]

@alreadydone thanks for noticing! It seems like I forgot to change a few names in the comments. I fixed it here: #9807