[Merged by Bors] - feat(category_theory/sites/*): Dense subsite

[erdOne]

Defined cover_dense functors as functors into sites such that each object can be covered by images of the functor.
Proved that for a cover_dense functor G, any morphisms of presheaves G ⋙ ℱ ⟶ G ⋙ ℱ' can be glued into a
morphism ℱ ⟶ ℱ'.

---

[b-mehta]

Since you are working in this area, I should point out to you the known errata in Johnstone's definitions in this area: https://ncatlab.org/nlab/show/dense+sub-site#problems_with_another_definition, and further that the definitions of the comparison lemma are different across the Elephant, nLab, stacks, EGA and Caramello's topos text. My suggestion is to make sure you have a compiling version of the Comparison Lemma before merging too many definitions.

[jcommelin]

@erdOne I don't know this part of category theory too well. Bhavik's suggestion sounds like a good one. Can you please point out once you have a sorry-free proof of that comparison lemma (and where to find it)?

[erdOne]

There is a sorry free proof of the comparison lemma over at #9785

mathlib/src/category_theory/sites/comparison_lemma.lean

Lines 192 to 202 in 2bbac6f

	/--
	Cover-dense functors induces an equivalence of categories of sheaves.
	This is known as the comparison lemma. It requires that the sites are small and the target category
	is complete.
	-/
	noncomputable
	def Sheaf_iso (H : cover_dense K G) [has_limits A] : Sheaf (H.induced_topology) A ≌ Sheaf K A :=
	Sheaf_iso_of_dense_cover_preserving_cover_lifting A H
	(induced_topology_cover_preserving G K (λ _ T, H.functor_pullback_pushforward_covering T))
	(induced_topology_cover_lifting G K (λ _ T, H.functor_pullback_pushforward_covering T))

[alreadydone]

Hi @erdOne , thanks for the work. I now understand how to use this PR to extend a B-sheaf hom (I think I just hadn't read the code carefully enough), and would like to use this in my Gamma-Spec adjunction PR instead of my basis_le approach. I only have two issues with this PR:

• Can you just wrap sheaf_hom_restrict_eq and sheaf_hom_eq into an equiv with to_fun = sheaf_hom H and inv_fun = whisker_left G.op ? Then I wouldn't need an extensionality lemma and can directly apply the injectivity of the inverse, for example.

• Can you remove the assumption that ℱ is a sheaf? In my work in the topological case I only needed ℱ' to be a sheaf, and I see in app_hom you only used ℱ'.property, so it shouldn't be too hard to remove?

In addition, I would like to develop API in the situation of topological spaces, giving the hom extension equiv for (pre)sheaves there, and show that a functor into opens X is cover_dense iff its image is a basis. These should probably be put under topology/sheaves and is maybe out of scope of this PR.

[alreadydone]

lgtm! My Gamma-Spec adjunction work #9802 has been refactored to use this PR so I'm also eager to get this merged.

[jcommelin]

I think you can do

Suggested change

	begin
	have α' := sheaf_yoneda_hom H α,
	exact { app := λ X, yoneda.preimage (α'.app X),
	naturality' := λ X Y f, yoneda.map_injective (by simpa using α'.naturality f) }
	end
	have α' := sheaf_yoneda_hom H α,
	{ app := λ X, yoneda.preimage (α'.app X),
	naturality' := λ X Y f, yoneda.map_injective (by simpa using α'.naturality f) }

[erdOne]

Not really, but let ... in works for me.

[jcommelin]

What does simps do with the let statement? Does the output of simps? look the way you want it to be?

[erdOne]

It actually gives quite a decent looking lemma.
But now that I think about it, I probably want to make the implementation details more opaque, so I removed them.

[jcommelin]

I suggested one more change. After that, I this can be merged. Thanks!

bors d+

[bors]

✌️ erdOne can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[erdOne]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

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

[alreadydone]

This and another sheaf_iso above don't follow the same format. And can't this simply be presheaf_iso H i with some arguments made explicit? Or is it for the purpose of simps that you wrote down the individual fields? (I only noticed this after seeing a review message sent to my mailbox.)