CategoryTheory.Presieve.IsSeparatedFor.isSheafFor
theorem CategoryTheory.Presieve.IsSeparatedFor.isSheafFor :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
{R : CategoryTheory.Presieve X},
CategoryTheory.Presieve.IsSeparatedFor P R →
(∀ (x : CategoryTheory.Presieve.FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) →
CategoryTheory.Presieve.IsSheafFor P R
The theorem `CategoryTheory.Presieve.IsSeparatedFor.isSheafFor` states that for any category `C`, functor `P` from the opposite of `C` to the type `w`, an object `X` in `C`, and a presieve `R` on `X`, if `P` is separated for `R` and every family of elements in `P` compatible with `R` has an amalgamation, then `P` is a sheaf for `R`.
In simpler terms, this theorem provides a criterion for a presheaf to be a sheaf: it has to be separated (i.e., there is at most one way to glue elements together) and every compatible family of elements (i.e., elements that can be glued together) must have at least one way to be glued together (has an amalgamation). This reflects the informal idea in category theory of a sheaf as a presheaf where "local data glue uniquely".
More concisely: A presheaf on a category is a sheaf if and only if it is separated and every compatible family of elements has an amalgamation.
|
CategoryTheory.Presieve.extension_iff_amalgamation
theorem CategoryTheory.Presieve.extension_iff_amalgamation :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X}
{P : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (x : S.functor ⟶ P) (g : CategoryTheory.yoneda.obj X ⟶ P),
CategoryTheory.CategoryStruct.comp S.functorInclusion g = x ↔
(↑(CategoryTheory.Presieve.natTransEquivCompatibleFamily x)).IsAmalgamation (CategoryTheory.yonedaEquiv g)
This theorem, named `CategoryTheory.Presieve.extension_iff_amalgamation`, states that in the context of a given category `C`, an object `X` in `C`, a sieve `S` on `X`, and a functor `P` from the opposite of `C` to the category of types, for any natural transformation `x` from the functor represented by the sieve `S` to `P`, and any natural transformation `g` from the Yoneda embedding of `X` to `P`, the composition of the functor inclusion of `S` and `g` is equal to `x` if and only if `x`, when viewed as a compatible family via the natural transformation equivalence, is an amalgamation of `g` under the Yoneda equivalence.
This theorem is a tool used in the proof of the equivalence between the sheaf condition for a presheaf in terms of amalgamation and the yoneda sheaf condition.
More concisely: In a category `C`, given an object `X`, a sieve `S` on `X`, a functor `P` from the opposite of `C` to types, and natural transformations `x: S ⊣ P` and `g: X ≅ P`, `x ∘ incl_S = g` if and only if `x` is the amalgamation of `g` under the Yoneda embedding.
|
CategoryTheory.Presieve.extend_restrict
theorem CategoryTheory.Presieve.extend_restrict :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
{R : CategoryTheory.Presieve X}
{x : CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Sieve.generate R).arrows},
x.Compatible → (CategoryTheory.Presieve.FamilyOfElements.restrict ⋯ x).sieveExtend = x
The theorem `CategoryTheory.Presieve.extend_restrict` states that for a given category `C`, a presheaf `P` over the opposite category of `C`, and an object `X` in `C`, if we have a presieve `R` on `X` and a family `x` of elements for the sieve `S` generated by `R` that is compatible, then if we restrict `x` to `R` and then extend it back up to `S`, the resulting extension will be equal to `x`. In other words, in the given context of category theory, the process of restricting a family of elements to a smaller presieve and then extending it back does not change the original family of elements, provided they are compatible.
More concisely: For a presheaf over the opposite category of a given category, restricting and then extending a compatible family of elements through a compatible presieve results in the original family.
|
CategoryTheory.Presieve.IsSheafFor.functorInclusion_comp_extend
theorem CategoryTheory.Presieve.IsSheafFor.functorInclusion_comp_extend :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X}
{P : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (h : CategoryTheory.Presieve.IsSheafFor P S.arrows)
(f : S.functor ⟶ P), CategoryTheory.CategoryStruct.comp S.functorInclusion (h.extend f) = f
This theorem is stating that for any category `C`, object `X` of `C`, Grothendieck topology `S` on `X`, and presheaf `P` on `C`, if `P` is a sheaf for the arrows of `S`, then for any morphism `f` from the functor represented by `S` to `P`, the composition of `S.functorInclusion` and the extension of `f` over all objects `X` is equal to `f` itself. In other words, extending `f` to all of `X` doesn't change `f`. This condition is a fundamental property in category theory, ensuring the commutativity of the diagram involving `S`, `P` and the Yoneda embedding of `X` (`yX`), provided `P` is a sheaf for `S`.
More concisely: For any category `C`, object `X` of `C`, Grothendieck topology `S` on `X`, presheaf `P` on `C`, if `P` is a sheaf for the arrows of `S`, then the extension of any morphism `f` from `S.functorInclusion` to `P` over all objects `X` is equal to `f` itself.
|
CategoryTheory.Presieve.compatible_iff_sieveCompatible
theorem CategoryTheory.Presieve.compatible_iff_sieveCompatible :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
{S : CategoryTheory.Sieve X} (x : CategoryTheory.Presieve.FamilyOfElements P S.arrows),
x.Compatible ↔ x.SieveCompatible
This theorem is stating a property in category theory, specifically dealing with functors, sieves, and presieves. It says that for any category `C`, a functor `P` from the opposite category `Cᵒᵖ` to a type `w`, an object `X` in `C`, a sieve `S` of `X`, and a family of elements `x` of `P` indexed by the arrows of `S`, the family of elements `x` is compatible (in the sense of presieves) if and only if it is sieve-compatible.
More concisely: For any category C, functor P from Cⁱ to a type w, object X in C, sieve S of X, and family x of elements of P indexed by the arrows of S, the family x is a compatible presheaf if and only if it is sieve-compatible.
|
CategoryTheory.Presieve.IsSheafFor.unique_extend
theorem CategoryTheory.Presieve.IsSheafFor.unique_extend :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X}
{P : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (h : CategoryTheory.Presieve.IsSheafFor P S.arrows) {f : S.functor ⟶ P}
(t : CategoryTheory.yoneda.obj X ⟶ P),
CategoryTheory.CategoryStruct.comp S.functorInclusion t = f → t = h.extend f
This theorem, titled `CategoryTheory.Presieve.IsSheafFor.unique_extend`, states that for any category `C`, any object `X` in `C`, any sieve `S` on `X`, and any presheaf `P`, if `P` is a sheaf for the arrows of `S`, then for any morphism `f` from the functor of `S` to `P` and any transformation `t` from the Yoneda functor at `X` to `P`, if the composition of the inclusion of `S` functor with `t` equals to `f`, then `t` is uniquely determined as the extension of `f` by `h`. Here, `h` denotes a particular morphism indicated by the fact that `P` is a sheaf for the arrows of `S`. The theorem asserts the uniqueness of such an extension in the context of category theory.
More concisely: Given a category `C`, an object `X` in `C`, a sieve `S` on `X`, a presheaf `P`, and morphisms `f` from the functor of `S` to `P` and `t` from the Yoneda functor at `X` to `P` with `ft = P.to_fun (S.inclusion) x` for some `x` in `X`, if `P` is a sheaf for the arrows of `S`, then `t` is uniquely the extension of `f` by `h` for some `h` in `P(X)`.
|
CategoryTheory.Presieve.isSheafFor_iff_yonedaSheafCondition
theorem CategoryTheory.Presieve.isSheafFor_iff_yonedaSheafCondition :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X}
{P : CategoryTheory.Functor Cᵒᵖ (Type v₁)},
CategoryTheory.Presieve.IsSheafFor P S.arrows ↔ CategoryTheory.Presieve.YonedaSheafCondition P S
This theorem states that the Yoneda version of the sheaf condition is equivalent to the sheaf condition for any category `C`, object `X` of `C`, sieve `S` on `X`, and presheaf `P`. In other words, for a given category, object, sieve, and presheaf, the presheaf satisfies the sheaf condition if and only if it satisfies the Yoneda sheaf condition. This is a formalization of Theorem C2.1.4 from the book "The Elephant".
In the context of category theory, the sheaf condition is a property that certain kinds of mathematical objects (such as presheaves) must satisfy. The Yoneda condition is a version of the sheaf condition that is often easier to work with.
More concisely: For any category `C`, object `X` of `C`, sieve `S` on `X`, and presheaf `P`, the presheaf `P` satisfies the sheaf condition if and only if it satisfies the Yoneda sheaf condition.
|
CategoryTheory.Presieve.restrict_inj
theorem CategoryTheory.Presieve.restrict_inj :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
{R : CategoryTheory.Presieve X}
{x₁ x₂ : CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Sieve.generate R).arrows},
x₁.Compatible →
x₂.Compatible →
CategoryTheory.Presieve.FamilyOfElements.restrict ⋯ x₁ =
CategoryTheory.Presieve.FamilyOfElements.restrict ⋯ x₂ →
x₁ = x₂
The theorem `CategoryTheory.Presieve.restrict_inj` says that for a category `C` and a contravariant functor `P` from `C` to the category of types, and a presieve `R` on an object `X` in `C`, if two compatible families of elements for the presheaf `P` on the sieve generated by `R` are equal when restricted to `R`, then the two families of elements are equal. This theorem generalizes the idea that two functions on a set are equal if and only if they are equal on a generating subset. This has an important role in the theory of presheaves in category theory.
More concisely: Given a category C, a contravariant functor P from C to Types, and a presieve R on an object X in C, if two compatible families of elements in the presheaf P restricted to R are equal, then they are equal as families in P.
|
CategoryTheory.Presieve.isSheafFor_singleton_iso
theorem CategoryTheory.Presieve.isSheafFor_singleton_iso :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type w)),
CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.singleton (CategoryTheory.CategoryStruct.id X))
This theorem states that for any category `C` and any object `X` in `C`, every presheaf `P` is a sheaf for the singleton family that contains only the identity morphism on `X`. In other words, every presheaf is a sheaf when we only consider the presieve consisting of the identity morphism. This is a result listed as C2.1.5(i) in the "Elephant" book on category theory.
More concisely: Every presheaf on a category is a sheaf with respect to the singleton family consisting of the identity morphism on an object.
|
CategoryTheory.Presieve.extend_agrees
theorem CategoryTheory.Presieve.extend_agrees :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C}
{R : CategoryTheory.Presieve X} {x : CategoryTheory.Presieve.FamilyOfElements P R},
x.Compatible → ∀ {f : Y ⟶ X} (hf : R f), x.sieveExtend f ⋯ = x f hf
The theorem `CategoryTheory.Presieve.extend_agrees` states that in any category `C`, for any presheaf `P` (a functor from the opposite category `Cᵒᵖ` to the category of types `(Type w)`), any objects `X` and `Y` in `C`, any presieve `R` over `X`, and any family `x` of elements of `P` indexed by `R` that is compatible (meaning that it satisfies certain coherence conditions), then for any morphism `f` from `Y` to `X` that is in the presieve `R`, the result of extending the family `x` to include `f` matches the original family at `f`. In other words, extending a family of elements of a presheaf to include a new morphism does not change the original elements of the family.
More concisely: For any category C, presheaf P, objects X and Y, presieve R, and compatible family x of elements of P indexed by R, extending x along any morphism f in R from Y to X does not alter the value of x at X.
|
CategoryTheory.Presieve.isSheafFor_subsieve
theorem CategoryTheory.Presieve.isSheafFor_subsieve :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type w))
{S : CategoryTheory.Sieve X} {R : CategoryTheory.Presieve X},
S.arrows ≤ R →
(∀ ⦃Y : C⦄ (f : Y ⟶ X), CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.pullback f S).arrows) →
CategoryTheory.Presieve.IsSheafFor P R
The theorem `CategoryTheory.Presieve.isSheafFor_subsieve` states that if `P` is a sheaf with respect to every pullback of a sieve `S`, then `P` is a sheaf for any presieve `R` that contains `S`. Here, `P` is a contravariant functor from the category `C` to the category of types, `S` is a sieve on an object `X` in `C`, and `R` is a presieve on `X`. The term "pullback of a sieve `S`" refers to a new sieve derived from `S` by composing all its morphisms (arrows) with a given morphism. The theorem is part of Category Theory and is closely related to the statement C2.1.6 in the "Elephant" book on Category Theory.
More concisely: If a contravariant functor `P` is a sheaf with respect to every pullback of a sieve `S` in a category `C`, then `P` is a sheaf for any presieve `R` containing `S`.
|
CategoryTheory.Presieve.IsSeparatedFor.ext
theorem CategoryTheory.Presieve.IsSeparatedFor.ext :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
{R : CategoryTheory.Presieve X},
CategoryTheory.Presieve.IsSeparatedFor P R →
∀ {t₁ t₂ : P.obj (Opposite.op X)}, (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → P.map f.op t₁ = P.map f.op t₂) → t₁ = t₂
The theorem `CategoryTheory.Presieve.IsSeparatedFor.ext` states that for any category `C`, presheaf `P` and object `X` in `C`, and any presieve `R` on `X`, if the presheaf `P` is separated for the presieve `R`, then for any two objects `t₁` and `t₂` in the category opposite to `C` formed by `P`, if for all objects `Y` in `C` and morphisms `f` from `Y` to `X` that are in the presieve `R`, the mapping of `f` under the action of `P` on `t₁` is equal to its action on `t₂`, then `t₁` is equal to `t₂`. In mathematical terms, this theorem is stating a condition under which two objects are equal in a category if they are related through a functor under certain conditions.
More concisely: If a presheaf on a category is separated for a presieve, then two objects mapping identically under that presheaf for all morphisms in the presieve are equal.
|
CategoryTheory.Presieve.IsSheafFor.hom_ext
theorem CategoryTheory.Presieve.IsSheafFor.hom_ext :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X}
{P : CategoryTheory.Functor Cᵒᵖ (Type v₁)},
CategoryTheory.Presieve.IsSheafFor P S.arrows →
∀ (t₁ t₂ : CategoryTheory.yoneda.obj X ⟶ P),
CategoryTheory.CategoryStruct.comp S.functorInclusion t₁ =
CategoryTheory.CategoryStruct.comp S.functorInclusion t₂ →
t₁ = t₂
The theorem `CategoryTheory.Presieve.IsSheafFor.hom_ext` states that given a category `C`, an object `X` of `C`, a sieve `S` on `X`, and a presheaf `P` of type `Cᵒᵖ (Type v₁)`, if `P` is a sheaf for the sieve `S` on `X`, then any two natural transformations `t₁` and `t₂` from the Yoneda embedding of `X` to `P` that agree when restricted to the subfunctor specified by `S`, must be equal. In other words, the theorem provides a uniqueness property for natural transformations into a sheaf that agree on a given sieve.
More concisely: Given a category `C`, an object `X` in `C`, a sieve `S` on `X`, and a sheaf `P` over `S` on `X`, any two natural transformations from the Yoneda embedding of `X` to `P` that agree on the subfunctor specified by `S` are equal.
|
CategoryTheory.Presieve.FamilyOfElements.Compatible.sieveExtend
theorem CategoryTheory.Presieve.FamilyOfElements.Compatible.sieveExtend :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
{R : CategoryTheory.Presieve X} {x : CategoryTheory.Presieve.FamilyOfElements P R},
x.Compatible → x.sieveExtend.Compatible
The theorem `CategoryTheory.Presieve.FamilyOfElements.Compatible.sieveExtend` states that for any category `C`, functor `P` from `Cᵒᵖ` to the category of types, object `X` of `C`, presieve `R` on `X`, and a family of elements `x` of `R` under `P`, if the family `x` is compatible, then the extension of this compatible family to the generated sieve is also compatible. In other words, the operation of extending a compatible family of elements to the generated sieve preserves compatibility.
More concisely: For any category `C`, functor `P`, object `X` in `C`, presieve `R` on `X`, and a family `x` of elements of `R` under `P` that are compatible, the extended family obtained by adding to `x` all elements of `P(X)` in the generated sieve of `R` is also compatible.
|
CategoryTheory.Presieve.FamilyOfElements.Compatible.restrict
theorem CategoryTheory.Presieve.FamilyOfElements.Compatible.restrict :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
{R₁ R₂ : CategoryTheory.Presieve X} (h : R₁ ≤ R₂) {x : CategoryTheory.Presieve.FamilyOfElements P R₂},
x.Compatible → (CategoryTheory.Presieve.FamilyOfElements.restrict h x).Compatible
This theorem states that in the context of category theory, if we have a category `C` and a functor `P` from the opposite category `Cᵒᵖ` to the category of types `Type w`, along with two presieves `R₁` and `R₂` on an object `X` in `C` such that `R₁` is a subset of `R₂`, then the restriction of a family of elements `x` of `P` that is compatible with `R₂` to `R₁` remains a compatible family of elements. In other words, if a family of elements of a presheaf is compatible with a certain presieve, it remains compatible when restricted to any smaller presieve.
More concisely: If `C` is a category, `P` is a functor from `Cᵒᵖ` to `Type w`, `X` is an object in `C`, `R₁` and `R₂` are two presheaves on `X` with `R₁ ⊆ R₂`, and `x` is a family of elements of `P` compatible with `R₂`, then `x` is also compatible with `R₁`.
|
CategoryTheory.Presieve.IsSheafFor.isSeparatedFor
theorem CategoryTheory.Presieve.IsSheafFor.isSeparatedFor :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
{R : CategoryTheory.Presieve X},
CategoryTheory.Presieve.IsSheafFor P R → CategoryTheory.Presieve.IsSeparatedFor P R
In the realm of category theory, this theorem states that if a functor `P` is a sheaf for a presieve `R`, then `P` is also separated for `R`. This means that for every family of elements `x` of the presheaf `P`, and for any two amalgamations `t₁` and `t₂` of `x`, if `t₁` and `t₂` are both amalgamations of `x`, then `t₁` must equal `t₂`. In simpler terms, a presheaf that is a sheaf for a given presieve will have at most one amalgamation for each family of elements, making it separated for that presieve.
More concisely: If `P` is a sheaf for the presieve `R` in category theory, then `P` is separated by `R`, meaning that for every family of elements `x` in `P`, any two amalgamations of `x` are equal.
|
CategoryTheory.Presieve.IsSheafFor.valid_glue
theorem CategoryTheory.Presieve.IsSheafFor.valid_glue :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C}
{R : CategoryTheory.Presieve X} (t : CategoryTheory.Presieve.IsSheafFor P R)
{x : CategoryTheory.Presieve.FamilyOfElements P R} (hx : x.Compatible) (f : Y ⟶ X) (Hf : R f),
P.map f.op (t.amalgamate x hx) = x f Hf
The theorem `CategoryTheory.Presieve.IsSheafFor.valid_glue` states that for any category `C`, functor `P` from the opposite category of `C` to any type `w`, objects `X` and `Y` in `C`, a presieve `R` on `X`, a proof `t` that `P` is a sheaf for `R`, a family of elements `x` of `P` over `R` that are compatible, an arrow `f` from `Y` to `X` and a proof `Hf` that `f` is in the presieve `R`, the application of the functor `P` to `f` and the amalgamation of `x` under `t` and `hx` equals to the application of `x` to `f` and `Hf`. In other words, this theorem ensures that the process of amalgamating a compatible family of elements preserves the structure of the sheaf.
More concisely: For any category `C`, functor `P : C^op -> Type`, objects `X, Y in C`, presieve `R on X`, sheaf proof `t for R and P`, compatible family `x : P X -> R`, arrow `f : Y -> X` in `R`, and proof `Hf : f ∈ R`, we have `P f (amalgamate t x hx) = (P f x) (hx)`.
|
CategoryTheory.Presieve.isSheafFor_top_sieve
theorem CategoryTheory.Presieve.isSheafFor_top_sieve :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type w)),
CategoryTheory.Presieve.IsSheafFor P ⊤.arrows
This theorem states that for every presheaf P in any category C, P is a sheaf with respect to the maximal sieve. Here, the presheaf is a functor P from the opposite category of C to Type. The maximal sieve is a collection of all morphisms in the category that have a fixed object X as their codomain. In other words, any presheaf is a sheaf when considered with respect to the largest possible collection of morphisms in the category.
More concisely: Every presheaf in a category is a sheaf with respect to the maximal sieve.
|
CategoryTheory.Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor
theorem CategoryTheory.Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
{R : CategoryTheory.Presieve X},
(CategoryTheory.Presieve.IsSeparatedFor P R ∧
∀ (x : CategoryTheory.Presieve.FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) ↔
CategoryTheory.Presieve.IsSheafFor P R
The theorem `CategoryTheory.Presieve.isSeparatedFor_and_exists_isAmalgamation_iff_isSheafFor` states that a presheaf `P` is a sheaf for a presieve `R` if and only if it is separated for `R` and there exists an amalgamation for all families of elements of `P` compatible with `R`. In other words, for a presheaf `P` and a presieve `R`, the presheaf `P` is a sheaf for the presieve `R` if there is at most one amalgamation for each family of elements of `P` (this is the separation condition), and there is at least one amalgamation for each family of elements of `P` that is compatible with `R` (this is the existence condition).
More concisely: A presheaf is a sheaf for a given presieve if and only if it satisfies the separation condition (at most one amalgamation per family) and the existence condition (there exists an amalgamation for each family compatible with the presieve).
|
CategoryTheory.Presieve.isSheafFor_iff_generate
theorem CategoryTheory.Presieve.isSheafFor_iff_generate :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
(R : CategoryTheory.Presieve X),
CategoryTheory.Presieve.IsSheafFor P R ↔
CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.generate R).arrows
This theorem, denoted as C2.1.3 in the Elephant book, states that for any category `C`, any presheaf `P` of types over `C`, any object `X` of `C`, and any presieve `R` of arrows into `X`, the presheaf `P` is a sheaf for the presieve `R` if and only if `P` is a sheaf for the sieve generated by `R`. This is significant because it creates a link between the notion of a sheaf for a given set of arrows and a sheaf for the smallest sieve containing this set. The sieve generated by `R` consists of all arrows that factor through arrows in `R`.
More concisely: For any category `C`, presheaf `P` over `C`, object `X` in `C`, and sieve `R` of arrows into `X`, `P` is a sheaf for `R` if and only if it is a sheaf for the sieve generated by `R`.
|
CategoryTheory.Presieve.restrict_extend
theorem CategoryTheory.Presieve.restrict_extend :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
{R : CategoryTheory.Presieve X} {x : CategoryTheory.Presieve.FamilyOfElements P R},
x.Compatible → CategoryTheory.Presieve.FamilyOfElements.restrict ⋯ x.sieveExtend = x
The theorem `CategoryTheory.Presieve.restrict_extend` states that, for any category `C`, any functor `P` from the opposite of `C` to the type `w`, any object `X` in `C`, any presieve `R` on `X`, and any family of elements `x` for the presieve `R` that is compatible, the restriction of the extension of `x` to the sieve generated by `R` is equal to `x`. In simpler terms, if you extend a family of elements `x` in a certain way and then restrict it back, you get the original `x`. This theorem is a fundamental property in the categorical theory, specifically in dealing with presieves and sieves.
More concisely: For any category C, functor P from C\^op to w, object X in C, presieve R on X, and compatible family x for R, the restriction of the extension of x along R is equal to x.
|
CategoryTheory.Presieve.IsSheafFor.isAmalgamation
theorem CategoryTheory.Presieve.IsSheafFor.isAmalgamation :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
{R : CategoryTheory.Presieve X} (t : CategoryTheory.Presieve.IsSheafFor P R)
{x : CategoryTheory.Presieve.FamilyOfElements P R} (hx : x.Compatible), x.IsAmalgamation (t.amalgamate x hx)
The theorem `CategoryTheory.Presieve.IsSheafFor.isAmalgamation` states that for any category `C`, any presheaf `P` of types over the opposite category of `C`, any object `X` in `C`, any presieve `R` on `X`, and any compatible family of elements `x` of the presheaf `P` over the presieve `R`, if `P` is a sheaf for the presieve `R`, then the amalgamation of the compatible family `x` is indeed an amalgamation of `x`.
In simpler terms, this theorem guarantees the existence and uniqueness of an amalgamation (a common "merging" element) for a compatible family of elements in a presheaf, given the presheaf is a sheaf for the presieve. This is a central concept in category theory, particularly in the understanding of sheaves.
More concisely: Given a category `C`, a presheaf `P` over `C^op`, an object `X` in `C`, a presieve `R` on `X`, and a compatible family `x` of elements in `P` over `R`, if `P` is a sheaf for `R`, then the amalgamation of `x` exists and is unique in `P` over `X`.
|
CategoryTheory.Presieve.isSheafFor_subsieve_aux
theorem CategoryTheory.Presieve.isSheafFor_subsieve_aux :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type w))
{S : CategoryTheory.Sieve X} {R : CategoryTheory.Presieve X},
S.arrows ≤ R →
CategoryTheory.Presieve.IsSheafFor P S.arrows →
(∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
R f → CategoryTheory.Presieve.IsSeparatedFor P (CategoryTheory.Sieve.pullback f S).arrows) →
CategoryTheory.Presieve.IsSheafFor P R
The theorem `CategoryTheory.Presieve.isSheafFor_subsieve_aux` states that for any category `C`, object `X` in `C`, presheaf `P`, sieve `S` on `X`, and presieve `R` on `X`, if the arrows of `S` are a subset of `R` and `P` is a sheaf for `S`, and also if for every morphism `f` in `R`, `P` is separated for the pullback of `S` along `f`, then `P` is a sheaf for `R`. This theorem is closely related to the result stated in the reference [Elephant] C2.1.6(i). A presheaf is said to be a sheaf for a particular presieve if it satisfies certain conditions of amalgamation and locality, and being separated for a presieve means there is at most one amalgamation.
More concisely: If `P` is a presheaf on a category `C`, `X` is an object in `C`, `S` is a sieve on `X`, `R` is a presieve on `X` containing `S`, and for every morphism `f` in `R`, `P` is separated for the pullback of `S` along `f` and `P` is a sheaf for `S`, then `P` is a sheaf for `R`.
|
CategoryTheory.Presieve.isSheafFor_iso
theorem CategoryTheory.Presieve.isSheafFor_iso :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
{R : CategoryTheory.Presieve X} {P' : CategoryTheory.Functor Cᵒᵖ (Type w)},
(P ≅ P') → CategoryTheory.Presieve.IsSheafFor P R → CategoryTheory.Presieve.IsSheafFor P' R
The theorem `CategoryTheory.Presieve.isSheafFor_iso` states that for any category `C`, any contravariant functor `P` from `C` to the category of types, any object `X` of `C`, any presieve `R` on `X`, and any other contravariant functor `P'` from `C` to the category of types, if `P` is isomorphic to `P'` and `P` is a sheaf for `R`, then `P'` is also a sheaf for `R`. This theorem demonstrates that being a sheaf for a presieve is a property that is preserved under isomorphism, which can be considered as a mathematical or hygienic property of the sheaf.
More concisely: If `P` is an isomorphic contravariant functor to `P'` and `P` is a sheaf for the presieve `R` in category `C`, then `P'` is also a sheaf for `R`.
|
CategoryTheory.Presieve.isAmalgamation_restrict
theorem CategoryTheory.Presieve.isAmalgamation_restrict :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
{R₁ R₂ : CategoryTheory.Presieve X} (h : R₁ ≤ R₂) (x : CategoryTheory.Presieve.FamilyOfElements P R₂)
(t : P.obj (Opposite.op X)),
x.IsAmalgamation t → (CategoryTheory.Presieve.FamilyOfElements.restrict h x).IsAmalgamation t
The theorem `CategoryTheory.Presieve.isAmalgamation_restrict` states that in a category 'C', for any presheaf 'P' and for any two presieves 'R₁' and 'R₂' on an object 'X' such that 'R₁' is included in 'R₂', if a family of elements 'x' of the presheaf 'P' over the presieve 'R₂' amalgamates to an element 't' of 'P', then the family of elements obtained by restricting 'x' to 'R₁' also amalgamates to 't'. In other words, the process of amalgamation is stable under restriction of presieves.
More concisely: If presheaf 'P' over category 'C', presieves 'R₁' and 'R₂' on object 'X' with 'R₁' included in 'R₂', and a family of elements 'x' in 'P' over 'R₂' amalgamates to an element 't' in 'P', then the family of elements 'x' restricted to 'R₁' also amalgamates to 't'.
|