TopCat.Presheaf.toTypes_isSheaf
theorem TopCat.Presheaf.toTypes_isSheaf : ∀ (X : TopCat) (T : ↑X → Type u), (X.presheafToTypes T).IsSheaf
This theorem asserts that for every topological space `X` and for every type family `T` indexed over the points of `X`, the presheaf of (not necessarily continuous) functions to `T` forms a sheaf. Note that this result also holds when we consider dependent functions to a type family `T`, hence the proof is done for the more general case.
More concisely: For every topological space X and type family T indexed over X, the presheaf of functions from X to T forms a sheaf.
|
TopCat.Presheaf.toType_isSheaf
theorem TopCat.Presheaf.toType_isSheaf : ∀ (X : TopCat) (T : Type u), (X.presheafToType T).IsSheaf
This theorem states that for any topological space `X` and any target type `T`, the presheaf of functions (not necessarily continuous) from `X` to `T` satisfies the sheaf condition. In the context of category theory, a presheaf assigns to each open set in a topological space a set or type, and to each inclusion of open sets a function on the assigned types. The sheaf condition ensures that this assignment is "local", in the sense that the value on a larger open set is completely determined by the values on smaller open sets that cover it. This theorem is a fundamental result in sheaf theory, which is a branch of algebraic topology.
More concisely: Given any topological space X and type T, the presheaf of functions from X to T satisfies the sheaf condition.
|