8 Stacks

Chapter 8 of the Stacks Project, Stacks, Tag 0266: the 12 sections of its 13 with a tag that a declaration carries, one article each, in the Stacks Project's order. Their 76 tags are carried by 128 declarations of the repository (all in StacksFrontier) and 15 registered declarations.

Section8.2 Presheaves of morphisms associated to fibred categories #

Section 8.2 of the Stacks Project, Tag 02Z9. 5 tags here are carried by 6 declarations of the repository (all in StacksFrontier) and 4 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 026A, a lemma

Tag 026A in the Stacks Project.

CategoryTheory.Functor.morRestrict_id, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Descent/IsStack/MorPresheaf.lean, line 131. The attribute's comment: “restriction along the identity”.

Restricting a section of Mor(x, y) along an identity of 𝒮/U leaves it unchanged.

lemma morRestrict_id (x y : p.Fiber U) (g : Over U)
    (m : pullbackFiber p x g.hom ⟶ pullbackFiber p y g.hom) :
    morRestrict p x y (𝟙 g) m = m

CategoryTheory.Functor.morRestrict_comp, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Descent/IsStack/MorPresheaf.lean, line 139. The attribute's comment: “compatibility with composition: φ|_{V″} = (φ|_{V′})|_{V″}”.

Restricting a section of Mor(x, y) along a composite is restricting along the two factors in turn.

lemma morRestrict_comp (x y : p.Fiber U) {g₁ g₂ g₃ : Over U} (h₁ : g₁ ⟶ g₂) (h₂ : g₂ ⟶ g₃)
    (m : pullbackFiber p x g₃.hom ⟶ pullbackFiber p y g₃.hom) :
    morRestrict p x y (h₁ ≫ h₂) m = morRestrict p x y h₁ (morRestrict p x y h₂ m)

Tag 02ZB, a definition

Tag 02ZB in the Stacks Project.

CategoryTheory.Functor.morPresheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Descent/IsStack/MorPresheaf.lean, line 150.

The presheaf Mor(x, y) on 𝒮/U of a fibred category p: its sections over f : V ⟶ U are the morphisms f^* x ⟶ f^* y of the fibre over V, and its restriction maps are CategoryTheory.Functor.morRestrict.

noncomputable def morPresheaf (x y : p.Fiber U) : (Over U)ᵒᵖ ⥤ Type v₂

CategoryTheory.Functor.isomSubpresheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/IsomPresheaf.lean, line 120. The attribute's comment: “The subpresheaf Isom(x, y) of Mor(x, y); the presheaf Mor(x, y) itself is CategoryTheory.Functor.morPresheaf.”.

Stacks 02ZB, the subpresheaf Isom(x, y) of Mor(x, y): over f : V ⟶ U its sections are the morphisms f^* x ⟶ f^* y of the fibre over V that are isomorphisms. This is a subpresheaf because restriction preserves isomorphisms, CategoryTheory.Functor.isIso_morRestrict.

noncomputable def isomSubpresheaf (x y : p.Fiber U) : Subfunctor (morPresheaf p x y)

Tag 042V, a lemma

Tag 042V in the Stacks Project.

CategoryTheory.Functor.IsFibredOneMorphism.morPresheafMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/TwoFibreProductMorPresheafMap.lean, line 380.

The map of presheaves Mor(x, y) ⟶ Mor(F x, F y) induced by a 1-morphism of fibred categories over 𝒞: over g it applies F to a section and conjugates by the comparison isomorphisms IsFibredOneMorphism.mapPullbackFiberIso.

noncomputable def morPresheafMap (hF : IsFibredOneMorphism p r₀ F₀) {U : 𝒞} (a b : p.Fiber U) :
    morPresheaf p a b ⟶ morPresheaf r₀ ((fiberFunctorOfCompEq hF.comp_eq U).obj a)
      ((fiberFunctorOfCompEq hF.comp_eq U).obj b)

Tag 02ZA, a remark

Tag 02ZA in the Stacks Project.

Declarations registered for the tag:

CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom registered with add_to_stacks in StacksCore/CategoryTheory/Sites/Descent/MorphismPresheaf.lean, line 21 (StacksCore): “Remark 8.2.4 observes that a category fibred in groupoids is equivalent to the fibred category of a contravariant functor into groupoids, and that for the latter the restriction maps of the presheaf Mor(x, y) of Definition 8.2.2 need no coherence isomorphisms. Mathlib works in exactly that model: for a pseudofunctor from the locally discrete bicategory on the opposite of the base into Cat, this is the restriction map from a morphism of the fibre over Y to a morphism of the fibre over Y', with the coherence isomorphisms carried by mapComp'.”.
CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom_id registered with add_to_stacks in StacksCore/CategoryTheory/Sites/Descent/MorphismPresheaf.lean, line 29 (StacksCore): “Restriction along an identity is the identity, the first half of the functoriality that Remark 8.2.4 says is trivial in this model.”.
CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom_pullHom registered with add_to_stacks in StacksCore/CategoryTheory/Sites/Descent/MorphismPresheaf.lean, line 32 (StacksCore): “Restriction respects composition, the second half of that functoriality.”.
CategoryTheory.Pseudofunctor.presheafHom registered with add_to_stacks in StacksCore/CategoryTheory/Sites/Descent/MorphismPresheaf.lean, line 34 (StacksCore): “The presheaf Mor(x, y) itself: the presheaf on Over S whose sections over a morphism p : X ⟶ S are the morphisms from the pullback of M along p to the pullback of N along p. Assembling it is Lemma 8.2.1, which Remark 8.2.4 is a remark about; the further ingredient the remark cites, invariance of Mor(x, y) under an equivalence of fibred categories (Lemma 042V), is not covered here.”.

Tag 04SI, a lemma

Tag 04SI in the Stacks Project.

CategoryTheory.Functor.isFiberedInSetoids_and_isoClassPresheaf_iso_isomPresheaf, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/IsomPresheafTwoFibreProduct.lean, line 582.

Stacks 04SI. Let 𝒞 be a category, let p : 𝒮 ⥤ 𝒞 be a fibred category, let U be an object of 𝒞 and let x, y be objects of the fibre category 𝒮_U. Denote x, y : 𝒞/U ⥤ 𝒮 also the corresponding 1-morphisms (a : V ⟶ U) ↦ a^* x (Stacks 004B). Then

the 2-fibre product 𝒮 ×_{𝒮 × 𝒮, (x, y)} 𝒞/U, whose objects over a : V ⟶ U are the triples (z, α : z ≅ a^* x, β : z ≅ a^* y) with z an object and α, β isomorphisms of 𝒮_V, is fibred in setoids over 𝒞/U, and

Isom(x, y) is the presheaf of sets corresponding to that category fibred in setoids (Stacks 04SC), namely its presheaf of isomorphism classes of objects of the fibres, the identification sending the class of (z, α, β) to β ∘ α⁻¹.

The second part is an isomorphism of presheaves, hence data: it is CategoryTheory.Functor.IsomPresheafTwoFibreProduct.presheafIso, pinned by the requirement that it send the class of (z, α, β) to β ∘ α⁻¹, which determines it, every class being the class of such a triple.

noncomputable def isFiberedInSetoids_and_isoClassPresheaf_iso_isomPresheaf
    (p : 𝒮 ⥤ 𝒞) [p.IsFibered] {U : 𝒞} (x y : p.Fiber U) :
    PProd (IsomPresheafTwoFibreProduct.proj p x y).IsFiberedInSetoids
      { e : (IsomPresheafTwoFibreProduct.proj p x y).isoClassPresheaf ≅
          p.isomPresheaf x y ⋙ uliftFunctor.{max u₁ v₁ u₂, v₂} //
        ∀ P : IsomPresheafTwoFibreProduct.Tot p x y,
          (e.hom.app (op P.y) (isoClassMk _ ⟨P, rfl⟩)).down.1.1 = P.iso.inv.1 ≫ P.iso.hom.2 }

Sources

LeanCategoryTheory.Functor.morRestrict_id · CategoryTheory.Functor.morRestrict_comp · CategoryTheory.Functor.morPresheaf · CategoryTheory.Functor.isomSubpresheaf · CategoryTheory.Functor.IsFibredOneMorphism.morPresheafMap · CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom · CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom_id · CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom_pullHom

Section8.3 Descent data in fibred categories #

Section 8.3 of the Stacks Project, Tag 02ZC. 7 tags here are carried by 13 declarations of the repository (all in StacksFrontier) and 11 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 026B, a definition

Tag 026B in the Stacks Project.

CategoryTheory.Functor.SieveDescentDatum, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Descent/IsStack/SieveDescentDatum.lean, line 57. The attribute's comment: “(1), sieve-indexed, with no chosen fibre products U i ×_U U j”. References: SGA 3 IV (2.1), “descent datum”; SGA 4½ Arcata (1.4.4).

A descent datum relative to a sieve R on U: an object of the fibre over V for each arrow f : V ⟶ U of R, and for each pair of arrows of R and each pair of morphisms ε, ε' into their sources agreeing over U, an isomorphism between the chosen pullbacks along ε and ε' of the two attached objects, compatible with composition and with base change.

structure SieveDescentDatum (p : 𝒳 ⥤ 𝒮) [p.IsFibered] {U : 𝒮} (R : Sieve U)

CategoryTheory.Functor.FamilyDescentDatum, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Descent/PullbackDescentData.lean, line 81. The attribute's comment: “The category DD(𝒰) for a fibred category: its objects (1), its morphisms (2) and its category structure (3). Indexed by an arbitrary object mapping to two members of the family in place of the chosen fibre products U i ×_U U i', which the two presentations agree over whenever those exist, by CategoryTheory.Pseudofunctor.DescentData'.descentDataEquivalence.”. References: SGA 3 IV (2.1), “descent datum”; SGA 1 VIII (7.8), “more general”.

The category of descent data relative to a family of morphisms with fixed target 𝒰 = {U i ⟶ U} for a fibred category p : 𝒳 ⥤ 𝒮: an object of the fibre 𝒳_{U i} for every i, together with a gluing isomorphism between the two pullbacks of these objects to any object Y mapping to U i and to U i' compatibly over U, subject to the cocycle condition and to compatibility with further base change.

abbrev FamilyDescentDatum (p : 𝒳 ⥤ 𝒮) [p.IsFibered] {U : 𝒮} (𝒰 : PreZeroHypercover.{w} U)

Declarations registered for the tag:

Pseudofunctor.DescentData' registered with add_to_stacks in StacksCore/CategoryTheory/Sites/Descent/DescentData.lean, line 41 (StacksCore): “(1)”.
Pseudofunctor.DescentData'.Hom registered with add_to_stacks in StacksCore/CategoryTheory/Sites/Descent/DescentData.lean, line 42 (StacksCore): “(2)”.
Pseudofunctor.DescentData'.instCategory registered with add_to_stacks in StacksCore/CategoryTheory/Sites/Descent/DescentData.lean, line 43 (StacksCore): “(3), the category DD(𝒰)”.

Tag 026C, remarks

Tag 026C in the Stacks Project.

CategoryTheory.Functor.DescentDatum.diagonalPullback_eq_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/InheritedTopology/Stack.lean, line 370. The attribute's comment: “diagonal identity”.

Let D be a descent datum for p fibred in groupoids, and Δ : V i ⟶ Vijk i i i the diagonal. A fibre automorphism e of x i which is the pullback along Δ of each of the three gluing isomorphisms of the triple (i, i, i) is the identity.

theorem DescentDatum.diagonalPullback_eq_id
    (D : DescentDatum p V f Vij pr₁ pr₂ hVij Vijk s₁₂ s₂₃ hVijk q₁ q₂ q₃ hq₁ hq₂ hq₃)
    (hp : p.IsFiberedInGroupoids) (i : I) {Δ : V i ⟶ Vijk i i i}
    {hΔ₁ : 𝟙 (V i) = Δ ≫ q₁ i i i} {hΔ₂ : 𝟙 (V i) = Δ ≫ q₂ i i i}
    {hΔ₃ : 𝟙 (V i) = Δ ≫ q₃ i i i}
    {e : D.x i ⟶ D.x i}
    (he : FibreHom p (D.x i) (D.x i) (D.hx i) (D.hx i) e)
    (heij : IsRestrictionOf p Δ hΔ₁ hΔ₂ (D.wi i i i) (D.wj i i i)
      (Restriction.id p (D.x i) (D.hx i)) (Restriction.id p (D.x i) (D.hx i))
      (D.αij i i i) e)
    (hejk : IsRestrictionOf p Δ hΔ₂ hΔ₃ (D.wj i i i) (D.wk i i i)
      (Restriction.id p (D.x i) (D.hx i)) (Restriction.id p (D.x i) (D.hx i))
      (D.αjk i i i) e)
    (heik : IsRestrictionOf p Δ hΔ₁ hΔ₃ (D.wi i i i) (D.wk i i i)
      (Restriction.id p (D.x i) (D.hx i)) (Restriction.id p (D.x i) (D.hx i))
      (D.αik i i i) e) :
    e = 𝟙 (D.x i)

CategoryTheory.Functor.DescentDatum.gluing_comp_switchPullback_eq_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/InheritedTopology/Stack.lean, line 397. The attribute's comment: “flip identity”.

Let D be a descent datum and Δ₁₃ : Vij i j ⟶ Vijk i j i the morphism whose composites with the three projections are pr₁ i j, pr₂ i j and pr₁ i j. If σφ is the pullback along Δ₁₃ of the (j, k) gluing isomorphism of the triple (i, j, i), then φ i j ≫ σφ = 𝟙.

theorem DescentDatum.gluing_comp_switchPullback_eq_id
    (D : DescentDatum p V f Vij pr₁ pr₂ hVij Vijk s₁₂ s₂₃ hVijk q₁ q₂ q₃ hq₁ hq₂ hq₃)
    (i j : I) {Δ₁₃ : Vij i j ⟶ Vijk i j i}
    {hΔ₁ : pr₁ i j = Δ₁₃ ≫ q₁ i j i} {hΔ₂ : pr₂ i j = Δ₁₃ ≫ q₂ i j i}
    {hΔ₃ : pr₁ i j = Δ₁₃ ≫ q₃ i j i}
    {σφ : (D.xrji i j).pt ⟶ (D.xrij i j).pt}
    (hσφ : FibreHom p (D.xrji i j).pt (D.xrij i j).pt
      (D.xrji i j).hpt (D.xrij i j).hpt σφ)
    (hij : IsRestrictionOf p Δ₁₃ hΔ₁ hΔ₂ (D.wi i j i) (D.wj i j i)
      (D.xrij i j) (D.xrji i j) (D.αij i j i) (D.φ i j))
    (hji : IsRestrictionOf p Δ₁₃ hΔ₂ hΔ₃ (D.wj i j i) (D.wk i j i)
      (D.xrji i j) (D.xrij i j) (D.αjk i j i) σφ)
    (hik : IsRestrictionOf p Δ₁₃ hΔ₁ hΔ₃ (D.wi i j i) (D.wk i j i)
      (D.xrij i j) (D.xrij i j) (D.αik i j i) (𝟙 (D.xrij i j).pt)) :
    D.φ i j ≫ σφ = 𝟙 (D.xrij i j).pt

Tag 02ZD, a lemma

Tag 02ZD in the Stacks Project.

CategoryTheory.Functor.FamilyDescentDatum.pull, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Descent/PullbackDescentData.lean, line 95. The attribute's comment: “(1) the descent datum (g i ^* Y (α i), (g i × g i') ^* φ (α i) (α i'))”.

Stacks 02ZD (1). The descent datum relative to 𝒰 = {U i ⟶ U} obtained from a descent datum (Y j, φ j j') relative to 𝒱 = {V j ⟶ V} by pulling back along a morphism of families Φ = (α, h, g): its object over U i is the chosen pullback g i ^* Y (α i), and its gluing morphisms are those of (Y j, φ j j') pulled back along the g i.

noncomputable def pull (Φ : 𝒰.HomOver 𝒱 h) (D : FamilyDescentDatum p 𝒱) :
    FamilyDescentDatum p 𝒰

CategoryTheory.Functor.FamilyDescentDatum.pullFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Descent/PullbackDescentData.lean, line 131. The attribute's comment: “(2) the functor from descent data relative to 𝒱 to descent data relative to 𝒰”.

Stacks 02ZD (2). Pulling back descent data along a morphism of families Φ = (α, h, g) from 𝒰 to 𝒱 is a functor from the category of descent data relative to 𝒱 to the category of descent data relative to 𝒰.

noncomputable def pullFunctor (Φ : 𝒰.HomOver 𝒱 h) :
    FamilyDescentDatum p 𝒱 ⥤ FamilyDescentDatum p 𝒰

CategoryTheory.Functor.FamilyDescentDatum.pullFunctorIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Descent/PullbackDescentData.lean, line 155. The attribute's comment: “(3) for two morphisms of families over one and the same h : U ⟶ V”.

Stacks 02ZD (3). Two morphisms of families Φ = (α, h, g) and Φ' = (α', h, g') from 𝒰 to 𝒱 lying over one and the same morphism h : U ⟶ V of the targets induce canonically isomorphic functors on descent data. The component of the isomorphism at a descent datum (Y j, φ j j') and an index i is the gluing isomorphism of that datum between g i ^* Y (α i) and g' i ^* Y (α' i).

noncomputable def pullFunctorIso (Φ Φ' : 𝒰.HomOver 𝒱 h) : pullFunctor p Φ ≅ pullFunctor p Φ'

CategoryTheory.Functor.FamilyDescentDatum.pullFunctorIsoOfEq, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Descent/PullbackDescentData.lean, line 173. The attribute's comment: “(3) for morphisms of families over h and over h' with h' = h, as in Stacks”.

Stacks 02ZD (3), with the hypothesis h = h' on the two morphisms of targets stated as such: morphisms of families Φ over h and Φ' over h' with h' = h induce canonically isomorphic functors on descent data.

noncomputable def pullFunctorIsoOfEq {h' : U ⟶ V} (Φ : 𝒰.HomOver 𝒱 h) (Φ' : 𝒰.HomOver 𝒱 h')
    (hh : h' = h) : pullFunctor p Φ ≅ pullFunctor p Φ'

Declarations registered for the tag:

Pseudofunctor.DescentData.pullFunctorObj registered with add_to_stacks in StacksCore/CategoryTheory/Sites/Descent/DescentData.lean, line 84 (StacksCore): “(1)”.
Pseudofunctor.DescentData.pullFunctor registered with add_to_stacks in StacksCore/CategoryTheory/Sites/Descent/DescentData.lean, line 85 (StacksCore): “(2)”.
Pseudofunctor.DescentData.pullFunctorIso registered with add_to_stacks in StacksCore/CategoryTheory/Sites/Descent/DescentData.lean, line 86 (StacksCore): “(3), with h = h' built in by sharing p”.

Tag 02ZE, a definition

Tag 02ZE in the Stacks Project.

CategoryTheory.Functor.FamilyDescentDatum.pullFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Descent/PullbackDescentData.lean, line 131.

Stacks 02ZD (2). Pulling back descent data along a morphism of families Φ = (α, h, g) from 𝒰 to 𝒱 is a functor from the category of descent data relative to 𝒱 to the category of descent data relative to 𝒰.

noncomputable def pullFunctor (Φ : 𝒰.HomOver 𝒱 h) :
    FamilyDescentDatum p 𝒱 ⥤ FamilyDescentDatum p 𝒰

Declarations registered for the tag:

Pseudofunctor.DescentData.pullFunctor registered with add_to_stacks in StacksCore/CategoryTheory/Sites/Descent/DescentData.lean, line 91 (StacksCore).

Tag 026E, a definition

Tag 026E in the Stacks Project.

CategoryTheory.Functor.SieveDescentDatum.ofFiber, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Descent/IsStack/OfFiber.lean, line 55. The attribute's comment: “(1) and (2) are one construction, read at two sieves: the trivial descent datum (X, id_X) on {𝟙 U} is this datum at the sieve generated by 𝟙 U, and the canonical descent datum (f_i^* X, can) on {f_i : U_i → U} is this datum at the sieve that family generates, with can the canonical comparison CategoryTheory.Functor.pullbackFiberComparison.”. References: SGA 3 IV (2.1), “canonical descent datum”.

The descent datum of an object x of the fibre over U: its chosen pullbacks, glued by the canonical comparisons of their iterated chosen pullbacks.

noncomputable def ofFiber (x : p.Fiber U) (R : Sieve U) : SieveDescentDatum p R

CategoryTheory.Functor.SieveDescentDatum.IsEffective, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Descent/IsStack/SieveDescentDatum.lean, line 111. The attribute's comment: “(3), effectivity of a descent datum, stated as the existence of an object x of the fibre over U and a cartesian morphism from each object of the datum to x compatible with the gluing isomorphisms, in place of an isomorphism with (f_i^* X, can).”. References: SGA 3 IV (3.5.1).

A descent datum is effective when it comes from an object x of the fibre over U: there is a cartesian morphism from each of its objects to x, compatibly with the gluing isomorphisms.

def IsEffective : Prop

Declarations registered for the tag:

Pseudofunctor.DescentData.ofObj registered with add_to_stacks in StacksCore/CategoryTheory/Sites/Descent/DescentData.lean, line 60 (StacksCore): “(1) and (2)”.
Pseudofunctor.toDescentData registered with add_to_stacks in StacksCore/CategoryTheory/Sites/Descent/DescentData.lean, line 61 (StacksCore): “(2), as a functor 𝒮_U ⥤ DD(𝒰)”.
Functor.essImage registered with add_to_stacks in StacksCore/CategoryTheory/Sites/Descent/DescentData.lean, line 62 (StacksCore): “(3), effectivity is (F.toDescentData f).essImage”.

Tag 026D, a lemma

Tag 026D in the Stacks Project.

CategoryTheory.Functor.pullbackFiberComparison_comp_compIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stackification/StageThreeStack.lean, line 112. The attribute's comment: “can_ij = (α_{pr₁, f_j})_X ∘ (α_{pr₀, f_i})_X⁻¹, where can is the gluing isomorphism pullbackFiberComparison of the canonical descent datum of Stacks 026E (2); stated as the commuting square, with α⁻¹ the contraction pullbackFiberCompIso of Stacks 02XO and f_i ∘ pr₀ = f_j ∘ pr₁ carried by pullbackFiberCongr”.

The comparison of two chosen pullbacks of a chosen pullback is the comparison of the two chosen pullbacks along the composites.

theorem pullbackFiberComparison_comp_compIso {T : 𝒮} (y : p.Fiber T) {V W Z : 𝒮} {g : V ⟶ T}
    {g' : W ⟶ T} (ε : Z ⟶ V) (ε' : Z ⟶ W) (heq : ε ≫ g = ε' ≫ g') :
    (pullbackFiberComparison y ε ε' heq).hom ≫ (pullbackFiberCompIso y g' ε').hom =
      (pullbackFiberCompIso y g ε).hom ≫ (pullbackFiberCongr y heq).hom

Declarations registered for the tag:

Pseudofunctor.DescentData.ofObj_hom registered with add_to_stacks in StacksCore/CategoryTheory/Sites/Descent/DescentData.lean, line 51 (StacksCore).

Tag 0GEA, a lemma

Tag 0GEA in the Stacks Project.

CategoryTheory.Functor.isEquivalence_toFamilyDescentDatum_of_homOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Descent/OfRefinement.lean, line 548.

Stacks 0GEA. Let 𝒱 = {V j ⟶ U} ⟶ 𝒰 = {U i ⟶ U} be a morphism of families of morphisms with fixed target given by 𝟙 U, a reindexing α : J → I and morphisms V j ⟶ U (α j), and let p be a fibred category. Assume that the fibre products U i₁ ×_U U i₂, U i ×_U V j and U i₁ ×_U U i₂ ×_U V j exist, that 𝒮_U ⟶ DD(𝒱) is an equivalence, that 𝒮_{U i} ⟶ DD(𝒱_i) is fully faithful for every i, and that 𝒮_{U i₁ ×_U U i₂} ⟶ DD(𝒱_{i₁i₂}) is faithful for every i₁, i₂, where 𝒱_i and 𝒱_{i₁i₂} are the base changes of 𝒱. Then 𝒮_U ⟶ DD(𝒰) is an equivalence.

theorem isEquivalence_toFamilyDescentDatum_of_homOver {p : 𝒳 ⥤ C} [p.IsFibered] {U : C}
    {𝒰 : PreZeroHypercover.{w} U} {𝒱 : PreZeroHypercover.{w'} U} (Φ : 𝒱.HomOver 𝒰 (𝟙 U))
    [∀ i₁ i₂, HasPullback (𝒰.f i₁) (𝒰.f i₂)]
    [∀ i j, HasPullback (𝒰.f i) (𝒱.f j)]
    [∀ i₁ i₂ j, HasPullback (pullback.fst (𝒰.f i₁) (𝒰.f i₂) ≫ 𝒰.f i₁) (𝒱.f j)]
    (h₂ : (toFamilyDescentDatum p 𝒱).IsEquivalence)
    (h₃ : ∀ i, Nonempty (toFamilyDescentDatum p (𝒱.pullback₁ (𝒰.f i))).FullyFaithful)
    (h₄ : ∀ i₁ i₂, (toFamilyDescentDatum p
      (𝒱.pullback₁ (pullback.fst (𝒰.f i₁) (𝒰.f i₂) ≫ 𝒰.f i₁))).Faithful) :
    (toFamilyDescentDatum p 𝒰).IsEquivalence

Sources

LeanCategoryTheory.Functor.SieveDescentDatum · CategoryTheory.Functor.FamilyDescentDatum · Pseudofunctor.DescentData' · Pseudofunctor.DescentData'.Hom · Pseudofunctor.DescentData'.instCategory · CategoryTheory.Functor.DescentDatum.diagonalPullback_eq_id · CategoryTheory.Functor.DescentDatum.gluing_comp_switchPullback_eq_id · CategoryTheory.Functor.FamilyDescentDatum.pull

Section8.4 Stacks #

Section 8.4 of the Stacks Project, Tag 0268. 9 tags here are carried by 15 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 026F, a definition

Tag 026F in the Stacks Project.

CategoryTheory.Functor.IsStack, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Descent/IsStack/Defs.lean, line 44. The attribute's comment: “for a functor, the three conditions being the three fields”.

The three conditions of Stacks 026F for a functor p : 𝒳 ⥤ 𝒮: p is a fibred category, the presheaves Mor(x, y) of Stacks 02ZB are sheaves, and descent along a covering sieve is effective.

Condition (2) refers to the chosen pullbacks that condition (1) provides, which is why its field reintroduces isFibered as an instance.

structure IsStack (p : 𝒳 ⥤ 𝒮) (J : GrothendieckTopology 𝒮) : Prop

Tag 02ZF, a lemma

Tag 02ZF in the Stacks Project.

CategoryTheory.Functor.isStack_iff_isEquivalence_toDescentData, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/DescentDataEquivalence.lean, line 375.

Stacks 02ZF. Let p : 𝒳 ⥤ 𝒮 be a fibred category over a site (𝒮, J). Then p is a stack if and only if, for every covering 𝒰 = {f i : U i ⟶ U} of the site, the functor 𝒳_U ⥤ DD(𝒰) sending an object of the fibre over U to its canonical descent datum relative to 𝒰 is an equivalence.

theorem isStack_iff_isEquivalence_toDescentData (J : GrothendieckTopology 𝒮) :
    p.IsStack J ↔ ∀ ⦃U : 𝒮⦄ (𝒰 : PreZeroHypercover.{max u₁ v₁} U), 𝒰.sieve₀ ∈ J U →
      ((pullbackPseudofunctor p).toDescentData 𝒰.f).IsEquivalence

Tag 04TU, a lemma

Tag 04TU in the Stacks Project.

CategoryTheory.Functor.IsStack.fullSubcategory, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Descent/IsStack.lean, line 113.

Let p : 𝒳 ⥤ 𝒮 be a stack over the site (𝒮, J) and let P cut out a full subcategory of 𝒳. If P is closed under strongly cartesian pullbacks and locally closed, both read fibrewise through IsoOverId, then the restriction of p to that full subcategory is a stack.

theorem IsStack.fullSubcategory (p : 𝒳 ⥤ 𝒮) (J : GrothendieckTopology 𝒮) (hp : IsStack p J)
    (P : ObjectProperty 𝒳) (h1 : ClosedUnderStronglyCartesian p P)
    (h3 : haveI : p.IsPreFibered := hp.isFibered.toIsPreFibered; LocallyClosed p P J) :
    IsStack (Functor.restrict p P) J

Tag 042W, a lemma

Tag 042W in the Stacks Project.

CategoryTheory.BasedCategory.isStack_iff_of_equivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/Transport.lean, line 32.

Let (𝒞, J) be a site and let 𝒳, 𝒴 be categories over 𝒞. If 𝒳 and 𝒴 are equivalent as categories over 𝒞, then 𝒳 is a stack over 𝒞 if and only if 𝒴 is.

theorem BasedCategory.isStack_iff_of_equivalence
    (e : BasedCategory.Equivalence 𝒳 𝒴) (J : GrothendieckTopology 𝒞) :
    𝒳.p.IsStack J ↔ 𝒴.p.IsStack J

Tag 02ZG, a definition

Tag 02ZG in the Stacks Project.

CategoryTheory.BasedStack, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/TwoCategory.lean, line 62. The attribute's comment: “(1)”.

Stacks 02ZG (1). An object of the 2-category of stacks over the site (𝒞, J): a category over 𝒞 whose structure functor is a stack.

structure BasedStack (𝒞 : Type u₁) [Category.{v₁} 𝒞] (J : GrothendieckTopology 𝒞)

CategoryTheory.BasedStack.Hom, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/TwoCategory.lean, line 78. The attribute's comment: “(2)”.

Stacks 02ZG (2). A 1-morphism of stacks over 𝒞: a functor G between the underlying categories with p' ∘ G = p, which carries strongly cartesian morphisms to strongly cartesian morphisms. The first condition is the field w of a BasedFunctor and is repeated as comp_eq inside Functor.IsFibredOneMorphism.

structure Hom (𝒳 𝒴 : BasedStack.{v₁, v₂, u₁, u₂} 𝒞 J)

CategoryTheory.BasedStack.homCategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/TwoCategory.lean, line 109. The attribute's comment: “(3)”.

Stacks 02ZG (3). The 2-morphisms between two 1-morphisms of stacks: the morphisms of functors t with p'(t_x) = 𝟙 (p x) for every object x, that is the BasedNatTrans between the underlying functors over 𝒞. Nothing is imposed on a 2-morphism beyond that, so this category of 1-morphisms is the one of the ambient 2-category BasedCategory 𝒞.

instance homCategory (𝒳 𝒴 : BasedStack.{v₁, v₂, u₁, u₂} 𝒞 J) : Category (𝒳 ⟶ 𝒴)

CategoryTheory.BasedStack.bicategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/TwoCategory.lean, line 203.

Stacks 02ZG. The 2-category of stacks over the site (𝒞, J): the sub-2-category of the 2-category of fibred categories over 𝒞 (Stacks 02XP) whose objects are the stacks over 𝒞, whose 1-morphisms are the functors over 𝒞 preserving strongly cartesian morphisms, and whose 2-morphisms are the morphisms of functors whose components lie over identities.

instance bicategory : Bicategory (BasedStack.{v₁, v₂, u₁, u₂} 𝒞 J)

Tag 026G, a lemma

Tag 026G in the Stacks Project.

CategoryTheory.TwoFibreProductOver.isStack_structureFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/TwoFibreProductDescentIndependentBase.lean, line 647.

The 2-fibre product of stacks over a site (𝒞, J) is a stack, with the hom universe of the site independent of the hom universe of the three categories of the cospan: if p𝒳, p𝒴, p𝒮 are stacks over (𝒞, J) and F, G are 1-morphisms of fibred categories over 𝒞, then the structure functor of the explicit 2-fibre product 𝒳 ×_𝒮 𝒴 is again a stack.

theorem isStack_structureFunctor
    (p𝒳 : 𝒳 ⥤ 𝒞) (p𝒴 : 𝒴 ⥤ 𝒞) (p𝒮 : 𝒮 ⥤ 𝒞) (F : 𝒳 ⥤ 𝒮) (G : 𝒴 ⥤ 𝒮)
    (J : GrothendieckTopology 𝒞) (h𝒳 : Functor.IsStack p𝒳 J) (h𝒴 : Functor.IsStack p𝒴 J)
    (h𝒮 : Functor.IsStack p𝒮 J) (hF : Functor.IsFibredOneMorphism p𝒳 p𝒮 F)
    (hG : Functor.IsFibredOneMorphism p𝒴 p𝒮 G) :
    Functor.IsStack (TwoFibreProductOver.structureFunctor p𝒳 p𝒴 p𝒮 F G) J

Tag 04WQ, a lemma

Tag 04WQ in the Stacks Project.

CategoryTheory.Stack.Hom.isFullyFaithful_iff_morSheafIso, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Descent/IsPrestack.lean, line 248.

Stacks 04WQ. A 1-morphism of stacks is fully faithful if and only if it induces isomorphisms on the sheaves of morphisms.

Condition (1) is read fibrewise here rather than on the total categories, which is what makes the implication from (2) available without the reduction to strongly cartesian morphisms of the Stacks proof; see Stack.Hom.IsFullyFaithful.

theorem isFullyFaithful_iff_morSheafIso (F : Stack.Hom T T') :
    F.IsFullyFaithful ↔ F.MorSheafIso

Tag 046N, a lemma

Tag 046N in the Stacks Project.

CategoryTheory.Functor.isEquivalenceOver_iff_locallyEssSurjOnFibers, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/InheritedTopology/FullyFaithfulEquivalence.lean, line 55.

Stacks 046N. Let (𝒞, J) be a site, let p : 𝒳 ⥤ 𝒞 and q : 𝒴 ⥤ 𝒞 be stacks over 𝒞 and let F : 𝒳 ⥤ 𝒴 be a fully faithful 1-morphism of fibred categories over 𝒞. Then the following are equivalent:

F is an equivalence over 𝒞;

for every object U of 𝒞 and every object x of the fibre of 𝒴 over U there is a covering sieve of U along each member f of which f^* x is in the essential image of the functor induced by F on the fibres over the source of f.

theorem isEquivalenceOver_iff_locallyEssSurjOnFibers
    {p : 𝒳 ⥤ 𝒞} {q : 𝒴 ⥤ 𝒞} {F : 𝒳 ⥤ 𝒴} {J : GrothendieckTopology 𝒞}
    (h₁ : p.IsStack J) (h₂ : q.IsStack J) (hF : IsFibredOneMorphism p q F)
    [F.Full] [F.Faithful] :
    Nonempty (IsEquivalenceOver p q F) ↔ LocallyEssSurjOnFibers h₂.isFibered hF.comp_eq J

Tag 03ZZ, a remark

Tag 03ZZ in the Stacks Project.

CategoryTheory.Functor.small_fibreRepresentatives, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/FibreRepresentatives.lean, line 102. The attribute's comment: “the cutdown: a full subcategory of 𝒳 whose objects form a set”.

The objects of the cutdown form a set: they are indexed by the pairs of an object U of 𝒮 and an object of the small model of 𝒳_U.

instance small_fibreRepresentatives :
    ObjectProperty.Small.{max u₁ w} (p.fibreRepresentatives)

CategoryTheory.Functor.small_fiber_restrict_fibreRepresentatives, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/FibreRepresentatives.lean, line 118. The attribute's comment: “the cutdown: each of its fibres is a set”.

Each fibre of the cutdown is a set at the universe of condition (4): the fibre over U is covered by the small model of 𝒳_U.

instance small_fiber_restrict_fibreRepresentatives (U : 𝒮) :
    Small.{w} ((p.restrict p.fibreRepresentatives).Fiber U)

CategoryTheory.Functor.isEquivalence_ι_fibreRepresentatives, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/FibreRepresentatives.lean, line 140. The attribute's comment: “(b): the inclusion of the cutdown is fully faithful and essentially surjective”.

Stacks 03ZZ (b). The inclusion 𝒳_small ⥤ 𝒳 of the cutdown is fully faithful and essentially surjective.

theorem isEquivalence_ι_fibreRepresentatives : (p.fibreRepresentatives).ι.IsEquivalence

CategoryTheory.Functor.IsStack.fibreRepresentatives, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/FibreRepresentatives.lean, line 145. The attribute's comment: “(a): the restriction of p to the cutdown satisfies the conditions of 026F”.

Stacks 03ZZ (a). If p : 𝒳 ⥤ 𝒮 satisfies the three conditions of Stacks 026F over the site (𝒮, J), then so does its restriction to the cutdown; that is, the cutdown is a stack.

theorem IsStack.fibreRepresentatives (J : GrothendieckTopology 𝒮) (hp : p.IsStack J) :
    (p.restrict p.fibreRepresentatives).IsStack J

Sources

LeanCategoryTheory.Functor.IsStack · CategoryTheory.Functor.isStack_iff_isEquivalence_toDescentData · CategoryTheory.Functor.IsStack.fullSubcategory · CategoryTheory.BasedCategory.isStack_iff_of_equivalence · CategoryTheory.BasedStack · CategoryTheory.BasedStack.Hom · CategoryTheory.BasedStack.homCategory · CategoryTheory.BasedStack.bicategory

Section8.5 Stacks in groupoids #

Section 8.5 of the Stacks Project, Tag 02ZH. 6 tags here are carried by 9 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02ZI, a definition

Tag 02ZI in the Stacks Project.

CategoryTheory.Functor.IsStackInGroupoids, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/InheritedTopology/Stack.lean, line 236.

A functor p : 𝒮 ⥤ 𝒞 is a stack in groupoids over the site (𝒞, J) if 1. p is fibred in groupoids; 2. for all x y over U, the presheaf Isom(x, y) satisfies the sheaf condition for every covering family of J, with overlaps given by fibre products; and 3. every descent datum relative to a covering family of J is effective.

A covering family { f i : V i ⟶ U } is one whose generated sieve Sieve.ofArrows V f lies in J U.

structure IsStackInGroupoids (p : 𝒮 ⥤ 𝒞) (J : GrothendieckTopology 𝒞) : Prop

Tag 02ZJ, a lemma

Tag 02ZJ in the Stacks Project.

CategoryTheory.Functor.stackInGroupoids_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/GroupoidTFAE.lean, line 100.

Stacks 02ZJ. Let (𝒞, J) be a site and let p : 𝒮 ⥤ 𝒞 be a category over 𝒞. The following are equivalent: (1) p is a stack in groupoids over 𝒞, that is p is fibred in groupoids, the presheaves Isom(x, y) on 𝒞/U are sheaves, and every descent datum relative to a covering is effective (Stacks 02ZI); (2) p is a stack over 𝒞 and all its fibre categories are groupoids; (3) p is fibred in groupoids over 𝒞 and is a stack over 𝒞.

public theorem stackInGroupoids_tfae (p : 𝒮 ⥤ 𝒞) (J : GrothendieckTopology 𝒞) :
    List.TFAE
      [ ∃ h : p.IsFiberedInGroupoids,
          haveI : p.IsFibered := h.isFibered
          (∀ (U : 𝒞) (x y : p.Fiber U),
              Presheaf.IsSheaf (J.over U) (p.isomPresheaf x y)) ∧ p.HasEffectiveDescent J,
        p.IsStack J ∧ ∀ U : 𝒞, IsGroupoid (p.Fiber U),
        p.IsFiberedInGroupoids ∧ p.IsStack J ]

Tag 03YI, a lemma

Tag 03YI in the Stacks Project.

CategoryTheory.Functor.IsStack.isStackInGroupoids_stronglyCartesianOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/GroupoidOfStack.lean, line 421.

The category fibred in groupoids associated to a stack is a stack in groupoids. Let (𝒞, J) be a site and let p : 𝒮 ⥤ 𝒞 be a stack (Stacks 026F). Let p' : 𝒮' ⥤ 𝒞 be the category fibred in groupoids associated to 𝒮 constructed in Stacks 03WQ: the objects of 𝒮' are those of 𝒮, its morphisms are the strongly cartesian morphisms of 𝒮, and p' is the restriction of p. Then p' is a stack in groupoids (Stacks 02ZI): it is fibred in groupoids, its presheaves Isom(x, y) are sheaves, and every descent datum relative to a covering family of J is effective.

public theorem IsStack.isStackInGroupoids_stronglyCartesianOver
    {p : 𝒮 ⥤ 𝒞} {J : GrothendieckTopology 𝒞} (hp : p.IsStack J) :
    haveI : p.IsFibered := hp.isFibered
    haveI : (stronglyCartesianOver p).IsMultiplicative :=
      stronglyCartesianOver_isMultiplicative p
    IsStackInGroupoids.{w} (wideSubcategoryInclusion (stronglyCartesianOver p) ⋙ p) J

Tag 042X, a lemma

Tag 042X in the Stacks Project.

CategoryTheory.BasedCategory.isFiberedInGroupoids_and_isStack_iff_of_equivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/GroupoidTransport.lean, line 119.

Stacks 042X. Let (𝒞, J) be a site and let 𝒳, 𝒴 be categories over 𝒞. If 𝒳 and 𝒴 are equivalent as categories over 𝒞, then 𝒳 is a stack in groupoids over 𝒞 if and only if 𝒴 is.

"Stack in groupoids" is read as clause (3) of Stacks 02ZJ, fibred in groupoids together with being a stack, which is the reading 042X's proof uses; the two conjuncts transport by BasedCategory.isFiberedInGroupoids_iff_of_equivalence and by Stacks 042W, BasedCategory.isStack_iff_of_equivalence.

theorem BasedCategory.isFiberedInGroupoids_and_isStack_iff_of_equivalence
    (e : BasedCategory.Equivalence 𝒳 𝒴) (J : GrothendieckTopology 𝒞) :
    𝒳.p.IsFiberedInGroupoids ∧ 𝒳.p.IsStack J ↔
      𝒴.p.IsFiberedInGroupoids ∧ 𝒴.p.IsStack J

Tag 02ZK, a definition

Tag 02ZK in the Stacks Project.

CategoryTheory.StackInGroupoids, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/Groupoid.lean, line 137. The attribute's comment: “(1)”.

Stacks 02ZK (1). An object of the 2-category of stacks in groupoids over the site (𝒞, J): a category over 𝒞 whose structure functor is a stack in groupoids.

structure StackInGroupoids (𝒞 : Type u₁) [Category.{v₁} 𝒞] (J : GrothendieckTopology 𝒞)

CategoryTheory.StackInGroupoids.bicategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/Groupoid.lean, line 153.

Stacks 02ZK. The 2-category of stacks in groupoids over the site (𝒞, J): the sub-2-category of the 2-category of stacks over 𝒞 (Stacks 02ZG) whose objects are the stacks in groupoids. Since every morphism of a category fibred in groupoids is strongly cartesian, no condition is imposed on a 1-morphism beyond being a functor over 𝒞 — see CategoryTheory.StackInGroupoids.isFibredOneMorphism — so this is the full sub-2-category of the 2-category BasedCategory 𝒞 of categories over 𝒞 spanned by the stacks in groupoids.

instance StackInGroupoids.bicategory :
    Bicategory (StackInGroupoids.{w, v₁, v₂, u₁, u₂} 𝒞 J)

CategoryTheory.StackInGroupoids.homEquivBasedFunctor, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/Groupoid.lean, line 167. The attribute's comment: “(2)”.

Stacks 02ZK (2). The 1-morphisms of the 2-category of stacks in groupoids are the functors over 𝒞: a 1-morphism 𝒳 ⟶ 𝒴 is the same thing as a BasedFunctor, that is a functor G with p' ∘ G = p.

def homEquivBasedFunctor : (𝒳 ⟶ 𝒴) ≃ (𝒳.toBasedCategory ⥤ᵇ 𝒴.toBasedCategory)

CategoryTheory.StackInGroupoids.twoHomEquivBasedNatTrans, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/Groupoid.lean, line 178. The attribute's comment: “(3)”.

Stacks 02ZK (3). The 2-morphisms of the 2-category of stacks in groupoids are the morphisms of functors whose components lie over identities: a 2-morphism F ⟶ G is the same thing as a BasedNatTrans, that is a morphism of functors t with p'(t_x) = 𝟙 (p x) for every object x.

def twoHomEquivBasedNatTrans {𝒳 𝒴 : StackInGroupoids.{w, v₁, v₂, u₁, u₂} 𝒞 J} (F G : 𝒳 ⟶ 𝒴) :
    (F ⟶ G) ≃ BasedNatTrans F.hom G.hom

Tag 02ZL, a lemma

Tag 02ZL in the Stacks Project.

CategoryTheory.TwoFibreProductOver.isStack_isFiberedInGroupoids_structureFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/SetoidTwoFibreProduct.lean, line 125.

Stacks 02ZL. The 2-fibre product of stacks in groupoids over a site (𝒞, J) is a stack in groupoids: the construction of Stacks 0040 does not leave the 2-category of stacks in groupoids.

"Stack in groupoids" is spelled out as its two conditions, being a stack over (𝒞, J) and being fibred in groupoids, because the library's CategoryTheory.Functor.IsStackInGroupoids is a second, unrelated rendering of the notion (see the implementation notes of StacksFrontier.CategoryTheory.Sites.Stack.Setoid). The first condition is Stacks 026G and the second is Stacks 0041; the hypotheses on F and G are only that they are strictly over 𝒞, since a functor over 𝒞 into a category fibred in groupoids automatically preserves strongly cartesian morphisms.

theorem isStack_isFiberedInGroupoids_structureFunctor {J : GrothendieckTopology 𝒞}
    (h𝒳 : Functor.IsStack p𝒳 J) (h𝒴 : Functor.IsStack p𝒴 J) (h𝒮 : Functor.IsStack p𝒮 J)
    (g𝒳 : p𝒳.IsFiberedInGroupoids) (g𝒴 : p𝒴.IsFiberedInGroupoids)
    (g𝒮 : p𝒮.IsFiberedInGroupoids) (hF : F ⋙ p𝒮 = p𝒳) (hG : G ⋙ p𝒮 = p𝒴) :
    Functor.IsStack (structureFunctor p𝒳 p𝒴 p𝒮 F G) J ∧
      (structureFunctor p𝒳 p𝒴 p𝒮 F G).IsFiberedInGroupoids

Sources

LeanCategoryTheory.Functor.IsStackInGroupoids · CategoryTheory.Functor.stackInGroupoids_tfae · CategoryTheory.Functor.IsStack.isStackInGroupoids_stronglyCartesianOver · CategoryTheory.BasedCategory.isFiberedInGroupoids_and_isStack_iff_of_equivalence · CategoryTheory.StackInGroupoids · CategoryTheory.StackInGroupoids.bicategory · CategoryTheory.StackInGroupoids.homEquivBasedFunctor · CategoryTheory.StackInGroupoids.twoHomEquivBasedNatTrans

Section8.6 Stacks in setoids #

Section 8.6 of the Stacks Project, Tag 042Y. 11 tags here are carried by 14 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 042Z, a definition

Tag 042Z in the Stacks Project.

CategoryTheory.Functor.IsStackInSetoids, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/Setoid.lean, line 91. The attribute's comment: “(1)”.

Stacks 042Z. A stack in setoids over the site (𝒞, J): a stack over 𝒞 all of whose fibre categories are setoids, that is groupoids in which there is at most one morphism between any two objects.

structure Functor.IsStackInSetoids (p : 𝒮 ⥤ 𝒞) (J : GrothendieckTopology 𝒞) : Prop

CategoryTheory.Functor.IsStackInSets, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/Setoid.lean, line 104. The attribute's comment: “(2)”.

Stacks 042Z. A stack in sets, also called a stack in discrete categories, over the site (𝒞, J): a stack over 𝒞 all of whose fibre categories are discrete.

structure Functor.IsStackInSets (p : 𝒮 ⥤ 𝒞) (J : GrothendieckTopology 𝒞) : Prop

Tag 0430, a lemma

Tag 0430 in the Stacks Project.

CategoryTheory.Functor.isStackInSets_iff_isSheaf_objPresheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/FiberedInSets.lean, line 272.

Let (𝒞, J) be a site. Under the equivalence of Categories, Stacks 02Y2 between presheaves of sets on 𝒞 and categories fibred in sets over 𝒞, the stacks in sets correspond precisely to the sheaves: a category fibred in sets p : 𝒮 ⥤ 𝒞 is a stack in sets over (𝒞, J) if and only if its presheaf of objects U ↦ Ob(𝒮_U) is a sheaf.

theorem isStackInSets_iff_isSheaf_objPresheaf (J : GrothendieckTopology 𝒞) :
    p.IsStackInSets J ↔ Presheaf.IsSheaf J (objPresheaf p)

Tag 0432, a lemma

Tag 0432 in the Stacks Project.

CategoryTheory.BasedCategory.isStackInSetoids_iff_isStackInSets_of_equivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/SetoidToSets.lean, line 117.

Let (𝒞, J) be a site, let 𝒳 be a category fibred in setoids over 𝒞, and let 𝒴 be a category fibred in sets equivalent to 𝒳 as a category over 𝒞. Then 𝒳 is a stack in setoids if and only if 𝒴 is a stack in sets.

theorem BasedCategory.isStackInSetoids_iff_isStackInSets_of_equivalence
    {𝒞 : Type u₁} [Category.{v₁} 𝒞] {𝒳 𝒴 : BasedCategory.{v₂, u₂} 𝒞}
    (e : BasedCategory.Equivalence 𝒳 𝒴) [𝒳.p.IsFiberedInSetoids] [𝒴.p.IsFiberedInSets]
    (J : GrothendieckTopology 𝒞) :
    𝒳.p.IsStackInSetoids J ↔ 𝒴.p.IsStackInSets J

CategoryTheory.BasedCategory.isStackInSetoids_iff_isSheaf_objPresheaf_of_equivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/SetoidToSets.lean, line 131. The attribute's comment: “the "in other words" sentence: iff the presheaf U ↦ Ob(𝒮_U)/≅ is a sheaf”.

Let (𝒞, J) be a site, let 𝒳 be a category fibred in setoids over 𝒞, and let 𝒴 be a category fibred in sets equivalent to 𝒳 as a category over 𝒞. Then 𝒳 is a stack in setoids if and only if the presheaf of objects U ↦ Ob(𝒴_U) of 𝒴 is a sheaf. Its value at U is identified with the set Ob(𝒳_U)/≅ of isomorphism classes of the fibre of 𝒳 over U by CategoryTheory.BasedCategory.Equivalence.fiberQuotientEquiv.

theorem BasedCategory.isStackInSetoids_iff_isSheaf_objPresheaf_of_equivalence
    {𝒞 : Type u₁} [Category.{v₁} 𝒞] {𝒳 𝒴 : BasedCategory.{v₂, u₂} 𝒞}
    (e : BasedCategory.Equivalence 𝒳 𝒴) [𝒳.p.IsFiberedInSetoids] [𝒴.p.IsFiberedInSets]
    (J : GrothendieckTopology 𝒞) :
    𝒳.p.IsStackInSetoids J ↔ Presheaf.IsSheaf J (Functor.objPresheaf 𝒴.p)

Tag 0431, a lemma

Tag 0431 in the Stacks Project.

CategoryTheory.BasedCategory.isStackInSetoids_iff_of_equivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/Transport.lean, line 40.

Let (𝒞, J) be a site and let 𝒳, 𝒴 be categories over 𝒞. If 𝒳 and 𝒴 are equivalent as categories over 𝒞, then 𝒳 is a stack in setoids over 𝒞 if and only if 𝒴 is.

theorem BasedCategory.isStackInSetoids_iff_of_equivalence
    (e : BasedCategory.Equivalence 𝒳 𝒴) (J : GrothendieckTopology 𝒞) :
    𝒳.p.IsStackInSetoids J ↔ 𝒴.p.IsStackInSetoids J

Tag 0433, a definition

Tag 0433 in the Stacks Project.

CategoryTheory.StackInSetoids, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/Setoid.lean, line 134.

Stacks 0433. An object of the 2-category of stacks in setoids over the site (𝒞, J): a category over 𝒞 whose structure functor is a stack in setoids.

structure StackInSetoids (𝒞 : Type u₁) [Category.{v₁} 𝒞] (J : GrothendieckTopology 𝒞)

CategoryTheory.StackInSetoids.bicategory, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/Setoid.lean, line 148.

Stacks 0433. The 2-category of stacks in setoids over the site (𝒞, J): the full sub-2-category of the 2-category BasedCategory 𝒞 of categories over 𝒞 spanned by the stacks in setoids. A 1-morphism 𝒳 ⟶ 𝒴 is a functor G over 𝒞, that is with p' ∘ G = p, and a 2-morphism F ⟶ G is a morphism of functors t with p'(t_x) = 𝟙 (p x) for every object x.

instance StackInSetoids.bicategory : Bicategory (StackInSetoids.{v₁, v₂, u₁, u₂} 𝒞 J)

Tag 0434, a lemma

Tag 0434 in the Stacks Project.

CategoryTheory.TwoFibreProductOver.isStackInSetoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/SetoidTwoFibreProduct.lean, line 143.

Stacks 0434. The 2-fibre product of stacks in setoids over a site (𝒞, J) is a stack in setoids: the construction of Stacks 0040 does not leave the 2-category of stacks in setoids.

Its three conditions are Stacks 026G (isStack_structureFunctor), Stacks 0041 (fiber_isGroupoid) and thinness of the fibres (fiber_isThin). Nothing is asked of F and G beyond being strictly over 𝒞, since a functor over 𝒞 into a category fibred in groupoids automatically preserves strongly cartesian morphisms.

theorem isStackInSetoids {J : GrothendieckTopology 𝒞} (h𝒳 : p𝒳.IsStackInSetoids J)
    (h𝒴 : p𝒴.IsStackInSetoids J) (h𝒮 : p𝒮.IsStackInSetoids J)
    (hF : F ⋙ p𝒮 = p𝒳) (hG : G ⋙ p𝒮 = p𝒴) :
    (structureFunctor p𝒳 p𝒴 p𝒮 F G).IsStackInSetoids J

Tag 05UI, a lemma

Tag 05UI in the Stacks Project.

CategoryTheory.Functor.isStackInSetoids_twoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/InheritedTopology/TwoFibreProductSetoid.lean, line 98.

Let 𝒯 be a stack in groupoids and 𝒮 a stack over the site (𝒞, J), and let ℛ be a stack in setoids. Let f : 𝒯 ⥤ 𝒮 and g : ℛ ⥤ 𝒮 be 1-morphisms with f faithful. Then the 2-fibre product 𝒯 ×_{f, 𝒮, g} ℛ is a stack in setoids.

theorem Functor.isStackInSetoids_twoFibreProduct (J : GrothendieckTopology 𝒞)
    (h𝒯 : Functor.IsStack p𝒯 J) (g𝒯 : p𝒯.IsFiberedInGroupoids)
    (hℛ : pℛ.IsStackInSetoids J) (h𝒮 : Functor.IsStack p𝒮 J)
    (hF : p𝒯.IsFibredOneMorphism p𝒮 f) (hG : pℛ.IsFibredOneMorphism p𝒮 g) [f.Faithful] :
    (TwoFibreProductOver.structureFunctor p𝒯 pℛ p𝒮 f g).IsStackInSetoids J

Tag 05UJ, a lemma

Tag 05UJ in the Stacks Project.

CategoryTheory.Functor.isStackInSetoids_twoFibreProduct_of_isStackInSetoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/InheritedTopology/TwoFibreProductSetoid.lean, line 109.

Let 𝒮 be a stack over the site (𝒞, J) and let 𝒮₁, 𝒮₂ be stacks in setoids, with 1-morphisms f_i : 𝒮_i ⥤ 𝒮. Then 𝒮₁ ×_{f₁, 𝒮, f₂} 𝒮₂ is a stack in setoids.

theorem Functor.isStackInSetoids_twoFibreProduct_of_isStackInSetoids
    (J : GrothendieckTopology 𝒞)
    (h𝒯 : p𝒯.IsStackInSetoids J) (hℛ : pℛ.IsStackInSetoids J)
    (h𝒮 : Functor.IsStack p𝒮 J)
    (hF : p𝒯.IsFibredOneMorphism p𝒮 f) (hG : pℛ.IsFibredOneMorphism p𝒮 g) :
    (TwoFibreProductOver.structureFunctor p𝒯 pℛ p𝒮 f g).IsStackInSetoids J

Tag 06DV, a lemma

Tag 06DV in the Stacks Project.

CategoryTheory.Functor.faithful_of_faithful_fst, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/FaithfulDescent.lean, line 253.

Stacks 06DV. In a 2-cartesian diagram of categories fibred in groupoids over a site with 𝒯₁ a stack, if every object of a fibre of 𝒮₁ is locally in the essential image of F : 𝒮₂ ⥤ 𝒮₁ and the first projection 𝒮₂ ×_{𝒮₁} 𝒯₁ ⥤ 𝒮₂ is faithful, then G : 𝒯₁ ⥤ 𝒮₁ is faithful.

By Stacks 003Z faithfulness may be checked on the fibres; there the fibres of 𝒯₁ are groupoids, so two morphisms α, β : y ⟶ y' with G α = G β differ by the endomorphism β ∘ α⁻¹ of y, which G sends to the identity and which is therefore the identity by CategoryTheory.Functor.eq_id_of_map_eq_id_of_locallyEssSurj.

theorem faithful_of_faithful_fst (hFeq : F ⋙ p𝒮₁ = p𝒮₂) (hGeq : G ⋙ p𝒮₁ = p𝒯₁)
    (hgpd₁ : p𝒮₁.IsFiberedInGroupoids) (hgpdT : p𝒯₁.IsFiberedInGroupoids)
    {J : GrothendieckTopology 𝒞} (hstack : p𝒯₁.IsStack J)
    (hloc : LocallyEssSurjOnFibers hgpd₁.isFibered hFeq J)
    (hfst : (TwoFibreProductOver.fst p𝒮₂ p𝒯₁ p𝒮₁ F G).Faithful) :
    G.Faithful

Tag 05W9, a lemma

Tag 05W9 in the Stacks Project.

CategoryTheory.Functor.isStackInSetoids_of_isStackInSetoids_twoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/SetoidDescent.lean, line 124.

Stacks 05W9. In a 2-cartesian diagram of stacks in groupoids over a site, if F is fully faithful, every object of a fibre of 𝒮₁ is locally in the essential image of F, and the 2-fibre product 𝒮₂ ×_{𝒮₁} 𝒯₁ is a stack in setoids, then 𝒯₁ is a stack in setoids.

Being a stack and having groupoid fibres are hypotheses — they are what makes 𝒯₁ a stack in groupoids — so the content is thinness of the fibres of 𝒯₁, and that is CategoryTheory.Functor.eq_id_of_fibre_isThin_of_locallyEssSurj applied to β ∘ α⁻¹, the fibres of 𝒯₁ being groupoids.

theorem isStackInSetoids_of_isStackInSetoids_twoFibreProduct (hFeq : F ⋙ p𝒮₁ = p𝒮₂)
    (hGeq : G ⋙ p𝒮₁ = p𝒯₁) (hgpd₁ : p𝒮₁.IsFiberedInGroupoids)
    (hgpd₂ : p𝒮₂.IsFiberedInGroupoids) (hgpdT : p𝒯₁.IsFiberedInGroupoids)
    [F.Full] [F.Faithful] {J : GrothendieckTopology 𝒞} (hstack : p𝒯₁.IsStack J)
    (hloc : LocallyEssSurjOnFibers hgpd₁.isFibered hFeq J)
    (hT₂ : (TwoFibreProductOver.structureFunctor p𝒮₂ p𝒯₁ p𝒮₁ F G).IsStackInSetoids J) :
    p𝒯₁.IsStackInSetoids J

Tag 0CKJ, a lemma

Tag 0CKJ in the Stacks Project.

CategoryTheory.Functor.isStack_of_faithful_of_isSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/FaithfulGroupoidDescent.lean, line 320.

Descent along a faithful 1-morphism into a stack in groupoids. Let (𝒞, J) be a site and let F : 𝒮 ⥤ 𝒯 be a 1-morphism of categories fibred in groupoids over 𝒞, that is a functor with F ⋙ q = p. Assume that (1) 𝒯 is a stack in groupoids over 𝒞, (2) for every object U of 𝒞 the functor 𝒮_U ⥤ 𝒯_U of fibre categories is faithful, and (3) for every object y of 𝒯 over U the presheaf on 𝒞/U sending h : V ⟶ U to the isomorphism classes of pairs (x, f) with x an object of 𝒮_V and f : F(x) ⟶ h^* y a morphism of 𝒯_V is a sheaf. Then 𝒮 is a stack in groupoids over 𝒞.

Condition (3) is the two hypotheses hsep and hglue, in which a pair over h is a morphism f : F.obj x ⟶ y lying over h, and the class of (x₂, f₂) is the restriction of the class of (x₁, f₁) along g : W ⟶ V when F.map c ≫ f₁ = f₂ for some lift c : x₂ ⟶ x₁ of g.

public theorem isStack_of_faithful_of_isSheaf {p : 𝒮 ⥤ 𝒞} {q : 𝒯 ⥤ 𝒞} {F : 𝒮 ⥤ 𝒯}
    {J : GrothendieckTopology 𝒞} (hp : p.IsFiberedInGroupoids) (hq : q.IsFiberedInGroupoids)
    (hF : F ⋙ q = p) (hT : q.IsStack J)
    (hfaithful : ∀ U : 𝒞, (Fiber.fiberInclusion (p := p) (S := U) ⋙ F).Faithful)
    (hsep : ∀ (y : 𝒯) ⦃V : 𝒞⦄ (h : V ⟶ q.obj y) (R : Sieve V), R ∈ J V →
      ∀ ⦃x x' : 𝒮⦄ (f : F.obj x ⟶ y) (f' : F.obj x' ⟶ y),
        q.IsHomLift h f → q.IsHomLift h f' →
        (∀ ⦃W : 𝒞⦄ (g : W ⟶ V), R g → ∃ (z : 𝒮) (c : z ⟶ x) (c' : z ⟶ x'),
          p.IsHomLift g c ∧ p.IsHomLift g c' ∧ F.map c ≫ f = F.map c' ≫ f') →
        ∃ e : x ⟶ x', p.IsHomLift (𝟙 V) e ∧ F.map e ≫ f' = f)
    (hglue : ∀ (y : 𝒯) ⦃V : 𝒞⦄ (h : V ⟶ q.obj y) (R : Sieve V), R ∈ J V →
      ∀ (x : ∀ ⦃W : 𝒞⦄ (g : W ⟶ V), R g → 𝒮)
        (f : ∀ ⦃W : 𝒞⦄ (g : W ⟶ V) (hg : R g), F.obj (x g hg) ⟶ y),
        (∀ ⦃W : 𝒞⦄ (g : W ⟶ V) (hg : R g), q.IsHomLift (g ≫ h) (f g hg)) →
        (∀ ⦃W W' : 𝒞⦄ (g : W ⟶ V) (hg : R g) (k : W' ⟶ W),
          ∃ c : x (k ≫ g) (R.downward_closed hg k) ⟶ x g hg,
            p.IsHomLift k c ∧ F.map c ≫ f g hg = f (k ≫ g) (R.downward_closed hg k)) →
        ∃ (x₀ : 𝒮) (f₀ : F.obj x₀ ⟶ y), q.IsHomLift h f₀ ∧
          ∀ ⦃W : 𝒞⦄ (g : W ⟶ V) (hg : R g), ∃ c : x g hg ⟶ x₀,
            p.IsHomLift g c ∧ F.map c ≫ f₀ = f g hg) :
    p.IsStack J

Sources

LeanCategoryTheory.Functor.IsStackInSetoids · CategoryTheory.Functor.IsStackInSets · CategoryTheory.Functor.isStackInSets_iff_isSheaf_objPresheaf · CategoryTheory.BasedCategory.isStackInSetoids_iff_isStackInSets_of_equivalence · CategoryTheory.BasedCategory.isStackInSetoids_iff_isSheaf_objPresheaf_of_equivalence · CategoryTheory.BasedCategory.isStackInSetoids_iff_of_equivalence · CategoryTheory.StackInSetoids · CategoryTheory.StackInSetoids.bicategory

Section8.7 The inertia stack #

Section 8.7 of the Stacks Project, Tag 036X. 2 tags here are carried by 5 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 036Y, a lemma

Tag 036Y in the Stacks Project.

CategoryTheory.RelativeInertia.isStack, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/Inertia.lean, line 140. The attribute's comment: “(1)”.

The relative inertia I_{𝒮/𝒮'} of a 1-morphism F of stacks over the site (𝒞, J), with its structure functor π ⋙ p, is a stack over 𝒞; taking F = p and p' = 𝟭 𝒞, so is the absolute inertia I_𝒮.

Only the fibredness half of the conclusion is proved, from Stacks 034H (2); the descent of morphisms and the effectivity of descent for the inertia are the hypotheses hmor and heff.

theorem isStack (hp : p.IsStack J) (_hp' : p'.IsStack J) (hF : p.IsFibredOneMorphism p' F)
    (hmor : haveI : (RelativeInertia.π F ⋙ p).IsFibered :=
        RelativeInertia.isFibered F p p' hp.isFibered hF
      ∀ (U : 𝒞) (x y : (RelativeInertia.π F ⋙ p).Fiber U),
        Functor.IsMorSheaf (RelativeInertia.π F ⋙ p) J U x y)
    (heff : haveI : (RelativeInertia.π F ⋙ p).IsFibered :=
        RelativeInertia.isFibered F p p' hp.isFibered hF
      Functor.HasEffectiveDescent (RelativeInertia.π F ⋙ p) J) :
    Functor.IsStack (RelativeInertia.π F ⋙ p) J

CategoryTheory.RelativeInertia.isStack_and_fiber_isGroupoid, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/Inertia.lean, line 160. The attribute's comment: “(2)”.

If 𝒮 and 𝒮' are stacks in groupoids over the site (𝒞, J), then so is the relative inertia I_{𝒮/𝒮'}; taking F = p and p' = 𝟭 𝒞, so is the absolute inertia I_𝒮.

Being a stack in groupoids is written out as being a stack with groupoid fibres; the stack condition on the inertia is the hypothesis hst, which is part (1), and what is proved here is the remaining content, that the fibres of the inertia are groupoids.

theorem isStack_and_fiber_isGroupoid (_hp : p.IsStack J) (hgp : ∀ U, IsGroupoid (p.Fiber U))
    (_hp' : p'.IsStack J) (_hgp' : ∀ U, IsGroupoid (p'.Fiber U))
    (hst : Functor.IsStack (RelativeInertia.π F ⋙ p) J) :
    Functor.IsStack (RelativeInertia.π F ⋙ p) J ∧
      ∀ U, IsGroupoid ((RelativeInertia.π F ⋙ p).Fiber U)

CategoryTheory.RelativeInertia.isStackInSetoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/Inertia.lean, line 173. The attribute's comment: “(3)”.

If 𝒮 and 𝒮' are stacks in setoids over the site (𝒞, J), then so is the relative inertia I_{𝒮/𝒮'}; taking F = p and p' = 𝟭 𝒞, so is the absolute inertia I_𝒮.

The stack condition on the inertia is the hypothesis hst, which is part (1); what is proved here is the remaining content, that the fibres of the inertia are setoids.

theorem isStackInSetoids (hp : p.IsStackInSetoids J) (_hp' : p'.IsStackInSetoids J)
    (hst : Functor.IsStack (RelativeInertia.π F ⋙ p) J) :
    (RelativeInertia.π F ⋙ p).IsStackInSetoids J

Tag 04ZM, a lemma

Tag 04ZM in the Stacks Project.

CategoryTheory.RelativeInertia.π_isEquivalence_iff, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/Inertia.lean, line 189.

Let (𝒞, J) be a site and let 𝒮 be a stack in groupoids over 𝒞, written out as a stack with groupoid fibres. The forgetful 1-morphism π : I_𝒮 ⥤ 𝒮 of the absolute inertia is an equivalence if and only if 𝒮 is a stack in setoids.

theorem π_isEquivalence_iff (hp : p.IsStack J) (hg : ∀ U, IsGroupoid (p.Fiber U)) :
    (RelativeInertia.π p).IsEquivalence ↔ p.IsStackInSetoids J

CategoryTheory.RelativeInertia.π_comp_neutralSection_eq_id, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/Inertia.lean, line 204.

For a stack in setoids the neutral section x ↦ (x, 𝟙) is a strict two-sided inverse of π, so π is an isomorphism of categories over 𝒞 and in particular an equivalence in the 2-category of stacks over 𝒞, not merely an equivalence of categories.

theorem π_comp_neutralSection_eq_id (h : p.IsStackInSetoids J) :
    RelativeInertia.π p ⋙ RelativeInertia.neutralSection p = 𝟭 (AbsoluteInertia p)

Sources

LeanCategoryTheory.RelativeInertia.isStack · CategoryTheory.RelativeInertia.isStack_and_fiber_isGroupoid · CategoryTheory.RelativeInertia.isStackInSetoids · CategoryTheory.RelativeInertia.π_isEquivalence_iff · CategoryTheory.RelativeInertia.π_comp_neutralSection_eq_id

Section8.8 Stackification of fibred categories #

Section 8.8 of the Stacks Project, Tag 02ZM. 5 tags here are carried by 9 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02ZN, a lemma

Tag 02ZN in the Stacks Project.

CategoryTheory.Functor.exists_isStackification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stackification/Stackification.lean, line 80.

Let (𝒞, J) be a site and let q : 𝒴 ⥤ 𝒞 be a fibred category. There exist a stack q' : 𝒴' ⥤ 𝒞 over (𝒞, J) and a 1-morphism G : 𝒴 ⥤ 𝒴' of fibred categories over 𝒞 such that

for every U and all x, y in the fibre 𝒴_U the map Mor(x, y) ⟶ Mor(G x, G y) of presheaves on 𝒞/U exhibits its target as the sheafification of its source, and

every object of a fibre of 𝒴' is, along a covering sieve of the base, in the essential image of the functor induced by G on fibres.

The objects and morphisms of 𝒴' live in Type (max t₁ t₂ w vb), the morphism universe of 𝒴.

theorem exists_isStackification :
    ∃ (𝒴' : Type (max t₁ t₂ w vb)) (inst : Category.{max t₁ t₂ w vb} 𝒴'),
      letI := inst
      ∃ (q' : 𝒴' ⥤ 𝒞) (instq : q'.IsFibered),
        letI := instq
        ∃ (G : 𝒴 ⥤ 𝒴') (hG : q.IsFibredOneMorphism q' G),
          q'.IsStack J ∧
            (∀ (U : 𝒞) (x y : q.Fiber U),
                Presheaf.IsLocallyInjective (J.over U) (hG.morPresheafMap x y) ∧
                  Presheaf.IsLocallySurjective (J.over U) (hG.morPresheafMap x y)) ∧
              ∀ (U : 𝒞) (x' : q'.Fiber U), ∃ R ∈ J U, ∀ ⦃V : 𝒞⦄ ⦃f : V ⟶ U⦄, R.arrows f →
                (fiberFunctorOfCompEq hG.comp_eq V).essImage (pullbackFiber q' x' f)

Tag 0435, a lemma

Tag 0435 in the Stacks Project.

CategoryTheory.Functor.Stackification.extend, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stackification/UniversalPropertyFunctor.lean, line 989.

The functor underlying the extension of F along G, Stacks 0435. Its value on an object X of 𝒮' is the object of 𝒳 to which the images under F of a chosen local presentation of X descend, and its value on a morphism is the morphism glued from the transfers along G of the transition morphisms of the chosen presentations.

noncomputable def extend : 𝒮' ⥤ 𝒳

CategoryTheory.Functor.Stackification.extend_isFibredOneMorphism, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stackification/UniversalPropertyFunctor.lean, line 1006.

The extension is a 1-morphism of fibred categories over 𝒞: it is strictly over 𝒞 and preserves strongly cartesian morphisms.

theorem extend_isFibredOneMorphism :
    p'.IsFibredOneMorphism q (extend hG hF hmor hqmor hobj hdesc)

CategoryTheory.Functor.Stackification.unit, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stackification/UniversalPropertyFunctor.lean, line 1225.

The 2-isomorphism G ⋙ H ≅ F of Stacks 0435. Its component at A compares the object of 𝒳 that the chosen presentation of G A descends to with F A, and it is an isomorphism because both are descents of presentations of one and the same object of 𝒮'.

noncomputable def unit : G ⋙ extend hG hF hmor hqmor hobj hdesc ≅ F

CategoryTheory.Functor.Stackification.isHomLift_unit_app, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stackification/UniversalPropertyFunctor.lean, line 1239.

Every component of the 2-isomorphism lies over an identity, so it is a 2-morphism of fibred categories over 𝒞.

lemma isHomLift_unit_app (A : 𝒮) :
    q.IsHomLift (𝟙 (p.obj A)) ((unit hG hF hmor hqmor hobj hdesc).hom.app A)

Tag 04W9, a lemma

Tag 04W9 in the Stacks Project.

CategoryTheory.Functor.Stackification.restrict_isEquivalence, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stackification/UniversalPropertyUniqueness.lean, line 850.

Stacks 04W9. Restriction along a stackification G : 𝒮 ⥤ 𝒮' is an equivalence from the category of 1-morphisms 𝒮' ⥤ 𝒳 of fibred categories over 𝒞 into a stack, and their 2-morphisms, onto the category of 1-morphisms 𝒮 ⥤ 𝒳 and their 2-morphisms.

theorem restrict_isEquivalence : (restrictMor (q := q) hG).IsEquivalence

CategoryTheory.Functor.Stackification.restrictEquivalence, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stackification/UniversalPropertyUniqueness.lean, line 860.

The canonical equivalence of morphism categories of Stacks 04W9, Mor_{Stacks/𝒞}(𝒮', 𝒳) ≌ Mor_{Fib/𝒞}(𝒮, 𝒳). Its functor is restriction along the stackification G, and a quasi-inverse is the extension of Stacks 0435.

noncomputable def restrictEquivalence : FibredMor p' q ≌ FibredMor p q

Tag 04Y1, a lemma

Tag 04Y1 in the Stacks Project.

CategoryTheory.TwoFibreProductOver.isStackification_stackifyMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stackification/TwoFibreProduct.lean, line 1332.

Stacks 04Y1. Let (𝒞, J) be a site, let f : 𝒳 ⥤ 𝒴 and g : 𝒵 ⥤ 𝒴 be 1-morphisms of fibred categories over 𝒞, and let i : 𝒳 ⥤ 𝒳', j : 𝒴 ⥤ 𝒴', k : 𝒵 ⥤ 𝒵' be stackifications (Stacks 02ZP: the targets are stacks over (𝒞, J), the induced maps Mor(x, y) ⟶ Mor(i x, i y) of presheaves on 𝒞/U are locally bijective, and every object of the target is locally in the essential image), and let f' : 𝒳' ⥤ 𝒴', g' : 𝒵' ⥤ 𝒴' be 1-morphisms of fibred categories over 𝒞 2-commuting with f and g along i, j, k via vertical 2-isomorphisms α, β. Then the stackification of the 2-fibre product is the 2-fibre product of the stackifications: the 2-fibre product 𝒳' ×_{𝒴'} 𝒵' is a stack over (𝒞, J) — it is a fibred category by Stacks 02XQ — and the canonical 1-morphism 𝒳 ×_𝒴 𝒵 ⥤ 𝒳' ×_{𝒴'} 𝒵', CategoryTheory.TwoFibreProductOver.stackifyMap, is a 1-morphism of fibred categories over 𝒞 which is a stackification of 𝒳 ×_𝒴 𝒵, in the same two clauses.

theorem isStackification_stackifyMap {J : GrothendieckTopology 𝒞}
    (h𝒳 : p𝒳.IsFibered) (h𝒴 : p𝒴.IsFibered) (h𝒵 : p𝒵.IsFibered)
    (hs𝒳' : p𝒳'.IsStack J) (hs𝒴' : p𝒴'.IsStack J) (hs𝒵' : p𝒵'.IsStack J)
    (hf : p𝒳.IsFibredOneMorphism p𝒴 f) (hg : p𝒵.IsFibredOneMorphism p𝒴 g)
    (hf' : p𝒳'.IsFibredOneMorphism p𝒴' f') (hg' : p𝒵'.IsFibredOneMorphism p𝒴' g')
    (hi : p𝒳.IsFibredOneMorphism p𝒳' i) (hj : p𝒴.IsFibredOneMorphism p𝒴' j)
    (hk : p𝒵.IsFibredOneMorphism p𝒵' k)
    (hmor𝒳 : haveI : p𝒳.IsFibered := h𝒳
      haveI : p𝒳'.IsFibered := hs𝒳'.isFibered
      ∀ (V : 𝒞) (x₁ x₂ : p𝒳.Fiber V),
        Presheaf.IsLocallyInjective (J.over V) (hi.morPresheafMap x₁ x₂) ∧
          Presheaf.IsLocallySurjective (J.over V) (hi.morPresheafMap x₁ x₂))
    (hobj𝒳 : ∀ x' : 𝒳', ∃ R ∈ J (p𝒳'.obj x'), ∀ ⦃V : 𝒞⦄ (u : V ⟶ p𝒳'.obj x'), R.arrows u →
      ∃ (x : 𝒳) (φ : i.obj x ⟶ x'), p𝒳'.IsStronglyCartesian u φ)
    (hmor𝒴 : haveI : p𝒴.IsFibered := h𝒴
      haveI : p𝒴'.IsFibered := hs𝒴'.isFibered
      ∀ (V : 𝒞) (y₁ y₂ : p𝒴.Fiber V),
        Presheaf.IsLocallyInjective (J.over V) (hj.morPresheafMap y₁ y₂) ∧
          Presheaf.IsLocallySurjective (J.over V) (hj.morPresheafMap y₁ y₂))
    (_hobj𝒴 : ∀ y' : 𝒴', ∃ R ∈ J (p𝒴'.obj y'), ∀ ⦃V : 𝒞⦄ (u : V ⟶ p𝒴'.obj y'), R.arrows u →
      ∃ (y : 𝒴) (φ : j.obj y ⟶ y'), p𝒴'.IsStronglyCartesian u φ)
    (hmor𝒵 : haveI : p𝒵.IsFibered := h𝒵
      haveI : p𝒵'.IsFibered := hs𝒵'.isFibered
      ∀ (V : 𝒞) (z₁ z₂ : p𝒵.Fiber V),
        Presheaf.IsLocallyInjective (J.over V) (hk.morPresheafMap z₁ z₂) ∧
          Presheaf.IsLocallySurjective (J.over V) (hk.morPresheafMap z₁ z₂))
    (hobj𝒵 : ∀ z' : 𝒵', ∃ R ∈ J (p𝒵'.obj z'), ∀ ⦃V : 𝒞⦄ (u : V ⟶ p𝒵'.obj z'), R.arrows u →
      ∃ (z : 𝒵) (φ : k.obj z ⟶ z'), p𝒵'.IsStronglyCartesian u φ)
    (α : i ⋙ f' ≅ f ⋙ j) (hα : ∀ x : 𝒳, p𝒴'.IsHomLift (𝟙 (p𝒳.obj x)) (α.hom.app x))
    (β : k ⋙ g' ≅ g ⋙ j) (hβ : ∀ z : 𝒵, p𝒴'.IsHomLift (𝟙 (p𝒵.obj z)) (β.hom.app z)) :
    haveI : p𝒳.IsFibered := h𝒳
    haveI : p𝒴.IsFibered := h𝒴
    haveI : p𝒵.IsFibered := h𝒵
    haveI : p𝒳'.IsFibered := hs𝒳'.isFibered
    haveI : p𝒴'.IsFibered := hs𝒴'.isFibered
    haveI : p𝒵'.IsFibered := hs𝒵'.isFibered
    haveI : (structureFunctor p𝒳 p𝒵 p𝒴 f g).IsFibered :=
      isFibered_structureFunctor p𝒳 p𝒵 p𝒴 f g hf hg
    haveI : (structureFunctor p𝒳' p𝒵' p𝒴' f' g').IsFibered :=
      isFibered_structureFunctor p𝒳' p𝒵' p𝒴' f' g' hf' hg'
    (structureFunctor p𝒳' p𝒵' p𝒴' f' g').IsStack J ∧
      ∃ hH : Functor.IsFibredOneMorphism (structureFunctor p𝒳 p𝒵 p𝒴 f g)
          (structureFunctor p𝒳' p𝒵' p𝒴' f' g') (stackifyMap hi hj hk α hα β hβ),
        (∀ (U : 𝒞) (P Q : (structureFunctor p𝒳 p𝒵 p𝒴 f g).Fiber U),
            Presheaf.IsLocallyInjective (J.over U) (hH.morPresheafMap P Q) ∧
              Presheaf.IsLocallySurjective (J.over U) (hH.morPresheafMap P Q)) ∧
          ∀ P' : TwoFibreProductOver p𝒳' p𝒵' p𝒴' f' g', ∃ R ∈ J P'.base,
            ∀ ⦃V : 𝒞⦄ (u : V ⟶ P'.base), R.arrows u →
              ∃ (P : TwoFibreProductOver p𝒳 p𝒵 p𝒴 f g)
                (Φ : (stackifyMap hi hj hk α hα β hβ).obj P ⟶ P'),
                (structureFunctor p𝒳' p𝒵' p𝒴' f' g').IsStronglyCartesian u Φ

Tag 06NS, a lemma

Tag 06NS in the Stacks Project.

CategoryTheory.RelativeInertia.isStackification_functoriality, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/FiberedCategory/InertiaStackification.lean, line 1333.

The stackification of the inertia is the inertia of the stackification. Let (𝒞, J) be a site, let p : 𝒳 ⥤ 𝒞 be a fibred category over 𝒞 and let G : 𝒳 ⥤ 𝒳' be the stackification of 𝒳 (Stacks 02ZN): a 1-morphism hG of fibred categories over 𝒞 whose target p' is a stack, such that (hmor) for every U and all x, y in 𝒳_U the induced map Mor(x, y) ⟶ Mor(G x, G y) of presheaves on 𝒞/U is locally injective and locally surjective, its target being a sheaf, and such that (hobj) every object x' of 𝒳' admits a covering sieve R of p'.obj x' with x'|_V in the essential image of 𝒳_V ⥤ 𝒳'_V for every f : V ⟶ p'.obj x' in R.

Then the inertia I_{𝒳'} is a stack over 𝒞, and the functoriality 1-morphism I_G : I_𝒳 ⥤ I_{𝒳'}, (x, α) ↦ (G x, G α), is a stackification of the inertia I_𝒳: it is a 1-morphism of fibred categories over 𝒞 and it satisfies the same two conditions.

public theorem RelativeInertia.isStackification_functoriality
    {p : 𝒳 ⥤ 𝒞} {p' : 𝒳' ⥤ 𝒞} {G : 𝒳 ⥤ 𝒳'} {J : GrothendieckTopology 𝒞} [p.IsFibered]
    (hG : p.IsFibredOneMorphism p' G) (hp' : p'.IsStack J)
    (hmor : haveI : p'.IsFibered := hp'.isFibered
      ∀ (U : 𝒞) (x y : p.Fiber U),
        Presheaf.IsLocallyInjective (J.over U)
            (Functor.IsFibredOneMorphism.morPresheafMap hG x y) ∧
          Presheaf.IsLocallySurjective (J.over U)
            (Functor.IsFibredOneMorphism.morPresheafMap hG x y))
    (hobj : ∀ x' : 𝒳', ∃ R ∈ J (p'.obj x'), ∀ ⦃V : 𝒞⦄ (f : V ⟶ p'.obj x'), R f →
      ∃ (y : 𝒳) (φ : G.obj y ⟶ x'), p'.IsStronglyCartesian f φ) :
    haveI : p'.IsFibered := hp'.isFibered
    haveI : (RelativeInertia.toBase p).IsFibered :=
      RelativeInertia.isFibered p p (𝟭 𝒞) inferInstance (Functor.isFibredOneMorphism_id p)
    haveI : (RelativeInertia.toBase p').IsFibered :=
      RelativeInertia.isFibered p' p' (𝟭 𝒞) hp'.isFibered (Functor.isFibredOneMorphism_id p')
    (RelativeInertia.toBase p').IsStack J ∧
      ∃ hIG : (RelativeInertia.toBase p).IsFibredOneMorphism (RelativeInertia.toBase p')
          (RelativeInertia.functoriality p p' G hG.comp_eq),
        (∀ (U : 𝒞) (A B : (RelativeInertia.toBase p).Fiber U),
            Presheaf.IsLocallyInjective (J.over U)
                (Functor.IsFibredOneMorphism.morPresheafMap hIG A B) ∧
              Presheaf.IsLocallySurjective (J.over U)
                (Functor.IsFibredOneMorphism.morPresheafMap hIG A B)) ∧
          ∀ A' : RelativeInertia p', ∃ R ∈ J ((RelativeInertia.toBase p').obj A'),
            ∀ ⦃V : 𝒞⦄ (f : V ⟶ (RelativeInertia.toBase p').obj A'), R f →
              ∃ (A : RelativeInertia p)
                (φ : (RelativeInertia.functoriality p p' G hG.comp_eq).obj A ⟶ A'),
                (RelativeInertia.toBase p').IsStronglyCartesian f φ

Sources

LeanCategoryTheory.Functor.exists_isStackification · CategoryTheory.Functor.Stackification.extend · CategoryTheory.Functor.Stackification.extend_isFibredOneMorphism · CategoryTheory.Functor.Stackification.unit · CategoryTheory.Functor.Stackification.isHomLift_unit_app · CategoryTheory.Functor.Stackification.restrict_isEquivalence · CategoryTheory.Functor.Stackification.restrictEquivalence · CategoryTheory.TwoFibreProductOver.isStackification_stackifyMap

Section8.9 Stackification of categories fibred in groupoids #

Section 8.9 of the Stacks Project, Tag 02ZO. 3 tags here are carried by 9 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 02ZP, a lemma

Tag 02ZP in the Stacks Project.

CategoryTheory.Functor.Stackification.isFiberedInGroupoids_of_isStackification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stackification/GroupoidStackification.lean, line 255.

Stacks 02ZP. Let (𝒞, J) be a site, let p : 𝒮 ⥤ 𝒞 be a category fibred in groupoids and let G : 𝒮 ⥤ 𝒮' exhibit the stack p' : 𝒮' ⥤ 𝒞 as the stackification of the fibred category underlying 𝒮 — that is, let G be a 1-morphism of fibred categories over 𝒞 satisfying the two clauses of Stacks 02ZN. Then p' is fibred in groupoids.

This is the whole content of Stacks 02ZP over Stacks 02ZN: the source runs the same construction and observes that it lands in groupoid fibres. The statement is conditional on being given the stackification, the construction of Stacks 02ZN not being assembled in the tree yet; once it is, it supplies hsp', hG, hmor and hobj.

By Stacks 003V it suffices that every fibre of 𝒮' be a groupoid, which is CategoryTheory.Functor.Stackification.isGroupoid_fiber.

theorem isFiberedInGroupoids_of_isStackification : p'.IsFiberedInGroupoids

CategoryTheory.Functor.Stackification.isStackInGroupoids_of_isStackification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stackification/GroupoidStackification.lean, line 267.

Stacks 02ZP, as the source states it: 𝒮' is a stack in groupoids. The IsStack half is the hypothesis hsp' and the IsFiberedInGroupoids half is CategoryTheory.Functor.Stackification.isFiberedInGroupoids_of_isStackification; together with hmor and hobj, which are the two clauses of the source's statement carried unchanged from hypothesis to conclusion, this says that the given G exhibits 𝒮' as the stackification of 𝒮 in groupoids.

theorem isStackInGroupoids_of_isStackification :
    p'.IsFiberedInGroupoids ∧ p'.IsStack J

CategoryTheory.Functor.Stackification.nonempty_isEquivalenceOver_of_locally_fullyFaithful, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stackification/Uniqueness.lean, line 161. The attribute's comment: “the determinacy half of the statement — 𝒮' is determined up to 2-isomorphism by clauses (1) and (2) — read as: a 1-morphism from a stackification into a stack whose composite with the stackification again satisfies the two clauses is an equivalence over the site. The existence half is the construction of Stacks 02ZN, not assembled in the tree; the uniqueness of the 2-isomorphism is Stacks 04W9, CategoryTheory.Functor.Stackification.restrict_isEquivalence; and the groupoid half of 02ZP is CategoryTheory.Functor.Stackification.isStackInGroupoids_of_isStackification”.

The determinacy clause of Stacks 02ZN and 02ZP, in the form a consumer uses. Let G : 𝒜 ⥤ ℬ exhibit the stack p' as the stackification of the fibred category p — that is, let it satisfy the two clauses hGmor and hGobj — and let H : ℬ ⥤ 𝒳 be a 1-morphism of fibred categories into a stack q. If the composite G ⋙ H satisfies the same two clauses, then H is an equivalence of p' with q over 𝒞.

So two stackifications of one fibred category have equivalent targets, and the comparison realising the equivalence is any 1-morphism between them compatible with the two presentations. The two clauses, which for a given stackification are hypotheses carried to the conclusion by CategoryTheory.Functor.Stackification.isStackInGroupoids_of_isStackification, thereby become a criterion on G ⋙ H.

H is fully faithful by CategoryTheory.Functor.Stackification.full_of_extension and .faithful_of_extension, Stacks 04WQ for a 1-morphism out of a stackification, whose hypotheses are precisely the clauses on G and on the composite. It is locally essentially surjective on fibres because G ⋙ H is, a local preimage under the composite being one under H. Stacks 046N, CategoryTheory.Functor.isEquivalenceOver_iff_locallyEssSurjOnFibers, then concludes.

theorem nonempty_isEquivalenceOver_of_locally_fullyFaithful :
    Nonempty (IsEquivalenceOver p' q H)

CategoryTheory.Functor.Stackification.nonempty_isEquivalenceOver_extend, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stackification/Uniqueness.lean, line 264. The attribute's comment: “the determinacy half of the statement — 𝒮' is determined up to 2-isomorphism by clauses (1) and (2) — for the canonical extension: a 1-morphism into a stack satisfying the two clauses exhibits that stack as the stackification, so the extension of Stacks 0435 is an equivalence over the site. The existence half is the construction of Stacks 02ZN, not assembled in the tree; the uniqueness of the 2-isomorphism is Stacks 04W9, CategoryTheory.Functor.Stackification.restrict_isEquivalence; and the groupoid half of 02ZP is CategoryTheory.Functor.Stackification.isStackInGroupoids_of_isStackification”.

A stackification is determined up to 2-isomorphism: the "moreover" of Stacks 02ZN, repeated by Stacks 02ZP. Let G : 𝒜 ⥤ ℬ exhibit the stack p' as the stackification of the fibred category p, and let F : 𝒜 ⥤ 𝒳 be a 1-morphism into a stack q satisfying the same two clauses — hFmor, that the induced maps of morphism presheaves are locally bijective, and hFobj, that every object of a fibre of q is locally in the essential image of F on fibres. Then the extension of F along G supplied by the universal property, Stacks 0435, is an equivalence of p' with q over 𝒞.

So a 1-morphism satisfying the two clauses does not merely land in a stack: it exhibits its target as the stackification. The extension is compatible with the two presentations by CategoryTheory.Functor.Stackification.unit, which is the 2-isomorphism G ⋙ H ≅ F, so the equivalence identifies the two presentations and not just the two targets.

theorem nonempty_isEquivalenceOver_extend :
    Nonempty (IsEquivalenceOver p' q
      (extend hG hF hGmor hq.isMorSheaf hGobj hq.hasEffectiveDescent))

Tag 0436, a lemma

Tag 0436 in the Stacks Project.

CategoryTheory.Functor.Stackification.extendGroupoid, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stackification/UniversalPropertyGroupoid.lean, line 81.

Let (𝒞, J) be a site, let p : 𝒮 ⥤ 𝒞 be a category fibred in groupoids, let G : 𝒮 ⥤ 𝒮' exhibit the stack in groupoids p' as the stackification of 𝒮, and let F : 𝒮 ⥤ 𝒳 be a 1-morphism of categories over 𝒞 into a stack in groupoids. This is the extension H : 𝒮' ⥤ 𝒳 of F along G.

noncomputable def extendGroupoid : 𝒮' ⥤ 𝒳

CategoryTheory.Functor.Stackification.extendGroupoid_comp_eq, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stackification/UniversalPropertyGroupoid.lean, line 90.

The extension H : 𝒮' ⥤ 𝒳 is strictly over 𝒞: H ⋙ q = p'.

theorem extendGroupoid_comp_eq :
    extendGroupoid hp hp' hsp' hq hsq hG hF hmor hobj ⋙ q = p'

CategoryTheory.Functor.Stackification.unitGroupoid, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stackification/UniversalPropertyGroupoid.lean, line 107.

The 2-isomorphism G ⋙ H ≅ F between F and the composite of G with its extension.

noncomputable def unitGroupoid :
    G ⋙ extendGroupoid hp hp' hsp' hq hsq hG hF hmor hobj ≅ F

CategoryTheory.Functor.Stackification.isHomLift_unitGroupoid_app, a lemma in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stackification/UniversalPropertyGroupoid.lean, line 117.

Every component of the 2-isomorphism G ⋙ H ≅ F lies over an identity morphism of 𝒞.

lemma isHomLift_unitGroupoid_app (A : 𝒮) :
    q.IsHomLift (𝟙 (p.obj A)) ((unitGroupoid hp hp' hsp' hq hsq hG hF hmor hobj).hom.app A)

Tag 04Y2, a lemma

Tag 04Y2 in the Stacks Project.

CategoryTheory.TwoFibreProductOver.isStackification_of_isStackification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stackification/TwoFibreProductGroupoid/IsStackification.lean, line 353.

Stacks 04Y2. Let (𝒞, J) be a site, let f : 𝒳 ⥤ 𝒴 and g : 𝒵 ⥤ 𝒴 be 1-morphisms of categories fibred in groupoids over 𝒞, let i : 𝒳 ⥤ 𝒳', j : 𝒴 ⥤ 𝒴', k : 𝒵 ⥤ 𝒵' be stackifications (Stacks 02ZP: the targets are stacks in groupoids, the induced maps Mor(x, y) ⟶ Mor(i x, i y) of presheaves on 𝒞/U are locally bijective, and every object of the target is locally in the essential image), and let f' : 𝒳' ⥤ 𝒴', g' : 𝒵' ⥤ 𝒴' be 1-morphisms over 𝒞 2-commuting with f and g along i, j, k via vertical 2-isomorphisms α, β. Then the stackification of the 2-fibre product is the 2-fibre product of the stackifications: the 2-fibre product 𝒳' ×_{𝒴'} 𝒵' is a stack over (𝒞, J) — a stack in groupoids, being fibred in groupoids by Stacks 0041 — and every canonical 1-morphism H : 𝒳 ×_𝒴 𝒵 ⥤ 𝒳' ×_{𝒴'} 𝒵', that is every morphism of the two 2-commutative squares, is a 1-morphism of fibred categories over 𝒞 which is a stackification of 𝒳 ×_𝒴 𝒵, in the same two clauses.

public theorem isStackification_of_isStackification {J : GrothendieckTopology 𝒞} {p𝒳 : 𝒳 ⥤ 𝒞}
    {p𝒴 : 𝒴 ⥤ 𝒞} {p𝒵 : 𝒵 ⥤ 𝒞} {p𝒳' : 𝒳' ⥤ 𝒞} {p𝒴' : 𝒴' ⥤ 𝒞} {p𝒵' : 𝒵' ⥤ 𝒞}
    (h𝒳 : p𝒳.IsFiberedInGroupoids) (h𝒴 : p𝒴.IsFiberedInGroupoids) (h𝒵 : p𝒵.IsFiberedInGroupoids)
    (h𝒳' : p𝒳'.IsFiberedInGroupoids) (h𝒴' : p𝒴'.IsFiberedInGroupoids)
    (h𝒵' : p𝒵'.IsFiberedInGroupoids) (hs𝒳' : p𝒳'.IsStack J) (hs𝒴' : p𝒴'.IsStack J)
    (hs𝒵' : p𝒵'.IsStack J) {f : 𝒳 ⥤ 𝒴} {g : 𝒵 ⥤ 𝒴} (hf : f ⋙ p𝒴 = p𝒳) (hg : g ⋙ p𝒴 = p𝒵)
    {f' : 𝒳' ⥤ 𝒴'} {g' : 𝒵' ⥤ 𝒴'} (hf' : f' ⋙ p𝒴' = p𝒳') (hg' : g' ⋙ p𝒴' = p𝒵') {i : 𝒳 ⥤ 𝒳'}
    {j : 𝒴 ⥤ 𝒴'} {k : 𝒵 ⥤ 𝒵'} (hi : i ⋙ p𝒳' = p𝒳) (hj : j ⋙ p𝒴' = p𝒴) (hk : k ⋙ p𝒵' = p𝒵)
    (hmor𝒳 :
      haveI : p𝒳.IsFibered := h𝒳.isFibered
      haveI : p𝒳'.IsFibered := h𝒳'.isFibered
      ∀ (U : 𝒞) (x₁ x₂ : p𝒳.Fiber U),
        Presheaf.IsLocallyInjective (J.over U)
            ((h𝒳'.isFibredOneMorphism hi).morPresheafMap x₁ x₂) ∧
          Presheaf.IsLocallySurjective (J.over U)
            ((h𝒳'.isFibredOneMorphism hi).morPresheafMap x₁ x₂))
    (hobj𝒳 :
      ∀ x' : 𝒳',
        ∃ R ∈ J (p𝒳'.obj x'),
          ∀ ⦃V : 𝒞⦄ (u : V ⟶ p𝒳'.obj x'),
            R u → ∃ (x : 𝒳) (φ : i.obj x ⟶ x'), p𝒳'.IsStronglyCartesian u φ)
    (hmor𝒴 :
      haveI : p𝒴.IsFibered := h𝒴.isFibered
      haveI : p𝒴'.IsFibered := h𝒴'.isFibered
      ∀ (U : 𝒞) (y₁ y₂ : p𝒴.Fiber U),
        Presheaf.IsLocallyInjective (J.over U)
            ((h𝒴'.isFibredOneMorphism hj).morPresheafMap y₁ y₂) ∧
          Presheaf.IsLocallySurjective (J.over U)
            ((h𝒴'.isFibredOneMorphism hj).morPresheafMap y₁ y₂))
    (_hobj𝒴 :
      ∀ y' : 𝒴',
        ∃ R ∈ J (p𝒴'.obj y'),
          ∀ ⦃V : 𝒞⦄ (u : V ⟶ p𝒴'.obj y'),
            R u → ∃ (y : 𝒴) (φ : j.obj y ⟶ y'), p𝒴'.IsStronglyCartesian u φ)
    (hmor𝒵 :
      haveI : p𝒵.IsFibered := h𝒵.isFibered
      haveI : p𝒵'.IsFibered := h𝒵'.isFibered
      ∀ (U : 𝒞) (z₁ z₂ : p𝒵.Fiber U),
        Presheaf.IsLocallyInjective (J.over U)
            ((h𝒵'.isFibredOneMorphism hk).morPresheafMap z₁ z₂) ∧
          Presheaf.IsLocallySurjective (J.over U)
            ((h𝒵'.isFibredOneMorphism hk).morPresheafMap z₁ z₂))
    (hobj𝒵 :
      ∀ z' : 𝒵',
        ∃ R ∈ J (p𝒵'.obj z'),
          ∀ ⦃V : 𝒞⦄ (u : V ⟶ p𝒵'.obj z'),
            R u → ∃ (z : 𝒵) (φ : k.obj z ⟶ z'), p𝒵'.IsStronglyCartesian u φ)
    (α : i ⋙ f' ≅ f ⋙ j) (hα : ∀ x : 𝒳, p𝒴'.IsHomLift (𝟙 (p𝒳.obj x)) (α.hom.app x))
    (β : k ⋙ g' ≅ g ⋙ j) (hβ : ∀ z : 𝒵, p𝒴'.IsHomLift (𝟙 (p𝒵.obj z)) (β.hom.app z))
    {H : TwoFibreProductOver p𝒳 p𝒵 p𝒴 f g ⥤ TwoFibreProductOver p𝒳' p𝒵' p𝒴' f' g'}
    (γ : H ⋙ fst p𝒳' p𝒵' p𝒴' f' g' ≅ fst p𝒳 p𝒵 p𝒴 f g ⋙ i)
    (hγ : ∀ P : TwoFibreProductOver p𝒳 p𝒵 p𝒴 f g, p𝒳'.IsHomLift (𝟙 P.base) (γ.hom.app P))
    (δ : H ⋙ snd p𝒳' p𝒵' p𝒴' f' g' ≅ snd p𝒳 p𝒵 p𝒴 f g ⋙ k)
    (hδ : ∀ P : TwoFibreProductOver p𝒳 p𝒵 p𝒴 f g, p𝒵'.IsHomLift (𝟙 P.base) (δ.hom.app P))
    (hψ :
      Functor.whiskerLeft H (psi p𝒳' p𝒵' p𝒴' f' g') ≫ Functor.whiskerRight δ.hom g' =
        Functor.whiskerRight γ.hom f' ≫
          Functor.whiskerLeft (fst p𝒳 p𝒵 p𝒴 f g) α.hom ≫
          Functor.whiskerRight (psi p𝒳 p𝒵 p𝒴 f g) j ≫
          Functor.whiskerLeft (snd p𝒳 p𝒵 p𝒴 f g) β.inv) :
    haveI : (structureFunctor p𝒳 p𝒵 p𝒴 f g).IsFibered :=
      (isFiberedInGroupoids p𝒳 p𝒵 p𝒴 f g h𝒳 h𝒵 h𝒴 hf hg).isFibered
    haveI : (structureFunctor p𝒳' p𝒵' p𝒴' f' g').IsFibered :=
      (isFiberedInGroupoids p𝒳' p𝒵' p𝒴' f' g' h𝒳' h𝒵' h𝒴' hf' hg').isFibered
    (structureFunctor p𝒳' p𝒵' p𝒴' f' g').IsStack J ∧
      ∃ hH :
        Functor.IsFibredOneMorphism (structureFunctor p𝒳 p𝒵 p𝒴 f g)
          (structureFunctor p𝒳' p𝒵' p𝒴' f' g') H,
        (∀ (U : 𝒞) (P Q : (structureFunctor p𝒳 p𝒵 p𝒴 f g).Fiber U),
            Presheaf.IsLocallyInjective (J.over U) (hH.morPresheafMap P Q) ∧
              Presheaf.IsLocallySurjective (J.over U) (hH.morPresheafMap P Q)) ∧
          ∀ P' : TwoFibreProductOver p𝒳' p𝒵' p𝒴' f' g',
            ∃ R ∈ J P'.base,
              ∀ ⦃V : 𝒞⦄ (u : V ⟶ P'.base),
                R u →
                  ∃ (P : TwoFibreProductOver p𝒳 p𝒵 p𝒴 f g) (φ : H.obj P ⟶ P'),
                    (structureFunctor p𝒳' p𝒵' p𝒴' f' g').IsStronglyCartesian u φ

Sources

LeanCategoryTheory.Functor.Stackification.isFiberedInGroupoids_of_isStackification · CategoryTheory.Functor.Stackification.isStackInGroupoids_of_isStackification · CategoryTheory.Functor.Stackification.nonempty_isEquivalenceOver_of_locally_fullyFaithful · CategoryTheory.Functor.Stackification.nonempty_isEquivalenceOver_extend · CategoryTheory.Functor.Stackification.extendGroupoid · CategoryTheory.Functor.Stackification.extendGroupoid_comp_eq · CategoryTheory.Functor.Stackification.unitGroupoid · CategoryTheory.Functor.Stackification.isHomLift_unitGroupoid_app

Section8.10 Inherited topologies #

Section 8.10 of the Stacks Project, Tag 06NT. 6 tags here are carried by 15 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06NU, a lemma

Tag 06NU in the Stacks Project.

CategoryTheory.Functor.inheritedPrecoverage_hasIsos, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/InheritedSite.lean, line 137. The attribute's comment: “Axiom (1): isomorphisms cover.”.

Stacks 06NU, axiom (1) of a site: a family consisting of a single isomorphism of 𝒮 is a covering, because an isomorphism is strongly cartesian and its image is an isomorphism of 𝒞.

instance inheritedPrecoverage_hasIsos [Precoverage.HasIsos K] :
    Precoverage.HasIsos (p.inheritedPrecoverage K)

CategoryTheory.Functor.inheritedPrecoverage_isStableUnderComposition, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/InheritedSite.lean, line 150. The attribute's comment: “Axiom (2): coverings are stable under composition.”.

Stacks 06NU, axiom (2) of a site: refining a covering by coverings again gives a covering, because a composition of strongly cartesian morphisms is strongly cartesian (Stacks 02XL) and the images compose to a covering of 𝒞.

instance inheritedPrecoverage_isStableUnderComposition
    [Precoverage.IsStableUnderComposition K] :
    Precoverage.IsStableUnderComposition (p.inheritedPrecoverage K)

CategoryTheory.Functor.inheritedPrecoverage_hasPullbacks, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/InheritedSite.lean, line 173. The attribute's comment: “Axiom (3), existence of the fibre products.”.

Stacks 06NU, the existence half of axiom (3) of a site: given a covering { x i ⟶ x } of 𝒮 and a morphism y ⟶ x, the fibre products x i ×_x y exist. This is Stacks 06N5, applied to the strongly cartesian morphism x i ⟶ x and the fibre product of the images, which exists in 𝒞.

instance inheritedPrecoverage_hasPullbacks [p.IsFibered] [HasPullbacks 𝒞] :
    (p.inheritedPrecoverage K).HasPullbacks

CategoryTheory.Functor.inheritedPrecoverage_isStableUnderBaseChange, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/InheritedSite.lean, line 184. The attribute's comment: “Axiom (3), the base change of a covering is a covering.”.

Stacks 06NU, the covering half of axiom (3) of a site: the family of projections { x i ×_x y ⟶ y } of a covering { x i ⟶ x } along y ⟶ x is again a covering. Both conditions transfer from { x i ⟶ x } by the two base-change lemmas above.

instance inheritedPrecoverage_isStableUnderBaseChange [p.IsFibered] [HasPullbacks 𝒞]
    [Precoverage.IsStableUnderBaseChange K] :
    Precoverage.IsStableUnderBaseChange (p.inheritedPrecoverage K)

Tag 06NV, a definition

Tag 06NV in the Stacks Project.

CategoryTheory.Functor.inheritedTopology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/InheritedSite.lean, line 207.

The Grothendieck topology on a fibred category p : 𝒮 ⥤ 𝒞 inherited from a topology J on the base: the topology generated by the collection CategoryTheory.Functor.inheritedPrecoverage of Stacks 06NU, whose covering families are the families of strongly p-cartesian morphisms whose family of images covers in (𝒞, J).

def inheritedTopology (p : 𝒮 ⥤ 𝒞) (J : GrothendieckTopology 𝒞) : GrothendieckTopology 𝒮

Tag 06NW, a lemma

Tag 06NW in the Stacks Project.

CategoryTheory.Functor.IsFibredOneMorphism.isContinuous_and_isCocontinuous_inheritedTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/InheritedTopology/Functoriality.lean, line 179.

Let (𝒞, J) be a site and let F : 𝒳 ⥤ 𝒴 be a 1-morphism of fibred categories over 𝒞 (Stacks 02XP), so that F ⋙ q = p and F preserves strongly cartesian morphisms. Then F is a continuous and a cocontinuous functor between the topologies that 𝒳 and 𝒴 inherit from 𝒞 (Stacks 06NV).

public theorem IsFibredOneMorphism.isContinuous_and_isCocontinuous_inheritedTopology
    [HasPullbacks 𝒞] (J : GrothendieckTopology 𝒞) {p : 𝒳 ⥤ 𝒞} {q : 𝒴 ⥤ 𝒞} {F : 𝒳 ⥤ 𝒴}
    [p.IsFibered] [q.IsFibered] (hF : p.IsFibredOneMorphism q F) :
    F.IsContinuous (p.inheritedTopology J) (q.inheritedTopology J) ∧
      F.IsCocontinuous (p.inheritedTopology J) (q.inheritedTopology J)

CategoryTheory.Functor.IsFibredOneMorphism.inverseImageCompSheafToPresheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/InheritedTopology/Functoriality.lean, line 265.

The inverse image of the morphism of topoi induced by a 1-morphism of fibred categories is plain restriction along F.op: as a functor to presheaves on 𝒳 it is sheafToPresheaf followed by precomposition with F.op, with no sheafification intervening.

def IsFibredOneMorphism.inverseImageCompSheafToPresheafIso :
    letI := (hF.isContinuous_and_isCocontinuous_inheritedTopology J).1
    F.sheafPushforwardContinuous A (p.inheritedTopology J) (q.inheritedTopology J) ⋙
        sheafToPresheaf (p.inheritedTopology J) A ≅
      sheafToPresheaf (q.inheritedTopology J) A ⋙ (whiskeringLeft _ _ _).obj F.op

CategoryTheory.Functor.IsFibredOneMorphism.inverseImage_obj_obj_obj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/InheritedTopology/Functoriality.lean, line 276.

The formula f⁻¹(𝒢)(x) = 𝒢(F x): the sections of the inverse image of a sheaf 𝒢 on 𝒴 over an object x of 𝒳 are the sections of 𝒢 over F x.

theorem IsFibredOneMorphism.inverseImage_obj_obj_obj :
    letI := (hF.isContinuous_and_isCocontinuous_inheritedTopology J).1
    ∀ (𝒢 : Sheaf (q.inheritedTopology J) A) (x : 𝒳),
      ((F.sheafPushforwardContinuous A (p.inheritedTopology J)
            (q.inheritedTopology J)).obj 𝒢).obj.obj (Opposite.op x) =
        𝒢.obj.obj (Opposite.op (F.obj x))

CategoryTheory.Functor.IsFibredOneMorphism.preservesFiniteLimits_inverseImage, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/InheritedTopology/Functoriality.lean, line 288.

The inverse image f⁻¹ of the morphism of topoi induced by a 1-morphism of fibred categories preserves finite limits.

theorem IsFibredOneMorphism.preservesFiniteLimits_inverseImage [HasFiniteLimits A] :
    letI := (hF.isContinuous_and_isCocontinuous_inheritedTopology J).1
    PreservesFiniteLimits (F.sheafPushforwardContinuous A (p.inheritedTopology J)
      (q.inheritedTopology J))

CategoryTheory.Functor.IsFibredOneMorphism.directImageCompSheafToPresheafIso, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/InheritedTopology/Functoriality.lean, line 305.

The direct image of the morphism of topoi is the right Kan extension along F.op, taken on sheaves: as a functor to presheaves on 𝒴 it is sheafToPresheaf followed by F.op.ran.

noncomputable def IsFibredOneMorphism.directImageCompSheafToPresheafIso
    [∀ (G : 𝒳ᵒᵖ ⥤ A), F.op.HasPointwiseRightKanExtension G] :
    letI := (hF.isContinuous_and_isCocontinuous_inheritedTopology J).2
    F.sheafPushforwardCocontinuous A (p.inheritedTopology J) (q.inheritedTopology J) ⋙
        sheafToPresheaf (q.inheritedTopology J) A ≅
      sheafToPresheaf (p.inheritedTopology J) A ⋙ F.op.ran

CategoryTheory.Functor.IsFibredOneMorphism.sheafAdjunctionInheritedTopology, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/InheritedTopology/Functoriality.lean, line 319.

The morphism of topoi f : Sh(𝒳) ⟶ Sh(𝒴) induced by a 1-morphism of fibred categories F, as the adjunction f⁻¹ ⊣ f_* between the two inherited sites, with f⁻¹ the restriction F.sheafPushforwardContinuous and f_* the right Kan extension F.sheafPushforwardCocontinuous.

noncomputable def IsFibredOneMorphism.sheafAdjunctionInheritedTopology
    [∀ (G : 𝒳ᵒᵖ ⥤ A), F.op.HasPointwiseRightKanExtension G] :
    letI := (hF.isContinuous_and_isCocontinuous_inheritedTopology J).1
    letI := (hF.isContinuous_and_isCocontinuous_inheritedTopology J).2
    F.sheafPushforwardContinuous A (p.inheritedTopology J) (q.inheritedTopology J) ⊣
      F.sheafPushforwardCocontinuous A (p.inheritedTopology J) (q.inheritedTopology J)

Tag 0CN0, a lemma

Tag 0CN0 in the Stacks Project.

CategoryTheory.Functor.IsFiberedInGroupoids.isEquivalence_overPost, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Gerbe/Localization.lean, line 114. The attribute's comment: “the equivalence of categories 𝒳/x ⥤ 𝒞/U”.

For p : 𝒳 ⥤ 𝒞 fibred in groupoids and x an object of 𝒳, the functor Over.post p : 𝒳/x ⥤ 𝒞/p x induced by p is an equivalence of categories.

theorem IsFiberedInGroupoids.isEquivalence_overPost (hp : p.IsFiberedInGroupoids) (x : 𝒳) :
    (Over.post (X := x) p).IsEquivalence

CategoryTheory.Functor.IsInheritedTopology.mem_over_iff_functorPushforward, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Gerbe/Localization.lean, line 153. The attribute's comment: “coverings of x' in 𝒳/x correspond to coverings of p x' in 𝒞/U”.

For p fibred in groupoids and J𝒳 inherited from (𝒞, J), a sieve on an object of 𝒳/x is covering for the topology that J𝒳 induces on 𝒳/x exactly when its image under Over.post p is covering for the topology that J induces on 𝒞/p x.

theorem IsInheritedTopology.mem_over_iff_functorPushforward (hp : p.IsFiberedInGroupoids)
    {J : GrothendieckTopology 𝒞} {J𝒳 : GrothendieckTopology 𝒳}
    (hJ : _root_.CategoryTheory.Functor.IsInheritedTopology.{max u₂ v₂} p J J𝒳)
    {x : 𝒳} (Y : Over x) (S : Sieve Y) :
    S ∈ (J𝒳.over x) Y ↔
      Sieve.functorPushforward (Over.post p) S ∈
        (J.over (p.obj x)) ((Over.post (X := x) p).obj Y)

Tag 06NX, a lemma

Tag 06NX in the Stacks Project.

CategoryTheory.Functor.isStackInGroupoids_of_isFiberedInGroupoids, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/InheritedTopology/Basic.lean, line 35.

Let (𝒞, J) be a site, let p : 𝒳 ⥤ 𝒞 and q : 𝒴 ⥤ 𝒞 be stacks in groupoids over 𝒞 and let F : 𝒳 ⥤ 𝒴 be a 1-morphism of categories over 𝒞, that is F ⋙ q = p. If F makes 𝒳 a category fibred in groupoids over 𝒴, then 𝒳 is a stack in groupoids over 𝒴 for the topology J𝒴 inherited from (𝒞, J).

theorem isStackInGroupoids_of_isFiberedInGroupoids
    (J : GrothendieckTopology 𝒞) (J𝒴 : GrothendieckTopology 𝒴)
    (p : 𝒳 ⥤ 𝒞) (q : 𝒴 ⥤ 𝒞) (F : 𝒳 ⥤ 𝒴)
    (hp : IsStackInGroupoids.{w} p J) (hq : IsStackInGroupoids.{w} q J)
    (hF₁ : F ⋙ q = p)
    (hF₂ : F.IsFiberedInGroupoids)
    (hJ𝒴 : IsInheritedTopology.{w} q J J𝒴) :
    IsStackInGroupoids.{w} F J𝒴

Tag 09WX, a lemma

Tag 09WX in the Stacks Project.

CategoryTheory.Functor.isStack_comp_of_isInheritedTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/InheritedTopology/StackOverStack/IsStack.lean, line 315.

Let (𝒞, J) be a site, let p : 𝒳 ⥤ 𝒞 be a stack over 𝒞, endow 𝒳 with the topology J𝒳 inherited from (𝒞, J) and let q : 𝒴 ⥤ 𝒳 be a stack over (𝒳, J𝒳). Then 𝒴 is a stack over 𝒞, along q ⋙ p; and if p and q define stacks in groupoids, that is if both are fibred in groupoids, then 𝒴 is a stack in groupoids over 𝒞.

public theorem isStack_comp_of_isInheritedTopology (hp : p.IsStack J)
    (hJ𝒳 : IsInheritedTopology.{max u₂ v₂} p J J𝒳) (hq : q.IsStack J𝒳) :
    (q ⋙ p).IsStack J ∧
      (p.IsFiberedInGroupoids →
        q.IsFiberedInGroupoids → (q ⋙ p).IsFiberedInGroupoids ∧ (q ⋙ p).IsStack J)

Sources

LeanCategoryTheory.Functor.inheritedPrecoverage_hasIsos · CategoryTheory.Functor.inheritedPrecoverage_isStableUnderComposition · CategoryTheory.Functor.inheritedPrecoverage_hasPullbacks · CategoryTheory.Functor.inheritedPrecoverage_isStableUnderBaseChange · CategoryTheory.Functor.inheritedTopology · CategoryTheory.Functor.IsFibredOneMorphism.isContinuous_and_isCocontinuous_inheritedTopology · CategoryTheory.Functor.IsFibredOneMorphism.inverseImageCompSheafToPresheafIso · CategoryTheory.Functor.IsFibredOneMorphism.inverseImage_obj_obj_obj

Section8.11 Gerbes #

Section 8.11 of the Stacks Project, Tag 06NY. 8 tags here are carried by 10 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 06NZ, a definition

Tag 06NZ in the Stacks Project.

CategoryTheory.Functor.IsGerbe, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Gerbe/Defs.lean, line 58.

A gerbe over the site (𝒞, J) is a category p : 𝒮 ⥤ 𝒞 over 𝒞 which is a stack in groupoids over 𝒞 (Stacks 02ZI), locally nonempty, and locally connected.

def IsGerbe (p : 𝒮 ⥤ 𝒞) (J : GrothendieckTopology 𝒞) : Prop

Tag 06P0, a lemma

Tag 06P0 in the Stacks Project.

CategoryTheory.isGerbeOver_iff_of_isEquivalenceOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Gerbe/Equivalence.lean, line 296.

Stacks 06P0, in the relative form: a 1-morphism over 𝒴 that is an equivalence over 𝒴 makes 𝒳 a gerbe over 𝒴 exactly when its target is one. The source statement is the case 𝒴 = 𝒞, q = 𝟭 𝒞, where IsGerbeOver J (𝟭 𝒞) · is being a gerbe over the site (𝒞, J) by isGerbeOver_id_iff and being an equivalence over 𝒴 is being an equivalence over 𝒞.

theorem isGerbeOver_iff_of_isEquivalenceOver {J : GrothendieckTopology 𝒞} {q : 𝒴 ⥤ 𝒞}
    {F : 𝒳 ⥤ 𝒴} {F' : 𝒳' ⥤ 𝒴} {a : 𝒳 ⥤ 𝒳'} (ha : a ⋙ F' = F)
    (e : Functor.IsEquivalenceOver F F' a) :
    IsGerbeOver J q F ↔ IsGerbeOver J q F'

Tag 06P1, a lemma

Tag 06P1 in the Stacks Project.

CategoryTheory.isGerbe_of_factorization_iff_isGerbeOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Gerbe/WhenGerbe.lean, line 322.

Stacks 06P1. Let (𝒞, J) be a site, let q : 𝒴 ⥤ 𝒞 and F ⋙ q : 𝒳 ⥤ 𝒞 be stacks in groupoids over 𝒞 and let J𝒴 be the topology on 𝒴 inherited from (𝒞, J). Let F = a ⋙ F' be a factorization of F through an equivalence a over 𝒞 with F' fibred in groupoids — a factorization of exactly the kind Stacks 06N7 produces. Then clause (1) of Stacks 06P1 — that F' is a gerbe over the site (𝒴, J𝒴) — holds exactly when clause (2) does, that is exactly when IsGerbeOver J q F.

Since the right-hand side does not mention the factorization, this also says that clause (1) holds for one such factorization exactly when it holds for every one, which is the source's parenthesis "for some (equivalently any)".

The equivalence a is asked to be an equivalence over 𝒞, as the source asks and as Stacks 06N7 delivers, not over 𝒴: CategoryTheory.isGerbeOver_iff_of_isEquivalenceOver, the relative Stacks 06P0, assumes the latter, and 06N7's factorization does not satisfy it — see StacksFrontier.CategoryTheory.Sites.Gerbe.BaseEquivalence, which supplies the version used here.

theorem isGerbe_of_factorization_iff_isGerbeOver {𝒳' : Type u₄} [Category.{v₄} 𝒳']
    {F' : 𝒳' ⥤ 𝒴} {a : 𝒳 ⥤ 𝒳'} (ha : a ⋙ F' = F)
    (e : Functor.IsEquivalenceOver (F ⋙ q) (F' ⋙ q) a)
    (hp' : Functor.IsStackInGroupoids.{max u₃ v₃} (F' ⋙ q) J)
    (hq : Functor.IsStackInGroupoids.{max u₃ v₃} q J) (hF' : F'.IsFiberedInGroupoids)
    (hJ𝒴 : Functor.IsInheritedTopology.{max u₃ v₃} q J J𝒴) :
    F'.IsGerbe.{max u₃ v₃} J𝒴 ↔ IsGerbeOver J q F

Tag 06P2, a definition

Tag 06P2 in the Stacks Project.

CategoryTheory.IsGerbeOver, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Gerbe/Basic.lean, line 117.

Stacks 06P2. F makes 𝒳 a gerbe over 𝒴, where q : 𝒴 ⥤ 𝒞 fibres 𝒴 over the site (𝒞, J) and F ⋙ q fibres 𝒳 over it: both fibrations are fibred in groupoids, every object of 𝒴 is locally in the image of F, and every morphism of a fibre of q between F-images is locally the F-image of a morphism of a fibre of F ⋙ q. The last two conditions are Stacks 06P1 (2)(a) and (2)(b).

structure IsGerbeOver (J : GrothendieckTopology 𝒞) (q : 𝒴 ⥤ 𝒞) (F : 𝒳 ⥤ 𝒴) : Prop

Tag 06P3, a lemma

Tag 06P3 in the Stacks Project.

CategoryTheory.IsGerbeOver.twoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Gerbe/Pullback.lean, line 292.

Stacks 06P3. Let 𝒳' = 𝒴' ×_𝒴 𝒳 be the 2-fibre product over 𝒞 of G : 𝒴' ⥤ 𝒴 and F : 𝒳 ⥤ 𝒴, where 𝒳 sits over 𝒞 by F ⋙ q and 𝒴' by G ⋙ q. If F makes 𝒳 a gerbe over 𝒴 and 𝒴' is fibred in groupoids over 𝒞, then the first projection makes 𝒳' a gerbe over 𝒴'.

Both local conditions are pulled back along G: an object of 𝒳 over a member of a covering whose F-image is a restriction of G y' is the second component of an object of 𝒳' over that member whose first component is a restriction of y', and a morphism of 𝒳 matching the G-image of b' is the second component of a morphism of 𝒳' whose first component is the restriction of b'.

theorem IsGerbeOver.twoFibreProduct {J : GrothendieckTopology 𝒞} (hF : IsGerbeOver J q F)
    (hG : (G ⋙ q).IsFiberedInGroupoids) :
    IsGerbeOver J (G ⋙ q) (fst (G ⋙ q) (F ⋙ q) q G F)

Tag 06R3, a lemma

Tag 06R3 in the Stacks Project.

CategoryTheory.IsGerbeOver.comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Gerbe/Basic.lean, line 174.

Stacks 06R3. If 𝒳 is a gerbe over 𝒴 and 𝒴 is a gerbe over 𝒵, then 𝒳 is a gerbe over 𝒵.

This is also Stacks 06R8, the same statement for morphisms of algebraic stacks: the source proves 06R8 by citing 06R3, and an algebraic stack is a category fibred in groupoids over the big fppf site, so the two differ only in the generality of the ambient site.

theorem comp (hF : IsGerbeOver J (G ⋙ r) F) (hG : IsGerbeOver J r G) :
    IsGerbeOver J r (F ⋙ G)

Tag 06P4, a lemma

Tag 06P4 in the Stacks Project.

CategoryTheory.IsGerbeOver.of_twoFibreProduct, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Gerbe/Pullback.lean, line 333.

Stacks 06P4. Let 𝒳' = 𝒴' ×_𝒴 𝒳 be the 2-fibre product over 𝒞 of G : 𝒴' ⥤ 𝒴 and F : 𝒳 ⥤ 𝒴. If every object of 𝒴 is locally in the image of G — the condition CategoryTheory.IsGerbeOver.locally_essSurj for G — and the first projection makes 𝒳' a gerbe over 𝒴', then F makes 𝒳 a gerbe over 𝒴.

This is the converse direction of Stacks 06P3: the two local conditions are descended along G. For the first, an object y' of 𝒴' whose G-image restricts y is refined by a covering along which 𝒳' has objects over y', and their second components are objects of 𝒳 whose F-images restrict y. For the second, two restrictions of x₁ and x₂ and the comparison isomorphisms G y' ≅ F x₁|_V, G y' ≅ F x₂|_V obtained from b assemble into two objects of 𝒳' with the same first component y', so that the identity of y' is a morphism of a fibre between their images; local fullness of the first projection then supplies the morphism of 𝒳 wanted.

theorem IsGerbeOver.of_twoFibreProduct {J : GrothendieckTopology 𝒞} (hq : q.IsFiberedInGroupoids)
    (hFq : (F ⋙ q).IsFiberedInGroupoids)
    (hGsurj : ∀ {U : 𝒞} (y : 𝒴), q.obj y = U → ∃ S ∈ J U,
      ∀ ⦃V : 𝒞⦄ (f : V ⟶ U), S f → ∃ (y' : 𝒴') (ψ : G.obj y' ⟶ y), q.IsHomLift f ψ)
    (h : IsGerbeOver J (G ⋙ q) (fst (G ⋙ q) (F ⋙ q) q G F)) :
    IsGerbeOver J q F

Tag 0CJY, a lemma

Tag 0CJY in the Stacks Project.

CategoryTheory.Gerbe.exists_sheaf_iso_morPresheaf_self_uliftFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Gerbe/BandedSheaf.lean, line 1158.

Stacks 0CJY, with no hypothesis on the universes. Let p : 𝒮 ⥤ 𝒞 be a gerbe over the site (𝒞, J): fibred in groupoids, a stack, locally nonempty and locally connected. Assume that for every U and every object x of the fibre 𝒮_U the sheaf of groups Aut(x) = Isom(x, x) = Mor(x, x) on 𝒞/U is abelian, that is that the endomorphisms of every object of every fibre commute. Then there are

a sheaf 𝒢 of abelian groups on 𝒞, and

for every U and every object x of 𝒮_U an isomorphism θ x : 𝒢|_U ≅ Aut(x) of sheaves of groups on 𝒞/U, that is an isomorphism of presheaves whose components are multiplicative,

such that for every U and every morphism φ : x ⟶ y of 𝒮_U conjugation by φ carries θ x to θ y: on sections over g : V ⟶ U one has θ y a = φ|_V ∘ θ x a ∘ (φ|_V)⁻¹.

𝒢 is the band, CategoryTheory.Gerbe.Band, which lives in Type (max u₁ v₁ v₂) and not in the universe v₂ of Aut(x); the isomorphism of (2) is therefore stated against the universe lift of Aut(x), which is what makes the statement true in every universe. See CategoryTheory.Gerbe.exists_sheaf_iso_morPresheaf_self for the unlifted form, which needs UnivLE.{max u₁ v₁, v₂} and is false without it.

public theorem exists_sheaf_iso_morPresheaf_self_uliftFunctor (p : 𝒮 ⥤ 𝒞)
    (J : GrothendieckTopology 𝒞) (hp : p.IsFiberedInGroupoids) (hst : p.IsStack J)
    (hne : p.LocallyNonempty J) (hlc : p.LocallyConnected J)
    (habel : ∀ (U : 𝒞) (x : p.Fiber U) (α β : x ⟶ x), α ≫ β = β ≫ α) :
    haveI : p.IsFibered := hp.isFibered
    haveI : ∀ U : 𝒞, IsGroupoid (p.Fiber U) := hp.fiber_isGroupoid
    ∃ (𝒢 : Sheaf J CommGrpCat.{max u₁ v₁ v₂})
      (θ : ∀ (U : 𝒞) (x : p.Fiber U),
        (Over.forget U).op ⋙ 𝒢.obj ⋙ forget CommGrpCat.{max u₁ v₁ v₂} ≅
          p.morPresheaf x x ⋙ uliftFunctor.{max u₁ v₁, v₂}),
      (∀ (U : 𝒞) (x : p.Fiber U) (g : Over U) (a b : 𝒢.obj.obj (op g.left)),
          ((θ U x).hom.app (op g) (a * b)).down =
            ((θ U x).hom.app (op g) a).down ≫ ((θ U x).hom.app (op g) b).down) ∧
        ∀ (U : 𝒞) (x y : p.Fiber U) (φ : x ⟶ y) (g : Over U) (a : 𝒢.obj.obj (op g.left)),
          ((θ U y).hom.app (op g) a).down =
            pullbackFiberHom (CategoryTheory.inv φ) g.hom ≫ ((θ U x).hom.app (op g) a).down ≫
              pullbackFiberHom φ g.hom

CategoryTheory.Gerbe.exists_sheaf_iso_morPresheaf_self, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Gerbe/BandedSheaf.lean, line 1196.

Stacks 0CJY. Let p : 𝒮 ⥤ 𝒞 be a gerbe over the site (𝒞, J) whose automorphism sheaves are abelian. Then there are a sheaf 𝒢 of abelian groups on 𝒞 and, for every U and every object x of the fibre 𝒮_U, an isomorphism θ x : 𝒢|_U ≅ Aut(x) of sheaves of groups on 𝒞/U, and these are compatible with conjugation.

The hypothesis UnivLE.{max u₁ v₁, v₂} is what makes 𝒢 exist in the universe v₂ of the morphisms of 𝒮, and it cannot be dropped: Type 0-many copies of a nontrivial ℤ/2-gerbe give a band whose sections at the top object have cardinality 2 ^ |Type 0|, which is the cardinality of no Type 0. Without it the statement still holds in the form CategoryTheory.Gerbe.exists_sheaf_iso_morPresheaf_self_uliftFunctor, with Aut(x) lifted into the universe 𝒢 is valued in.

public theorem exists_sheaf_iso_morPresheaf_self [UnivLE.{max u₁ v₁, v₂}] (p : 𝒮 ⥤ 𝒞)
    (J : GrothendieckTopology 𝒞) (hp : p.IsFiberedInGroupoids) (hst : p.IsStack J)
    (hne : p.LocallyNonempty J) (hlc : p.LocallyConnected J)
    (habel : ∀ (U : 𝒞) (x : p.Fiber U) (α β : x ⟶ x), α ≫ β = β ≫ α) :
    haveI : p.IsFibered := hp.isFibered
    haveI : ∀ U : 𝒞, IsGroupoid (p.Fiber U) := hp.fiber_isGroupoid
    ∃ (𝒢 : Sheaf J CommGrpCat.{v₂})
      (θ : ∀ (U : 𝒞) (x : p.Fiber U),
        (Over.forget U).op ⋙ 𝒢.obj ⋙ forget CommGrpCat.{v₂} ≅ p.morPresheaf x x),
      (∀ (U : 𝒞) (x : p.Fiber U) (g : Over U) (a b : 𝒢.obj.obj (op g.left)),
          (θ U x).hom.app (op g) (a * b) =
            (θ U x).hom.app (op g) a ≫ (θ U x).hom.app (op g) b) ∧
        ∀ (U : 𝒞) (x y : p.Fiber U) (φ : x ⟶ y) (g : Over U) (a : 𝒢.obj.obj (op g.left)),
          (θ U y).hom.app (op g) a =
            pullbackFiberHom (CategoryTheory.inv φ) g.hom ≫ (θ U x).hom.app (op g) a ≫
              pullbackFiberHom φ g.hom

CategoryTheory.Gerbe.exists_sheaf_iso_morPresheaf_self_uliftFunctor_base, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Gerbe/BandedSheaf.lean, line 1240.

Stacks 0CJY, with the compatibility of the comparisons over varying base object. Let p : 𝒮 ⥤ 𝒞 be a gerbe over the site (𝒞, J) whose automorphism sheaves are abelian. Then there are a sheaf 𝒢 of abelian groups on 𝒞 and, for every U and every object x of the fibre 𝒮_U, an isomorphism θ x : 𝒢|_U ≅ Aut(x) of sheaves of groups on 𝒞/U, such that

each θ x is multiplicative on sections,

for φ : x ⟶ y in 𝒮_U, conjugation by φ carries θ x to θ y, and

θ x read on sections over g : Over U is θ (x|_g) read on sections over the identity of g.left, conjugated by the contraction of the chosen pullback along that identity.

Clauses (1) and (2) are the conclusion of Stacks 0CJY as the source states it, so this is CategoryTheory.Gerbe.exists_sheaf_iso_morPresheaf_self_uliftFunctor with (3) added. Clause (3) is the compatibility of the local comparisons over varying U whose verification the source's proof omits; for the band it is CategoryTheory.Gerbe.Band.fiberHom_pullbackFiber_base, the naturality of a band section. It is what makes "the sheaf of abelian groups constructed in Stacks 0CJY" pin 𝒢 down well enough to use it as the coefficient sheaf of Stacks 0CK0, so that no hypothesis of CategoryTheory.Gerbe.exists_band_nonempty_fiber_of_cohomology_vanishing has to be assumed.

public theorem exists_sheaf_iso_morPresheaf_self_uliftFunctor_base (p : 𝒮 ⥤ 𝒞)
    (J : GrothendieckTopology 𝒞) (hp : p.IsFiberedInGroupoids) (hst : p.IsStack J)
    (hne : p.LocallyNonempty J) (hlc : p.LocallyConnected J)
    (habel : ∀ (U : 𝒞) (x : p.Fiber U) (α β : x ⟶ x), α ≫ β = β ≫ α) :
    haveI : p.IsFibered := hp.isFibered
    haveI : ∀ U : 𝒞, IsGroupoid (p.Fiber U) := hp.fiber_isGroupoid
    ∃ (𝒢 : Sheaf J CommGrpCat.{max u₁ v₁ v₂})
      (θ : ∀ (U : 𝒞) (x : p.Fiber U),
        (Over.forget U).op ⋙ 𝒢.obj ⋙ forget CommGrpCat.{max u₁ v₁ v₂} ≅
          p.morPresheaf x x ⋙ uliftFunctor.{max u₁ v₁, v₂}),
      (∀ (U : 𝒞) (x : p.Fiber U) (g : Over U) (a b : 𝒢.obj.obj (op g.left)),
          ((θ U x).hom.app (op g) (a * b)).down =
            ((θ U x).hom.app (op g) a).down ≫ ((θ U x).hom.app (op g) b).down) ∧
        (∀ (U : 𝒞) (x y : p.Fiber U) (φ : x ⟶ y) (g : Over U) (a : 𝒢.obj.obj (op g.left)),
          ((θ U y).hom.app (op g) a).down =
            pullbackFiberHom (CategoryTheory.inv φ) g.hom ≫ ((θ U x).hom.app (op g) a).down ≫
              pullbackFiberHom φ g.hom) ∧
        ∀ (U : 𝒞) (x : p.Fiber U) (g : Over U) (a : 𝒢.obj.obj (op g.left)),
          ((θ U x).hom.app (op g) a).down =
            (pullbackFiberIdIso (pullbackFiber p x g.hom)).inv ≫
              ((θ g.left (pullbackFiber p x g.hom)).hom.app (op (Over.mk (𝟙 g.left))) a).down ≫
                (pullbackFiberIdIso (pullbackFiber p x g.hom)).hom

Sources

LeanCategoryTheory.Functor.IsGerbe · CategoryTheory.isGerbeOver_iff_of_isEquivalenceOver · CategoryTheory.isGerbe_of_factorization_iff_isGerbeOver · CategoryTheory.IsGerbeOver · CategoryTheory.IsGerbeOver.twoFibreProduct · CategoryTheory.IsGerbeOver.comp · CategoryTheory.IsGerbeOver.of_twoFibreProduct · CategoryTheory.Gerbe.exists_sheaf_iso_morPresheaf_self_uliftFunctor

Section8.12 Functoriality for stacks #

Section 8.12 of the Stacks Project, Tag 04WA. 12 tags here are carried by 17 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04WB, a lemma

Tag 04WB in the Stacks Project.

CategoryTheory.StrictPullback.isFibered_structureFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/Functoriality/Pushforward.lean, line 163.

Stacks 04WB. If p : 𝒮 ⥤ 𝒟 is a fibred category, then so is the pushforward u^p𝒮 ⥤ 𝒞 along any functor u : 𝒞 ⥤ 𝒟.

theorem isFibered_structureFunctor (u : 𝒞 ⥤ 𝒟) (p : 𝒮 ⥤ 𝒟) [p.IsFibered] :
    (structureFunctor u p).IsFibered

Tag 04WC, a lemma

Tag 04WC in the Stacks Project.

CategoryTheory.StrictPullback.isStack_structureFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/Functoriality/PushforwardStack.lean, line 66.

Stacks 04WC. If p : 𝒮 ⥤ 𝒟 is a stack over the site (𝒟, K), then the pushforward u^p𝒮 ⥤ 𝒞 along a continuous functor of sites u : 𝒞 ⥤ 𝒟 is a stack over (𝒞, J).

Continuity of u in the sense of Stacks 00WU is [u.IsContinuous J K] together with the commutation with fibre products, [HasPullbacks 𝒞] and [PreservesLimitsOfShape WalkingCospan u]; see the implementation notes.

theorem isStack_structureFunctor (J : GrothendieckTopology 𝒞) (K : GrothendieckTopology 𝒟)
    (u : 𝒞 ⥤ 𝒟) [u.IsContinuous J K] [HasPullbacks 𝒞] [PreservesLimitsOfShape WalkingCospan u]
    (p : 𝒮 ⥤ 𝒟) (hp : Functor.IsStack p K) :
    Functor.IsStack (structureFunctor u p) J

Tag 04WD, a lemma

Tag 04WD in the Stacks Project.

CategoryTheory.StrictPullback.isStack_isFiberedInGroupoids_structureFunctor, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/Functoriality/PushforwardStack.lean, line 106.

Stacks 04WD. If p : 𝒮 ⥤ 𝒟 is a stack in groupoids over the site (𝒟, K), then the pushforward u^p𝒮 ⥤ 𝒞 along a continuous functor of sites u : 𝒞 ⥤ 𝒟 is a stack in groupoids over (𝒞, J).

theorem isStack_isFiberedInGroupoids_structureFunctor (J : GrothendieckTopology 𝒞)
    (K : GrothendieckTopology 𝒟) (u : 𝒞 ⥤ 𝒟) [u.IsContinuous J K] [HasPullbacks 𝒞]
    [PreservesLimitsOfShape WalkingCospan u] (p : 𝒮 ⥤ 𝒟) (hp : Functor.IsStack p K)
    (hp' : p.IsFiberedInGroupoids) :
    Functor.IsStack (structureFunctor u p) J ∧
      (structureFunctor u p).IsFiberedInGroupoids

Tag 04WE, a definition

Tag 04WE in the Stacks Project.

CategoryTheory.pushforwardFibredCategory, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/Functoriality/Pushforward.lean, line 188.

Stacks 04WE. Notation: for a morphism of sites f : 𝒟 → 𝒞 given by a continuous functor u : 𝒞 ⥤ 𝒟 and a fibred category p : 𝒮 ⥤ 𝒟, one writes f_*𝒮 for the fibred category u^p𝒮 over 𝒞 and calls it the pushforward of 𝒮 along f. The topologies J and K and the continuity of u play no role in the construction; they are the data of f, which is what this notation names.

def pushforwardFibredCategory (J : GrothendieckTopology 𝒞) (K : GrothendieckTopology 𝒟)
    (u : 𝒞 ⥤ 𝒟) [u.IsContinuous J K] (p : 𝒮 ⥤ 𝒟) [p.IsFibered] :
    StrictPullback u p ⥤ 𝒞

Tag 04WF, a lemma

Tag 04WF in the Stacks Project.

CategoryTheory.Comma.hasRightCalculusOfFractions_stronglyCartesianOver, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/Functoriality/PullbackFractions.lean, line 273.

The morphisms with identity base component and strongly cartesian fibre component form a right multiplicative system. Let u : 𝒞 ⥤ 𝒟 be a functor, let p : 𝒮 ⥤ 𝒞 be a fibred category, assume 𝒞 has nonempty finite limits and that u commutes with nonempty finite limits. In the category u_pp 𝒮 = Comma (𝟭 𝒟) (p ⋙ u), whose objects are the triples (U, φ : V ⟶ u(U), x ∈ 𝒮_U), consider the set R of morphisms (a, id_V, α) : (U', φ' : V ⟶ u(U'), x') ⟶ (U, φ : V ⟶ u(U), x) whose 𝒟-component is an identity and whose α is strongly cartesian. Then R is a right multiplicative system: it contains the identities and is stable under composition (RMS1), every left fraction over R can be turned into a right fraction (RMS2), and two morphisms equalized by postcomposition with an element of R are equalized by precomposition with an element of R (RMS3).

public theorem Comma.hasRightCalculusOfFractions_stronglyCartesianOver
    (p : 𝒮 ⥤ 𝒞) (u : 𝒞 ⥤ 𝒟) [p.IsFibered] [HasNonemptyFiniteLimits 𝒞]
    (hu : ∀ (J : Type) [SmallCategory J] [FinCategory J] [Nonempty J],
      Limits.PreservesLimitsOfShape J u) :
    MorphismProperty.HasRightCalculusOfFractions
      (fun (X Y : Comma (𝟭 𝒟) (p ⋙ u)) (f : X ⟶ Y) =>
        (∃ h : X.left = Y.left, f.left = eqToHom h) ∧ stronglyCartesianOver p f.right)

Tag 04WG, a lemma

Tag 04WG in the Stacks Project.

CategoryTheory.Comma.pullbackLocalization, an abbrev in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/Functoriality/PullbackFibred.lean, line 125.

u_p 𝒮 = R⁻¹ u_pp 𝒮, the localization of u_pp 𝒮 = Comma (𝟭 𝒟) (p ⋙ u) at the set R of Stacks 04WF.

abbrev pullbackLocalization

CategoryTheory.Comma.pullbackProj, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/Functoriality/PullbackFibred.lean, line 140.

The structure functor p_p : u_p 𝒮 ⥤ 𝒟, the extension of p_pp to the localization u_p 𝒮 obtained from the universal property because p_pp inverts R. This is how u_p 𝒮 is regarded as a category over 𝒟.

noncomputable def pullbackProj : pullbackLocalization p u ⥤ 𝒟

CategoryTheory.Comma.isFibered_pullbackProj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/Functoriality/PullbackFibred.lean, line 328.

u_p 𝒮 is a fibred category over 𝒟 (Stacks 04WG). Let u : 𝒞 ⥤ 𝒟 be a functor, let p : 𝒮 ⥤ 𝒞 be a fibred category, assume 𝒞 has nonempty finite limits and that u commutes with nonempty finite limits, so that the set R of Stacks 04WF is a right multiplicative system. Then the structure functor p_p : u_p 𝒮 ⥤ 𝒟 of the localization u_p 𝒮 = R⁻¹ u_pp 𝒮 is a fibred category: every morphism β : V' ⟶ V of 𝒟 and every object of u_p 𝒮 over V admit a strongly cartesian lift, namely the image of the reindexing morphism (id_U, β, id_x).

theorem isFibered_pullbackProj
    (hu : ∀ (J : Type) [SmallCategory J] [FinCategory J] [Nonempty J],
      Limits.PreservesLimitsOfShape J u) :
    (pullbackProj p u).IsFibered

Tag 04WH, a lemma

Tag 04WH in the Stacks Project.

CategoryTheory.Comma.isFiberedInGroupoids_pullbackProj, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/Functoriality/PullbackGroupoid.lean, line 186.

u_p 𝒮 is fibred in groupoids over 𝒟 (Stacks 04WH). With notation and assumptions as in Stacks 04WG — u : 𝒞 ⥤ 𝒟 a functor commuting with nonempty finite limits, 𝒞 with nonempty finite limits, and u_p 𝒮 = R⁻¹ u_pp 𝒮 the localization of u_pp 𝒮 = Comma (𝟭 𝒟) (p ⋙ u) at the set R of Stacks 04WF, regarded as a category over 𝒟 through p_p = Comma.pullbackProj p u — if p : 𝒮 ⥤ 𝒞 is fibred in groupoids then so is p_p.

By Stacks 04WG the functor p_p is fibred, and its fibres are groupoids (Comma.isGroupoid_fiber_pullbackProj), so this is Stacks 003V.

theorem isFiberedInGroupoids_pullbackProj (hp : p.IsFiberedInGroupoids)
    (hu : ∀ (J : Type) [SmallCategory J] [FinCategory J] [Nonempty J],
      Limits.PreservesLimitsOfShape J u) :
    (pullbackProj p u).IsFiberedInGroupoids

Tag 04WI, a lemma

Tag 04WI in the Stacks Project.

CategoryTheory.equivalenceIsFibredOneMorphismStrictPullbackPullbackLocalization, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/Functoriality/PullbackAdjunction.lean, line 1440.

The pullback of a fibred category along u is adjoint to the pushforward along u (Stacks 04WI). Let u : 𝒞 ⥤ 𝒟 be a functor, let p : 𝒮 ⥤ 𝒞 and q : 𝒯 ⥤ 𝒟 be fibred categories, assume 𝒞 has nonempty finite limits and that u commutes with nonempty finite limits. Then the morphism category Mor_{Fib/𝒞}(𝒮, u^p 𝒯) of 1-morphisms 𝒮 ⟶ u^p 𝒯 of fibred categories over 𝒞 is canonically equivalent to the morphism category Mor_{Fib/𝒟}(u_p 𝒮, 𝒯) of 1-morphisms u_p 𝒮 ⟶ 𝒯 of fibred categories over 𝒟, where u^p 𝒯 is the pushforward of 𝒯 along u (Stacks 04WB) and u_p 𝒮 is the pullback of 𝒮 along u (Stacks 04WG). Each morphism category is realized as the full subcategory of the category of based functors on those which preserve strongly cartesian morphisms, its morphisms being the morphisms of functors whose components lie over identities of the base.

noncomputable def equivalenceIsFibredOneMorphismStrictPullbackPullbackLocalization {𝒞 : Type u₁}
    [Category.{v₁} 𝒞] {𝒟 : Type u₂} [Category.{v₂} 𝒟] {𝒮 : Type u₃} [Category.{v₃} 𝒮] {𝒯 : Type u₄}
    [Category.{v₄} 𝒯] (u : 𝒞 ⥤ 𝒟) (p : 𝒮 ⥤ 𝒞) (q : 𝒯 ⥤ 𝒟) [p.IsFibered] [q.IsFibered]
    [HasNonemptyFiniteLimits 𝒞]
    (hu :
      ∀ (J : Type) [SmallCategory J] [FinCategory J] [Nonempty J],
        Limits.PreservesLimitsOfShape J u) :
    ObjectProperty.FullSubcategory
        (fun G :
            BasedCategory.ofFunctor p ⥤ᵇ
              BasedCategory.ofFunctor (StrictPullback.structureFunctor u q) =>
          Functor.IsFibredOneMorphism p (StrictPullback.structureFunctor u q) G.toFunctor) ≌
      ObjectProperty.FullSubcategory
        (fun G : BasedCategory.ofFunctor (Comma.pullbackProj p u) ⥤ᵇ BasedCategory.ofFunctor q =>
          Functor.IsFibredOneMorphism (Comma.pullbackProj p u) q G.toFunctor)

Tag 04WJ, a definition

Tag 04WJ in the Stacks Project.

CategoryTheory.Comma.pullbackStack, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/Functoriality/PullbackStack.lean, line 115.

The pullback f⁻¹𝒮 of the stack 𝒮 along the morphism of sites f (Stacks 04WJ), given as its structure functor over 𝒟.

f : 𝒟 ⟶ 𝒞 is the morphism of sites attached to the continuous functor u : 𝒞 ⥤ 𝒟 by Sites 00X6, 𝒮 is a stack over (𝒞, J), and f⁻¹𝒮 is the stackification over (𝒟, K) of the fibred category u_p 𝒮 = Comma.pullbackLocalization p u of Stacks 04WG. The stackification is supplied: q : 𝒳 ⥤ 𝒟 is a stack over (𝒟, K) and G : u_p 𝒮 ⥤ 𝒳 is a 1-morphism of fibred categories over 𝒟 satisfying the two clauses of Stacks 02ZN — local bijectivity of the induced maps of morphism presheaves, and local essential surjectivity on fibres. Relative to that data, f⁻¹𝒮 is q.

def pullbackStack (p : 𝒮 ⥤ 𝒞) (u : 𝒞 ⥤ 𝒟) [p.IsFibered] [HasFiniteLimits 𝒞]
    [PreservesFiniteLimits u] [u.IsContinuous J K] {𝒳 : Type u₄} [Category.{max u₂ u₃ vb v} 𝒳]
    {q : 𝒳 ⥤ 𝒟} [q.IsFibered] {G : pullbackLocalization p u ⥤ 𝒳}
    (_hs : p.IsStack J) (_hq : q.IsStack K)
    (hG : (pullbackProj p u).IsFibredOneMorphism q G)
    (_hmor : ∀ (V : 𝒟) (x y : (pullbackProj p u).Fiber V),
      Presheaf.IsLocallyInjective (K.over V) (hG.morPresheafMap x y) ∧
        Presheaf.IsLocallySurjective (K.over V) (hG.morPresheafMap x y))
    (_hobj : ∀ (V : 𝒟) (x' : q.Fiber V), ∃ R ∈ K V, ∀ ⦃W : 𝒟⦄ ⦃g : W ⟶ V⦄, R.arrows g →
      (Functor.fiberFunctorOfCompEq hG.comp_eq W).essImage (Functor.pullbackFiber q x' g)) :
    𝒳 ⥤ 𝒟

CategoryTheory.Comma.pullbackStackMap, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/Functoriality/PullbackStack.lean, line 131.

The canonical 1-morphism u_p 𝒮 ⥤ f⁻¹𝒮 (Stacks 04WJ), exhibiting the pullback of 𝒮 along f as the stackification of u_p 𝒮.

def pullbackStackMap (p : 𝒮 ⥤ 𝒞) (u : 𝒞 ⥤ 𝒟) [p.IsFibered] [HasFiniteLimits 𝒞]
    [PreservesFiniteLimits u] [u.IsContinuous J K] {𝒳 : Type u₄} [Category.{max u₂ u₃ vb v} 𝒳]
    {q : 𝒳 ⥤ 𝒟} [q.IsFibered] {G : pullbackLocalization p u ⥤ 𝒳}
    (_hs : p.IsStack J) (_hq : q.IsStack K)
    (hG : (pullbackProj p u).IsFibredOneMorphism q G)
    (_hmor : ∀ (V : 𝒟) (x y : (pullbackProj p u).Fiber V),
      Presheaf.IsLocallyInjective (K.over V) (hG.morPresheafMap x y) ∧
        Presheaf.IsLocallySurjective (K.over V) (hG.morPresheafMap x y))
    (_hobj : ∀ (V : 𝒟) (x' : q.Fiber V), ∃ R ∈ K V, ∀ ⦃W : 𝒟⦄ ⦃g : W ⟶ V⦄, R.arrows g →
      (Functor.fiberFunctorOfCompEq hG.comp_eq W).essImage (Functor.pullbackFiber q x' g)) :
    pullbackLocalization p u ⥤ 𝒳

Tag 04WK, a lemma

Tag 04WK in the Stacks Project.

CategoryTheory.Functor.equivalenceFibredMorStrictPullbackStackification, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/Functoriality/PullbackStackAdjunction.lean, line 194.

The pullback of a stack along f is adjoint to the pushforward along f (Stacks 04WK). Let f : 𝒟 ⟶ 𝒞 be the morphism of sites given by a functor u : 𝒞 ⥤ 𝒟 as in Sites 00X6, let p : 𝒮 ⥤ 𝒞 be a fibred category and let q : 𝒯 ⥤ 𝒟 be a stack. Let G : u_p 𝒮 ⥤ 𝒮' exhibit 𝒮' as the stackification of the pullback u_p 𝒮 of Stacks 04WG, in the sense of Stacks 02ZN, so that 𝒮' = f⁻¹𝒮 is the pullback of Stacks 04WJ. Then the morphism category Mor_{Stacks/𝒞}(𝒮, f_*𝒯) of 1-morphisms 𝒮 ⟶ f_*𝒯 over 𝒞 and their 2-morphisms is canonically equivalent to the morphism category Mor_{Stacks/𝒟}(f⁻¹𝒮, 𝒯), where f_*𝒯 = u^p 𝒯 is the pushforward of Stacks 04WB. The equivalence is the composite of Stacks 04WI, the same adjunction at the level of fibred categories, with Stacks 04W9, restriction along the stackification G.

This statement is conditional on being given a stackification G: its hypotheses are the unfolded clauses of Stacks 02ZN, which that construction supplies once it is assembled.

noncomputable def equivalenceFibredMorStrictPullbackStackification
    (hu : ∀ (J : Type) [SmallCategory J] [FinCategory J] [Nonempty J],
      Limits.PreservesLimitsOfShape J u)
    (hG : (Comma.pullbackProj p u).IsFibredOneMorphism p' G)
    (hmor : ∀ (V : 𝒟) (x y : (Comma.pullbackProj p u).Fiber V),
      Presheaf.IsLocallyInjective (K.over V) (hG.morPresheafMap x y) ∧
        Presheaf.IsLocallySurjective (K.over V) (hG.morPresheafMap x y))
    (hqmor : ∀ (V : 𝒟) (x y : q.Fiber V), IsMorSheaf q K V x y)
    (hobj : ∀ (V : 𝒟) (x' : p'.Fiber V), ∃ R ∈ K V, ∀ ⦃W : 𝒟⦄ ⦃f : W ⟶ V⦄, R.arrows f →
      (fiberFunctorOfCompEq hG.comp_eq W).essImage (pullbackFiber p' x' f))
    (hdesc : HasEffectiveDescent q K) :
    FibredMor p (StrictPullback.structureFunctor u q) ≌ FibredMor p' q

CategoryTheory.Functor.equivalenceFibredMorPushforwardPullbackStack, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/Functoriality/PullbackStackAdjunction.lean, line 240.

Stacks 04WK, written with the pushforward f_*𝒯 of Stacks 04WE and the pullback f⁻¹𝒮 of Stacks 04WJ. Let f : 𝒟 ⟶ 𝒞 be the morphism of sites attached by Sites 00X6 to a continuous functor u : 𝒞 ⥤ 𝒟 between a finitely complete (𝒞, J) and (𝒟, K) which is left exact, let 𝒮 be a stack over (𝒞, J) and let 𝒯 be a stack over (𝒟, K). Then

Mor_{Stacks/𝒞}(𝒮, f_*𝒯) ≃ Mor_{Stacks/𝒟}(f⁻¹𝒮, 𝒯).

The pullback f⁻¹𝒮 is represented by the supplied stackification of u_p 𝒮: the stack q : 𝒳 ⥤ 𝒟 and the 1-morphism G : u_p 𝒮 ⥤ 𝒳 satisfying the clauses hG, hmor, hobj of Stacks 02ZN. So this statement too is conditional on being given a stackification, which Stacks 02ZN supplies once assembled.

The instance [t.IsFibered] is implied by ht and is taken separately only because the notation f_*𝒯 of Stacks 04WE needs it to elaborate.

noncomputable def equivalenceFibredMorPushforwardPullbackStack
    (hs : p.IsStack J) (hq : q.IsStack K)
    (hG : (Comma.pullbackProj p u).IsFibredOneMorphism q G)
    (hmor : ∀ (V : 𝒟) (x y : (Comma.pullbackProj p u).Fiber V),
      Presheaf.IsLocallyInjective (K.over V) (hG.morPresheafMap x y) ∧
        Presheaf.IsLocallySurjective (K.over V) (hG.morPresheafMap x y))
    (hobj : ∀ (V : 𝒟) (x' : q.Fiber V), ∃ R ∈ K V, ∀ ⦃W : 𝒟⦄ ⦃g : W ⟶ V⦄, R.arrows g →
      (fiberFunctorOfCompEq hG.comp_eq W).essImage (pullbackFiber q x' g))
    (ht : t.IsStack K) :
    FibredMor p (pushforwardFibredCategory J K u t) ≌ FibredMor q t

Tag 04WR, a lemma

Tag 04WR in the Stacks Project.

CategoryTheory.pullback_stackification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/Functoriality/PullbackStackification/LocalEssSurj.lean, line 259.

Let f : 𝒟 ⟶ 𝒞 be the morphism of sites given by a continuous u : 𝒞 ⥤ 𝒟 satisfying the hypotheses of Sites 00X6, let p : 𝒮 ⥤ 𝒞 be a fibred category and let G : 𝒮 ⥤ 𝒮' be its stackification (clauses (1) and (2) of Stacks 02ZN, spelled out as hmor and hobj). Let G' : u_p 𝒮' ⥤ 𝒯 exhibit the stack q : 𝒯 ⥤ 𝒟 as the stackification of u_p 𝒮' — that is, let 𝒯 be f⁻¹𝒮' in the sense of Stacks 04WJ — and let H : u_p 𝒮 ⥤ 𝒯 be the canonical functor, pinned down by its restriction Q ⋙ H = Φ ⋙ Q' ⋙ G' along the localization functor. Then H exhibits 𝒯 as the stackification of u_p 𝒮: f⁻¹𝒮' is the stackification of u_p 𝒮.

theorem pullback_stackification
    [p.IsFibered] [p'.IsFibered] [HasNonemptyFiniteLimits 𝒞]
    (J : GrothendieckTopology 𝒞) (K : GrothendieckTopology 𝒟) [u.IsContinuous J K]
    (hu : ∀ (J' : Type) [SmallCategory J'] [FinCategory J'] [Nonempty J'],
      Limits.PreservesLimitsOfShape J' u)
    (hGG : p.IsFibredOneMorphism p' G)
    (hmor : ∀ (U : 𝒞) (x y : p.Fiber U),
      Presheaf.IsLocallyInjective (J.over U) (hGG.morPresheafMap x y) ∧
        Presheaf.IsLocallySurjective (J.over U) (hGG.morPresheafMap x y))
    (hobj : ∀ (U : 𝒞) (x' : p'.Fiber U), ∃ R ∈ J U, ∀ ⦃U₁ : 𝒞⦄ ⦃d : U₁ ⟶ U⦄, R.arrows d →
      (Functor.fiberFunctorOfCompEq hGG.comp_eq U₁).essImage (Functor.pullbackFiber p' x' d))
    {q : 𝒯 ⥤ 𝒟} (hq : q.IsStack K)
    {G' : Comma.pullbackLocalization p' u ⥤ 𝒯}
    (hG' : haveI : (Comma.pullbackProj p' u).IsFibered := Comma.isFibered_pullbackProj p' u hu
      (Comma.pullbackProj p' u).IsFibredOneMorphism q G')
    (hmor' : haveI : (Comma.pullbackProj p' u).IsFibered := Comma.isFibered_pullbackProj p' u hu
      haveI : q.IsFibered := hq.isFibered
      ∀ (V : 𝒟) (x y : (Comma.pullbackProj p' u).Fiber V),
        Presheaf.IsLocallyInjective (K.over V) (hG'.morPresheafMap x y) ∧
          Presheaf.IsLocallySurjective (K.over V) (hG'.morPresheafMap x y))
    (hobj' : haveI : q.IsFibered := hq.isFibered
      ∀ (V : 𝒟) (z : q.Fiber V), ∃ T ∈ K V, ∀ ⦃V₁ : 𝒟⦄ ⦃β : V₁ ⟶ V⦄, T.arrows β →
        (Functor.fiberFunctorOfCompEq hG'.comp_eq V₁).essImage (Functor.pullbackFiber q z β))
    (H : Comma.pullbackLocalization p u ⥤ 𝒯)
    (hH : (Comma.idBaseStronglyCartesian p u).Q ⋙ H =
      commaMapOver u hGG.comp_eq ⋙ (Comma.idBaseStronglyCartesian p' u).Q ⋙ G') :
    haveI : (Comma.pullbackProj p u).IsFibered := Comma.isFibered_pullbackProj p u hu
    haveI : q.IsFibered := hq.isFibered
    ∃ hH' : (Comma.pullbackProj p u).IsFibredOneMorphism q H,
      (∀ (V : 𝒟) (x y : (Comma.pullbackProj p u).Fiber V),
          Presheaf.IsLocallyInjective (K.over V) (hH'.morPresheafMap x y) ∧
            Presheaf.IsLocallySurjective (K.over V) (hH'.morPresheafMap x y)) ∧
        ∀ (V : 𝒟) (z : q.Fiber V), ∃ T ∈ K V, ∀ ⦃V₁ : 𝒟⦄ ⦃β : V₁ ⟶ V⦄, T.arrows β →
          (Functor.fiberFunctorOfCompEq hH'.comp_eq V₁).essImage
            (Functor.pullbackFiber q z β)

Tag 04WS, a lemma

Tag 04WS in the Stacks Project.

CategoryTheory.Comma.equivalenceOverPullbackStackCan, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/Functoriality/PullbackStackEquivalence.lean, line 1092. The attribute's comment: “(1)”.

Stacks 04WS (1), as data. Let u : 𝒞 ⥤ 𝒟 satisfy the assumptions of Sites 00XU — continuous, cocontinuous, fully faithful, 𝒞 finitely complete and u left exact — and let f : 𝒟 ⟶ 𝒞 be the associated morphism of sites. Let 𝒮 be a stack over (𝒞, J) and let G : u_p 𝒮 ⥤ f⁻¹𝒮 exhibit f⁻¹𝒮 as the stackification of u_p 𝒮 over (𝒟, K) in the sense of Stacks 02ZN. Then the canonical functor 𝒮 ⟶ f_*f⁻¹𝒮 is an equivalence of stacks over 𝒞: a quasi-inverse strictly over 𝒞, together with vertical unit and counit isomorphisms.

By Stacks 046N it suffices that the canonical functor be fully faithful and that every object of a fibre of f_*f⁻¹𝒮 be locally in its essential image on fibres, which are CategoryTheory.Comma.fullyFaithful_pullbackStackCan and CategoryTheory.Comma.locallyEssSurjOnFibers_pullbackStackCan.

The statement is conditional on being given a stackification, which Stacks 02ZN supplies once assembled.

noncomputable def equivalenceOverPullbackStackCan
    (hobj : ∀ (V : 𝒟) (x' : q.Fiber V), ∃ R ∈ K V, ∀ ⦃W : 𝒟⦄ ⦃g : W ⟶ V⦄, R.arrows g →
      (Functor.fiberFunctorOfCompEq hG.comp_eq W).essImage (Functor.pullbackFiber q x' g)) :
    Functor.IsEquivalenceOver p (StrictPullback.structureFunctor u q)
      (pullbackStackCan p u hG)

CategoryTheory.Comma.equivalenceFibredMorPullbackStack, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/Functoriality/PullbackStackEquivalence.lean, line 1172. The attribute's comment: “(2)”.

Stacks 04WS (2), for the pullbacks given by supplied stackifications. Let u : 𝒞 ⥤ 𝒟 satisfy the assumptions of Sites 00XU and let f : 𝒟 ⟶ 𝒞 be the associated morphism of sites. For stacks 𝒮 and 𝒮₂ over (𝒞, J) with pullbacks f⁻¹𝒮 and f⁻¹𝒮₂ given by supplied stackifications of u_p 𝒮 and u_p 𝒮₂ (Stacks 04WJ), the morphism categories

Mor_{Stacks/𝒞}(𝒮, 𝒮₂) and Mor_{Stacks/𝒟}(f⁻¹𝒮, f⁻¹𝒮₂)

are canonically equivalent. The equivalence is the composite of post-composition with the canonical equivalence 𝒮₂ ⟶ f_*f⁻¹𝒮₂ of clause (1) with the adjunction of Stacks 04WK at 𝒯 = f⁻¹𝒮₂; the direction f⁻¹ is its quasi-inverse.

Both clauses are conditional on being given stackifications, which Stacks 02ZN supplies once assembled.

noncomputable def equivalenceFibredMorPullbackStack :
    Functor.FibredMor p p₂ ≌
      Functor.FibredMor q q₂

Sources

LeanCategoryTheory.StrictPullback.isFibered_structureFunctor · CategoryTheory.StrictPullback.isStack_structureFunctor · CategoryTheory.StrictPullback.isStack_isFiberedInGroupoids_structureFunctor · CategoryTheory.pushforwardFibredCategory · CategoryTheory.Comma.hasRightCalculusOfFractions_stronglyCartesianOver · CategoryTheory.Comma.pullbackLocalization · CategoryTheory.Comma.pullbackProj · CategoryTheory.Comma.isFibered_pullbackProj

Section8.13 Stacks and localization #

Section 8.13 of the Stacks Project, Tag 04WT. 2 tags here are carried by 6 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 04WU, a lemma

Tag 04WU in the Stacks Project.

CategoryTheory.Over.isStack_forget_iff_isSheaf, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Stack/OverIsStack.lean, line 312.

Let (𝒞, J) be a site and let U be an object of 𝒞. The localization j_U : 𝒞/U ⥤ 𝒞 is a stack over 𝒞 if and only if the representable presheaf h_U is a sheaf.

theorem isStack_forget_iff_isSheaf (J : GrothendieckTopology 𝒞) :
    (Over.forget U).IsStack J ↔ Presheaf.IsSheaf J (yoneda.obj U)

Tag 04WV, a lemma

Tag 04WV in the Stacks Project.

CategoryTheory.Functor.isStack_comp_forget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/StacksAndLocalization.lean, line 246.

Construction A for stacks. Let U be an object of 𝒞 whose representable presheaf h_U is a sheaf, and let p : 𝒮 ⥤ 𝒞/U be a stack over the site (𝒞/U, J.over U). Then j_! p = p ⋙ j_U : 𝒮 ⥤ 𝒞 is a stack over (𝒞, J).

theorem isStack_comp_forget (p : 𝒳 ⥤ Over U) {J : GrothendieckTopology 𝒞}
    (hU : Presheaf.IsSheaf J (yoneda.obj U)) (hp : p.IsStack (J.over U)) :
    (p ⋙ Over.forget U).IsStack J

CategoryTheory.Over.stackConstructionHomEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/StacksAndLocalization.lean, line 589.

Construction A is bijective on 1-morphisms, and is the identity on the underlying functor.

def stackConstructionHomEquiv
    (𝒮 𝒮' : BasedStack.{v₁, v₁, max u₁ v₁, max u₁ v₁} (Over U) (J.over U)) :
    (𝒮 ⟶ 𝒮') ≃
      StackPairHom U J hU (stackConstructionA U J hU 𝒮) (stackConstructionA U J hU 𝒮')

CategoryTheory.Over.stackConstructionHom₂Equiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/StacksAndLocalization.lean, line 629.

Construction A is bijective on 2-morphisms, and is the identity on the underlying morphism of functors.

def stackConstructionHom₂Equiv
    {𝒮 𝒮' : BasedStack.{v₁, v₁, max u₁ v₁, max u₁ v₁} (Over U) (J.over U)} (f g : 𝒮 ⟶ 𝒮') :
    (f ⟶ g) ≃ StackPairHom₂ U J hU (stackConstructionHomEquiv U J hU 𝒮 𝒮' f)
      (stackConstructionHomEquiv U J hU 𝒮 𝒮' g)

CategoryTheory.Over.isStack_of_comp_forget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/StacksOverSlice.lean, line 305.

Construction B of Stacks 04WV, at the level of stacks. Let U be an object of 𝒞 whose representable presheaf h_U is a sheaf, and let p : 𝒮 ⥤ 𝒞/U be a functor whose composite with the localization functor j_U is a stack over (𝒞, J). Then p itself is a stack over the site (𝒞/U, J.over U). This is the source's "in this case it is automatically the case that p : 𝒯 → 𝒞/U is a stack over 𝒞/U".

The proof is by reduction to three results rather than by a clause-by-clause verification:

the pushforward j_U^q 𝒮 of q = p ⋙ j_U along j_U is a stack over (𝒞/U, J.over U), by Stacks 04WC (CategoryTheory.StrictPullback.isStack_structureFunctor), j_U being a continuous functor of sites;

the full subcategory of j_U^q 𝒮 cut out by CategoryTheory.Over.LiesOverSlice is a stack, by Stacks 04TU (CategoryTheory.Functor.IsStack.fullSubcategory); this is the only place the hypothesis that h_U is a sheaf is used, in CategoryTheory.Over.locallyClosed_liesOverSlice;

𝒮 is isomorphic to that full subcategory as a category over 𝒞/U, so it is a stack by Stacks 042W (CategoryTheory.BasedCategory.Equivalence.isStack).

Two costs of this route, both stated here rather than hidden.

It carries the hypothesis [HasPullbacks 𝒞], which Stacks 04WV does not. It is inherited from Stacks 04WC, whose proof genuinely uses fibre products in the source site (CategoryTheory.StrictPullback.glue); the source's notion of a morphism of sites (Stacks 00WU) asks for them, and Mathlib's Functor.IsContinuous does not. So this is Construction B for a site with fibre products, which is a mild weakening of 04WV.

The universes are not pinned, and the earlier note here saying they were is superseded. The pushforward lives in Type (max u₁ v₁ u₂) with morphisms in max v₁ v₂, and 𝒮 used to be given there so that it and the full subcategory of the pushforward coincide; but the transport of the stack condition does not need that, because CategoryTheory.BasedCategory.Equivalence and Stacks 042W relate two categories over 𝒞 in independent object and morphism universes (CategoryTheory.BasedCategory.isStack_iff_of_equivalence), and CategoryTheory.Over.toSliceFullSub and CategoryTheory.Over.fromSliceFullSub are already stated at the file's general {𝒮 : Type u₂} [Category.{v₂} 𝒮]. So the statement below is given at that generality. The previously pinned case is recompiled as an instance of it, at the two universe settings where it is used: CategoryTheory.Over.isStack_map_iff and CategoryTheory.Over.isStack_of_comp_forget_slice keep their own statements unchanged and only their explicit universe applications of this result move.

theorem isStack_of_comp_forget [HasPullbacks 𝒞] {𝒮 : Type u₂} [Category.{v₂} 𝒮]
    (p : 𝒮 ⥤ Over U) {J : GrothendieckTopology 𝒞}
    (hU : Presheaf.IsSheaf J (yoneda.obj U)) (hq : (p ⋙ Over.forget U).IsStack J) :
    p.IsStack (J.over U)

CategoryTheory.Over.stackConstructionObjEquiv, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/CategoryTheory/Sites/Localization/StacksOverSlice.lean, line 425.

Constructions A and B of Stacks 04WV are mutually inverse on objects. A pair (𝒯, p) carries no information beyond p, because "p is a 1-morphism of categories over 𝒞" says exactly that the structure functor of 𝒯 is p ⋙ j_U; and the two stack conditions agree, by CategoryTheory.Functor.isStack_comp_forget in one direction and CategoryTheory.Over.isStack_of_comp_forget in the other.

Together with CategoryTheory.Over.stackConstructionHomEquiv and CategoryTheory.Over.stackConstructionHom₂Equiv, which are bijections on 1-morphisms and on 2-morphisms compatible with identities, composition and whiskering, this exhibits Constructions A and B as mutually inverse functors of the two 2-categories.

def stackConstructionObjEquiv :
    BasedStack.{v₁, v₁, max u₁ v₁, max u₁ v₁} (Over U) (J.over U) ≃ StackPair U J hU

Sources

LeanCategoryTheory.Over.isStack_forget_iff_isSheaf · CategoryTheory.Functor.isStack_comp_forget · CategoryTheory.Over.stackConstructionHomEquiv · CategoryTheory.Over.stackConstructionHom₂Equiv · CategoryTheory.Over.isStack_of_comp_forget · CategoryTheory.Over.stackConstructionObjEquiv

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

8 Stacks

Section8.2 Presheaves of morphisms associated to fibred categories#

Tag 026A, a lemma

Tag 02ZB, a definition

Tag 042V, a lemma

Tag 02ZA, a remark

Tag 04SI, a lemma

Sources

Section8.3 Descent data in fibred categories#

Tag 026B, a definition

Tag 026C, remarks

Tag 02ZD, a lemma

Tag 02ZE, a definition

Tag 026E, a definition

Tag 026D, a lemma

Tag 0GEA, a lemma

Sources

Section8.4 Stacks#

Tag 026F, a definition

Tag 02ZF, a lemma

Tag 04TU, a lemma

Tag 042W, a lemma

Tag 02ZG, a definition

Tag 026G, a lemma

Tag 04WQ, a lemma

Tag 046N, a lemma

Tag 03ZZ, a remark

Sources

Section8.5 Stacks in groupoids#

Tag 02ZI, a definition

Tag 02ZJ, a lemma

Tag 03YI, a lemma

Tag 042X, a lemma

Tag 02ZK, a definition

Tag 02ZL, a lemma

Sources

Section8.6 Stacks in setoids#

Tag 042Z, a definition

Tag 0430, a lemma

Tag 0432, a lemma

Tag 0431, a lemma

Tag 0433, a definition

Tag 0434, a lemma

Tag 05UI, a lemma

Tag 05UJ, a lemma

Tag 06DV, a lemma

Tag 05W9, a lemma

Tag 0CKJ, a lemma

Sources

Section8.7 The inertia stack#

Tag 036Y, a lemma

Tag 04ZM, a lemma

Sources

Section8.8 Stackification of fibred categories#

Tag 02ZN, a lemma

Tag 0435, a lemma

Tag 04W9, a lemma

Tag 04Y1, a lemma

Tag 06NS, a lemma

Sources

Section8.9 Stackification of categories fibred in groupoids#

Tag 02ZP, a lemma

Tag 0436, a lemma

Tag 04Y2, a lemma

Sources

Section8.10 Inherited topologies#

Tag 06NU, a lemma

Tag 06NV, a definition

Tag 06NW, a lemma

Tag 0CN0, a lemma

Tag 06NX, a lemma

Tag 09WX, a lemma

Sources

Section8.11 Gerbes#

Tag 06NZ, a definition

Tag 06P0, a lemma

Tag 06P1, a lemma

Tag 06P2, a definition

Tag 06P3, a lemma

Tag 06R3, a lemma

Section8.2 Presheaves of morphisms associated to fibred categories #

Section8.3 Descent data in fibred categories #

Section8.4 Stacks #

Section8.5 Stacks in groupoids #

Section8.6 Stacks in setoids #

Section8.7 The inertia stack #

Section8.8 Stackification of fibred categories #

Section8.9 Stackification of categories fibred in groupoids #

Section8.10 Inherited topologies #

Section8.11 Gerbes #

Section8.12 Functoriality for stacks #

Section8.13 Stacks and localization #