CategoryTheory.generate_discretePresieve_mem
theorem CategoryTheory.generate_discretePresieve_mem :
∀ (α : Type u),
CategoryTheory.Sieve.generate (CategoryTheory.discretePresieve α) ∈
CategoryTheory.typesGrothendieckTopology.sieves α
This theorem states that for any type `α`, the smallest sieve generated by the discrete presieve on `α` is a member of the sieves of the Grothendieck topology associated with the category of all types for `α`. In other words, the smallest sieve that contains all arrows in the discrete presieve (which only includes arrows whose domain is a singleton) is included in the collection of sieves that cover every element of `α` in the Grothendieck topology for the category of all types.
More concisely: The smallest sieve containing the discrete presieve is a sub-sieve of every sieve in the Grothendieck topology for the category of all types.
|
CategoryTheory.isSheaf_yoneda'
theorem CategoryTheory.isSheaf_yoneda' :
∀ {α : Type u},
CategoryTheory.Presieve.IsSheaf CategoryTheory.typesGrothendieckTopology (CategoryTheory.yoneda.obj α)
The theorem `CategoryTheory.isSheaf_yoneda'` states that for any type `α`, the Yoneda embedding applied to `α` is indeed a sheaf with respect to the Grothendieck topology for the category of all types. In other words, this theorem establishes the fact that the Yoneda embedding preserves the structure of sheaves, a fundamental concept in Grothendieck's theory of schemes and toposes, under the particular Grothendieck topology associated with the category of all types, where a sieve is considered a covering if it is jointly surjective.
More concisely: The Yoneda embedding of a type `α` is a sheaf in the category of types under the Grothendieck topology where a sieve is covering if it is jointly surjective.
|