Morphisms and representable fibers of stacks in groupoids

Stack morphisms, their fiber categories, and representability by an object of an arbitrary site are generic category theory. Geometric properties of the representing morphism remain in the corresponding geometric consumer layer.

@[reducible, inline]

abbrev CategoryTheory.StackMorphism {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (F G : StackInGroupoids C J) : Type (max (max u v) u_1)

A morphism of stacks is a strong transformation between their underlying pseudofunctors. Pullback naturality, identities, and composition are supplied by Mathlib's pseudofunctor API.

Equations

• CategoryTheory.StackMorphism F G = F.presheaf.StrongTrans G.presheaf

@[reducible, inline]

abbrev CategoryTheory.StackMorphism.app {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {F G : StackInGroupoids C J} (f : StackMorphism F G) (S : C) : Functor ↑(F.presheaf.obj { as := Opposite.op S }) ↑(G.presheaf.obj { as := Opposite.op S })

The functor induced by a stack morphism on the fiber over S.

Equations

• f.app S = (f.app { as := Opposite.op S }).toFunctor

@[reducible, inline]

abbrev CategoryTheory.StackMorphism.pullbackIso {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {F G : StackInGroupoids C J} (f : StackMorphism F G) {S T : C} (g : T ⟶ S) : (F.presheaf.map g.op.toLoc).toFunctor.comp (f.app T) ≅ (f.app S).comp (G.presheaf.map g.op.toLoc).toFunctor

The pseudonatural pullback comparison of a stack morphism along a site morphism.

Equations

• f.pullbackIso g = CategoryTheory.Cat.Hom.toNatIso (f.naturality g.op.toLoc)

@[reducible, inline]

abbrev CategoryTheory.StackMorphism.id {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (F : StackInGroupoids C J) : StackMorphism F F

The identity stack morphism, including its pseudonaturality coherence.

Equations

• CategoryTheory.StackMorphism.id F = CategoryTheory.Pseudofunctor.StrongTrans.id F.presheaf

@[reducible, inline]

abbrev CategoryTheory.StackMorphism.comp {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {F G H : StackInGroupoids C J} (f : StackMorphism F G) (g : StackMorphism G H) : StackMorphism F H

Composition of stack morphisms.

Equations

• f.comp g = CategoryTheory.Pseudofunctor.StrongTrans.vcomp f g

@[reducible, inline]

abbrev CategoryTheory.StackMorphism.Modification {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {F G : StackInGroupoids C J} (f g : StackMorphism F G) : Type (max u u_1)

A 2-morphism between stack morphisms is a modification.

Equations

• f.Modification g = CategoryTheory.Pseudofunctor.StrongTrans.Modification f g

@[reducible, inline]

abbrev CategoryTheory.StackMorphism.FiberCategory {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {F G : StackInGroupoids C J} (f : StackMorphism F G) {S : C} (y : ↑(G.presheaf.obj { as := Opposite.op S })) (T : Over S) : Type u_1

The groupoid fiber of a stack morphism over a test object and a chosen target object.

Equations

• f.FiberCategory y T = CategoryTheory.Core (CategoryTheory.StructuredArrow ((G.presheaf.map T.hom.op.toLoc).toFunctor.obj y) (f.app T.left))

structure CategoryTheory.StackMorphism.FiberRepresentation {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {F G : StackInGroupoids C J} (f : StackMorphism F G) {S : C} (y : ↑(G.presheaf.obj { as := Opposite.op S })) : Type (max (max u u_1) v)

An object of the site representing one fiber of a stack morphism.

• representing : Over S

  The representing object over S.

• fiberEquivalence (T : Over S) : Discrete (T ⟶ self.representing) ≌ f.FiberCategory y T

  The Yoneda comparison on every test object over S.

class CategoryTheory.StackMorphism.IsRepresentable {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {F G : StackInGroupoids C J} (f : StackMorphism F G) : Prop

A stack morphism is representable when every fiber over a test object has a representing object of the site.

• representation {S : C} (y : ↑(G.presheaf.obj { as := Opposite.op S })) : Nonempty (f.FiberRepresentation y)