CategoryTheory.Presieve.isSheaf_coverage
theorem CategoryTheory.Presieve.isSheaf_coverage :
∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_3, u_2} C] (K : CategoryTheory.Coverage C)
(P : CategoryTheory.Functor Cᵒᵖ (Type u_1)),
CategoryTheory.Presieve.IsSheaf (CategoryTheory.Coverage.toGrothendieck C K) P ↔
∀ {X : C}, ∀ R ∈ K.covering X, CategoryTheory.Presieve.IsSheafFor P R
The main theorem states that, given a coverage `K` on a category `C`, a presheaf valued in the category of types (`Type*`) on `C` is a sheaf for `K` if and only if it is a sheaf for the associated Grothendieck topology. This means that the sheaf condition applies not only to all sieves in the Grothendieck topology generated by `K`, but equivalently to all coverings in `K` itself. This establishes a strong connection between the notions of a sheaf for a coverage and a sheaf for a Grothendieck topology.
More concisely: A presheaf is a sheaf for a coverage in a category if and only if it is a sheaf for the Grothendieck topology generated by that coverage.
|
CategoryTheory.Coverage.pullback
theorem CategoryTheory.Coverage.pullback :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] (self : CategoryTheory.Coverage C) ⦃X Y : C⦄
(f : Y ⟶ X), ∀ S ∈ self.covering X, ∃ T ∈ self.covering Y, T.FactorsThruAlong S f
The theorem `CategoryTheory.Coverage.pullback` states the following: In any category `C` with a given coverage structure, for any covering sieve `S` on an object `X` and any morphism `f` from object `Y` to `X`, there exists a covering sieve `T` on `Y` such that `T` factors through `S` along `f`. This means that every arrow in `T` can be obtained from an arrow in `S` by precomposing it with `f`.
More concisely: For any category with coverage structure, given a covering sieve on an object and a morphism to that object, there exists a covering sieve on the domain of the morphism that maps to the given sieve.
|
CategoryTheory.Presieve.isSheaf_sup
theorem CategoryTheory.Presieve.isSheaf_sup :
∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_3, u_2} C] (K L : CategoryTheory.Coverage C)
(P : CategoryTheory.Functor Cᵒᵖ (Type u_1)),
CategoryTheory.Presieve.IsSheaf (CategoryTheory.Coverage.toGrothendieck C (K ⊔ L)) P ↔
CategoryTheory.Presieve.IsSheaf (CategoryTheory.Coverage.toGrothendieck C K) P ∧
CategoryTheory.Presieve.IsSheaf (CategoryTheory.Coverage.toGrothendieck C L) P
The theorem `CategoryTheory.Presieve.isSheaf_sup` states that for any category `C`, any two coverings `K` and `L` of `C`, and any functor `P` from the opposite category of `C` to the category of types, a presheaf `P` is a sheaf for the Grothendieck topology generated by the union of `K` and `L` if and only if `P` is a sheaf for the Grothendieck topology generated by `K` and `L` separately. In essence, this theorem is saying that the property of being a sheaf for a Grothendieck topology is preserved under the union of coverages.
More concisely: For any category C, any functor P from the opposite category of C to Type, and any coverings K and L of C, the presheaf P is a sheaf for the Grothendieck topology generated by K ∪ L if and only if it is a sheaf for the topologies generated by K and L separately.
|
CategoryTheory.Coverage.toGrothendieck_eq_sInf
theorem CategoryTheory.Coverage.toGrothendieck_eq_sInf :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] (K : CategoryTheory.Coverage C),
CategoryTheory.Coverage.toGrothendieck C K = sInf {J | K ≤ CategoryTheory.Coverage.ofGrothendieck C J}
This theorem presents an alternative characterization of the Grothendieck topology associated with a coverage `K`. Specifically, in the context of a category `C`, the Grothendieck topology derived from a given coverage `K` is equivalent to the infimum (greatest lower bound) of the set of all Grothendieck topologies, whose associated coverages contain `K`. This means that any Grothendieck topology that has an associated coverage including `K`, is 'larger' or 'above' the Grothendieck topology associated with `K` in the sense of the order defined on the set of Grothendieck topologies.
More concisely: The Grothendieck topology derived from a coverage `K` in a category `C` is the greatest lower bound of all Grothendieck topologies whose associated coverages contain `K`.
|