Commit 2024-11-27 09:56 3942daa8
View on Github →chore(CategoryTheory/Sites): split DenseSubsite (#19519)
The file CategoryTheory.Sites.DenseSubsite
is split into DenseSubsite.Basic
and DenseSubsite.SheafEquiv
, the latter containing the equivalence of categories of sheaves in case suitable limits exists. The file Sites.InducedTopology
is also moved to Sites.DenseSubsite
. (This split prepares for #19444 where the equivalence of categories of sheaves is obtained under a somewhat weaker condition.)