Stacks in groupoids

This file packages Mathlib's stack condition together with the additional groupoid-valued requirement used in algebraic geometry. Covers and Čech descent are the existing Sieve, Presieve, and Pseudofunctor.DescentData objects: this layer does not replace them with parallel definitions.

The construction is owned by CategoryTheory/Sites: it is generic in a category and a Grothendieck topology and imports no algebraic geometry. The declarations use the matching CategoryTheory namespace.

StackInGroupoids deliberately contains no algebraicity, representability, boundedness, or finiteness assertion. The only conditions are groupoid-valued fibers and effective descent for a chosen Grothendieck topology.

structure CategoryTheory.StackInGroupoids (C : Type u) [Category.{v, u} C] (J : GrothendieckTopology C) : Type (max (max u v) (w + 1))

A groupoid-valued pseudofunctor satisfying effective descent for J.

• presheaf : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat

  The contravariant groupoid-valued pseudofunctor.

• fiberIsGroupoid (X : LocallyDiscrete Cᵒᵖ) : IsGroupoid ↑(self.presheaf.obj X)

  Every fiber is a groupoid.

• isStack : self.presheaf.IsStack J

  Objects and morphisms satisfy effective descent for J.

instance CategoryTheory.StackInGroupoids.presheaf_obj_isGroupoid {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (F : StackInGroupoids C J) (X : LocallyDiscrete Cᵒᵖ) : IsGroupoid ↑(F.presheaf.obj X)

instance CategoryTheory.StackInGroupoids.presheaf_isStack {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (F : StackInGroupoids C J) : F.presheaf.IsStack J

structure CategoryTheory.StackInGroupoids.Cover {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (S : C) : Type (max (max (t + 1) u) v)

An explicitly indexed covering family for a Grothendieck topology.

• index : Type t

  The indexing type of the covering family.

• obj : self.index → C

  Schemes or site objects in the covering family.

• hom (i : self.index) : self.obj i ⟶ S

  The covering arrows.

• mem : Sieve.ofArrows self.obj self.hom ∈ J S

  The arrows generate a covering sieve.

@[reducible, inline]

abbrev CategoryTheory.StackInGroupoids.CechDescent {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (F : StackInGroupoids C J) {S : C} (U : Cover S) : Type (max (max (max (max u_2 u) u_1) v) u_1)

The category of Čech descent data for a covering family.

Equations

• F.CechDescent U = F.presheaf.DescentData U.hom

@[reducible, inline]

abbrev CategoryTheory.StackInGroupoids.toCechDescent {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (F : StackInGroupoids C J) {S : C} (U : Cover S) : Functor (↑(F.presheaf.obj { as := Opposite.op S })) (F.presheaf.DescentData U.hom)

Restrict an object and its morphisms to Čech descent data.

Equations

• F.toCechDescent U = F.presheaf.toDescentData U.hom

noncomputable def CategoryTheory.StackInGroupoids.cechDescentEquivalence {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (F : StackInGroupoids C J) {S : C} (U : Cover S) : ↑(F.presheaf.obj { as := Opposite.op S }) ≌ F.CechDescent U

The stack condition identifies a fiber with the category of Čech descent data for every covering family.

Equations

• F.cechDescentEquivalence U = (F.toCechDescent U).asEquivalence

noncomputable def CategoryTheory.StackInGroupoids.fullyFaithfulToCechDescent {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (F : StackInGroupoids C J) {S : C} (U : Cover S) : (F.toCechDescent U).FullyFaithful

Morphisms satisfy descent: restriction to a cover is fully faithful.

Equations

• F.fullyFaithfulToCechDescent U = F.presheaf.fullyFaithfulToDescentData U.hom ⋯

theorem CategoryTheory.StackInGroupoids.essSurjToCechDescent {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (F : StackInGroupoids C J) {S : C} (U : Cover S) : (F.toCechDescent U).EssSurj

Objects satisfy effective descent: every Čech descent object comes from an object over the base, up to isomorphism.

Refining the Grothendieck topology

Effective descent is antitone in the topology, and only in that direction. Every J₁-covering sieve is a J₂-covering sieve when J₁ ≤ J₂, so a stack for the finer topology is a stack for the coarser one. The converse is false and nothing below asserts it: descent for a coarse topology says nothing about the covers the finer topology adds. A consumer that needs the finer level has to prove it there.

theorem CategoryTheory.Pseudofunctor.IsStack.of_le {C : Type u} [Category.{v, u} C] {F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} {J₁ J₂ : GrothendieckTopology C} (h : J₁ ≤ J₂) [F.IsStack J₂] : F.IsStack J₁

Effective descent for a finer topology gives effective descent for every coarser topology. This is the only implication between the two conditions; there is no reverse transport.

def CategoryTheory.StackInGroupoids.ofLE {C : Type u} [Category.{v, u} C] {J₁ J₂ : GrothendieckTopology C} (h : J₁ ≤ J₂) (F : StackInGroupoids C J₂) : StackInGroupoids C J₁

Restrict a stack in groupoids along J₁ ≤ J₂ to the coarser topology. The pseudofunctor and its fibers are untouched; only the descent condition is weakened, so this loses information and cannot be inverted.

Equations

• CategoryTheory.StackInGroupoids.ofLE h F = { presheaf := F.presheaf, fiberIsGroupoid := ⋯, isStack := ⋯ }

@[simp]

theorem CategoryTheory.StackInGroupoids.ofLE_presheaf {C : Type u} [Category.{v, u} C] {J₁ J₂ : GrothendieckTopology C} (h : J₁ ≤ J₂) (F : StackInGroupoids C J₂) : (ofLE h F).presheaf = F.presheaf

def CategoryTheory.StackInGroupoids.Cover.ofLE {C : Type u} [Category.{v, u} C] {J₁ J₂ : GrothendieckTopology C} (h : J₁ ≤ J₂) {S : C} (U : Cover S) : Cover S

A covering family for a coarser topology is a covering family for a finer one, with the same index type and the same arrows.

Equations

• CategoryTheory.StackInGroupoids.Cover.ofLE h U = { index := U.index, obj := U.obj, hom := U.hom, mem := ⋯ }

@[simp]

theorem CategoryTheory.StackInGroupoids.Cover.ofLE_hom {C : Type u} [Category.{v, u} C] {J₁ J₂ : GrothendieckTopology C} (h : J₁ ≤ J₂) {S : C} (U : Cover S) (i : U.index) : (ofLE h U).hom i = U.hom i

@[simp]

theorem CategoryTheory.StackInGroupoids.Cover.ofLE_obj {C : Type u} [Category.{v, u} C] {J₁ J₂ : GrothendieckTopology C} (h : J₁ ≤ J₂) {S : C} (U : Cover S) (a✝ : U.index) : (ofLE h U).obj a✝ = U.obj a✝

@[simp]

theorem CategoryTheory.StackInGroupoids.Cover.ofLE_index {C : Type u} [Category.{v, u} C] {J₁ J₂ : GrothendieckTopology C} (h : J₁ ≤ J₂) {S : C} (U : Cover S) : (ofLE h U).index = U.index

Transport of the stack condition

structure CategoryTheory.StackEquivalence {C : Type u} [Category.{v, u} C] (F G : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) : Type (max (max u v) w)

Descent-compatible equivalence data between two pseudofunctors.

Mathlib currently has the pseudofunctor and descent-data APIs but no general pseudonatural-equivalence API. This structure records exactly the two equivalences and comparison square needed to transport the stack condition; it does not hide them behind an unproved equivalence principle.

• fiber (S : C) : ↑(F.obj { as := Opposite.op S }) ≌ ↑(G.obj { as := Opposite.op S })

  Equivalence on each fiber.

• descent {S : C} (R : Sieve S) : (F.DescentData fun (f : R.arrows.category) => f.obj.hom) ≌ G.DescentData fun (f : R.arrows.category) => f.obj.hom

  Equivalence on descent data for every sieve.

• comparison {S : C} (R : Sieve S) : (F.toDescentData fun (f : R.arrows.category) => f.obj.hom).comp (self.descent R).functor ≅ (self.fiber S).functor.comp (G.toDescentData fun (f : R.arrows.category) => f.obj.hom)

  Restriction to descent data commutes with the two equivalences.

theorem CategoryTheory.StackEquivalence.isStack_iff {C : Type u} [Category.{v, u} C] {F G : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat} (e : StackEquivalence F G) (J : GrothendieckTopology C) : F.IsStack J ↔ G.IsStack J

The stack condition is invariant under descent-compatible equivalence.

def CategoryTheory.StackInGroupoids.ofEquivalence {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (F : StackInGroupoids C J) (G : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat) (e : StackEquivalence F.presheaf G) (hG : ∀ (X : LocallyDiscrete Cᵒᵖ), IsGroupoid ↑(G.obj X)) : StackInGroupoids C J

Transport a stack in groupoids across descent-compatible equivalence. The groupoid condition on the target fibers remains explicit.

Equations

• F.ofEquivalence G e hG = { presheaf := G, fiberIsGroupoid := hG, isStack := ⋯ }