CategoryTheory.le_topology_of_closedSieves_isSheaf
theorem CategoryTheory.le_topology_of_closedSieves_isSheaf :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J₁ J₂ : CategoryTheory.GrothendieckTopology C},
CategoryTheory.Presieve.IsSheaf J₁ (CategoryTheory.Functor.closedSieves J₂) → J₁ ≤ J₂
The theorem `CategoryTheory.le_topology_of_closedSieves_isSheaf` states that for any category `C` and any two Grothendieck topologies `J₁` and `J₂` on `C`, if the presheaf of `J₂`-closed sieves is a `J₁`-sheaf, then `J₁` is less than or equal to `J₂`. Note that the converse is also true as shown by `classifier_isSheaf` and `isSheaf_of_le`.
More concisely: If a Grothendieck topology J₂ on a category C makes the sheaf of J₁-closed sieves a J₁-sheaf for some Grothendieck topology J₁ on C, then J₁ is less than or equal to J₂.
|
CategoryTheory.topology_eq_iff_same_sheaves
theorem CategoryTheory.topology_eq_iff_same_sheaves :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J₁ J₂ : CategoryTheory.GrothendieckTopology C},
J₁ = J₂ ↔
∀ (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))),
CategoryTheory.Presieve.IsSheaf J₁ P ↔ CategoryTheory.Presieve.IsSheaf J₂ P
The theorem `CategoryTheory.topology_eq_iff_same_sheaves` states that for any Category `C`, if two Grothendieck topologies `J₁` and `J₂` on `C` have the property that a presheaf `P` is a sheaf for `J₁` if and only if it is a sheaf for `J₂`, then `J₁` and `J₂` are equal. In other words, two Grothendieck topologies are the same if they precisely determine the same collection of sheaves.
More concisely: Two Grothendieck topologies on a category are equal if and only if they determine the same collection of sheaves.
|
CategoryTheory.GrothendieckTopology.isClosed_pullback
theorem CategoryTheory.GrothendieckTopology.isClosed_pullback :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X Y : C}
(f : Y ⟶ X) (S : CategoryTheory.Sieve X), J₁.IsClosed S → J₁.IsClosed (CategoryTheory.Sieve.pullback f S)
This theorem states that if we are given a category `C` with a Grothendieck topology `J₁`, along with objects `X` and `Y` in `C` and a morphism `f` from `Y` to `X`, then the property of being `J₁`-closed is preserved under pullback. Specifically, if a sieve `S` on `X` is `J₁`-closed, then the sieve obtained by pulling back `S` along `f` to get a sieve on `Y` is also `J₁`-closed. This means that closure under the Grothendieck topology is a property that is stable under the operation of pullback.
More concisely: Given a Grothendieck topology `J₁` on a category `C`, if a sieve `S` on an object `X` is `J₁`-closed, then the pullback of `S` along any morphism `f : Y → X` results in a `J₁`-closed sieve on `Y`.
|
CategoryTheory.topologyOfClosureOperator_self
theorem CategoryTheory.topologyOfClosureOperator_self :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C),
CategoryTheory.topologyOfClosureOperator J₁.closureOperator ⋯ = J₁
This theorem states that for any Grothendieck topology `J₁` on a category `C`, the topology derived from the closure operator of `J₁` is equivalent to `J₁` itself. In other words, if you create a closure operator from a Grothendieck topology and then use that to form a new topology, you end up with the original topology. This illustrates a core property of Grothendieck topologies in category theory.
More concisely: The derived topology from the closure operator of a Grothendieck topology on a category equals the original Grothendieck topology.
|
CategoryTheory.classifier_isSheaf
theorem CategoryTheory.classifier_isSheaf :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C),
CategoryTheory.Presieve.IsSheaf J₁ (CategoryTheory.Functor.closedSieves J₁)
The theorem `CategoryTheory.classifier_isSheaf` states that for any given category `C` and a Grothendieck topology `J₁` on `C`, the presheaf of `J₁`-closed sieves is a `J₁`-sheaf. This result is based on the proof from "Sheaves in Geometry and Logic" (MM92), Chapter III, Section 7, Lemma 1. In mathematical terms, it means that the presheaf that maps each object to the set of `J₁`-closed sieves on it satisfies the sheaf condition for every sieve in the topology `J₁`.
More concisely: The presheaf of `J₁`-closed sieves is a `J₁`-sheaf in any category `C` with a Grothendieck topology `J₁`.
|
CategoryTheory.GrothendieckTopology.le_close
theorem CategoryTheory.GrothendieckTopology.le_close :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C}
(S : CategoryTheory.Sieve X), S ≤ J₁.close S
This theorem states that for any category `C` and any Grothendieck topology `J₁` on `C`, for any object `X` in `C` and any sieve `S` on `X`, `S` is less than or equal to the closure of `S` under the Grothendieck topology `J₁`. In other words, the closure of a sieve under a Grothendieck topology always contains the original sieve.
More concisely: For any category `C` with Grothendieck topology `J₁`, and any object `X` and sieve `S` in `C`, we have `S ≤ J₁(S)`.
|
CategoryTheory.GrothendieckTopology.le_close_of_isClosed
theorem CategoryTheory.GrothendieckTopology.le_close_of_isClosed :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C}
{S T : CategoryTheory.Sieve X}, S ≤ T → J₁.IsClosed T → J₁.close S ≤ T
This theorem states that for any Category `C`, Grothendieck topology `J₁` on `C`, and any two Sieves `S` and `T` on an object `X` in `C`, if `S` is contained within `T` and `T` is closed in `J₁`, then the closure of `S` under the topology `J₁` is also contained within `T`. In other words, the closure of a sieve `S` is the largest closed sieve containing `S`, hence justifying the term "closure".
More concisely: Given a category `C` with Grothendieck topology `J₁`, if `S` is a sieve on an object `X` in `C` contained in a closed sieve `T`, then the closure of `S` under `J₁` is contained in `T`.
|
CategoryTheory.GrothendieckTopology.covers_iff_mem_of_isClosed
theorem CategoryTheory.GrothendieckTopology.covers_iff_mem_of_isClosed :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C}
{S : CategoryTheory.Sieve X}, J₁.IsClosed S → ∀ {Y : C} (f : Y ⟶ X), J₁.Covers S f ↔ S.arrows f
This theorem states that for any category `C`, given a Grothendieck topology `J₁` on `C`, and a sieve `S` on an object `X` in `C` that is `J₁`-closed, for any object `Y` in `C` and morphism `f` from `Y` to `X`, `J₁` covers `S` with respect to `f` if and only if `f` is contained in the arrows of `S`. Grothendieck topologies and sieves are used in category theory to study local properties of morphisms, and `J₁`-closed sieves represent particular collections of morphisms that satisfy certain closure conditions. This theorem specifically relates the covering property of the topology to the membership of a morphism in a sieve.
More concisely: For a Grothendieck topology `J₁` on a category `C`, a sieve `S` on an object `X` in `C` is `J₁`-covered by an arrow `f : Y → X` if and only if `f` is in `S`.
|
CategoryTheory.GrothendieckTopology.close_isClosed
theorem CategoryTheory.GrothendieckTopology.close_isClosed :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C}
(S : CategoryTheory.Sieve X), J₁.IsClosed (J₁.close S)
This theorem states that for any category `C`, any Grothendieck topology `J₁` on `C`, and any sieve `S` on an object `X` of `C`, the closure of `S` under the Grothendieck topology `J₁` is a closed sieve under `J₁`. The Grothendieck topology and the concept of a sieve are constructs from the field of category theory in mathematics. A Grothendieck topology provides a way to define what it means for a morphism (or arrow) in a category to be "covered", and a sieve is a collection of morphisms that satisfies certain conditions.
More concisely: Given a category `C` with Grothendieck topology `J₁`, the closure of a sieve `S` on an object `X` under `J₁` is a closed sieve.
|
CategoryTheory.GrothendieckTopology.pullback_close
theorem CategoryTheory.GrothendieckTopology.pullback_close :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X Y : C}
(f : Y ⟶ X) (S : CategoryTheory.Sieve X),
J₁.close (CategoryTheory.Sieve.pullback f S) = CategoryTheory.Sieve.pullback f (J₁.close S)
The theorem `CategoryTheory.GrothendieckTopology.pullback_close` states that for any category `C`, any Grothendieck topology `J₁` on `C`, any objects `X` and `Y` in `C`, any morphism `f` from `Y` to `X`, and any sieve `S` on `X`, the operation of closing a sieve under the topology `J₁` commutes with the operation of pulling back a sieve along a morphism. In other words, pulling back the closure of the sieve `S` under the topology `J₁` via the morphism `f` is the same as first pulling back the sieve `S` via `f` and then taking the closure under `J₁`. The closure of a sieve under a Grothendieck topology roughly means the largest sieve that contains the given one and satisfies the defining condition of the topology. The pullback of a sieve along a morphism is the inverse image of the sieve under the morphism.
More concisely: Given a category `C`, a Grothendieck topology `J₁` on `C`, objects `X`, `Y` in `C`, a morphism `f` from `Y` to `X`, and a sieve `S` on `X`, the closure of the pullback of `S` along `f` under `J₁` equals the pullback of the closure of `S` under `J₁` along `f`.
|
CategoryTheory.GrothendieckTopology.close_eq_top_iff_mem
theorem CategoryTheory.GrothendieckTopology.close_eq_top_iff_mem :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C}
(S : CategoryTheory.Sieve X), J₁.close S = ⊤ ↔ S ∈ J₁.sieves X
This theorem states that for any category `C`, Grothendieck topology `J₁` on `C`, and any sieve `S` on an object `X` in `C`, the closure operator applied to `S` under `J₁` is equal to the maximal sieve (`⊤`) if and only if `S` is an element of the set of sieves of `X` under `J₁`. This establishes that the topology is determined by the closure operator.
More concisely: For any category `C`, Grothendieck topology `J₁` on `C`, and object `X` in `C`, the closure of a sieve `S` under `J₁` equals the maximal sieve if and only if `S` is a sieve of `X` under `J₁`.
|
CategoryTheory.GrothendieckTopology.isClosed_iff_close_eq_self
theorem CategoryTheory.GrothendieckTopology.isClosed_iff_close_eq_self :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X : C}
(S : CategoryTheory.Sieve X), J₁.IsClosed S ↔ J₁.close S = S
This theorem states that for any category `C` and Grothendieck topology `J₁` on `C`, and for any sieve `S` on some object `X` in `C`, the sieve `S` is considered closed under the Grothendieck topology `J₁` if and only if the closure of the sieve `S` under `J₁` is equal to `S` itself. In other words, a sieve is closed under a Grothendieck topology when applying the closure operation to the sieve has no effect.
More concisely: A sieve in a category with respect to a Grothendieck topology is closed if and only if its closure under the topology equals the sieve itself.
|