CategoryTheory.Equalizer.Sieve.compatible_iff
theorem CategoryTheory.Equalizer.Sieve.compatible_iff :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C}
(S : CategoryTheory.Sieve X) (x : CategoryTheory.Equalizer.FirstObj P S.arrows),
((CategoryTheory.Equalizer.firstObjEqFamily P S.arrows).hom x).Compatible ↔
CategoryTheory.Equalizer.Sieve.firstMap P S x = CategoryTheory.Equalizer.Sieve.secondMap P S x
The theorem `CategoryTheory.Equalizer.Sieve.compatible_iff` states that for any category `C`, functor `P` from the opposite category of `C` to the category of types, `S` which is a sieve on an object `X` of `C`, and an element `x` of the first object of the equalizer associated with the arrows of `S` and `P`, the family of elements given by `x` is compatible if and only if the application of the `firstMap` and `secondMap` to `x` yield the same result. Here, compatibility refers to the condition that these mappings preserve the necessary structure to be equalizer maps in the category theory.
More concisely: For any category C, functor P from C�opf to Type, sieve S on an object X of C, and x in the equalizer of S and P, the family of elements given by x is compatible with S if and only if P(x) = firstMap x = secondMap x.
|
CategoryTheory.Equalizer.Sieve.equalizer_sheaf_condition
theorem CategoryTheory.Equalizer.Sieve.equalizer_sheaf_condition :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C}
(S : CategoryTheory.Sieve X),
CategoryTheory.Presieve.IsSheafFor P S.arrows ↔
Nonempty
(CategoryTheory.Limits.IsLimit
(CategoryTheory.Limits.Fork.ofι (CategoryTheory.Equalizer.forkMap P S.arrows) ⋯))
In the context of category theory, the theorem `CategoryTheory.Equalizer.Sieve.equalizer_sheaf_condition` states that for any category `C`, any presheaf `P` of types valued over `C`, and any sieve `S` on an object `X` of `C`, `P` is a sheaf for `S` if and only if there exists a limit of the fork defined by applying the function `CategoryTheory.Equalizer.forkMap` to `P` and the arrows of `S`. This limit is a particular kind of limit in category theory known as an equalizer, which captures the idea of solutions to certain equations in a category.
More concisely: For a category C, presheaf P over C, and sieve S on an object X of C, P is a sheaf for S if and only if the limit of the equalizer of P and the arrow composition in S, as defined by `CategoryTheory.Equalizer.forkMap`, exists.
|
CategoryTheory.Equalizer.Presieve.Arrows.compatible_iff
theorem CategoryTheory.Equalizer.Presieve.Arrows.compatible_iff :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {B : C}
{I : Type} (X : I → C) (π : (i : I) → X i ⟶ B) [inst_1 : (CategoryTheory.Presieve.ofArrows X π).hasPullbacks]
(x : CategoryTheory.Equalizer.Presieve.Arrows.FirstObj P X),
CategoryTheory.Presieve.Arrows.Compatible P π
((CategoryTheory.Limits.Types.productIso fun i => P.obj (Opposite.op (X i))).hom x) ↔
CategoryTheory.Equalizer.Presieve.Arrows.firstMap P X π x =
CategoryTheory.Equalizer.Presieve.Arrows.secondMap P X π x
The theorem `CategoryTheory.Equalizer.Presieve.Arrows.compatible_iff` states that for any category `C`, a functor `P` from the opposite of `C` to a type, a set of objects `X` in `C` indexed by `I`, and a family of morphisms `π` from `X` to an object `B`, given the condition that pullbacks exist for the presieve generated by `X` and `π`, an element `x` in the first object of the equalizer presieve of `X` is compatible (in the sense of the presieve arrows compatibility) if and only if the `firstMap` and the `secondMap` applied to `x` yield the same result. In other words, compatibility in this context is equivalent to these maps agreeing on `x`.
More concisely: Given a category `C`, a functor `P` from `C^{op}` to a type, a set of objects `X` in `C` indexed by `I`, morphisms `π : X → B`, and assuming pullbacks exist for the presieve generated by `X` and `π`, an element `x` in the first object of the equalizer presieve is compatible with `π` if and only if `firstMap(π(x)) = secondMap(x)`.
|
CategoryTheory.Equalizer.Presieve.Arrows.sheaf_condition
theorem CategoryTheory.Equalizer.Presieve.Arrows.sheaf_condition :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {B : C}
{I : Type} (X : I → C) (π : (i : I) → X i ⟶ B) [inst_1 : (CategoryTheory.Presieve.ofArrows X π).hasPullbacks],
CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Presieve.ofArrows X π) ↔
Nonempty
(CategoryTheory.Limits.IsLimit
(CategoryTheory.Limits.Fork.ofι (CategoryTheory.Equalizer.Presieve.Arrows.forkMap P X π) ⋯))
Given a category `C`, a contravariant functor `P` from `C` to the category of types, an object `B` in `C`, a type `I`, a function `X` from `I` to `C`, and a family of morphisms `π` from the images of `X` to `B`, this theorem states that `P` is a sheaf for the presieve generated by `X` and `π` if and only if there exists a limit for the fork given by the left morphism of the fork diagram. The existence of pullbacks for the presieve is assumed. This theorem is a formalization of the sheaf condition in category theory.
More concisely: A contravariant functor `P` from a category `C` to types is a sheaf for the presheaf generated by a function `X` from a type `I` to `C` and a family of morphisms `π` if and only if there exists a limit for the fork diagram formed by `X`, `π`, and the identity morphisms.
|
CategoryTheory.Equalizer.Presieve.compatible_iff
theorem CategoryTheory.Equalizer.Presieve.compatible_iff :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C}
(R : CategoryTheory.Presieve X) [inst_1 : R.hasPullbacks] (x : CategoryTheory.Equalizer.FirstObj P R),
((CategoryTheory.Equalizer.firstObjEqFamily P R).hom x).Compatible ↔
CategoryTheory.Equalizer.Presieve.firstMap P R x = CategoryTheory.Equalizer.Presieve.secondMap P R x
This theorem in Category Theory states that for any category `C`, functor `P : Cᵒᵖ → Type (max v u)`, object `X` of `C`, and `Presieve R` on `X`, if `R` has pullbacks and `x` is an element of the first object in the equalizer of `P` and `R`, then the family of elements represented by `x` is compatible if and only if the first and second map of the presieve equalizer applied to `x` yield the same result. Essentially, this theorem formalizes the condition for compatibility within the framework of equalizers and presieves in Category Theory.
More concisely: For any category `C`, functor `P : C⁰⁵ → Type (max v u)`, object `X` of `C`, presheaf `R` on `X` with pullbacks, and `x` in the equalizer of `P` and `R`, the family of elements represented by `x` is compatible if and only if `P(x, _) = R(x, _)` in `Type (max v u)`.
|
CategoryTheory.Equalizer.FirstObj.proof_1
theorem CategoryTheory.Equalizer.FirstObj.proof_1 :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max u_2 u_1)))
{X : C} (R : CategoryTheory.Presieve X),
CategoryTheory.Limits.HasLimit (CategoryTheory.Discrete.functor fun f => P.obj (Opposite.op f.fst))
This theorem states that for any category `C`, functor `P` from the opposite of `C` to the type `Type (max u_2 u_1)`, object `X` in `C`, and presieve `R` on `X`, there exists a limit for the functor obtained by assigning each element `f` in the discrete category (defined by the presieve `R`) to the object in the category of the functor `P` evaluated at the domain (first projection `f.fst`) of `f`, seen as an object in the opposite category of `C` (`Opposite.op f.fst`). In essence, this theorem is about the existence of certain limits in a functor category.
More concisely: For any category `C`, functor `P` from `Opposite C` to `Type`, object `X` in `C`, and presieve `R` on `X`, there exists a limit of the functor `P` along `R`.
|
CategoryTheory.Equalizer.Presieve.sheaf_condition
theorem CategoryTheory.Equalizer.Presieve.sheaf_condition :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C}
(R : CategoryTheory.Presieve X) [inst_1 : R.hasPullbacks],
CategoryTheory.Presieve.IsSheafFor P R ↔
Nonempty
(CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι (CategoryTheory.Equalizer.forkMap P R) ⋯))
The theorem `CategoryTheory.Equalizer.Presieve.sheaf_condition` states that for a given category `C`, a contravariant functor `P` from `C` to the category of types, and a presieve `R` on an object `X` in `C`, the functor `P` is a sheaf for the presieve `R` if and only if there exists an equalizer for the fork given by the map `CategoryTheory.Equalizer.forkMap P R`. In other words, the sheaf condition for a presieve in category theory can be checked by verifying whether a certain diagram, involving the functor applied to opposite morphisms in the presieve and the map into the product of the functor over the presieve, has an equalizer. This is a characterization of sheaves in terms of limit conditions in category theory.
More concisely: A contravariant functor is a sheaf for a presieve in a category if and only if there exists an equalizer for the corresponding fork involving the functor applied to opposite morphisms in the presieve and the map into the product of the functor over the presieve.
|