CategoryTheory.Presieve.firstMap_eq_secondMap
theorem CategoryTheory.Presieve.firstMap_eq_secondMap :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : C} (F : CategoryTheory.Functor Cᵒᵖ (Type (max u v))),
CategoryTheory.Presieve.IsSheafFor F
(CategoryTheory.Presieve.ofArrows Empty.elim fun a => instIsEmptyEmpty.elim a) →
CategoryTheory.Limits.IsInitial I →
∀ {α : Type} {X : α → C} (c : CategoryTheory.Limits.Cofan X)
[inst_1 : (CategoryTheory.Presieve.ofArrows X c.inj).hasPullbacks]
[inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : ∀ (i : α), CategoryTheory.Mono (c.inj i)],
(Pairwise fun i j =>
CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to (X i))
(CategoryTheory.Limits.initial.to (X j)) (c.inj i) (c.inj j)) →
CategoryTheory.Equalizer.Presieve.Arrows.firstMap F X c.inj =
CategoryTheory.Equalizer.Presieve.Arrows.secondMap F X c.inj
This theorem states that for a given category `C`, an object `I` in `C`, a contravariant functor `F` from `C` to the category of types, and a mapping `X` from some type `α` to `C`, if `F` is a sheaf for the presheaf defined by the empty set and the empty function, and `I` is an initial object in `C`, then the two parallel maps (referred to as the "first map" and "second map") in the equalizer diagram for the sheaf condition, corresponding to the inclusion maps in a disjoint coproduct, are equal. This equality holds under the conditions that the category `C` has an initial object, the arrows from the initial object to the images of `X` are monomorphisms (injective morphisms), and these arrows form a pullback, which is a special type of limit in category theory, for every distinct pair of elements in `α`. The theorem is a part of the theory of sheaves in category theory, and can be used in various fields of mathematics, including algebraic geometry and algebraic topology.
More concisely: For a category with an initial object `C`, an object `I` as its initial object, a contravariant sheaf `F` on `C` over the empty presheaf, and a mapping `X : α → C` with monomorphic and pullback-forming arrows from `I` to `X(α_i)` for distinct `α_i` in `α`, the first and second maps in the equalizer diagram of `F`'s sheaf condition are equal.
|
CategoryTheory.Presieve.isSheafFor_of_preservesProduct
theorem CategoryTheory.Presieve.isSheafFor_of_preservesProduct :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type (max u v)))
{α : Type} {X : α → C} (c : CategoryTheory.Limits.Cofan X),
CategoryTheory.Limits.IsColimit c →
∀ [inst_1 : (CategoryTheory.Presieve.ofArrows X c.inj).hasPullbacks]
[inst_2 :
CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun x => Opposite.op (X x)) F],
CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows X c.inj)
The theorem `CategoryTheory.Presieve.isSheafFor_of_preservesProduct` states that if a functor `F` preserves a particular product, then it is a sheaf for the corresponding presieve of arrows. More precisely, given a category `C`, a functor `F` from the opposite of `C` to a category of types, a function `X` from a type `α` to `C`, and a `Cofan` `c` over `X`, if `c` is a colimit, and if there are pullbacks for the presieve of arrows from `X` to `c.inj`, and `F` preserves the limit of the discrete functor from `X` to the opposite of the image of `X`, then `F` is a sheaf for the presieve of arrows from `X` to `c.inj`.
More concisely: If a functor preserves products in a category and satisfies certain conditions, then it is a sheaf for the presieve of arrows to a given object.
|