CategoryTheory.GrothendieckTopology.isGLB_sInf
theorem CategoryTheory.GrothendieckTopology.isGLB_sInf :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (s : Set (CategoryTheory.GrothendieckTopology C)),
IsGLB s (sInf s)
This theorem states that for any type `C` that is a category in category theory and any set `s` of Grothendieck topologies on `C`, the infimum (`sInf s`) is a greatest lower bound (GLB) of the set `s`. This means that the infimum of the set `s` is the largest element that is less than or equal to all elements in `s`, according to the partial order defined by the Grothendieck topology. Note that the infimum exists and is unique for any given set in a partially ordered set. The theorem is a formalization of a concept in category theory related to Grothendieck topologies, which can be found at https://stacks.math.columbia.edu/tag/00Z7.
More concisely: For any set `s` of Grothendieck topologies on a category `C`, the infimum of `s` is the greatest lower bound and is the unique element that is subsumed by all elements in `s` according to the partial order defined by Grothendieck topologies.
|
CategoryTheory.GrothendieckTopology.Cover.Arrow.hf
theorem CategoryTheory.GrothendieckTopology.Cover.Arrow.hf :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
{S : J.Cover X} (self : S.Arrow), S.sieve.arrows self.f
This theorem states that for any category "C", given an object "X" in "C" and a Grothendieck topology "J" on "C", if we have a cover "S" of "X" in the topology "J", then any arrow "self" in "S" is contained in the sieve of "S". In other words, any morphism referenced by "self.f" in the context of the cover "S" is a member of the arrows of the sieve of "S".
More concisely: For any object X in a category C and a Grothendieck topology J on C, if S is a cover of X in J, then for each self in S, the morphism self.f belongs to the sieve of S.
|
CategoryTheory.GrothendieckTopology.intersection_covering
theorem CategoryTheory.GrothendieckTopology.intersection_covering :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {S R : CategoryTheory.Sieve X}
(J : CategoryTheory.GrothendieckTopology C), R ∈ J.sieves X → S ∈ J.sieves X → R ⊓ S ∈ J.sieves X
This theorem states that in the context of a Grothendieck topology in category theory, if you have two covering sieves, R and S, on an object X in a category C, their intersection (denoted as R ⊓ S) is also a covering sieve. In simpler terms, if two sieves cover an object according to a given Grothendieck topology, their intersection will also cover that object.
More concisely: In a Grothendieck topology, the intersection of two covering sieves is a covering sieve.
|
CategoryTheory.GrothendieckTopology.covers_iff
theorem CategoryTheory.GrothendieckTopology.covers_iff :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (J : CategoryTheory.GrothendieckTopology C)
(S : CategoryTheory.Sieve X) (f : Y ⟶ X), J.Covers S f ↔ CategoryTheory.Sieve.pullback f S ∈ J.sieves Y
The theorem `CategoryTheory.GrothendieckTopology.covers_iff` states that for any category `C`, objects `X` and `Y` in `C`, a Grothendieck topology `J` on `C`, a sieve `S` on `X`, and a morphism `f : Y ⟶ X`, the sieve `S` on `X` `J`-covers the arrow `f` to `X` if and only if the pullback of `S` along `f` is in the sieves of `J` on `Y`. In other words, a sieve `S` covers a morphism under a Grothendieck topology if and only if the pullback of `S` through this morphism is a sieve in the topology at the domain of the morphism.
More concisely: A sieve on an object X in a category with a Grothendieck topology J covers the morphism f : Y ⟶ X if and only if the pullback of J-sieves on X along f is contained in the J-sieves on Y.
|
CategoryTheory.GrothendieckTopology.pullback_stable'
theorem CategoryTheory.GrothendieckTopology.pullback_stable' :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (self : CategoryTheory.GrothendieckTopology C) ⦃X Y : C⦄
⦃S : CategoryTheory.Sieve X⦄ (f : Y ⟶ X), S ∈ self.sieves X → CategoryTheory.Sieve.pullback f S ∈ self.sieves Y
The theorem `CategoryTheory.GrothendieckTopology.pullback_stable'` states that for any category `C` with a Grothendieck topology, given objects `X` and `Y` in `C`, a morphism `f` from `Y` to `X`, and a sieve `S` on `X` that is in the sieves of the Grothendieck topology on `X`, the pullback of the sieve `S` along the morphism `f` is in the sieves of the Grothendieck topology on `Y`. In other words, the Grothendieck topology is stable under the operation of pullback.
More concisely: Given a category with a Grothendieck topology, the pullback of a sieve in the topology along a morphism is still a sieve in the topology.
|
CategoryTheory.GrothendieckTopology.Cover.Relation.w
theorem CategoryTheory.GrothendieckTopology.Cover.Relation.w :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
{S : J.Cover X} (self : S.Relation),
CategoryTheory.CategoryStruct.comp self.g₁ self.f₁ = CategoryTheory.CategoryStruct.comp self.g₂ self.f₂
This theorem is part of the Grothendieck topology, a mathematical construct used in category theory. Specifically, it states that for any category `C` with a Grothendieck topology `J` and a cover `S` of an object `X` in `C`, for any relation `self` in `S`, the composition of morphisms `g₁` and `f₁` in the relation equals the composition of morphisms `g₂` and `f₂`. Here, a morphism is a sort of directed edge or relationship between two objects in the category, and composition of morphisms is akin to following two such edges in sequence. This theorem is essentially a commutativity condition for the involved morphisms under composition, which underlies the equivalence relation defined by a cover in the Grothendieck topology.
More concisely: For any category with a Grothendieck topology and a cover, the composition of any two morphisms in the cover is commutative.
|
CategoryTheory.GrothendieckTopology.pullback_stable
theorem CategoryTheory.GrothendieckTopology.pullback_stable :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {S : CategoryTheory.Sieve X}
(J : CategoryTheory.GrothendieckTopology C) (f : Y ⟶ X),
S ∈ J.sieves X → CategoryTheory.Sieve.pullback f S ∈ J.sieves Y
The theorem, known as the "pullback stability axiom", is an assertion in the context of Grothendieck topologies in category theory. Given a category `C`, objects `X` and `Y` in `C`, a morphism `f` from `Y` to `X`, a Grothendieck topology `J` on `C`, and a sieve `S` on `X`, if `S` is in the collection of sieves determined by the Grothendieck topology `J` at `X`, then the pullback of `S` along `f` is in the collection of sieves determined by `J` at `Y`. In essence, a Grothendieck topology is 'stable' under the operation of pulling back sieves along morphisms.
More concisely: Given a Grothendieck topology J on a category C and morphisms f : Y -> X in C, if S is a sieve on X belonging to the topology J at X, then the pullback of S along f belongs to the topology J at Y.
|
CategoryTheory.GrothendieckTopology.top_mem
theorem CategoryTheory.GrothendieckTopology.top_mem :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (X : C),
⊤ ∈ J.sieves X
This theorem, also known as the maximality axiom, states that for any category 'C' and any Grothendieck topology 'J' on 'C', the maximal sieve (represented as '⊤') is in the collection of sieves 'J.sieves' for any object 'X' of the category. In other words, in the context of Grothendieck topologies in category theory, the largest possible sieve is always considered a covering sieve for any given object in the category.
More concisely: In any category with a Grothendieck topology, the maximal sieve is a covering sieve for every object.
|
CategoryTheory.GrothendieckTopology.top_mem'
theorem CategoryTheory.GrothendieckTopology.top_mem' :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (self : CategoryTheory.GrothendieckTopology C) (X : C),
⊤ ∈ self.sieves X
This theorem states that for any category `C` and any object `X` in `C`, the Grothendieck topology associated with `C` must contain the top sieve for `X`. In other words, the collection of sieves associated with each object in the category must include the maximal sieve, which is represented by the top element (`⊤`). This is a fundamental property of Grothendieck topologies in category theory.
More concisely: In any category with a Grothendieck topology, the top sieve is contained in the topology for every object.
|
CategoryTheory.GrothendieckTopology.Cover.Relation.h₁
theorem CategoryTheory.GrothendieckTopology.Cover.Relation.h₁ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
{S : J.Cover X} (self : S.Relation), S.sieve.arrows self.f₁
The theorem `CategoryTheory.GrothendieckTopology.Cover.Relation.h₁` states that for any category `C` of type `u` and `X` being an object in `C`, given a Grothendieck topology `J` on `C` and a cover `S` of `X` in this topology, for any relation `self` in the cover `S`, the first arrow (`f₁`) of this relation is contained in the sieve of `S`. In other words, this is verifying the first condition in the definition of a Grothendieck pre-topology where covering sieves include certain arrows.
More concisely: For any category `C`, object `X` in `C`, Grothendieck topology `J` on `C`, and cover `S` of `X` in `J`, the first arrow of any relation in `S` lies in the sieve of `S`.
|
CategoryTheory.GrothendieckTopology.covering_of_eq_top
theorem CategoryTheory.GrothendieckTopology.covering_of_eq_top :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {S : CategoryTheory.Sieve X}
(J : CategoryTheory.GrothendieckTopology C), S = ⊤ → S ∈ J.sieves X
The theorem `CategoryTheory.GrothendieckTopology.covering_of_eq_top` states that for any given category `C`, object `X` in `C`, sieve `S` of `X` and a Grothendieck topology `J` on `C`, if `S` equals the maximal (or top) sieve, then `S` is a member of the sieves determined by the Grothendieck topology `J` at `X`. In other words, any maximal sieve on an object in a category is a covering for that object with respect to any Grothendieck topology on the category.
More concisely: For any category `C`, object `X` in `C`, and a Grothendieck topology `J` on `C`, if `S` is the maximal sieve of `X`, then `S` is a covering sieve of `X` in the sense of `J`.
|
CategoryTheory.GrothendieckTopology.transitive
theorem CategoryTheory.GrothendieckTopology.transitive :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {S : CategoryTheory.Sieve X}
(J : CategoryTheory.GrothendieckTopology C),
S ∈ J.sieves X →
∀ (R : CategoryTheory.Sieve X),
(∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → CategoryTheory.Sieve.pullback f R ∈ J.sieves Y) → R ∈ J.sieves X
The `CategoryTheory.GrothendieckTopology.transitive` theorem states that, for a given category `C`, an object `X` in `C`, a sieve `S` on `X`, and a Grothendieck topology `J` on `C`, if `S` belongs to the set of sieves associated with `X` in the topology `J`, then for any other sieve `R` on `X`, if for all objects `Y` in `C` and morphisms `f` from `Y` to `X` such that `f` is in the arrows of `S`, the pullback of `f` under `R` is in the sieves associated with `Y` in the topology `J`, then `R` is also in the sieves associated with `X` in the topology `J`. In other words, this is the transitivity property of Grothendieck topologies, which ensures that if a sieve `R` covers all arrows in `S` that are covered by the topology `J`, then `R` is also covered by `J`.
More concisely: Given a category `C`, an object `X` in `C`, a Grothendieck topology `J` on `C`, and a sieve `S` on `X` belonging to the topology `J`, if for all sieves `R` on `X` such that `S` is contained in `R` and every arrow `f` from an object `Y` to `X` in `S` has a pullback in `R` also belonging to `J`, then `R` is also in the topology `J`.
|
CategoryTheory.GrothendieckTopology.superset_covering
theorem CategoryTheory.GrothendieckTopology.superset_covering :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {S R : CategoryTheory.Sieve X}
(J : CategoryTheory.GrothendieckTopology C), S ≤ R → S ∈ J.sieves X → R ∈ J.sieves X
This theorem states that in the context of a given category `C` with an object `X` and two sieves `S` and `R` on `X`, if `S` is a subset of `R` and `S` is covering (i.e., belongs to the Grothendieck topology `J` on `X`), then `R` is also covering (i.e., belongs to the Grothendieck topology `J` on `X`). It is related to the definitions and discussions found in the provided references.
More concisely: If `S` is a covering sieve that is a subset of `R` in a Grothendieck topology on a category `C` with object `X`, then `R` is also a covering sieve.
|
CategoryTheory.GrothendieckTopology.transitive'
theorem CategoryTheory.GrothendieckTopology.transitive' :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (self : CategoryTheory.GrothendieckTopology C) ⦃X : C⦄
⦃S : CategoryTheory.Sieve X⦄,
S ∈ self.sieves X →
∀ (R : CategoryTheory.Sieve X),
(∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → CategoryTheory.Sieve.pullback f R ∈ self.sieves Y) → R ∈ self.sieves X
The theorem `CategoryTheory.GrothendieckTopology.transitive'` expresses the transitivity of sieves in a Grothendieck topology. In a given Grothendieck topology on a category `C`, if a sieve `S` on an object `X` is in the Grothendieck topology (i.e., `S` is a covering sieve for `X`), and for every morphism `f` from an object `Y` to `X` that `S` admits, the pullback of the sieve `R` along `f` is also a covering sieve for `Y`, then the sieve `R` is itself a covering sieve for `X`. In simpler terms, if every pullback of `R` is a covering sieve, then `R` is a covering sieve.
More concisely: In a Grothendieck topology, if a sieve is a covering sieve and every pullback of it along morphisms admitting it is also a covering sieve, then the sieve is a covering sieve.
|
CategoryTheory.GrothendieckTopology.ext
theorem CategoryTheory.GrothendieckTopology.ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J₁ J₂ : CategoryTheory.GrothendieckTopology C},
J₁.sieves = J₂.sieves → J₁ = J₂
This theorem is an extensionality lemma for Grothendieck topologies in category theory. It states that for any category "C" and two given Grothendieck topologies "J₁" and "J₂" on "C", if their "sieves" are equal, then these two topologies are identical. The "sieves" of a Grothendieck topology can be considered as a way to specify the 'coverage' of the topology, so the lemma essentially says that two Grothendieck topologies are the same if they cover the same 'area'. The proof is given in terms of the coercion to a pi-type instead of the projection `.sieves`.
More concisely: If two Grothendieck topologies on a category have equal sieves, then they are identical.
|
CategoryTheory.GrothendieckTopology.arrow_max
theorem CategoryTheory.GrothendieckTopology.arrow_max :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (J : CategoryTheory.GrothendieckTopology C)
(f : Y ⟶ X) (S : CategoryTheory.Sieve X), S.arrows f → J.Covers S f
This theorem, called `CategoryTheory.GrothendieckTopology.arrow_max`, states the maximality axiom in the form of an 'arrow'. In particular, for any category `C`, any objects `X` and `Y` in `C`, any Grothendieck topology `J` on `C`, any morphism `f` from `Y` to `X`, and any sieve `S` on `X`, if `f` is an arrow in `S`, then `J` covers `f` with `S`. In the language of category theory, this is stating that the Grothendieck topology `J` is maximal with respect to the arrows in `S`.
More concisely: For any category `C`, Grothendieck topology `J` on `C`, objects `X` and `Y` in `C`, morphism `f` from `Y` to `X`, and sieve `S` on `X`, if `f` is an element of `S` and `S` is a covering sieve in `J`, then `J` is maximal among all Grothendieck topologies on `C` containing `S` as a covering sieve.
|
CategoryTheory.GrothendieckTopology.Cover.condition
theorem CategoryTheory.GrothendieckTopology.Cover.condition :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
(S : J.Cover X), S.sieve ∈ J.sieves X
This theorem states that for any category 'C', object 'X' in 'C', and Grothendieck topology 'J' on 'C', if 'S' is a cover of 'X' with respect to 'J', then the sieve associated with 'S' belongs to the collection of sieves on 'X' determined by 'J'. In other words, every cover of an object in a category, under a particular Grothendieck topology, corresponds to a sieve in the set of sieves defined by that topology on that object.
More concisely: For any category 'C', object 'X' in 'C', and Grothendieck topology 'J' on 'C', the sieve of any cover 'S' of 'X' with respect to 'J' belongs to the collection of sieves on 'X' determined by 'J'.
|
CategoryTheory.GrothendieckTopology.Cover.Relation.h₂
theorem CategoryTheory.GrothendieckTopology.Cover.Relation.h₂ :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
{S : J.Cover X} (self : S.Relation), S.sieve.arrows self.f₂
This theorem states that for any category `C`, for any object `X` in `C`, for any Grothendieck topology `J` on `C`, and for any cover `S` of `X` in `J`, if we have a relation `self` in `S`, then the second arrow (`f₂`) of this relation is contained in the sieve formed by the arrows of `S`. In simpler terms, it tells us that the second part of any relation in a cover of a topological space in the category-theoretic sense is included in the set of arrows that make up that cover.
More concisely: For any object X in a category C with a Grothendieck topology J, if S is a cover of X in J and self is a relation in S, then the second arrow of self is in the sieve generated by S.
|
CategoryTheory.GrothendieckTopology.Cover.ext
theorem CategoryTheory.GrothendieckTopology.Cover.ext :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
(S T : J.Cover X), (∀ ⦃Y : C⦄ (f : Y ⟶ X), S.sieve.arrows f ↔ T.sieve.arrows f) → S = T
This theorem states that for any category `C`, any object `X` in `C`, and any Grothendieck topology `J` on `C`, two covers `S` and `T` of `X` with respect to `J` are equal if and only if for every object `Y` in `C` and every morphism `f` from `Y` to `X`, `f` is an arrow in the sieve associated to `S` if and only if `f` is an arrow in the sieve associated to `T`. In other words, the covers `S` and `T` are determined by the arrows in their associated sieves.
More concisely: For any category `C`, object `X`, and Grothendieck topology `J`, covers `S` and `T` of `X` with respect to `J` are equal if and only if their associated sieves have the same collections of morphisms to `X`.
|
Mathlib.CategoryTheory.Sites.Grothendieck._auxLemma.4
theorem Mathlib.CategoryTheory.Sites.Grothendieck._auxLemma.4 :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (J : CategoryTheory.GrothendieckTopology C)
(S : CategoryTheory.Sieve X) (f : Y ⟶ X), J.Covers S f = (CategoryTheory.Sieve.pullback f S ∈ J.sieves Y)
This theorem is about the relation between Grothendieck topologies and sieves in category theory. It states that, for any category `C` with objects `X` and `Y`, a Grothendieck topology `J` on `C`, a sieve `S` on `X`, and a morphism `f` from `Y` to `X`, the statement that `S` `J`-covers `f` is equivalent to the statement that the pullback of `S` by `f` is in the collection of sieves in `J` on `Y`. The pullback of `S` by `f` is the inverse image of `S` with `_ ≫ f`, and the `J`-cover is defined as the condition that this pullback belongs to the topology `J`.
More concisely: For a category `C`, object `X`, Grothendieck topology `J`, sieve `S` on `X`, and morphism `f: Y → X` in `C`, `S` `J`-covers `f` if and only if the pullback of `S` by `f` is in `J`.
|
CategoryTheory.GrothendieckTopology.arrow_stable
theorem CategoryTheory.GrothendieckTopology.arrow_stable :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (J : CategoryTheory.GrothendieckTopology C)
(f : Y ⟶ X) (S : CategoryTheory.Sieve X),
J.Covers S f → ∀ {Z : C} (g : Z ⟶ Y), J.Covers S (CategoryTheory.CategoryStruct.comp g f)
This theorem is known as the stability axiom in the arrow form in Grothendieck topology in a category. It states that for any category `C`, any two objects `X` and `Y` in `C`, a Grothendieck topology `J` on `C`, a morphism `f` from `Y` to `X`, and a sieve `S` on `X`, if the sieve `S` covers the morphism `f` according to the Grothendieck topology `J`, then for any object `Z` in `C` and any morphism `g` from `Z` to `Y`, the sieve `S` also covers the composition of the morphisms `g` and `f`. This means that the coverage of a morphism by a sieve in a Grothendieck topology is stable under precomposition with another morphism.
More concisely: Given any category `C`, Grothendieck topology `J`, objects `X`, `Y`, morphisms `f : Y -> X` and `g : Z -> Y`, and sieve `S` on `X` covering `f` in `J`, then `S` covers the composition `g ∘ f` as well.
|
CategoryTheory.GrothendieckTopology.arrow_trans
theorem CategoryTheory.GrothendieckTopology.arrow_trans :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (J : CategoryTheory.GrothendieckTopology C)
(f : Y ⟶ X) (S R : CategoryTheory.Sieve X),
J.Covers S f → (∀ {Z : C} (g : Z ⟶ X), S.arrows g → J.Covers R g) → J.Covers R f
This theorem, `CategoryTheory.GrothendieckTopology.arrow_trans`, states that in any category `C` with objects `X` and `Y`, and a Grothendieck topology `J`, for any morphism `f` from `Y` to `X`, and two sieves `S` and `R` on `X`, if `S` covers `f` and each arrow in `S` is covered by `R`, then `R` must also cover `f`. This is a formalization of the transitivity axiom in category theory, specifically in the context of Grothendieck topologies, and is expressed in 'arrow' form.
More concisely: Given a category with a Grothendieck topology, if a morphism is covered by a sieve and every arrow in the sieve is covered by another sieve, then the morphism is covered by the second sieve.
|