Prestacks: descent of morphisms #
Let C be a category and F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.
Given S : C, and objects M and N in F.obj (.mk (op S)),
we define a presheaf of types F.presheafHom M N on the category Over S:
its sections on an object T : Over S corresponding to a morphism p : X ⟶ S
are the type of morphisms p^* M ⟶ p^* N. We shall say that
F satisfies the descent of morphisms for a Grothendieck topology J
if these presheaves are all sheaves (typeclass F.IsPrestack J).
Terminological note #
In this file, we use the language of pseudofunctors to formalize prestacks. Similar notions could also be phrased in terms of fibered categories. In the mathematical literature, various uses of the words "prestacks" and "stacks" exists. Our definitions are consistent with Giraud's definition II 1.2.1 in Cohomologie non abélienne: a prestack is defined by the descent of morphisms condition with respect to a Grothendieck topology, and a stack by the effectiveness of the descent. However, contrary to Laumon and Moret-Bailly in Champs algébriques 3.1, we do not require that target categories are groupoids.
TODO #
- Relate this notion to the property that for any covering family
f i : X i ⟶ SforJ, the functorF.obj Sto the category of objects inF.obj (X i)for alliequipped with a descent datum is fully faithful. - Define a typeclass
IsStack(extendingIsPrestack?) by saying that the functors mentioned above are essentially surjective.
References #
Given a pseudofunctor F from LocallyDiscrete Cᵒᵖ to Cat, objects M₁ and M₂
of F over X₁ and X₂, morphisms f₁ : Y ⟶ X₁ and f₂ : Y ⟶ X₂, this is a version
of the pullback map (f₁^* M₁ ⟶ f₂^* M₂) → (g^* (f₁^* M₁) ⟶ g^* (f₂^* M₂)) by a
morphism g : Y' ⟶ Y, where we actually replace g^* (f₁^* M₁) by gf₁^* M₁
where gf₁ : Y' ⟶ X₁ is a morphism such that g ≫ f₁ = gf₁ (and similarly for M₂).
Equations
- One or more equations did not get rendered due to their size.
Instances For
If F is a pseudofunctor from Cᵒᵖ to Cat, and M and N are objects in
F.obj (.mk (op S)), this is the presheaf of morphisms from M to N: it sends
an object T : Over S corresponding to a morphism p : X ⟶ S to the type
of morphisms $$p^* M ⟶ p^* N$$.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Compatiblity isomorphism of Pseudofunctor.presheafHom with "restrictions".
Equations
- One or more equations did not get rendered due to their size.
Instances For
The property that a pseudofunctor F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
satisfies the descent property for morphisms, i.e. is a prestack.
(See the terminological note in the introduction of the file Sites.Descent.IsPrestack.)
- isSheaf {S : C} (M N : ↑(F.obj { as := Opposite.op S })) : Presheaf.IsSheaf (J.over S) (F.presheafHom M N)
Instances
If F is a prestack from Cᵒᵖ to Cat relatively to a Grothendieck topology J,
and M and N are two objects in F.obj (.mk (op S)), this is the sheaf of
morphisms from M to N: it sends an object T : Over S corresponding to
a morphism p : X ⟶ S to the type of morphisms $$p^* M ⟶ p^* N$$.
Equations
- F.sheafHom J M N = { val := F.presheafHom M N, cond := ⋯ }