diff --git a/Mathlib.lean b/Mathlib.lean index 2222cab2501bb5..753bf7d6d14237 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean b/Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean index 0e262a1820188b..9177a94d7ed33c 100644 --- a/Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean +++ b/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) : diff --git a/Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean b/Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean index b9ba82ac9ae75c..118c7cd230aecf 100644 --- a/Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean +++ b/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) diff --git a/Mathlib/CategoryTheory/Category/Cat.lean b/Mathlib/CategoryTheory/Category/Cat.lean index 060f11488b81b8..00d345d8680bb9 100644 --- a/Mathlib/CategoryTheory/Category/Cat.lean +++ b/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 diff --git a/Mathlib/CategoryTheory/Stack/Basic.lean b/Mathlib/CategoryTheory/Stack/Basic.lean new file mode 100644 index 00000000000000..0189d47be39652 --- /dev/null +++ b/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 diff --git a/Mathlib/CategoryTheory/Stack/Descent.lean b/Mathlib/CategoryTheory/Stack/Descent.lean new file mode 100644 index 00000000000000..5e5f0dd5c735b6 --- /dev/null +++ b/Mathlib/CategoryTheory/Stack/Descent.lean @@ -0,0 +1,180 @@ +/- +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.Bicategory.Functor.Pseudofunctor +import Mathlib.CategoryTheory.Bicategory.LocallyDiscrete +import Mathlib.CategoryTheory.Sites.Sieves + +/-! +# Descent data + +Let `C` be a category. Given a pseudofunctor `S` from `C` into the 2-category `Cat` and a +presieve `P` on an object `a : C`, a descent datum on `P` consists of +* an object `X f` of `S b` for each morphism `f : b ⟶ a` in `P`, and +* an isomorphism `φ g : S g (X f) ≅ X (g ≫ f)` for each `f : b ⟶ a` and `g : c ⟶ b`, +satisfying compatibility conditions for the identities and compositions. + +The set of descent data on `P` forms a category `DescentData S P`. + +-/ + +universe v u v₁ u₁ + +open CategoryTheory Opposite Bicategory Limits LocallyDiscrete + +variable {C : Type u} [Category.{v} C] + +namespace CategoryTheory + +namespace Pseudofunctor + +/-- The category `S X` associated with an object `X : C` by the pseudofunctor `S`. -/ +abbrev mkCat (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (X : C) : Cat := + S.obj (.mk (.op X)) + +/-- The functor `S X ⟶ S Y` associated with a morphism `f : Y ⟶ X` in `C` by +the pseudofunctor `S`. -/ +abbrev mkFunctor (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) {X Y : C} (f : Y ⟶ X) : + S.mkCat X ⟶ S.mkCat Y := + S.map (mkHom f.op) + +/-- The natural isomorphism `S (𝟙 X) ≅ 𝟙 (S X)`. -/ +abbrev mapIdCat (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (X : C) : + S.mkFunctor (𝟙 X) ≅ 𝟙 (S.mkCat X) := + S.mapId ⟨op X⟩ + +/-- The natural isomorphism `S (g ≫ f) ≅ S f ≫ S g`. -/ +abbrev mapCompCat (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) {X Y Z : C} + (f : Y ⟶ X) (g : Z ⟶ Y) : + (S.mkFunctor (g ≫ f)) ≅ S.mkFunctor f ≫ S.mkFunctor g := + S.mapComp (mkHom f.op) (mkHom g.op) + +/-- An auxiliary structure for descent data: it contains only data, with no conditions. -/ +structure PreDescentData (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) + {a : C} (P : Presieve a) where + /-- A family of objects in the category `S b` for each morphism `f : b ⟶ a` in + the presieve `P`. -/ + obj : ∀ {b : C} (f : b ⟶ a) (_ : P f := by cat_disch), S.mkCat b + /-- A family of isomorphisms `S g (obj f) ≅ obj (g ≫ f)` in `S c` for each composable pair + `c -g→ b -f→ a` with `P f` and `P (g ≫ f)`. -/ + iso : ∀ {b c : C} {f : b ⟶ a} (g : c ⟶ b) + (hf : P f := by cat_disch) (hg : P (g ≫ f) := by cat_disch), + (S.mkFunctor g).obj (obj f) ≅ obj (g ≫ f) + +/-- +Given a pseudofunctor `S` and a presieve `P` on an object `a` in the category `C`, the descent datum +for `S` consists of: +- `obj`: A family of objects in the category `S b` for each morphism `f : b ⟶ a` in + the presieve `P`. +- `iso`: A family of isomorphisms `S g (obj f) ≅ obj (g ≫ f)` in `S c` for each composable pair + `c -g→ b -f→ a` with `P f` and `P (g ≫ f)`. +- `iso_id`: The condition that the isomorphism associated with the identity morphism is compatible + with the isomorphism `S (𝟙 b) ≅ 𝟙 (S b)`. +- `iso_comp`: The condition that the isomorphism associated with the composition `h ≫ g` is + compatible with the isomorphism `S (h ≫ g) ≅ S h ≫ S g`. +-/ +structure DescentData (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) + {a : C} (P : Presieve a) extends PreDescentData S P where + iso_id {b} (f : b ⟶ a) (hf : P f := by cat_disch) : + iso (𝟙 b) = (S.mapIdCat b).app (obj f) ≪≫ eqToIso (by simp) + iso_comp {b c d} (f : b ⟶ a) (g : c ⟶ b) (h : d ⟶ c) + (hf : P f := by cat_disch) (hg : P (g ≫ f) := by cat_disch) + (hh : P (h ≫ g ≫ f) := by cat_disch) : + iso (h ≫ g) = + (S.mapCompCat g h).app (obj f) ≪≫ + (S.map (mkHom h.op)).mapIso (iso g) ≪≫ iso h ≪≫ eqToIso (by simp) + +namespace DescentData + +variable {S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}} {a : C} {P : Presieve a} + +/-- The homomorphism between two descent data. -/ +@[ext] +structure Hom (𝒟₁ 𝒟₂ : DescentData S P) where + /-- For each morphism `f : b ⟶ a` in `P`, a morphism `𝒟₁.obj f ⟶ 𝒟₂.obj f`. -/ + hom {b : C} (f : b ⟶ a) (_ : P f := by cat_disch) : 𝒟₁.obj f ⟶ 𝒟₂.obj f + comm {b c : C} (f : b ⟶ a) (g : c ⟶ b) + (hf : P f := by cat_disch) (hg : P (g ≫ f) := by cat_disch) : + (S.mkFunctor g).map (hom f) ≫ (𝒟₂.iso g).hom = (𝒟₁.iso g).hom ≫ hom (g ≫ f) := by cat_disch + +attribute [reassoc] Hom.comm + +/-- The identity morphisms on a descent datum. -/ +@[simps] +def Hom.id (𝒟 : DescentData S P) : Hom 𝒟 𝒟 where + hom f _ := 𝟙 (𝒟.obj f) + +/-- The composition of morphisms between descent data. -/ +@[simps] +def Hom.comp {𝒟₁ 𝒟₂ 𝒟₃ : DescentData S P} (η₁ : Hom 𝒟₁ 𝒟₂) (η₂ : Hom 𝒟₂ 𝒟₃) : Hom 𝒟₁ 𝒟₃ where + hom f _ := η₁.hom f ≫ η₂.hom f + comm f g hf hg := by + simp only [Functor.map_comp, Category.assoc] + rw [η₂.comm f g, η₁.comm_assoc f g] + +instance : Category (DescentData S P) where + Hom := Hom + id := Hom.id + comp := Hom.comp + +/-- Given a presieve on `a : C`, we have a descent datum for each object `x : S a`, +called the canonical descent datum. The object for `f : b ⟶ a` is given by `(S f) x`, +and the isomorphism for `c -g⟶ b -f⟶ a` is given by `S g ((S f) x) ≅ (S (g ≫ f)) x` +which is the `mapComp` isomorphism of the pseudofunctor `S`. -/ +@[simps] +def canonical (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (x : S.mkCat a) : + DescentData S P where + obj f _ := (S.mkFunctor f).obj x + iso g _ _ := (S.mapCompCat _ g).symm.app x + iso_id f _ := by + ext + dsimp only [Cat.comp_obj, Iso.app_hom, Iso.symm_hom, Cat.id_obj, Iso.trans_hom, eqToIso.hom] + rw [← eqToHom_app (by simp), ← Cat.whiskerLeft_app, ← NatTrans.comp_app] + congr 1 + dsimp only [mapCompCat, mkFunctor] + rw [S.mapComp_eq_right _ (show mkHom (𝟙 _).op = 𝟙 _ from rfl)] + dsimp only [op_id, op_comp, eqToIso_refl, Iso.trans_inv, Iso.refl_inv] + rw [S.mapComp_id_right_inv] + simp only [Category.assoc] + rw [Cat.rightUnitor_eqToIso, LocallyDiscrete.rightUnitor_inv, S.map₂_eqToHom] + simp only [eqToIso_refl, Iso.refl_hom, Category.comp_id, eqToHom_naturality_assoc, + Category.id_comp] + /- We need to give an argument. `rw [Category.id_comp]` alone does not work. -/ + rw [Category.id_comp (X := S.map (mkHom f.op) ≫ S.map (𝟙 _))] + rw [Category.comp_id (Y := S.map (mkHom f.op ≫ mkHom (𝟙 _)))] + iso_comp f g h _ _ _ := by + ext + dsimp only [Iso.app_hom, Iso.symm_hom, Iso.trans_hom, Functor.mapIso_hom, eqToIso.hom] + /- We manually write this to avoid a defeq abuse about the associator. Actually, I want to get + the RHS by `rw` or `simp`. Related discussion: + https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Functor.20identity.20.60.F0.9D.9F.AD.20_.20.E2.8B.99.20F.20.3D.20F.60.20is.20definitional.20equality/with/527059148 -/ + have : (S.mapCompCat g h).hom.app ((S.mkFunctor f).obj x) ≫ + (S.map (mkHom h.op)).map ((S.mapCompCat f g).inv.app x) = + (S.mkFunctor f ◁ (S.mapCompCat g h).hom ≫ (α_ _ _ _).inv ≫ + (S.mapCompCat f g).inv ▷ S.map (mkHom h.op)).app x := by + dsimp only [Cat.comp_obj, Cat.comp_app, Cat.whiskerLeft_app, Cat.whiskerRight_app] + rw [Cat.associator_eqToIso] + simp only [eqToIso_refl, Iso.refl_inv, Cat.id_app, Cat.comp_obj, Category.id_comp] + rw [reassoc_of% this, ← eqToHom_app (by simp)] + simp only [← NatTrans.comp_app] + congr 1 + dsimp only [mapCompCat, mkFunctor] + rw [S.mapComp_eq_right _ (show (mkHom (h ≫ g).op) = mkHom g.op ≫ mkHom h.op from rfl)] + rw [S.mapComp_eq_left (show (mkHom (g ≫ f).op) = mkHom f.op ≫ mkHom g.op from rfl)] + dsimp only [op_comp, eqToIso_refl, Iso.trans_inv, Iso.refl_inv] + simp only [Category.assoc] + rw [Category.id_comp (X := S.map (mkHom f.op) ≫ S.map (mkHom g.op ≫ mkHom h.op))] + rw [Category.id_comp (X := S.map (mkHom f.op ≫ mkHom g.op) ≫ S.map (mkHom h.op))] + rw [Category.id_comp (X := S.map (mkHom (f.op ≫ g.op) ≫ mkHom h.op))] + rw [Category.comp_id (Y := S.map (mkHom f.op ≫ mkHom (g.op ≫ h.op)))] + rw [S.mapComp_comp_right_inv] + rw [LocallyDiscrete.associator_hom] + rw [S.map₂_eqToHom] + +end DescentData + +end Pseudofunctor + +end CategoryTheory