CategoryTheory.SheafOfTypes.cond
theorem CategoryTheory.SheafOfTypes.cond :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
(self : CategoryTheory.SheafOfTypes J), CategoryTheory.Presieve.IsSheaf J self.val
The theorem `CategoryTheory.SheafOfTypes.cond` states that for any category `C` and any Grothendieck topology `J` on `C`, any sheaf of types over `J` is a sheaf in the sense of the `CategoryTheory.Presieve.IsSheaf` definition. In other words, for any object `X` in `C` and any sieve `S` in the topology `J` at `X`, the presheaf `self.val` satisfies the sheaf condition for the arrows of `S`.
More concisely: For any category `C` and Grothendieck topology `J` on `C`, a sheaf of types over `J` satisfies the sheaf condition with respect to `J` in the sense of `CategoryTheory.Presieve.IsSheaf`.
|
CategoryTheory.Presieve.isSheaf_bot
theorem CategoryTheory.Presieve.isSheaf_bot :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)},
CategoryTheory.Presieve.IsSheaf ⊥ P
The theorem `CategoryTheory.Presieve.isSheaf_bot` states that for any category `C` and any presheaf `P` on `C`, `P` is a sheaf for the bottom (or trivial) Grothendieck topology. In other words, regardless of the specific category or the presheaf, if the Grothendieck topology is the trivial one, then the presheaf always satisfies the sheaf condition.
More concisely: For any category `C` and presheaf `P` on `C`, `P` is a sheaf for the trivial Grothendieck topology.
|
CategoryTheory.SheafOfTypes.Hom.ext'
theorem CategoryTheory.SheafOfTypes.Hom.ext' :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
{X Y : CategoryTheory.SheafOfTypes J} (f g : X ⟶ Y), f.val = g.val → f = g
This theorem, in the context of category theory, states that for any category `C` with a Grothendieck topology `J`, and for any two sheaves of types `X` and `Y` over `J`, if there are two morphisms `f` and `g` from `X` to `Y`, and if these two morphisms have the same value, then `f` and `g` are equal. In simpler terms, it states that two morphisms between the same pair of sheaves are identical if their values are the same.
More concisely: In a category with a Grothendieck topology, two morphisms between the same pair of sheaves are equal if and only if they have the same value.
|
CategoryTheory.Presieve.IsSheaf.isSheafFor
theorem CategoryTheory.Presieve.IsSheaf.isSheafFor :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (J : CategoryTheory.GrothendieckTopology C)
{P : CategoryTheory.Functor Cᵒᵖ (Type w)},
CategoryTheory.Presieve.IsSheaf J P →
∀ (R : CategoryTheory.Presieve X),
CategoryTheory.Sieve.generate R ∈ J.sieves X → CategoryTheory.Presieve.IsSheafFor P R
This theorem asserts that for any category `C`, Grothendieck topology `J` on `C`, object `X` in `C`, and presheaf `P` (which is a functor from the opposite category of `C` to the category of types), if `P` is a sheaf for the topology `J`, then for any presieve `R` on `X`, if the sieve generated by `R` belongs to the sieves of `X` in `J`, then `P` is a sheaf for `R`.
In other words, if a presheaf satisfies the sheaf condition for every sieve in a topology, it will also satisfy the sheaf condition for any presieve that generates a sieve in that topology.
More concisely: If a presheaf is a sheaf for a Grothendieck topology, then it is a sheaf for any presieve generating a sieve in that topology.
|
CategoryTheory.Sieve.forallYonedaIsSheaf_iff_colimit
theorem CategoryTheory.Sieve.forallYonedaIsSheaf_iff_colimit :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (S : CategoryTheory.Sieve X),
(∀ (W : C), CategoryTheory.Presieve.IsSheafFor (CategoryTheory.yoneda.obj W) S.arrows) ↔
Nonempty (CategoryTheory.Limits.IsColimit S.arrows.cocone)
This theorem states that for any category `C` and any object `X` in `C`, a sieve `S` on `X` is a colimit if and only if all Yoneda presheaves satisfy the sheaf condition for `S`. In other words, for every object `W` in `C`, the Yoneda presheaf `CategoryTheory.yoneda.obj W` is a sheaf for the arrows of `S`, if and only if there exists a colimit for the cocone formed by the arrows of `S`. Here, a sieve is a certain kind of subset of the arrows (morphisms) with codomain `X`, the Yoneda presheaf is a functor associated with the object `W`, and a colimit is a universal cocone for a given diagram in a category.
More concisely: A sieve on an object X in a category is a colimit if and only if the Yoneda presheaf satisfies the sheaf condition for all arrows with codomain X in the category.
|
CategoryTheory.Presieve.isSheaf_pretopology
theorem CategoryTheory.Presieve.isSheaf_pretopology :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)}
[inst_1 : CategoryTheory.Limits.HasPullbacks C] (K : CategoryTheory.Pretopology C),
CategoryTheory.Presieve.IsSheaf (CategoryTheory.Pretopology.toGrothendieck C K) P ↔
∀ {X : C}, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor P R
This theorem states that for a topology that is generated by a basis, the sheaf condition needs to be checked only on the basis presieves. In other words, given a category `C`, a contravariant functor `P` from `C` to the category of types, and a pretopology `K` on `C`, a presheaf `P` is a sheaf for the Grothendieck topology associated to `K` if and only if for every object `X` in `C` and every covering `R` in the coverings of `X` according to `K`, `P` satisfies the sheaf condition for `R`. This implies that the sheaf condition can be verified locally on the basic coverings defined by the pretopology.
More concisely: A contravariant functor is a sheaf for a given Grothendieck topology if it satisfies the sheaf condition on coverings defined by the topology's basis.
|
CategoryTheory.Presieve.isSheaf_iso
theorem CategoryTheory.Presieve.isSheaf_iso :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)}
(J : CategoryTheory.GrothendieckTopology C) {P' : CategoryTheory.Functor Cᵒᵖ (Type w)},
(P ≅ P') → CategoryTheory.Presieve.IsSheaf J P → CategoryTheory.Presieve.IsSheaf J P'
The theorem `CategoryTheory.Presieve.isSheaf_iso` states that the property of being a sheaf is preserved by isomorphism. In particular, it says that for a given category `C`, functor `P`, Grothendieck topology `J`, and another functor `P'`, if `P` is isomorphic to `P'` (denoted by `P ≅ P'` in Lean), then if `P` is a sheaf for the topology `J`, it follows that `P'` is also a sheaf for the topology `J`. In other words, isomorphism does not affect the sheaf property of a functor with respect to a given topology.
More concisely: If functors `P` and `P'` are isomorphic in a category `C` with respect to a Grothendieck topology `J`, then `P` being a sheaf implies that `P'` is also a sheaf for `J`.
|
CategoryTheory.SheafOfTypes.Hom.ext
theorem CategoryTheory.SheafOfTypes.Hom.ext :
∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.GrothendieckTopology C}
{X Y : CategoryTheory.SheafOfTypes J} (x y : X.Hom Y), x.val = y.val → x = y
This theorem states that for any category 'C' with a Grothendieck topology 'J', and for any two sheaves of types 'X' and 'Y' over this category, if two morphisms 'x' and 'y' from 'X' to 'Y' have the same underlying function (i.e., 'x.val = y.val'), then these two morphisms are indeed the same (i.e., 'x = y'). Essentially, it establishes the injectivity of the function assigning to each morphism of sheaves its underlying function.
More concisely: If 'C' is a category with a Grothendieck topology 'J', and 'X' and 'Y' are sheaves over 'C', then two morphisms 'x' and 'y' from 'X' to 'Y' with equal underlying functions (i.e., x.val = y.val) are equal as morphisms (i.e., x = y).
|