CategoryTheory.coherentTopology.subcanonical
theorem CategoryTheory.coherentTopology.subcanonical :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Precoherent C],
CategoryTheory.Sheaf.Subcanonical (CategoryTheory.coherentTopology C)
The theorem states that the coherent topology on a precoherent category is subcanonical. In other words, given a category `C` that is precoherent, the coherent topology on `C` is less than or equal to the canonical topology. This means that every representable functor is a sheaf with respect to the coherent topology.
More concisely: In a precoherent category, the coherent topology is finer than the canonical topology, making every representable functor a sheaf.
|
CategoryTheory.coherentTopology.isSheaf_yoneda_obj
theorem CategoryTheory.coherentTopology.isSheaf_yoneda_obj :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Precoherent C] (W : C),
CategoryTheory.Presieve.IsSheaf (CategoryTheory.coherentTopology C) (CategoryTheory.yoneda.obj W)
This theorem states that for any category `C` that is both precoherent and a category (in the sense of Category Theory), and for any object `W` in that category `C`, the Yoneda functor applied to that object `W` is a sheaf with respect to the coherent topology on `C`.
In other words, the Yoneda functor, which maps each object to the set of morphisms from that object to `W`, preserves the property of being a sheaf under the coherent topology. This means that it satisfies the sheaf condition for every sieve in the topology, where a sieve is a collection of morphisms that is closed under precomposition with morphisms within the category. This theorem is significant because sheaves are central to many areas of mathematics, including algebraic geometry and number theory.
More concisely: The Yoneda functor maps any object in a precoherent category to a sheaf with respect to the coherent topology.
|