Documentation

DerivedAlgGeo.CategoryTheory.Sites.Descent

Descent and stacks #

Extensions of Mathlib's CategoryTheory/Sites/Descent/, where IsStack is defined: stacks in groupoids, discrete stacks from sheaves, stack morphisms, and site-object representability. StackInGroupoids.lean declares the structure and does not re-export its directory, so this umbrella imports the children directly.