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.)

Estimated changes