feat(CategoryTheory): define descent data by presieves

Mathlib.lean

@@ -2778,6 +2778,8 @@ import Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
 import Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
 import Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
 import Mathlib.CategoryTheory.Square
+import Mathlib.CategoryTheory.Stack.Basic
+import Mathlib.CategoryTheory.Stack.Descent
 import Mathlib.CategoryTheory.Subobject.ArtinianObject
 import Mathlib.CategoryTheory.Subobject.Basic
 import Mathlib.CategoryTheory.Subobject.Comma

Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean

@@ -155,7 +155,37 @@ def comp (F : Pseudofunctor B C) (G : Pseudofunctor C D) : Pseudofunctor B D whe
 
 section
 
-variable (F : Pseudofunctor B C) {a b : B}
+variable (F : Pseudofunctor B C) {a b c d : B}
+
+@[reassoc, to_app]
+lemma map₂_associator_inv (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :
+    F.map₂ (α_ f g h).inv =
+    (F.mapComp f (g ≫ h)).hom ≫ F.map f ◁ (F.mapComp g h).hom ≫
+    (α_ (F.map f) (F.map g) (F.map h)).inv ≫
+    (F.mapComp f g).inv ▷ F.map h ≫ (F.mapComp (f ≫ g) h).inv := by
+  apply eq_of_inv_eq_inv
+  simp only [IsIso.inv_comp, IsIso.Iso.inv_inv, inv_whiskerRight, assoc, inv_whiskerLeft,
+    IsIso.Iso.inv_hom]
+  rw [← F.map₂_inv]
+  simp
+
+@[reassoc, to_app]
+lemma map₂_left_unitor_inv (f : a ⟶ b) :
+    F.map₂ (λ_ f).inv =
+    (λ_ (F.map f)).inv ≫ (F.mapId a).inv ▷ F.map f ≫ (F.mapComp (𝟙 a) f).inv := by
+  apply eq_of_inv_eq_inv
+  simp only [IsIso.inv_comp, IsIso.Iso.inv_inv, inv_whiskerRight, assoc]
+  rw [← F.map₂_inv]
+  simp
+
+@[reassoc, to_app]
+lemma map₂_right_unitor_inv (f : a ⟶ b) :
+    F.map₂ (ρ_ f).inv =
+    (ρ_ (F.map f)).inv ≫ F.map f ◁ (F.mapId b).inv ≫ (F.mapComp f (𝟙 b)).inv := by
+  apply eq_of_inv_eq_inv
+  simp only [IsIso.inv_comp, IsIso.Iso.inv_inv, inv_whiskerLeft, assoc]
+  rw [← F.map₂_inv]
+  simp
 
 @[reassoc, to_app]
 lemma mapComp_assoc_right_hom {c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :
@@ -185,6 +215,34 @@ lemma mapComp_assoc_left_inv {c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d)
     (F.mapComp f (g ≫ h)).inv ≫ F.map₂ (α_ f g h).inv :=
   F.toLax.mapComp_assoc_left _ _ _
 
+@[reassoc, to_app]
+lemma mapComp_comp_left (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :
+    (F.mapComp (f ≫ g) h).hom = F.map₂ (α_ f g h).hom ≫
+      (F.mapComp f (g ≫ h)).hom ≫ F.map f ◁ (F.mapComp g h).hom ≫
+        (α_ (F.map f) (F.map g) (F.map h)).inv ≫ (F.mapComp f g).inv ▷ F.map h := by
+  simp [map₂_associator]
+
+@[reassoc, to_app]
+lemma mapComp_comp_left_inv (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :
+    (F.mapComp (f ≫ g) h).inv = (F.mapComp f g).hom ▷ F.map h ≫
+      (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F.mapComp g h).inv ≫
+        (F.mapComp f (g ≫ h)).inv ≫ F.map₂ (α_ f g h).inv := by
+  simp [map₂_associator_inv]
+
+@[reassoc, to_app]
+lemma mapComp_comp_right (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :
+    (F.mapComp f (g ≫ h)).hom = F.map₂ (α_ f g h).inv ≫
+      (F.mapComp (f ≫ g) h).hom ≫ (F.mapComp f g).hom ▷ F.map h ≫
+        (α_ (F.map f) (F.map g) (F.map h)).hom ≫ F.map f ◁ (F.mapComp g h).inv := by
+  simp [map₂_associator_inv]
+
+@[reassoc, to_app]
+lemma mapComp_comp_right_inv (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :
+    (F.mapComp f (g ≫ h)).inv = F.map f ◁ (F.mapComp g h).hom ≫
+      (α_ (F.map f) (F.map g) (F.map h)).inv ≫ (F.mapComp f g).inv ▷ F.map h ≫
+        (F.mapComp (f ≫ g) h).inv ≫ F.map₂ (α_ f g h).hom := by
+  simp [map₂_associator]
+
 @[reassoc, to_app]
 lemma mapComp_id_left_hom (f : a ⟶ b) : (F.mapComp (𝟙 a) f).hom =
     F.map₂ (λ_ f).hom ≫ (λ_ (F.map f)).inv ≫ (F.mapId a).inv ▷ F.map f := by
@@ -241,6 +299,20 @@ lemma whiskerLeft_mapId_inv (f : a ⟶ b) : F.map f ◁ (F.mapId b).inv =
     (ρ_ (F.map f)).hom ≫ F.map₂ (ρ_ f).inv ≫ (F.mapComp f (𝟙 b)).hom := by
   simpa using congrArg (·.inv) (F.whiskerLeftIso_mapId f)
 
+theorem mapComp_eq_left {a b c : B} {f f' : a ⟶ b} (η : f = f') (g : b ⟶ c) :
+    F.mapComp f g = eqToIso (by rw [η]) ≪≫ F.mapComp f' g ≪≫ eqToIso (by rw [η]) := by
+  ext
+  dsimp only [trans_hom, eqToIso.hom]
+  rw [eqToHom_iso_hom_naturality (fun i ↦ F.mapComp i g) η.symm]
+  simp only [eqToHom_trans_assoc, eqToHom_refl, id_comp]
+
+theorem mapComp_eq_right {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g = g') :
+    F.mapComp f g = eqToIso (by rw [η]) ≪≫ F.mapComp f g' ≪≫ eqToIso (by rw [η]) := by
+  ext
+  dsimp only [trans_hom, eqToIso.hom]
+  rw [eqToHom_iso_hom_naturality (fun i ↦ F.mapComp f i) η.symm]
+  simp only [eqToHom_trans_assoc, eqToHom_refl, id_comp]
+
 /-- More flexible variant of `mapId`. (See the file `Bicategory.Functor.Strict`
 for applications to strict bicategories.) -/
 def mapId' {b : B} (f : b ⟶ b) (hf : f = 𝟙 b := by cat_disch) :

Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean

@@ -62,8 +62,13 @@ instance categoryStruct [CategoryStruct.{v} C] : CategoryStruct (LocallyDiscrete
 
 variable [CategoryStruct.{v} C]
 
+/-- Construct a 1-morphism in the locally discrete bicategory. -/
+abbrev mkHom {a b : C} (f : a ⟶ b) :
+    mk a ⟶ mk b :=
+  ⟨f⟩
+
 @[simp]
-lemma id_as (a : LocallyDiscrete C) : (𝟙 a : Discrete (a.as ⟶ a.as)).as = 𝟙 a.as :=
+lemma id_as (a : LocallyDiscrete C) : (𝟙 a : a ⟶ a).as = 𝟙 a.as :=
   rfl
 
 @[simp]
@@ -81,6 +86,10 @@ instance subsingleton2Hom {a b : LocallyDiscrete C} (f g : a ⟶ b) : Subsinglet
 theorem eq_of_hom {X Y : LocallyDiscrete C} {f g : X ⟶ Y} (η : f ⟶ g) : f = g :=
   Discrete.ext η.1.1
 
+theorem eq_eqToHom {X Y : LocallyDiscrete C} {f g : X ⟶ Y} (η : f ⟶ g) :
+    η = eqToHom (eq_of_hom η) :=
+  Subsingleton.elim _ _
+
 end LocallyDiscrete
 
 variable (C)
@@ -107,6 +116,36 @@ end
 
 namespace Bicategory
 
+namespace LocallyDiscrete
+
+theorem associator_hom {C : Type u} [Category.{v} C] {a b c d : LocallyDiscrete C}
+    (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :
+    (α_ f g h).hom = eqToHom (Category.assoc _ _ _) :=
+  rfl
+
+theorem associator_inv {C : Type u} [Category.{v} C] {a b c d : LocallyDiscrete C}
+    (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :
+    (α_ f g h).inv = eqToHom (Category.assoc _ _ _).symm :=
+  rfl
+
+theorem leftUnitor_hom {C : Type u} [Category.{v} C] {a b : LocallyDiscrete C} (f : a ⟶ b) :
+    (λ_ f).hom = eqToHom (Category.id_comp _) :=
+  rfl
+
+theorem leftUnitor_inv {C : Type u} [Category.{v} C] {a b : LocallyDiscrete C} (f : a ⟶ b) :
+    (λ_ f).inv = eqToHom (Category.id_comp _).symm :=
+  rfl
+
+theorem rightUnitor_hom {C : Type u} [Category.{v} C] {a b : LocallyDiscrete C} (f : a ⟶ b) :
+    (ρ_ f).hom = eqToHom (Category.comp_id _) :=
+  rfl
+
+theorem rightUnitor_inv {C : Type u} [Category.{v} C] {a b : LocallyDiscrete C} (f : a ⟶ b) :
+    (ρ_ f).inv = eqToHom (Category.comp_id _).symm :=
+  rfl
+
+end LocallyDiscrete
+
 /-- A bicategory is locally discrete if the categories of 1-morphisms are discrete. -/
 abbrev IsLocallyDiscrete (B : Type*) [Bicategory B] := ∀ (b c : B), IsDiscrete (b ⟶ c)
 

Mathlib/CategoryTheory/Category/Cat.lean

@@ -137,6 +137,16 @@ lemma associator_inv_app {B C D E : Cat} (F : B ⟶ C) (G : C ⟶ D) (H : D ⟶
     (α_ F G H).inv.app X = eqToHom (by simp) :=
   rfl
 
+theorem associator_eqToIso {B C D E : Cat} (F : B ⟶ C) (G : C ⟶ D) (H : D ⟶ E) :
+    α_ F G H = eqToIso (by simp) :=
+  rfl
+
+theorem rightUnitor_eqToIso {B C : Cat} (F : B ⟶ C) : ρ_ F = eqToIso (by simp) :=
+  rfl
+
+theorem leftUnitor_eqToIso {B C : Cat} (F : B ⟶ C) : λ_ F = eqToIso (by simp) :=
+  rfl
+
 /-- The identity in the category of categories equals the identity functor. -/
 theorem id_eq_id (X : Cat) : 𝟙 X = 𝟭 X := rfl
 

Mathlib/CategoryTheory/Stack/Basic.lean

@@ -0,0 +1,103 @@
+/-
+Copyright (c) 2025 Yuma Mizuno. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yuma Mizuno
+-/
+import Mathlib.CategoryTheory.Sites.Over
+import Mathlib.CategoryTheory.Stack.Descent
+
+/-!
+# Stacks
+
+Let `C` be a category equipped with a Grothendieck topology `J`. A stack is a pseudofunctor `S` from
+`C` into the 2-category `Cat` such that
+* for any object `a : C` and any pair of objects `x, y : S a`, the presheaf of morphisms between
+  `x` and `y` is a sheaf with respect to the topology `J`, and
+* for any object `a : C` and any sieve `R ∈ J a`, any descent datum on `R` is
+  effective, i.e., it is isomorphic to the canonical descent datum associated with some object
+  of `S a`.
+
+-/
+
+universe v u v₁ u₁
+
+open CategoryTheory Opposite Bicategory Pseudofunctor LocallyDiscrete
+
+namespace CategoryTheory
+
+namespace Pseudofunctor
+
+variable {C : Type u} [Category.{v} C]
+
+/-- For a pseudofunctor on `C`, an object `a : C`, and two objects `x y : S a`, we define
+`homPreSheaf S a x y` as a functor `(Over a)ᵒᵖ ⥤ Type v₁` that sends an object `b` over `a`
+(this is a morphism `b ⟶ a` in `C`) to the hom-set `(S b) x ⟶ (S b) y` in the category `S b`. -/
+@[simps]
+def homPreSheaf (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (a : C) (x y : S.mkCat a) :
+    (Over a)ᵒᵖ ⥤ Type v₁ where
+  obj b := (S.mkFunctor b.unop.hom).obj x ⟶ (S.mkFunctor b.unop.hom).obj y
+  map {b c} g ϕ :=
+    eqToHom (by simp) ≫ (S.mapCompCat b.unop.hom g.unop.left).hom.app x ≫
+    (S.mkFunctor g.unop.left).map ϕ ≫
+    (S.mapCompCat b.unop.hom g.unop.left).inv.app y ≫ eqToHom (by simp)
+  map_id := by
+    rintro ⟨x, _, f : x ⟶ a⟩
+    ext g
+    dsimp only [Functor.id_obj, Functor.const_obj_obj, unop_id, Over.id_left, Cat.comp_obj,
+      mapCompCat, op_id, types_id_apply]
+    rw [S.mapComp_eq_right _ (show (mkHom (𝟙 (op x))) = 𝟙 _ from rfl)]
+    simp only [eqToIso_refl, Iso.trans_refl, Iso.refl_trans]
+    rw [S.mapComp_id_right_hom, S.mapComp_id_right_inv]
+    rw [LocallyDiscrete.rightUnitor_hom, LocallyDiscrete.rightUnitor_inv]
+    simp only [S.map₂_eqToHom, Cat.comp_app, Cat.comp_obj, Cat.eqToHom_app, Cat.id_obj,
+      Cat.rightUnitor_inv_app, eqToHom_refl, Cat.whiskerLeft_app, Category.id_comp,
+      Category.comp_id, eqToHom_iso_hom_naturality, eqToHom_naturality_assoc, Category.assoc,
+      eqToHom_trans_assoc]
+    simp [Cat.rightUnitor_hom_app]
+  map_comp := by
+    rintro ⟨b, _, f : b ⟶ a⟩ ⟨c, _, g : c ⟶ a⟩ ⟨d, _, h : d ⟶ a⟩ ⟨i, _, eqi⟩ ⟨j, _, eqj⟩
+    have eqi : i ≫ f = g := by simpa using eqi
+    have eqj : j ≫ g = h := by simpa using eqj
+    have eqi' : mkHom g.op = mkHom f.op ≫ mkHom i.op :=
+      congrArg mkHom (congrArg Quiver.Hom.op (eqi.symm))
+    have eqj' : mkHom h.op = mkHom g.op ≫ mkHom j.op :=
+      congrArg mkHom (congrArg Quiver.Hom.op (eqj.symm))
+    ext ϕ
+    dsimp only [Functor.id_obj, Functor.const_obj_obj, unop_comp, Quiver.Hom.unop_op',
+      Over.comp_left, Cat.comp_obj, mapCompCat, op_comp, types_comp_apply]
+    rw [S.mapComp_eq_right _ (show (mkHom (i.op ≫ j.op) = mkHom i.op ≫ mkHom j.op) from rfl)]
+    rw [S.mapComp_eq_left (show mkHom g.op = mkHom f.op ≫ mkHom i.op from eqi')]
+    dsimp only [eqToIso_refl, Iso.trans_hom, Iso.refl_hom, Cat.comp_app, Cat.comp_obj, Cat.id_app,
+      Iso.trans_inv, Iso.refl_inv]
+    simp only [Category.comp_id, Category.assoc]
+    rw [Category.id_comp (X := (S.map (mkHom f.op ≫ mkHom (i.op ≫ j.op))).obj x)]
+    rw [Category.id_comp (X := (S.map (mkHom i.op ≫ mkHom j.op)).obj ((S.map (mkHom f.op)).obj y))]
+    rw [Category.id_comp (X := (S.map (mkHom f.op ≫ mkHom (i.op ≫ j.op))).obj y)]
+    rw [S.mapComp_comp_right_app, S.mapComp_comp_right_inv]
+    simp only [Cat.comp_obj, associator_inv, S.map₂_eqToHom, Cat.eqToHom_app,
+      Cat.associator_hom_app, eqToHom_refl, Category.id_comp, associator_hom, Cat.comp_app,
+      Cat.whiskerLeft_app, Cat.associator_inv_app, Cat.whiskerRight_app, Category.assoc,
+      eqToHom_trans, NatTrans.naturality_assoc, Cat.comp_map, Iso.inv_hom_id_app_assoc,
+      eqToHom_trans_assoc, eqToIso.hom, Functor.map_comp, eqToHom_map, eqToIso.inv]
+
+open Pseudofunctor
+
+variable {J : GrothendieckTopology C}
+
+/-- A `Pseudofunctor` `S : LocallyDiscrete Cᵒᵖ ⥤ Cat` is a stack (with respect to a
+Grothendieck topology `J` on `C`) if:
+1. for any object `a : C` and any `x y : S.mkCat a`, the presheaf `S.homPreSheaf a x y` is a sheaf
+  for the topology `J.over a`.
+2. for any covering sieve `R ∈ J a`, any descent datum `d` relative to `R` is effective, that is,
+  there exists an object `x : S a` such that `d` is isomorphic to the canonical descent datum
+  associated with `x`. -/
+@[stacks 026F]
+structure IsStack (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) : Prop where
+  is_sheaf_of_hom (a : C) (x y : S.mkCat a) :
+    Presieve.IsSheaf (J.over a) (S.homPreSheaf a x y)
+  is_descent_effective (a : C) (R : Sieve a) (_ : R ∈ J a) (d : S.DescentData R) :
+    ∃ x : S.mkCat a, Nonempty (d ≅ DescentData.canonical S x)
+
+end Pseudofunctor
+
+end CategoryTheory