Prestacks: descent of morphisms #
Let C be a category and F : 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.
References #
- [Jean Giraud, Cohomologie non abélienne][giraud1971]
- [Gérard Laumon and Laurent Moret-Bailly, Champs algébriques][laumon-morel-bailly-2000]
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
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
Instances For
The bijection (M ⟶ N) ≃ (F.presheafHom M N).obj (op (Over.mk (𝟙 S))).
Equations
Instances For
Compatibility isomorphism of Pseudofunctor.presheafHom with "restrictions".
Equations
Instances For
The property that a pseudofunctor F : 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$.