Definition of B-sheaves

Stream: Is there code for X?

[Gareth Ma]

Is there a definition of B-sheaves in Mathlib, or e.g. how should I construct a sheaf on a topological space by specifying the data on the basis (with some proofs)? Maybe equivalently, is 009O in Mathlib?

Math.SE tells me that the corresponding notion for Grothendieck topologies should be a dense sub-site, for which I find docs#CategoryTheory.Functor.IsDenseSubsite.sheafEquiv, but I am not familiar enough with Grothendieck topologies (yet) to tell if it's even correct lol

[Gareth Ma]

(deleted)

[Andrew Yang]

Maybe docs#TopCat.Opens.coverDense_inducedFunctor and docs#CategoryTheory.Functor.sheafInducedTopologyEquivOfIsCoverDense

[Gareth Ma]

Okay I think I understand, thanks.