CategoryTheory.Sheaf.isSheaf_of_representable
theorem CategoryTheory.Sheaf.isSheaf_of_representable :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type v))
[inst_1 : P.Representable], CategoryTheory.Presieve.IsSheaf (CategoryTheory.Sheaf.canonicalTopology C) P
The theorem `CategoryTheory.Sheaf.isSheaf_of_representable` states that for any category `C` and any representable functor `P` from the opposite category `Cᵒᵖ` to the category of types `Type v`, `P` is a sheaf for the canonical topology on `C`. In other words, for every category and every representable functor defined on its opposite, the functor is sheaf for the finest (or largest) topology where all representable presheaves are sheaves. This essentially says that representable functors satisfy the sheaf condition for any sieve in the canonical topology.
More concisely: A representable functor from the opposite category of a category to the category of types is a sheaf for the canonical topology.
|
CategoryTheory.Sheaf.le_finestTopology
theorem CategoryTheory.Sheaf.le_finestTopology :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Ps : Set (CategoryTheory.Functor Cᵒᵖ (Type v)))
(J : CategoryTheory.GrothendieckTopology C),
(∀ P ∈ Ps, CategoryTheory.Presieve.IsSheaf J P) → J ≤ CategoryTheory.Sheaf.finestTopology Ps
This theorem states that for any given category `C` and a set of covariant functors `Ps` from the opposite of `C` to some type `v`, along with a Grothendieck topology `J` on `C`, if each functor `P` in `Ps` is a sheaf for the topology `J`, then `J` is a subtopology of the finest (largest) Grothendieck topology for which all the functors in `Ps` are sheaves. This is a statement about the relationship between a collection of sheaves, a topology, and the finest topology under which those sheaves are still sheaves.
More concisely: If `C` is a category, `Ps` is a set of covariant functors from `C^op` to some type `v`, and `J` is a Grothendieck topology on `C` such that each functor `P` in `Ps` is a sheaf for `J`, then `J` is a subtopology of the finest Grothendieck topology containing all `P` in `Ps` as sheaves.
|
CategoryTheory.Sheaf.isSheafFor_trans
theorem CategoryTheory.Sheaf.isSheafFor_trans :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type v))
(R S : CategoryTheory.Sieve X),
CategoryTheory.Presieve.IsSheafFor P R.arrows →
(∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
S.arrows f → CategoryTheory.Presieve.IsSeparatedFor P (CategoryTheory.Sieve.pullback f R).arrows) →
(∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
R.arrows f → CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.pullback f S).arrows) →
CategoryTheory.Presieve.IsSheafFor P S.arrows
This theorem states that given two sieves `R` and `S` over a category `C` and an object `X` in `C`, to demonstrate that a presheaf `P` is a sheaf for `S`, we can instead show three things:
1. `P` is a sheaf for `R`,
2. `P` is a sheaf for the pullback of `S` along any arrow in `R`, and
3. `P` is separated for the pullback of `R` along any arrow in `S`.
A presheaf `P` is a sheaf for a sieve `R` if it satisfies certain properties that allow it to "glue" local data defined on `R` into a global section in `P`. Separation for a presheaf involves uniqueness of such "gluing".
The theorem is an auxiliary lemma used in the construction of the finest topology, and it is adapted from the Elephant book, Lemma C2.1.7(ii), with some modifications suggested in a Math StackExchange post.
More concisely: Given a presheaf `P` on a category `C`, to show that `P` is a sheaf for a sieve `S`, it suffices to prove that `P` is a sheaf for the generating sieve `R`, is a sheaf for the pullback of `S` along any arrow in `R`, and is separated for the pullback of `R` along any arrow in `S`.
|
CategoryTheory.Sheaf.sheaf_for_finestTopology
theorem CategoryTheory.Sheaf.sheaf_for_finestTopology :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type v)}
(Ps : Set (CategoryTheory.Functor Cᵒᵖ (Type v))),
P ∈ Ps → CategoryTheory.Presieve.IsSheaf (CategoryTheory.Sheaf.finestTopology Ps) P
This theorem, `CategoryTheory.Sheaf.sheaf_for_finestTopology`, asserts that for any category `C` and a set `Ps` of presheaves (functors from the opposite category `Cᵒᵖ` to the category of types `Type v`), if a presheaf `P` is an element of `Ps`, then `P` is a sheaf for the finest (largest) Grothendieck topology on `Ps`. In other words, the presheaf `P` satisfies the sheaf condition for every sieve in the Grothendieck topology generated by `Ps`.
More concisely: For any category `C` and a set `Ps` of presheaves on `C`, if a presheaf `P` is in `Ps`, then `P` is a sheaf with respect to the finest Grothendieck topology generated by `Ps`.
|
CategoryTheory.Sheaf.isSheaf_yoneda_obj
theorem CategoryTheory.Sheaf.isSheaf_yoneda_obj :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
CategoryTheory.Presieve.IsSheaf (CategoryTheory.Sheaf.canonicalTopology C) (CategoryTheory.yoneda.obj X)
The theorem `CategoryTheory.Sheaf.isSheaf_yoneda_obj` states that for any category `C`, and for any `X` in `C`, the representable presheaf `yoneda.obj X` is a sheaf with respect to the canonical topology on `C`. The canonical topology is defined as the finest (largest) topology for which every representable presheaf is a sheaf. This means that `yoneda.obj X` satisfies the sheaf condition for every sieve in the canonical topology on `C`.
More concisely: For any category C and object X in C, the representable presheaf yoneda.obj X is a sheaf with respect to the canonical topology on C.
|
CategoryTheory.Sheaf.isSheafFor_bind
theorem CategoryTheory.Sheaf.isSheafFor_bind :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type v))
(U : CategoryTheory.Sieve X) (B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → CategoryTheory.Sieve Y),
CategoryTheory.Presieve.IsSheafFor P U.arrows →
(∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), CategoryTheory.Presieve.IsSheafFor P (B hf).arrows) →
(∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y),
CategoryTheory.Presieve.IsSeparatedFor P (CategoryTheory.Sieve.pullback g (B h)).arrows) →
CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.bind U.arrows B).arrows
The theorem `CategoryTheory.Sheaf.isSheafFor_bind` is a result in category theory, stating that for a given category `C`, an object `X` in `C`, a functor `P` from the opposite category of `C` to the category of types, a sieve `U` on `X`, and a dependent function `B` that assigns to each morphism in `U` a sieve on its domain, if `P` is a sheaf for `U`, `P` is a sheaf for each sieve in `B`, and `P` is separated for any pullback of any sieve in `B`, then `P` is a sheaf for the sieve obtained by binding `U` with `B`. This result is useful in demonstrating that functor `P` satisfies the sheaf condition for a certain sieve, which is a key notion in the theory of sheaves in category theory. This theorem is an adaptation from the Elephant book, Lemma C2.1.7(i) with suggestions from a Math StackExchange answer.
More concisely: If `P: C^op -> Type` is a sheaf for a sieve `U` on `X` in `C`, and for each morphism `f in U` and sieve `V on Dom(f)`, `P` is a sheaf for `V` and separated in the pullback of `U` along `f`, then `P` is a sheaf for the sieve obtained by binding `U` and `{B(f)}` over each `f in U`.
|
CategoryTheory.Sheaf.Subcanonical.isSheaf_of_representable
theorem CategoryTheory.Sheaf.Subcanonical.isSheaf_of_representable :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C},
CategoryTheory.Sheaf.Subcanonical J →
∀ (P : CategoryTheory.Functor Cᵒᵖ (Type v)) [inst_1 : P.Representable], CategoryTheory.Presieve.IsSheaf J P
The theorem `CategoryTheory.Sheaf.Subcanonical.isSheaf_of_representable` states that if `J` is a subcanonical Grothendieck topology in a category `C`, then any representable presheaf `P` (a presheaf that is naturally isomorphic to the representable functor) in `C` is a `J`-sheaf. In other words, the presheaf `P` satisfies the sheaf condition for every sieve in the topology `J`, which means that it is a sheaf with respect to the topology `J`.
More concisely: If `J` is a subcanonical Grothendieck topology on a category `C`, then every representable presheaf in `C` is a `J`-sheaf.
|
CategoryTheory.Sheaf.Subcanonical.of_yoneda_isSheaf
theorem CategoryTheory.Sheaf.Subcanonical.of_yoneda_isSheaf :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C),
(∀ (X : C), CategoryTheory.Presieve.IsSheaf J (CategoryTheory.yoneda.obj X)) →
CategoryTheory.Sheaf.Subcanonical J
The theorem `CategoryTheory.Sheaf.Subcanonical.of_yoneda_isSheaf` states that for any category `C` and any Grothendieck topology `J` on `C`, if every object `X` in `C` satisfies the condition that the functor `yoneda.obj X` is a `J`-sheaf, then `J` is subcanonical. In other words, if all representable functors (given by the Yoneda embedding) are `J`-sheaves, then the topology `J` is smaller than or equal to the canonical topology, and thus is considered subcanonical.
More concisely: If every representable functor in a category with a Grothendieck topology is a sheaf for that topology, then the topology is subcanonical.
|