CategoryTheory.Sieve.functor_galoisConnection
theorem CategoryTheory.Sieve.functor_galoisConnection :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C),
GaloisConnection (CategoryTheory.Sieve.functorPushforward F) (CategoryTheory.Sieve.functorPullback F)
This theorem states that for any two categories `C` and `D` and a functor `F` from `C` to `D`, the functions `functorPushforward` and `functorPullback` form a Galois connection. This Galois connection is a relationship between two order-preserving functions such that for all sieves `R` in `C` and `S` in `D`, the sieve `R` is a subset of the pullback of `S` if and only if the pushforward of `R` is a subset of `S`. In mathematical terms, this means that for all sieves `R` and `S`, `R ≤ F^*(S)` if and only if `F_*(R) ≤ S`, where `F^*` is the pullback functor and `F_*` is the pushforward functor.
More concisely: For any functor F from category C to category D, the pullback and pushforward functions of F form a Galois connection, i.e., for all sieves R in C and S in D, R ≤ F^*(S) if and only if F_(R) ≤ S.
|
CategoryTheory.Sieve.id_mem_iff_eq_top
theorem CategoryTheory.Sieve.id_mem_iff_eq_top :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X},
S.arrows (CategoryTheory.CategoryStruct.id X) ↔ S = ⊤
This theorem states that for any category `C`, any object `X` in `C`, and any sieve `S` on `X`, if the identity arrow (or morphism) on `X` is in the sieve `S`, then `S` must be the top or maximal sieve on `X`. In other words, if a sieve includes the identity morphism on an object, it is the largest possible sieve on that object.
More concisely: In any category, if a sieve on an object contains the identity morphism, then it is the maximal (or top) sieve on that object.
|
Mathlib.CategoryTheory.Sites.Sieves._auxLemma.4
theorem Mathlib.CategoryTheory.Sites.Sieves._auxLemma.4 :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (self : CategoryTheory.Sieve X) {Y Z : C}
{f : Y ⟶ X}, self.arrows f → ∀ (g : Z ⟶ Y), self.1 (CategoryTheory.CategoryStruct.comp g f) = True
This theorem states that for any category `C`, and any object `X` in this category, let `self` be a sieve on `X`. If an arrow `f` from some object `Y` to `X` is in this sieve, then for any arrow `g` from any object `Z` to `Y`, the composition of `g` and `f` (`g ≫ f`) also belongs to the sieve `self`. This establishes that sieves in a category are stable under precomposition.
More concisely: For any category C and object X, if a sieve on X contains an arrow from Y to X, then it also contains the composition of any arrow from Z to Y with that arrow.
|
CategoryTheory.Sieve.pullback_top
theorem CategoryTheory.Sieve.pullback_top :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X},
CategoryTheory.Sieve.pullback f ⊤ = ⊤
This theorem states that for any category `C`, and any two objects `X` and `Y` in `C`, and any morphism `f` from `Y` to `X`, the pullback of the top sieve (denoted as ⊤, which includes all morphisms into the object in the category) along `f` is still the top sieve. In other words, the pullback of the maximum (top) sieve through any morphism remains the maximum (top) sieve.
More concisely: For any category C, any objects X and Y, and morphism f from Y to X, the pullback of the top sieve along f is equal to the top sieve.
|
CategoryTheory.Sieve.pullback_monotone
theorem CategoryTheory.Sieve.pullback_monotone :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X),
Monotone (CategoryTheory.Sieve.pullback f)
This theorem states that for any category `C`, and any morphism `f` from an object `Y` to another object `X` in `C`, the pullback operation (which assigns to each sieve on `X` a sieve on `Y` that is the inverse image of the original sieve under the morphism `f`) is monotone. In other words, if a sieve `S` is "less than or equal to" a sieve `T` (in the sense that every morphism in `S` is also in `T`), then the pullback of `S` under `f` is "less than or equal to" the pullback of `T` under `f`. This property is crucial in many constructions involving categories and functors.
More concisely: Given any category `C`, any morphism `f` from object `Y` to `X`, and sieves `S` and `T` on `X` with `S ⊆ T`, the pullback of `S` under `f` is contained in the pullback of `T` under `f`.
|
CategoryTheory.Sieve.pullback_eq_top_iff_mem
theorem CategoryTheory.Sieve.pullback_eq_top_iff_mem :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {S : CategoryTheory.Sieve X} (f : Y ⟶ X),
S.arrows f ↔ CategoryTheory.Sieve.pullback f S = ⊤
This theorem states that for any category `C`, for any objects `X`, `Y` in `C`, and for any morphism `f` from `Y` to `X`, and for any sieve `S` on `X`, the morphism `f` is in the sieve `S` if and only if the pullback of the sieve `S` along the morphism `f` is the maximal sieve on `Y`. Here, the pullback of a sieve `S` along a morphism `f` is the set of morphisms that, when composed with `f`, are in `S`. The maximal sieve on an object is the set of all morphisms into that object.
More concisely: For any category C, morphism f from Y to X, and sieve S on X, f is in S if and only if the pullback of S along f is the maximal sieve on Y.
|
CategoryTheory.Sieve.ext
theorem CategoryTheory.Sieve.ext :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {R S : CategoryTheory.Sieve X},
(∀ ⦃Y : C⦄ (f : Y ⟶ X), R.arrows f ↔ S.arrows f) → R = S
This theorem is stating that in any category `C`, for any object `X` in `C` and any two sieves `R` and `S` on `X`, if for all objects `Y` in `C` and all morphisms `f` from `Y` to `X`, `f` is an arrow of sieve `R` if and only if `f` is an arrow of sieve `S`, then sieve `R` must be equal to sieve `S`. In other words, two sieves on the same object are equal if they have the same set of morphisms.
More concisely: In any category, two sieves on an object are equal if and only if they have the same set of morphisms to that object.
|
CategoryTheory.Sieve.pullbackArrows_comm
theorem CategoryTheory.Sieve.pullbackArrows_comm :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
{X Y : C} (f : Y ⟶ X) (R : CategoryTheory.Presieve X),
CategoryTheory.Sieve.generate (CategoryTheory.Presieve.pullbackArrows f R) =
CategoryTheory.Sieve.pullback f (CategoryTheory.Sieve.generate R)
This theorem states that in a category 'C' having pullbacks, for any objects 'X' and 'Y' and a morphism 'f' from 'Y' to 'X', and for a presieve 'R' on 'X', the action of generating a sieve from the pullback of the presieve 'R' along the morphism 'f' is equivalent to the action of first generating a sieve from the presieve 'R' and then taking the pullback along 'f'. In other words, the operations of generating a sieve and pulling back a sieve commute with each other.
More concisely: In a pullback-stable category C, for any morphism f : Y -> X and presieve R on X, the pullback of R along f is equal to the restriction of R along the pullback of f.
|
CategoryTheory.Sieve.generate_sieve
theorem CategoryTheory.Sieve.generate_sieve :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X),
CategoryTheory.Sieve.generate S.arrows = S
The theorem `CategoryTheory.Sieve.generate_sieve` states that for any category `C` and any object `X` in this category, if `S` is a Sieve on `X`, then generating a Sieve from the arrows of `S` yields `S` itself. In other words, the generation process does not alter an existing Sieve. This highlights that the `generate` function is idempotent on sieves in the context of category theory.
More concisely: For any category C and object X, generating a sieve from the arrows of a sieve S on X results in S itself.
|
CategoryTheory.Presieve.FunctorPushforwardStructure.fac
theorem CategoryTheory.Presieve.FunctorPushforwardStructure.fac :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X : C}
{S : CategoryTheory.Presieve X} {Y : D} {f : Y ⟶ F.obj X}
(self : CategoryTheory.Presieve.FunctorPushforwardStructure F S f),
f = CategoryTheory.CategoryStruct.comp self.lift (F.map self.premap)
The theorem `CategoryTheory.Presieve.FunctorPushforwardStructure.fac` states that in any category `C` and `D` with objects `X` and `Y` respectively, and a functor `F` from `C` to `D`, for any set `S` of arrows in `C` all with codomain `X`, and any morphism `f` from `Y` to the functor's object at `X`, there exists a factorization of the morphism `f`. This factorization is such that `f` equals the composition of the lift of `f` and the map of the premap of `f` via the functor `F`. It's essentially saying that the morphism `f` can be decomposed into a sequence of two other morphisms.
More concisely: For any functor F from category C to category D, given an object X in C and an arrow f from an object Y in D to F.X, there exists a factorization of f as the composition of the lift of f along the preimage map under F and the preimage map itself.
|
CategoryTheory.Sieve.pullback_eq_top_of_mem
theorem CategoryTheory.Sieve.pullback_eq_top_of_mem :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (S : CategoryTheory.Sieve X) {f : Y ⟶ X},
S.arrows f → CategoryTheory.Sieve.pullback f S = ⊤
This theorem, `CategoryTheory.Sieve.pullback_eq_top_of_mem`, states that for all categories `C` with objects `X` and `Y`, and for a given sieve `S` on `X` and a morphism `f` from `Y` to `X`, if `f` is a member of the set of arrows of `S`, then the pullback of `S` along `f` is the top sieve on `Y`. In other words, if a morphism from `Y` to `X` is in a sieve on `X`, then pulling this sieve back along this morphism gives us the maximal sieve (i.e., the sieve containing all possible morphisms) on `Y`.
More concisely: Given a category `C` with objects `X` and `Y`, a sieve `S` on `X`, and a morphism `f` from `Y` to `X` in `S`, the pullback of `S` along `f` is the top sieve on `Y`.
|
CategoryTheory.Presieve.singleton.mk
theorem CategoryTheory.Presieve.singleton.mk :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X},
CategoryTheory.Presieve.singleton f f
The theorem `CategoryTheory.Presieve.singleton.mk` states that for any category `C` and any two objects `X` and `Y` in `C`, for any morphism `f` from `Y` to `X`, `f` is in the presieve generated by `f`. In other words, the morphism `f` is included in the singleton presieve of `f`. This makes sense because a singleton presieve, by definition, is the set that only contains the morphism used to generate it.
More concisely: For any category C, morphism f : C.Obj X → C.Obj Y, and object X, Y in C, f ∈ {g | ∃ h : C.Morset.singleton h, C.Morset.mem (C.Morset.singleton h) f}.
|
CategoryTheory.Presieve.FunctorPushforwardStructure.cover
theorem CategoryTheory.Presieve.FunctorPushforwardStructure.cover :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X : C}
{S : CategoryTheory.Presieve X} {Y : D} {f : Y ⟶ F.obj X}
(self : CategoryTheory.Presieve.FunctorPushforwardStructure F S f), S self.premap
The theorem `CategoryTheory.Presieve.FunctorPushforwardStructure.cover` states that for any category `C` and `D`, any functor `F` from `C` to `D`, any object `X` in `C`, any presieve `S` on `X`, any object `Y` in `D`, and any morphism `f` from `Y` to the image of `X` under `F`, if you have a FunctorPushforwardStructure (a structure which gives the details of how a particular morphism can be factored through the action of the functor) for `F`, `S` and `f`, then the morphism `premap` (which is a part of the FunctorPushforwardStructure) is in the presieve `S`. In other words, the preimage of the given morphism under the functor falls under the specified presieve.
More concisely: Given a functor $F$ from category $C$ to $D$, an object $X$ in $C$, a presieve $S$ on $X$, an object $Y$ in $D$, and a morphism $f$ from $Y$ to $F(X)$, if there exists a FunctorPushforwardStructure for $F$, $S$, and $f$, then $f \circ \text{image}(g) \in S$ for any $g$ in the presieve $S$.
|
CategoryTheory.Sieve.generate_of_contains_isSplitEpi
theorem CategoryTheory.Sieve.generate_of_contains_isSplitEpi :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {R : CategoryTheory.Presieve X} (f : Y ⟶ X)
[inst_1 : CategoryTheory.IsSplitEpi f], R f → CategoryTheory.Sieve.generate R = ⊤
The theorem `CategoryTheory.Sieve.generate_of_contains_isSplitEpi` states that for any category `C`, given two objects `X` and `Y` in `C`, a presieve `R` on `X`, and an arrow `f` from `Y` to `X` that is a split epimorphism. If `f` is contained in the presieve `R`, then the sieve generated by `R` is the maximal sieve. In other words, if a set of arrows contains a split epimorphism, it generates the largest possible sieve.
More concisely: Given a category `C`, an object `X`, a presieve `R` on `X`, and an arrow `f` from `Y` to `X` that is a split epimorphism contained in `R`, the sieve generated by `R` is the maximal sieve.
|
CategoryTheory.Sieve.pullback_comp
theorem CategoryTheory.Sieve.pullback_comp :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ Y}
(S : CategoryTheory.Sieve X),
CategoryTheory.Sieve.pullback (CategoryTheory.CategoryStruct.comp g f) S =
CategoryTheory.Sieve.pullback g (CategoryTheory.Sieve.pullback f S)
The theorem `CategoryTheory.Sieve.pullback_comp` states that for any category `C` with objects `X`, `Y`, and `Z`, and morphisms `f` from `Y` to `X` and `g` from `Z` to `Y`, for any Sieve `S` on `X`, pulling back the Sieve `S` along the composite morphism `g ≫ f` (i.e., `g` followed by `f`) is equivalent to first pulling back `S` along `f` and then pulling back the result along `g`. This theorem captures the intuitive idea that the order of pulling back sieves along a composition of morphisms doesn't matter.
More concisely: For any category C, morphisms f from Y to X and g from Z to Y, and sieve S on X, the pullback of S along the composite morphism g ≫ f is equal to the pullback of the pullback of S along f along g.
|
CategoryTheory.Sieve.le_generate
theorem CategoryTheory.Sieve.le_generate :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (R : CategoryTheory.Presieve X),
R ≤ (CategoryTheory.Sieve.generate R).arrows
The theorem `CategoryTheory.Sieve.le_generate` states that for any category `C` and an object `X` in `C`, any presieve `R` on `X` is less than or equal to the set of arrows in the sieve generated by `R`. In other words, all arrows in the presieve `R` are also contained in the generated sieve. This means that generating a sieve from a presieve `R` does not lose any arrows that were originally in `R`.
More concisely: For any category C and object X, every presieve R on X is contained in the sieve generated by R.
|
CategoryTheory.Sieve.downward_closed
theorem CategoryTheory.Sieve.downward_closed :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (self : CategoryTheory.Sieve X) {Y Z : C}
{f : Y ⟶ X}, self.arrows f → ∀ (g : Z ⟶ Y), self.arrows (CategoryTheory.CategoryStruct.comp g f)
This theorem, named "downward_closed", is a part of Category Theory in the Sieve section. It states that for any category 'C', an object 'X' in 'C', and a sieve on 'X', if a morphism 'f' from 'Y' to 'X' is in the sieve, then for any morphism 'g' from 'Z' to 'Y', the composite morphism 'g ≫ f' (the composition of 'g' and 'f') is also in the sieve. This property is often referred to as a sieve being "downward closed" or stable under precomposition.
More concisely: In any category 'C', a sieve on an object 'X' is downward closed if for every morphism 'f' from 'Y' to 'X' in the sieve and any morphism 'g' from 'Z' to 'Y', the composite morphism 'g ≫ f' is also in the sieve.
|
CategoryTheory.Sieve.pullback_id
theorem CategoryTheory.Sieve.pullback_id :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X},
CategoryTheory.Sieve.pullback (CategoryTheory.CategoryStruct.id X) S = S
The theorem `CategoryTheory.Sieve.pullback_id` states that for any category `C` and any object `X` in `C`, if we have a sieve `S` on `X`, then pulling back `S` via the identity morphism on `X` results in the original sieve `S`. This is essentially saying that the pullback operation preserves the identity, which is a common property in category theory.
More concisely: For any category $C$ and object $X$ in $C$, and any sieve $S$ on $X$, the pullback of $S$ along the identity morphism on $X$ equals $S$.
|
Mathlib.CategoryTheory.Sites.Sieves._auxLemma.10
theorem Mathlib.CategoryTheory.Sites.Sieves._auxLemma.10 :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {R S : CategoryTheory.Sieve X},
(R = S) = ∀ ⦃Y : C⦄ (f : Y ⟶ X), R.arrows f ↔ S.arrows f
This theorem states that for any category `C`, and any two sieves `R` and `S` on an object `X` in `C`, the sieves `R` and `S` are equal if and only if for any object `Y` in `C` and any morphism `f` from `Y` to `X`, `f` is in the sieve `R` if and only if `f` is in the sieve `S`. Essentially, two sieves are the same if they contain exactly the same morphisms.
More concisely: Two sieves on an object in a category are equal if and only if they contain the same morphisms.
|
CategoryTheory.Presieve.hasPullbacks.has_pullbacks
theorem CategoryTheory.Presieve.hasPullbacks.has_pullbacks :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {R : CategoryTheory.Presieve X}
[self : R.hasPullbacks] {Y Z : C} {f : Y ⟶ X}, R f → ∀ {g : Z ⟶ X}, R g → CategoryTheory.Limits.HasPullback f g
This theorem states that for any category `C`, any object `X` in `C`, and any presieve `R` on `X` that has pullbacks, for all arrows `f` from an object `Y` to `X` and `g` from an object `Z` to `X` such that both `f` and `g` are in `R`, the pullback of `f` and `g` exists. In mathematical terms, given two morphisms `f: Y -> X` and `g: Z -> X` in a category `C` such that `f` and `g` are in a presieve `R` on `X` with pullbacks, there exists a limit to the cospan formed by `f` and `g`.
More concisely: Given any category `C`, an object `X` in `C`, a presieve `R` on `X` with pullbacks, and morphisms `f: Y -> X` and `g: Z -> X` in `R`, there exists a pullback of `f` and `g`.
|
CategoryTheory.Sieve.galoisConnection
theorem CategoryTheory.Sieve.galoisConnection :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X),
GaloisConnection (CategoryTheory.Sieve.pushforward f) (CategoryTheory.Sieve.pullback f)
The theorem `CategoryTheory.Sieve.galoisConnection` states that for any category `C`, and any morphism `f` from an object `Y` to an object `X` within `C`, there is a Galois connection between the operation of pushing forward a sieve along `f` and the operation of pulling back a sieve along `f`. This means that for a given sieve on `Y`, pushing it forward along `f` and then pulling it back yields a sieve that is less than or equal to the original. And conversely, for a given sieve on `X`, pulling it back along `f` and then pushing it forward yields a sieve that is greater than or equal to the original.
More concisely: For any morphism `f` in a category `C` and any sieve on `Y`, the image of the sieve under `f` (pushed forward) is included in the pullback of the sieve along `f`, and conversely, for any sieve on `X`, the pullback of the sieve along `f` is included in the image of the sieve under `f`.
|