CategoryTheory.Presheaf.isSheaf_iff_isLimit_pretopology
theorem CategoryTheory.Presheaf.isSheaf_iff_isLimit_pretopology :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} A] (P : CategoryTheory.Functor Cᵒᵖ A)
[inst_2 : CategoryTheory.Limits.HasPullbacks C] (K : CategoryTheory.Pretopology C),
CategoryTheory.Presheaf.IsSheaf (CategoryTheory.Pretopology.toGrothendieck C K) P ↔
∀ ⦃X : C⦄,
∀ R ∈ K.coverings X,
Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone (CategoryTheory.Sieve.generate R).arrows.cocone.op))
The theorem `CategoryTheory.Presheaf.isSheaf_iff_isLimit_pretopology` states that for any category `C`, any category `A`, any presheaf `P` from the opposite of `C` to `A`, and any pretopology `K` on `C`, the presheaf `P` is a sheaf for the Grothendieck topology generated by `K` if and only if for every covering presieve `R` of `K` for any object `X` in `C`, there exists a limit cone (i.e., the cone is a limit) for the functor `P` applied to the opposite of the cone generated by the set of arrows contained in the sieve generated by `R`. The existence of such a limit cone represents the ability to "glue" sections of the presheaf together along the covering defined by `R`.
More concisely: A presheaf on a category is a sheaf for a given Grothendieck topology if and only if for every covering sieve, the presheaf restricts to a limit on the cone generated by the sieve.
|
CategoryTheory.Sheaf.Hom.mono_of_presheaf_mono
theorem CategoryTheory.Sheaf.Hom.mono_of_presheaf_mono :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C)
(A : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} A] {F G : CategoryTheory.Sheaf J A} (f : F ⟶ G)
[h : CategoryTheory.Mono f.val], CategoryTheory.Mono f
This theorem states that if a morphism `f` between two sheaves `F` and `G` in the context of a Grothendieck topology `J` is monic (i.e., left-cancellative) when seen as a presheaf morphism, then `f` is monic as a sheaf morphism as well. The theorem applies to any categories `C` and `A`. This is necessary to avoid a recursive loop in the class search, as a sheaf morphism is monic if and only if it is monic as a presheaf morphism under suitable conditions.
More concisely: If a morphism between sheaves is monic as a presheaf morphism in a Grothendieck topology, then it is also monic as a sheaf morphism.
|
CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget
theorem CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A' : Type u₂}
[inst_1 : CategoryTheory.Category.{max v₁ u₁, u₂} A'] (J : CategoryTheory.GrothendieckTopology C)
(P' : CategoryTheory.Functor Cᵒᵖ A') (s : CategoryTheory.Functor A' (Type (max v₁ u₁)))
[inst_2 : CategoryTheory.Limits.HasLimits A'] [inst_3 : CategoryTheory.Limits.PreservesLimits s]
[inst_4 : s.ReflectsIsomorphisms],
CategoryTheory.Presheaf.IsSheaf J P' ↔ CategoryTheory.Presheaf.IsSheaf J (P'.comp s)
In the context of a concrete category `(A, s)`, where the forgetful functor `s : A ⥤ Type v` both preserves limits and reflects isomorphisms, and `A` has limits, this theorem states that an `A`-valued presheaf `P : Cᵒᵖ ⥤ A` is a sheaf if and only if its underlying `Type`-valued presheaf `P ⋙ s : Cᵒᵖ ⥤ Type` is a sheaf. It's important to note that this lemma is applicable for "algebraic" categories, such as groups, abelian groups, and rings. However, it doesn't apply to the category of topological spaces, topological rings, and similar, since the property of reflecting isomorphisms doesn't hold for these.
More concisely: In a concrete category with a preserving and reflecting forgetful functor, an `A`-valued presheaf is a sheaf if and only if its underlying `Type`-valued presheaf is a sheaf (applicable to algebraic categories).
|
CategoryTheory.Presheaf.isLimit_iff_isSheafFor_presieve
theorem CategoryTheory.Presheaf.isLimit_iff_isSheafFor_presieve :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} A] (P : CategoryTheory.Functor Cᵒᵖ A) {X : C}
(R : CategoryTheory.Presieve X),
Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone (CategoryTheory.Sieve.generate R).arrows.cocone.op)) ↔
∀ (E : Aᵒᵖ), CategoryTheory.Presieve.IsSheafFor (P.comp (CategoryTheory.coyoneda.obj E)) R
The theorem `CategoryTheory.Presheaf.isLimit_iff_isSheafFor_presieve` states that for any category `C`, any category `A`, any presheaf `P : Cᵒᵖ ⥤ A` and any presieve `R` on an object `X` in `C`, the natural cone associated with `P` and the sieve generated by `R` is a limit cone if and only if for all objects `E` in the opposite category of `A`, the functor `Hom (E, P -)` is a sheaf with respect to the presieve `R`. Here, `Hom (E, P -)` is the functor that sends an object to its hom-set with `P` and a morphism to the induced function on hom-sets. This theorem provides a characterization of limit cones in terms of sheaves.
More concisely: A presheaf's natural cone is a limit cone if and only if the functor that sends an object to its hom-set with the presheaf and a morphism to the induced function on hom-sets is a sheaf for all objects in the opposite category, with respect to the given presieve.
|
CategoryTheory.Presheaf.w
theorem CategoryTheory.Presheaf.w :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} A] {U : C} (R : CategoryTheory.Presieve U)
(P : CategoryTheory.Functor Cᵒᵖ A) [inst_2 : CategoryTheory.Limits.HasProducts A]
[inst_3 : CategoryTheory.Limits.HasPullbacks C],
CategoryTheory.CategoryStruct.comp (CategoryTheory.Presheaf.forkMap R P) (CategoryTheory.Presheaf.firstMap R P) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.Presheaf.forkMap R P)
(CategoryTheory.Presheaf.secondMap R P)
The theorem `CategoryTheory.Presheaf.w` states that for any category `C` and `A`, a codomain `U` in `C`, a set of arrows `R` with codomain `U` (a presieve on `U`), and a presheaf `P` from the opposite category of `C` to `A`, if `A` has all products and `C` has all pullbacks, then the composition of the fork map of `R` and `P` with the first map of `R` and `P` is equal to the composition of the fork map of `R` and `P` with the second map of `R` and `P`. In other words, in the context of category theory, this theorem ensures the commutativity of a certain diagram related to presheaves, morphisms, and limits.
More concisely: For any presheaf P from the opposite category of a category C with pullbacks and products, the diagram commutes where the fork map of a set of arrows R with codomain U and the first and second maps of R with P are concerned.
|
CategoryTheory.Presheaf.subsingleton_iff_isSeparatedFor
theorem CategoryTheory.Presheaf.subsingleton_iff_isSeparatedFor :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} A] (P : CategoryTheory.Functor Cᵒᵖ A) {X : C}
(S : CategoryTheory.Sieve X),
(∀ (c : CategoryTheory.Limits.Cone (S.arrows.diagram.op.comp P)),
Subsingleton (c ⟶ P.mapCone S.arrows.cocone.op)) ↔
∀ (E : Aᵒᵖ), CategoryTheory.Presieve.IsSeparatedFor (P.comp (CategoryTheory.coyoneda.obj E)) S.arrows
The theorem `CategoryTheory.Presheaf.subsingleton_iff_isSeparatedFor` states that for any category `C`, category `A`, a presheaf `P` which is a contravariant functor from `C` to `A`, an object `X` in `C`, and a sieve `S` on `X`, the natural cone associated to `S` and `P` admits at most one morphism from every cone in the same category over the same diagram if and only if for all objects `E` in the opposite category of `A`, `Hom (E, P -)` is separated for the sieve `S`. Here `Hom (E, P -)` represents a functor that to every object `Y` in `C` assigns the set of morphisms from `E` to `P(Y)`. Being "separated" means that there is at most one way to amalgamate a family of elements of `P` which is compatible with `S`.
More concisely: For a contravariant presheaf \(P: C^{op} \to A\) over a category \(C\), an object \(X\) in \(C\), and a sieve \(S\) on \(X\), the natural cone over \(S\) and \(P\) has at most one morphism from every cone over the same diagram in \(C\) if and only if for every object \(E\) in \(A\), the functor \(Hom(E, P-)\) is separated for the sieve \(S\) in \(A\).
|
CategoryTheory.Presheaf.isSeparated_iff_subsingleton
theorem CategoryTheory.Presheaf.isSeparated_iff_subsingleton :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} A] (J : CategoryTheory.GrothendieckTopology C)
(P : CategoryTheory.Functor Cᵒᵖ A),
(∀ (E : A), CategoryTheory.Presieve.IsSeparated J (P.comp (CategoryTheory.coyoneda.obj (Opposite.op E)))) ↔
∀ ⦃X : C⦄,
∀ S ∈ J.sieves X,
∀ (c : CategoryTheory.Limits.Cone (S.arrows.diagram.op.comp P)),
Subsingleton (c ⟶ P.mapCone S.arrows.cocone.op)
The theorem `CategoryTheory.Presheaf.isSeparated_iff_subsingleton` states that a presheaf `P` is separated for a Grothendieck topology `J` if and only if for every covering sieve `S` in `J`, the natural cone associated with `P` and `S` admits at most one morphism from every other cone in the same category. This means that for each object `E` in category `A`, if the presheaf `P` composed with the co-Yoneda embedding of `E` is separated for the Grothendieck topology `J`, then for each category `C` object `X` and for each sieve `S` in the topology of `X`, every cone `c` in the category over the diagram of `S` composed with `P` is such that there's at most one morphism from `c` to the opposite of the cocone of `P` mapping over `S`. This is a precise formulation of the concept of a presheaf being separated for a given topology.
More concisely: A presheaf is separated for a Grothendieck topology if and only if for every covering sieve, the natural cone associated with the presheaf and sieve admits at most one morphism from every other cone in the same category.
|
CategoryTheory.Sheaf.Hom.ext
theorem CategoryTheory.Sheaf.Hom.ext :
∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C}
{A : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} A} {X Y : CategoryTheory.Sheaf J A} (x y : X.Hom Y),
x.val = y.val → x = y
This theorem states that for any two category-theory sheaves `X` and `Y` over a given Grothendieck topology `J`, any two morphisms (or homomorphisms) `x` and `y` from `X` to `Y` are equal if and only if their underlying functions (accessed by `.val`) are equal. This is often referred to as an extensionality theorem because it extends the concept of function equality (equality of outputs for all inputs) to a higher-level concept, in this case morphisms in a category.
More concisely: For any two sheaves X and Y over a Grothendieck topology J, two morphisms x and y from X to Y are equal if and only if their underlying functions have equal values.
|
CategoryTheory.Presheaf.isSheaf_iff_isLimit
theorem CategoryTheory.Presheaf.isSheaf_iff_isLimit :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} A] (J : CategoryTheory.GrothendieckTopology C)
(P : CategoryTheory.Functor Cᵒᵖ A),
CategoryTheory.Presheaf.IsSheaf J P ↔
∀ ⦃X : C⦄, ∀ S ∈ J.sieves X, Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone S.arrows.cocone.op))
The theorem states that a presheaf `P` is a sheaf for a Grothendieck topology `J` if and only if for every covering sieve `S` in the topology `J`, the natural cone associated to `P` and `S` is a limit cone. Here, `C` and `A` are categories, `J` is a Grothendieck topology on `C`, and `P` is a presheaf of category `A` on the opposite category of `C`. The covering sieve `S` belongs to the sieves of some object `X` in `C`, and the natural cone is derived from the presheaf `P` and the arrows of `S` mapped to a cocone and then made into an opposite (cocone.op).
More concisely: A presheaf P on the opposite category of C for a Grothendieck topology J is a sheaf if and only if for every covering sieve S in J, the natural cone from P and S is a limit cone.
|
CategoryTheory.Presheaf.secondObj.proof_2
theorem CategoryTheory.Presheaf.secondObj.proof_2 :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {A : Type u_4}
[inst_1 : CategoryTheory.Category.{u_3, u_4} A] {U : C} (R : CategoryTheory.Presieve U)
(P : CategoryTheory.Functor Cᵒᵖ A) [inst_2 : CategoryTheory.Limits.HasProducts A]
[inst_3 : CategoryTheory.Limits.HasPullbacks C],
CategoryTheory.Limits.HasLimit
(CategoryTheory.Discrete.functor fun fg =>
P.obj (Opposite.op (CategoryTheory.Limits.pullback ↑fg.1.snd ↑fg.2.snd)))
This theorem states that for a given category `C` and a presieve `R` on an object `U` of `C`, a functor `P` from the opposite category of `C` to another given category `A` (which has products), when the category `C` has pullbacks, there exists a limit for the functor that maps each element `fg` of the discrete category (formed from pairs of elements in the presieve `R`) to the object in `A` computed by the functor `P` evaluated at the pullback of the morphisms corresponding to `fg`. In other words, this theorem is a condition for the existence of limits of certain functors formed from a presheaf `P` and a presieve `R` within a category that has pullbacks and a target category that has products.
More concisely: Given a category with pullbacks `C`, a presieve `R` on an object `U` of `C`, and a functor `P` from `C^{op}` to a category with products `A`, there exists a limit for the functor `P` over the discrete category formed from pairs in `R` if and only if `C` has pullbacks.
|
CategoryTheory.Sheaf.hom_ext
theorem CategoryTheory.Sheaf.hom_ext :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
{A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A] {X Y : CategoryTheory.Sheaf J A} (x y : X ⟶ Y),
x.val = y.val → x = y
The theorem `CategoryTheory.Sheaf.hom_ext` states that for any category `C` with a Grothendieck topology `J`, another category `A`, and two sheaves `X` and `Y` over `A` with respect to the topology `J`, if two morphisms `x` and `y` from `X` to `Y` are such that their underlying functions (obtained using `.val`) are equal, then the morphisms `x` and `y` themselves are also equal. This theorem ensures that in the context of category theory and sheaf theory, the equality of morphisms can be determined by the equality of their underlying functions.
More concisely: If `C` is a category with a Grothendieck topology `J`, `A` is another category, and `X`, `Y` are sheaves over `A` with respect to `J`, then two morphisms `x : X -> Y` and `y : X -> Y` are equal if and only if their underlying functions `.val x` and `.val y` are equal.
|
CategoryTheory.Presheaf.isSheaf_of_iso_iff
theorem CategoryTheory.Presheaf.isSheaf_of_iso_iff :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} A] {J : CategoryTheory.GrothendieckTopology C}
{P P' : CategoryTheory.Functor Cᵒᵖ A},
(P ≅ P') → (CategoryTheory.Presheaf.IsSheaf J P ↔ CategoryTheory.Presheaf.IsSheaf J P')
This theorem states that for any categories `C` and `A`, any Grothendieck topology `J` on `C`, and any two functors `P` and `P'` from the opposite of `C` to `A` that are isomorphic, `P` is a sheaf with respect to `J` if and only if `P'` is a sheaf with respect to `J`. In other words, being a sheaf is a property that is preserved under isomorphism between functors.
More concisely: For any categories C, any Grothendieck topology J on C, and any oppositely isomorphic functors P and P' from the opposite of C to A, if one is a sheaf with respect to J then so is the other.
|
CategoryTheory.Presheaf.isLimit_iff_isSheafFor
theorem CategoryTheory.Presheaf.isLimit_iff_isSheafFor :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} A] (P : CategoryTheory.Functor Cᵒᵖ A) {X : C}
(S : CategoryTheory.Sieve X),
Nonempty (CategoryTheory.Limits.IsLimit (P.mapCone S.arrows.cocone.op)) ↔
∀ (E : Aᵒᵖ), CategoryTheory.Presieve.IsSheafFor (P.comp (CategoryTheory.coyoneda.obj E)) S.arrows
This theorem, `CategoryTheory.Presheaf.isLimit_iff_isSheafFor`, states that for any category `C`, category `A`, a presheaf `P : Cᵒᵖ ⥤ A`, a sieve `S` on an object `X` of `C`, there exists a limit cone associated with the presheaf and the sieve if and only if the presheaf `Hom(E, P -)` is a sheaf of types for every object `E` of the category `Aᵒᵖ` and the given sieve `S`.
More concisely: A presheaf over a category is a limit of its restriction to a sieve if and only if the associated Hom functor is a sheaf for that sieve.
|
CategoryTheory.Sheaf.cond
theorem CategoryTheory.Sheaf.cond :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
{A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A] (self : CategoryTheory.Sheaf J A),
CategoryTheory.Presheaf.IsSheaf J self.val
This theorem states that for any category `C` with a Grothendieck topology `J`, and any category `A`, if `self` is a sheaf on `J` with values in `A`, then `self.val`, which represents the presheaf associated with the sheaf `self`, is a sheaf on `J`. Essentially, this theorem is asserting that the underling presheaf of a sheaf, by definition, is a sheaf.
More concisely: For any category `C` with a Grothendieck topology `J` and any category `A`, if `self` is a sheaf on `J` with values in `A`, then the underlying presheaf `self.val` is also a sheaf on `J` with values in `A`.
|
CategoryTheory.Presheaf.isSheaf_iff_isSheaf'
theorem CategoryTheory.Presheaf.isSheaf_iff_isSheaf' :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A' : Type u₂}
[inst_1 : CategoryTheory.Category.{max v₁ u₁, u₂} A'] (J : CategoryTheory.GrothendieckTopology C)
(P' : CategoryTheory.Functor Cᵒᵖ A') [inst_2 : CategoryTheory.Limits.HasProducts A']
[inst_3 : CategoryTheory.Limits.HasPullbacks C],
CategoryTheory.Presheaf.IsSheaf J P' ↔ CategoryTheory.Presheaf.IsSheaf' J P'
This theorem states that for a category `C`, a type `A'` that is also a category, a Grothendieck topology `J` on `C`, and a functor `P'` from `C` to `A'`, if `A'` is a category with products and `C` is a category with pullbacks, then a presheaf `P'` is a sheaf with respect to `J` if and only if it is a sheaf according to the equalizer definition of a sheaf. In other words, the two definitions of a sheaf, the general one and the one using equalizers, are equivalent in this context.
More concisely: For a category `C`, a category `A'` with products, a Grothendieck topology `J` on `C`, and a functor `P'` from `C` to `A'`, the presheaf `P'` is a sheaf with respect to `J` if and only if it satisfies the equalizer definition of a sheaf.
|
CategoryTheory.Presheaf.firstObj.proof_1
theorem CategoryTheory.Presheaf.firstObj.proof_1 :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {A : Type u_4}
[inst_1 : CategoryTheory.Category.{u_3, u_4} A] {U : C} (R : CategoryTheory.Presieve U)
(P : CategoryTheory.Functor Cᵒᵖ A) [inst_2 : CategoryTheory.Limits.HasProducts A],
CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor fun f => P.obj (Opposite.op f.fst))
This theorem states that for any category `C`, category `A`, an object `U` in `C`, a presieve `R` on `U`, and a functor `P` from the opposite of `C` to `A`, if the category `A` has products, then there exists a limit for the functor which maps an arrow `f` to the object `P.obj` of the opposite of the domain of `f` in the discrete category of `C`.
Essentially, this establishes the existence of certain limits in the category `A` given the existence of products in that category, mapping elements in the presieve to objects in `A` via the functor `P`.
More concisely: Given a category `C`, a category `A` with products, an object `U` in `C`, a presieve `R` on `U`, and a functor `P` from `C^{op}` to `A`, there exists a limit for `P` over `R` in `A`.
|
CategoryTheory.isSheaf_iff_isSheaf_of_type
theorem CategoryTheory.isSheaf_iff_isSheaf_of_type :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C)
(P : CategoryTheory.Functor Cᵒᵖ (Type w)),
CategoryTheory.Presheaf.IsSheaf J P ↔ CategoryTheory.Presieve.IsSheaf J P
The theorem `CategoryTheory.isSheaf_iff_isSheaf_of_type` states that for any type `C` with a category structure, a Grothendieck topology `J` on `C`, and a presheaf `P` from the opposite category of `C` to the category of types, the presheaf `P` is a sheaf with respect to the topology `J` if and only if it satisfies the sheaf condition for every sieve in the topology `J`. In more mathematical terms, a presheaf is a sheaf if it is a sheaf for every sieve in the Grothendieck topology.
More concisely: A presheaf on a type with a category structure and a Grothendieck topology is a sheaf if and only if it satisfies the sheaf condition for every sieve in the topology.
|