From f12655ffc7dab52b28aefa068ecfbf5a3bd0842d Mon Sep 17 00:00:00 2001 From: Yuma Mizuno Date: Sat, 13 Sep 2025 06:26:36 +0100 Subject: [PATCH 1/6] wip --- .../Bicategory/LocallyDiscrete.lean | 23 +- Mathlib/CategoryTheory/Stack/Basic.lean | 62 ++ Mathlib/CategoryTheory/Stack/Descent.lean | 563 ++++++++++++++++++ 3 files changed, 647 insertions(+), 1 deletion(-) create mode 100644 Mathlib/CategoryTheory/Stack/Basic.lean create mode 100644 Mathlib/CategoryTheory/Stack/Descent.lean diff --git a/Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean b/Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean index b9ba82ac9ae75c..51a9f87745e3d8 100644 --- a/Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean +++ b/Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean @@ -55,6 +55,9 @@ instance [DecidableEq C] : DecidableEq (LocallyDiscrete C) := instance [Inhabited C] : Inhabited (LocallyDiscrete C) := ⟨⟨default⟩⟩ +-- abbrev Hom [CategoryStruct.{v} C] (a b : LocallyDiscrete C) : Type v := +-- Discrete (a.as ⟶ b.as) + instance categoryStruct [CategoryStruct.{v} C] : CategoryStruct (LocallyDiscrete C) where Hom a b := Discrete (a.as ⟶ b.as) id a := ⟨𝟙 a.as⟩ @@ -62,8 +65,12 @@ instance categoryStruct [CategoryStruct.{v} C] : CategoryStruct (LocallyDiscrete variable [CategoryStruct.{v} C] +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] @@ -83,6 +90,20 @@ theorem eq_of_hom {X Y : LocallyDiscrete C} {f g : X ⟶ Y} (η : f ⟶ g) : f = end LocallyDiscrete +namespace LocallyDiscrete + +variable [Category.{v} C] + +def idIso (a : C) : + mkHom (𝟙 a) ≅ 𝟙 (mk a) := + eqToIso rfl + +def compIso {a b c : C} (f : a ⟶ b) (g : b ⟶ c) : + mkHom (f ≫ g) ≅ mkHom f ≫ mkHom g := + eqToIso rfl + +end LocallyDiscrete + variable (C) variable [Category.{v} C] diff --git a/Mathlib/CategoryTheory/Stack/Basic.lean b/Mathlib/CategoryTheory/Stack/Basic.lean new file mode 100644 index 00000000000000..c73e604d216796 --- /dev/null +++ b/Mathlib/CategoryTheory/Stack/Basic.lean @@ -0,0 +1,62 @@ +import Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor +import Mathlib.CategoryTheory.Bicategory.LocallyDiscrete +import Mathlib.CategoryTheory.Category.Cat +import Mathlib.CategoryTheory.Sites.Grothendieck +import Mathlib.CategoryTheory.Sites.Sheaf +import Mathlib.CategoryTheory.Sites.Over + +universe v u v₁ u₁ + +open CategoryTheory Opposite Bicategory + +variable {C : Type u} [Category.{v} C] + +def homPreSheaf (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U : C) (x y : S.obj ⟨op U⟩) : + Opposite (Over U) ⥤ Type v₁ where + obj V := (S.map ⟨V.unop.hom.op⟩).obj x ⟶ (S.map ⟨V.unop.hom.op⟩).obj y + map {V V'} g := by + let f : Discrete (op U ⟶ op (unop V).left) := ⟨V.unop.hom.op⟩ + let f' : Discrete (op U ⟶ op (unop V').left) := ⟨V'.unop.hom.op⟩ + let g' : Discrete (op (unop V).left ⟶ op (unop V').left) := ⟨g.unop.left.op⟩ + have w : f.as ≫ g'.as = f'.as := by + simp [f, f', g'] + rw [← op_comp]; simp + let α := S.mapComp f g' + intro ϕ + let gϕ := (S.map g').map ϕ + let eq : ∀ x, (S.map f').obj x ≅ (S.map (f ≫ g')).obj x := + fun x ↦ eqToIso (by congr; apply Discrete.ext; simp [w]) + exact (eq x).hom ≫ α.hom.app x ≫ gϕ ≫ α.inv.app y ≫ (eq y).inv + + map_id := by + rintro ⟨⟨X, _, f⟩⟩ + ext g + simp only [Functor.id_obj, Functor.const_obj_obj, unop_id, Over.id_left, op_id, eqToIso.hom, + Cat.comp_obj, eqToIso.inv, types_id_apply] + dsimp at f g + erw [Pseudofunctor.mapComp_id_right_hom] + dsimp only [Cat.comp_app, Cat.comp_obj, Cat.id_obj, Cat.whiskerLeft_app] + simp only [Category.assoc] + erw [Pseudofunctor.mapComp_id_right_inv] + dsimp only [Cat.comp_app, Cat.comp_obj, Cat.id_obj, Cat.whiskerLeft_app] + simp only [Category.assoc, NatTrans.naturality_assoc, Cat.id_obj, Cat.id_map, + Iso.inv_hom_id_app_assoc] + rw [Cat.rightUnitor_inv_app] + rw [Cat.rightUnitor_hom_app] + simp only [Cat.comp_obj, Cat.id_obj, eqToHom_refl, Category.id_comp] + simp only [Pseudofunctor.map₂_right_unitor, Cat.comp_app, Cat.comp_obj, Cat.id_obj, + Cat.whiskerLeft_app, Category.assoc] + -- rw [Cat.rightUnitor_inv_app] + rw [Cat.rightUnitor_hom_app] + simp only [Cat.comp_obj, Cat.id_obj, eqToHom_refl, Category.id_comp] + have : (S.map₂ (ρ_ (⟨f.op⟩ : Discrete (op U ⟶ op X))).hom).app x ≫ (ρ_ (S.map (⟨f.op⟩ : Discrete (op U ⟶ op X)))).inv.app x = sorry := by + rw [Cat.rightUnitor_inv_app] + sorry + -- let _ := g.w + + map_comp := _ + +variable {J : GrothendieckTopology C} + +structure IsStack (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) where + isSheafOfHom : ∀ (U : C) (x y : S.obj ⟨op U⟩), Presieve.IsSheaf (J.over U) (homPreSheaf S U x y) diff --git a/Mathlib/CategoryTheory/Stack/Descent.lean b/Mathlib/CategoryTheory/Stack/Descent.lean new file mode 100644 index 00000000000000..2ddbc84313099e --- /dev/null +++ b/Mathlib/CategoryTheory/Stack/Descent.lean @@ -0,0 +1,563 @@ +import Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor +import Mathlib.CategoryTheory.Bicategory.LocallyDiscrete +import Mathlib.CategoryTheory.Category.Cat +import Mathlib.CategoryTheory.Sites.Grothendieck +import Mathlib.CategoryTheory.Sites.Sheaf +import Mathlib.CategoryTheory.Sites.Over + +noncomputable section + +universe v u v₁ u₁ v₂ + +open CategoryTheory Opposite Bicategory +open CategoryTheory.Limits LocallyDiscrete + + +variable {C : Type u} [Category.{v} C] + +namespace CategoryTheory + +namespace Presieve + +variable {X : C} + +class HasTriplewisePullbacks (R : Presieve X) extends HasPairwisePullbacks R where + -- has_pairwise_pullbacks : ∀ {Y Z} {f : Y ⟶ X} (_ : R f) {g : Z ⟶ X} (_ : R g), HasPullback f g + has_triplewise_pullbacks : + ∀ {X₁ X₂ X₃} {f₁ : X₁ ⟶ X} (_ : R f₁) {f₂ : X₂ ⟶ X} (_ : R f₂) {f₃ : X₃ ⟶ X} (_ : R f₃) + [HasPullback f₁ f₂] [HasPullback f₂ f₃], HasPullback (pullback.snd f₁ f₂) (pullback.fst f₂ f₃) + +instance (R : Presieve X) [HasPullbacks C] : R.HasTriplewisePullbacks := ⟨inferInstance⟩ + +instance {α : Type v₂} {X : α → C} {B : C} (π : (a : α) → X a ⟶ B) + [(Presieve.ofArrows X π).HasTriplewisePullbacks] (a b c : α) : + HasPullback (pullback.snd (π a) (π b)) (pullback.fst (π b) (π c)) := + Presieve.HasTriplewisePullbacks.has_triplewise_pullbacks + (Presieve.ofArrows.mk _) (Presieve.ofArrows.mk _) (Presieve.ofArrows.mk _) + +end Presieve + +namespace TriplePullback + +variable {U V₁ V₂ V₃ : C} + +abbrev triplePullback (f₁ : V₁ ⟶ U) (f₂ : V₂ ⟶ U) (f₃ : V₃ ⟶ U) + [HasPullback f₁ f₂] [HasPullback f₂ f₃] + [HasPullback (pullback.snd f₁ f₂) (pullback.fst f₂ f₃)] : C := + pullback (pullback.snd f₁ f₂) (pullback.fst f₂ f₃) + +inductive Direction | left | middle | right + +inductive DirectionPair + | left_middle : DirectionPair + | middle_right : DirectionPair + | left_right : DirectionPair + deriving Inhabited + +instance : OfNat Direction 0 := ⟨Direction.left⟩ +instance : OfNat Direction 1 := ⟨Direction.middle⟩ +instance : OfNat Direction 2 := ⟨Direction.right⟩ + +instance : Coe (ℕ × ℕ) DirectionPair where + coe d := + match d with + | (0, 1) => DirectionPair.left_middle + | (1, 2) => DirectionPair.middle_right + | (0, 2) => DirectionPair.left_right + | _ => Inhabited.default + +@[simp] +def DirectionPair.fst : DirectionPair → Direction + | DirectionPair.left_middle => 0 + | DirectionPair.middle_right => 1 + | DirectionPair.left_right => 0 + +@[simp] +def DirectionPair.snd : DirectionPair → Direction + | DirectionPair.left_middle => 1 + | DirectionPair.middle_right => 2 + | DirectionPair.left_right => 2 + +variable {V : Direction → C} (f : (i : Direction) → V i ⟶ U) +variable {HasPullback : ∀ i j : Direction, HasPullback (f i) (f j)} +variable [(Presieve.ofArrows V f).HasTriplewisePullbacks] + +def pr (p : DirectionPair) : triplePullback (f 0) (f 1) (f 2) ⟶ pullback (f p.fst) (f p.snd) := + match p with + | .left_middle => pullback.fst (pullback.snd (f 0) (f 1)) (pullback.fst (f 1) (f 2)) + | .middle_right => pullback.snd (pullback.snd (f 0) (f 1)) (pullback.fst (f 1) (f 2)) + | .left_right => + pullback.lift + (pullback.fst (pullback.snd (f 0) (f 1)) (pullback.fst (f 1) (f 2)) ≫ + pullback.fst (f 0) (f 1)) + (pullback.snd (pullback.snd (f 0) (f 1)) (pullback.fst (f 1) (f 2)) ≫ + pullback.snd (f 1) (f 2)) <| by + dsimp only [DirectionPair.fst, DirectionPair.snd] + rw [Category.assoc, pullback.condition, ← Category.assoc, pullback.condition, + Category.assoc, pullback.condition, Category.assoc] + +def prToSingle (i : Direction) : + triplePullback (f 0) (f 1) (f 2) ⟶ V i := + match i with + | 0 => pr f .left_middle ≫ pullback.fst (f 0) (f 1) + | 1 => pr f .left_middle ≫ pullback.snd (f 0) (f 1) + | 2 => pr f .middle_right ≫ pullback.snd (f 1) (f 2) + +variable {U : C} {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) +variable [(Presieve.ofArrows V f).HasTriplewisePullbacks] + +def pr₀₁₂_₀₁ (i j k : I) : + triplePullback (f i) (f j) (f k) ⟶ pullback (f i) (f j) := + pullback.fst (pullback.snd (f i) (f j)) (pullback.fst (f j) (f k)) + +def pr₀₁₂_₁₂ (i j k : I) : + triplePullback (f i) (f j) (f k) ⟶ pullback (f j) (f k) := + pullback.snd (pullback.snd (f i) (f j)) (pullback.fst (f j) (f k)) + +def pr₀₁₂_₀₂ (i j k : I) : + triplePullback (f i) (f j) (f k) ⟶ pullback (f i) (f k) := + pullback.lift (pr₀₁₂_₀₁ f i j k ≫ pullback.fst (f i) (f j)) + (pr₀₁₂_₁₂ f i j k ≫ pullback.snd (f j) (f k)) <| by + dsimp only [pr₀₁₂_₀₁, pr₀₁₂_₁₂] + rw [Category.assoc, pullback.condition, ← Category.assoc, pullback.condition, + Category.assoc, pullback.condition, Category.assoc] + +abbrev pr₀₁_₀ (i j : I) : + pullback (f i) (f j) ⟶ V i := + pullback.fst (f i) (f j) + +abbrev pr₀₁_₁ (i j : I) : + pullback (f i) (f j) ⟶ V j := + pullback.snd (f i) (f j) + +abbrev pr₁₂_₁ (j k : I) : + pullback (f j) (f k) ⟶ V j := + pullback.fst (f j) (f k) + +abbrev pr₁₂_₂ (j k : I) : + pullback (f j) (f k) ⟶ V k := + pullback.snd (f j) (f k) + +abbrev pr₀₂_₀ (i k : I) : + pullback (f i) (f k) ⟶ V i := + pullback.fst (f i) (f k) + +abbrev pr₀₂_₂ (i k : I) : + pullback (f i) (f k) ⟶ V k := + pullback.snd (f i) (f k) + +-- theorem pullback_condition₀ (i j k : I) : +-- pr₀₁₂_₀₁ f i j k ≫ pr₀₁_₀ f i j = pr₀₁₂_₀₂ f i j k ≫ pr₀₂_₀ f i k := by +-- simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app, pr₀₁₂_₀₁, pr₀₁₂_₀₂] + +-- theorem pullback_condition₁ (i j k : I) : +-- pr₀₁₂_₀₁ f i j k ≫ pr₀₁_₁ f i j = pr₀₁₂_₁₂ f i j k ≫ pr₁₂_₁ f j k := +-- pullback.condition + +-- theorem pullback_condition₂ (i j k : I) : +-- pr₀₁₂_₀₂ f i j k ≫ pr₀₂_₂ f i k = pr₀₁₂_₁₂ f i j k ≫ pr₁₂_₂ f j k := by +-- simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app, pr₀₁₂_₀₂, pr₀₁₂_₀₂, pr₀₁₂_₁₂] + +def pr₀₁₂_₀ (i j k : I) : triplePullback (f i) (f j) (f k) ⟶ V i := + pr₀₁₂_₀₁ f i j k ≫ pr₀₁_₀ f i j + +theorem pr₀₁₂_₀_def₀₁ {i j k : I} : + pr₀₁₂_₀ f i j k = pr₀₁₂_₀₁ f i j k ≫ pr₀₁_₀ f i j := + rfl + +theorem pr₀₁₂_₀_def₀₂ {i j k : I} : + pr₀₁₂_₀ f i j k = pr₀₁₂_₀₂ f i j k ≫ pr₀₂_₀ f i k := by + simp only [pr₀₁₂_₀_def₀₁, pr₀₁₂_₀₁, pr₀₁₂_₀₂, limit.lift_π, PullbackCone.mk_pt, + PullbackCone.mk_π_app] + +def pr₀₁₂_₁ (i j k : I) : triplePullback (f i) (f j) (f k) ⟶ V j := + pr₀₁₂_₀₁ f i j k ≫ pr₀₁_₁ f i j + +theorem pr₀₁₂_₁_def₀₁ {i j k : I} : + pr₀₁₂_₁ f i j k = pr₀₁₂_₀₁ f i j k ≫ pr₀₁_₁ f i j := + rfl + +theorem pr₀₁₂_₁_def₁₂ {i j k : I} : + pr₀₁₂_₁ f i j k = pr₀₁₂_₁₂ f i j k ≫ pr₁₂_₁ f j k := + pullback.condition + +def pr₀₁₂_₂ (i j k : I) : triplePullback (f i) (f j) (f k) ⟶ V k := + pr₀₁₂_₁₂ f i j k ≫ pr₁₂_₂ f j k + +theorem pr₀₁₂_₂_def₁₂ {i j k : I} : + pr₀₁₂_₂ f i j k = pr₀₁₂_₁₂ f i j k ≫ pr₁₂_₂ f j k := + rfl + +theorem pr₀₁₂_₂_def₀₂ {i j k : I} : + pr₀₁₂_₂ f i j k = pr₀₁₂_₀₂ f i j k ≫ pr₀₂_₂ f i k := by + simp only [pr₀₁₂_₂_def₁₂, pr₀₁₂_₁₂, pr₀₁₂_₀₂, limit.lift_π, PullbackCone.mk_pt, + PullbackCone.mk_π_app] + +end TriplePullback + +namespace Pseudofunctor + +open TriplePullback + +-- set_option pp.universes true + +def mkCat (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (X : C) : Cat := + S.obj ⟨op X⟩ + +-- def mkFunctor (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) {X Y : C} (f : Y ⟶ X) : +-- S.mkCat X ⟶ S.mkCat Y := +-- S.map ⟨op f⟩ + +-- def mkCat' (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (X : C) : Type u₁ := +-- S.obj ⟨op X⟩ + +abbrev mkFunctor (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) {X Y : C} (f : Y ⟶ X) : + S.mkCat X ⟶ S.mkCat Y := + S.map (LocallyDiscrete.mkHom (op f)) + +-- @[to_app?] +-- @[simps!?] +abbrev mapCompObj (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) {X Y Z : C} + (f : Y ⟶ X) (g : Z ⟶ Y) {x : S.mkCat X} : + (S.mkFunctor (g ≫ f)).obj x ≅ (S.mkFunctor g).obj ((S.mkFunctor f).obj x) := + (S.mapComp (mkHom (op f)) (mkHom (op g))).app x + +structure PreDescentData (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) + (U : C) {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) + [(Presieve.ofArrows V f).HasTriplewisePullbacks] where + /-- An object `Xᵢ` of `S Vᵢ` for each `i : I`. -/ + X : ∀ i, S.obj ⟨op (V i)⟩ + /-- An isomorphism `φᵢⱼ : pr₀* Xᵢ ≅ pr₁* Xⱼ` for each `i j : I`. -/ + φ : ∀ i j : I, + (S.mkFunctor (pullback.fst (f i) (f j))).obj (X i) ≅ + (S.mkFunctor (pullback.snd (f i) (f j))).obj (X j) + +namespace PreDescentData + +variable {S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}} + {U : C} {I : Type v₂} {V : I → C} {f : (i : I) → V i ⟶ U} + [(Presieve.ofArrows V f).HasTriplewisePullbacks] + +@[simp] +def objAtDirection (V : I → C) (i j k : I) : Direction → C + | 0 => V i + | 1 => V j + | 2 => V k + +@[simp] +def morAtDirection (f : (i : I) → V i ⟶ U) (i j k : I) : (d : Direction) → objAtDirection V i j k d ⟶ U + | 0 => f i + | 1 => f j + | 2 => f k + +instance {i j k : I} : + (Presieve.ofArrows (objAtDirection V i j k) (morAtDirection f i j k)).HasTriplewisePullbacks := + sorry + +instance {ι : Direction → I} : + (Presieve.ofArrows (fun j ↦ V (ι j)) fun j ↦ f (ι j)).HasTriplewisePullbacks := sorry + +def cocycleMap (d : PreDescentData S U f) (ι : Direction → I) (ij : DirectionPair) : + (S.mkFunctor (prToSingle (fun j ↦ f (ι j)) ij.fst)).obj (d.X (ι ij.fst)) ≅ + (S.mkFunctor (prToSingle (fun j ↦ f (ι j)) ij.snd)).obj (d.X (ι ij.snd)) := + let f' := fun j ↦ f (ι j) + let i := ij.fst + let j := ij.snd + calc + (S.mkFunctor (prToSingle f' i)).obj (d.X (ι i)) ≅ + (S.mkFunctor (pr f' ij ≫ pr₀₁_₀ f (ι i) (ι j))).obj (d.X (ι i)) := + (S.map₂Iso (Discrete.eqToIso' (congrArg op sorry))).app (d.X (ι i)) + _ ≅ (S.mkFunctor (pr₀₁_₀ f (ι i) (ι j)) ≫ S.mkFunctor (pr f' ij)).obj (d.X (ι i)) := + (S.mapComp (mkHom ((pr₀₁_₀ f (ι i) (ι j)).op)) (mkHom ((pr f' ij).op))).app (d.X (ι i)) + _ ≅ (S.mkFunctor (pr₀₁_₁ f (ι i) (ι j)) ≫ S.mkFunctor (pr f' ij)).obj (d.X (ι j)) := + /- Here is the main part. -/ + (S.mkFunctor (pr f' ij)).mapIso (d.φ (ι i) (ι j)) + _ ≅ (S.mkFunctor ((pr f' ij) ≫ pr₀₁_₁ f (ι i) (ι j))).obj (d.X (ι j)) := + (S.mapComp (mkHom ((pr₀₁_₁ f (ι i) (ι j)).op)) (mkHom ((pr f' ij).op))).symm.app (d.X (ι j)) + _ ≅ (S.mkFunctor (prToSingle f' j)).obj (d.X (ι j)) := + (S.map₂Iso (Discrete.eqToIso' (congrArg op sorry))).symm.app (d.X (ι j)) + +def cocycleMapAux (d : PreDescentData S U f) (ι : Direction → I) (ij : DirectionPair) : + (S.mkFunctor (prToSingle (fun j ↦ f (ι j)) ij.fst)) ≅ + (S.mkFunctor (pr₀₁_₀ f (ι ij.fst) (ι ij.snd)) ≫ S.mkFunctor (pr (fun j ↦ f (ι j)) ij)) := + let f' := fun j ↦ f (ι j) + let i := ij.fst + let j := ij.snd + calc + (S.mkFunctor (prToSingle f' i)) ≅ (S.mkFunctor (pr f' ij ≫ pr₀₁_₀ f (ι i) (ι j))) := + (S.map₂Iso (Discrete.eqToIso' (congrArg op sorry))) + _ ≅ (S.mkFunctor (pr₀₁_₀ f (ι i) (ι j)) ≫ S.mkFunctor (pr f' ij)) := + (S.mapComp (mkHom ((pr₀₁_₀ f (ι i) (ι j)).op)) (mkHom ((pr f' ij).op))) + +def cocycleMap₀₁ (d : PreDescentData S U f) (i j k : I) : + (S.mkFunctor (pr₀₁₂_₀ f i j k)).obj (d.X i) ≅ (S.mkFunctor (pr₀₁₂_₁ f i j k)).obj (d.X j) := + calc + (S.mkFunctor (pr₀₁₂_₀ f i j k)).obj (d.X i) ≅ + (S.mkFunctor (pr₀₁₂_₀₁ f i j k ≫ pr₀₁_₀ f i j)).obj (d.X i) := + (S.map₂Iso (Discrete.eqToIso' (congrArg op (pr₀₁₂_₀_def₀₁ f)))).app (d.X i) + _ ≅ (S.mkFunctor (pr₀₁_₀ f i j) ≫ S.mkFunctor (pr₀₁₂_₀₁ f i j k)).obj (d.X i) := + (S.mapComp (mkHom ((pr₀₁_₀ f i j).op)) (mkHom ((pr₀₁₂_₀₁ f i j k).op))).app (d.X i) + _ ≅ (S.mkFunctor (pr₀₁_₁ f i j) ≫ S.mkFunctor (pr₀₁₂_₀₁ f i j k)).obj (d.X j) := + /- Here is the main part. -/ + (S.mkFunctor (pr₀₁₂_₀₁ f i j k)).mapIso (d.φ i j) + _ ≅ (S.mkFunctor ((pr₀₁₂_₀₁ f i j k) ≫ pr₀₁_₁ f i j)).obj (d.X j) := + (S.mapComp (mkHom ((pr₀₁_₁ f i j).op)) (mkHom ((pr₀₁₂_₀₁ f i j k).op))).symm.app (d.X j) + _ ≅ (S.mkFunctor (pr₀₁₂_₁ f i j k)).obj (d.X j) := + (S.map₂Iso (Discrete.eqToIso' (congrArg op (pr₀₁₂_₁_def₀₁ f)))).symm.app (d.X j) + +def cocycleMap₁₂ (d : PreDescentData S U f) (i j k : I) : + (S.mkFunctor (pr₀₁₂_₁ f i j k)).obj (d.X j) ≅ (S.mkFunctor (pr₀₁₂_₂ f i j k)).obj (d.X k) := + calc + (S.mkFunctor (pr₀₁₂_₁ f i j k)).obj (d.X j) ≅ + (S.mkFunctor (pr₀₁₂_₁₂ f i j k ≫ pr₁₂_₁ f j k)).obj (d.X j) := + (S.map₂Iso (Discrete.eqToIso' (congrArg op (pr₀₁₂_₁_def₁₂ f)))).app (d.X j) + _ ≅ (S.mkFunctor (pr₁₂_₁ f j k) ≫ S.mkFunctor (pr₀₁₂_₁₂ f i j k)).obj (d.X j) := + (S.mapComp (mkHom ((pr₁₂_₁ f j k).op)) (mkHom ((pr₀₁₂_₁₂ f i j k).op))).app (d.X j) + _ ≅ (S.mkFunctor (pr₁₂_₂ f j k) ≫ S.mkFunctor (pr₀₁₂_₁₂ f i j k)).obj (d.X k) := + /- Here is the main part. -/ + (S.mkFunctor (pr₀₁₂_₁₂ f i j k)).mapIso (d.φ j k) + _ ≅ (S.mkFunctor ((pr₀₁₂_₁₂ f i j k) ≫ pr₁₂_₂ f j k)).obj (d.X k) := + (S.mapComp (mkHom ((pr₁₂_₂ f j k).op)) (mkHom ((pr₀₁₂_₁₂ f i j k).op))).symm.app (d.X k) + _ ≅ (S.mkFunctor (pr₀₁₂_₂ f i j k)).obj (d.X k) := + (S.map₂Iso (Discrete.eqToIso' (congrArg op (pr₀₁₂_₂_def₁₂ f)))).symm.app (d.X k) + +def cocycleMap₀₂ (d : PreDescentData S U f) (i j k : I) : + (S.mkFunctor (pr₀₁₂_₀ f i j k)).obj (d.X i) ≅ (S.mkFunctor (pr₀₁₂_₂ f i j k)).obj (d.X k) := + calc + (S.mkFunctor (pr₀₁₂_₀ f i j k)).obj (d.X i) ≅ + (S.mkFunctor (pr₀₁₂_₀₂ f i j k ≫ pr₀₂_₀ f i k)).obj (d.X i) := + (S.map₂Iso (Discrete.eqToIso' (congrArg op (pr₀₁₂_₀_def₀₂ f)))).app (d.X i) + _ ≅ (S.mkFunctor (pr₀₂_₀ f i k) ≫ S.mkFunctor (pr₀₁₂_₀₂ f i j k)).obj (d.X i) := + (S.mapComp (mkHom ((pr₀₂_₀ f i k).op)) (mkHom ((pr₀₁₂_₀₂ f i j k).op))).app (d.X i) + _ ≅ (S.mkFunctor (pr₀₂_₂ f i k) ≫ S.mkFunctor (pr₀₁₂_₀₂ f i j k)).obj (d.X k) := + /- Here is the main part. -/ + (S.mkFunctor (pr₀₁₂_₀₂ f i j k)).mapIso (d.φ i k) + _ ≅ (S.mkFunctor ((pr₀₁₂_₀₂ f i j k) ≫ pr₀₂_₂ f i k)).obj (d.X k) := + (S.mapComp (mkHom ((pr₀₂_₂ f i k).op)) (mkHom ((pr₀₁₂_₀₂ f i j k).op))).symm.app (d.X k) + _ ≅ (S.mkFunctor (pr₀₁₂_₂ f i j k)).obj (d.X k) := + (S.map₂Iso (Discrete.eqToIso' (congrArg op (pr₀₁₂_₂_def₀₂ f)))).symm.app (d.X k) + +#check op_comp + +end PreDescentData + +example (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) + (U : C) {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) + [(Presieve.ofArrows V f).HasTriplewisePullbacks] (d : PreDescentData S U f) : Prop := + ∀ i j k : I, + let ι : Direction → I + | .left => i + | .middle => j + | .right => k + d.cocycleMap ι .left_middle ≪≫ d.cocycleMap ι .middle_right = d.cocycleMap ι .left_right + +-- @[simp] +def fromDirection {I : Type v₂} (i j k : I) : Direction → I + | .left => i + | .middle => j + | .right => k + +@[simp] +theorem fromDirection_left {I : Type v₂} (i j k : I) : fromDirection i j k 0 = i := rfl + +@[simp] +theorem fromDirection_middle {I : Type v₂} (i j k : I) : fromDirection i j k 1 = j := rfl + +@[simp] +theorem fromDirection_right {I : Type v₂} (i j k : I) : fromDirection i j k 2 = k := rfl + + +def cocycleMap' {S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}} + {U : C} {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) + [(Presieve.ofArrows V f).HasTriplewisePullbacks] (d : PreDescentData S U f) (i j k : I) := + d.cocycleMap (fromDirection i j k) + +structure DescentData (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) + (U : C) {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) + [(Presieve.ofArrows V f).HasTriplewisePullbacks] extends PreDescentData S U f where + /-- The cocycle condition for `φᵢⱼ`. -/ + cocycle_condition : ∀ i j k : I, + -- PreDescentData.cocycleMap₀₁ toPreDescentData i j k ≪≫ + -- PreDescentData.cocycleMap₁₂ toPreDescentData i j k = + -- PreDescentData.cocycleMap₀₂ toPreDescentData i j k + toPreDescentData.cocycleMap (fromDirection i j k) .left_middle ≪≫ + toPreDescentData.cocycleMap (fromDirection i j k) .middle_right = + toPreDescentData.cocycleMap (fromDirection i j k) .left_right + + -- let φ₁₂ := + -- (mapCompObj _ _ _).hom ≫ (S.mkFunctor (pr₁₂ f i j k)).map (φ j k).hom ≫ (mapCompObj _ _ _).inv + -- let φ₀₂ := + -- (mapCompObj _ _ _).hom ≫ (S.mkFunctor (pr₀₂ f i j k)).map (φ i k).hom ≫ (mapCompObj _ _ _).inv + -- let φ₀₁ := + -- (mapCompObj _ _ _).hom ≫ (S.mkFunctor (pr₀₁ f i j k)).map (φ i j).hom ≫ (mapCompObj _ _ _).inv + -- φ₀₁ ≫ + -- (S.map₂ (Discrete.eqToHom' (by rw [pullback_condition₁]))).app (X j) ≫ φ₁₂ = + -- (S.map₂ (Discrete.eqToHom' (by rw [pullback_condition₀]))).app (X i) ≫ + -- φ₀₂ ≫ + -- (S.map₂ (Discrete.eqToHom' (by rw [pullback_condition₂]))).app (X k) + +namespace DescentData + +export PreDescentData (cocycleMap₀₁ cocycleMap₁₂ cocycleMap₀₂ cocycleMap) + -- PreDescentData.cocycleMap₁₂ + -- PreDescentData.cocycleMap₀₂ + +-- attribute [local simp] eqToHom_map + +def canonicalAux (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U : C) + {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) + [(Presieve.ofArrows V f).HasTriplewisePullbacks] (X : S.mkCat U) : + PreDescentData S U f where + X i := (S.mkFunctor (f i)).obj X + φ i j := + ((S.mapComp (mkHom (f i).op) (mkHom (pullback.fst (f i) (f j)).op)).symm ≪≫ + S.map₂Iso + ((compIso (f i).op (pullback.fst (f i) (f j)).op).symm ≪≫ + Discrete.eqToIso' (congrArg op pullback.condition) ≪≫ + compIso (f j).op (pullback.snd (f i) (f j)).op) ≪≫ + S.mapComp (mkHom (f j).op) (mkHom (pullback.snd (f i) (f j)).op)).app X + +open DirectionPair + +#check Pseudofunctor.map₂_associator_app + +variable {D E E' : Type} [Category D] [Category E][Category E'] +variable (F G H : C ⥤ D) {G : D ⥤ E} {H : E ⥤ E'} {X : C} +#check (H.obj (G.obj (F.obj X))) + +example (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U : C) + {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) + [(Presieve.ofArrows V f).HasTriplewisePullbacks] (X : S.mkCat U) (i j k : I) (p : DirectionPair) : + (canonicalAux S U f X).cocycleMap (fromDirection i j k) .left_middle = sorry := by + apply Iso.ext + dsimp only [fromDirection_left, fromDirection_middle, fromDirection_right, fst, canonicalAux, snd, + cocycleMap, - Cat.comp_obj, - eqToIso_refl, Iso.trans_def, Iso.trans_hom, Iso.app_hom, + Functor.mapIso_hom, Iso.refl_hom, PrelaxFunctor.mapFunctor_map, Iso.symm_hom, - eqToIso.hom, + NatTrans.comp_app, Functor.mapIso_inv, Iso.refl_inv] + simp only [- eqToHom_refl, PrelaxFunctor.map₂_id, Cat.id_app, Category.id_comp, + PrelaxFunctor.map₂_comp, Cat.comp_app, Category.assoc, Functor.map_comp, - eqToIso_refl, + Iso.refl_inv] + dsimp only [mkFunctor] + set pr₀₁ := (pr (fun j_1 ↦ f (fromDirection i j k j_1)) left_middle) + slice_lhs 2 3 => + change (S.map (mkHom (op (f i))) ◁ ((S.mapComp (mkHom (pr₀₁_₀ f i j).op) (mkHom pr₀₁.op)).hom)).app X ≫ + (((S.mapComp (mkHom (f i).op) (mkHom (pullback.fst (f i) (f j)).op)).inv ▷ S.map (mkHom (pr₀₁.op))).app X) + + simp only [PrelaxFunctor.map₂_id, Cat.id_app, Category.id_comp, PrelaxFunctor.map₂_comp, + Cat.comp_app, Category.assoc, Functor.map_comp] + set f' := (fun j_1 ↦ f (fromDirection i j k j_1)) + -- set S' := S.mkFunctor + simp + -- sorry + +def canonical (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U : C) + {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) (X : S.mkCat U) + [(Presieve.ofArrows V f).HasTriplewisePullbacks] : + DescentData S U f where + toPreDescentData := canonicalAux S U f X + cocycle_condition i j k := by + apply Iso.ext + dsimp only [Iso.trans_hom] + dsimp [canonicalAux, cocycleMap₀₁, cocycleMap₁₂, cocycleMap₀₂] + dsimp [PreDescentData.cocycleMap] + simp only [PrelaxFunctor.map₂_id, Cat.id_app, Category.id_comp, PrelaxFunctor.map₂_comp, + Cat.comp_app, Category.assoc, Functor.map_comp] + simp? + sorry + -- cocycle_condition i j k := by + -- -- intro i j k + -- dsimp + -- simp only [PrelaxFunctor.map₂_comp, Cat.comp_app, Category.assoc, Functor.map_comp] + -- -- dsimp [mapCompObj] + -- simp_rw [← Functor.map_comp_assoc] + -- simp_rw [← NatTrans.comp_app_assoc] + -- simp_rw [← S.map₂_comp_assoc] + + -- sorry + +instance (U : C) : + (Presieve.ofArrows (fun (_ : Unit) ↦ U) (fun _ ↦ 𝟙 U)).HasTriplewisePullbacks where + has_pullbacks := by + intro Y Z f hf g hg + rw [Presieve.ofArrows_pUnit] at hf + cases hf + exact hasPullback_of_left_iso (𝟙 U) g + has_triplewise_pullbacks := by + intro X₁ X₂ X₃ f₁ hf₁ f₂ hf₂ f₃ hf₃ _ _ + rw [Presieve.ofArrows_pUnit] at hf₁ hf₂ hf₃ + cases hf₁; cases hf₂; cases hf₃ + exact hasPullback_of_right_iso (pullback.snd (𝟙 U) (𝟙 U)) (pullback.fst (𝟙 U) (𝟙 U)) + +def trivial (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U : C) (X : S.mkCat U) : + DescentData S U (fun (_ : Unit) ↦ 𝟙 U) where + X _ := (S.mkFunctor (𝟙 U)).obj X + φ _ _ := + (S.map₂Iso (Discrete.eqToIso' (by rw [fst_eq_snd_of_mono_eq (𝟙 U)]))).app ((S.mkFunctor (𝟙 U)).obj X) + -- Iso.refl _ + cocycle_condition := by + -- ext x + intro ⟨⟩ ⟨⟩ ⟨⟩ + + dsimp only [Iso.app_hom, Lean.Elab.WF.paramLet, mapCompObj] + dsimp only [mkFunctor] + simp only [Functor.mapIso_hom, eqToIso.hom, PrelaxFunctor.mapFunctor_map, Iso.app_inv, + Category.assoc] + simp_rw [← NatTrans.comp_app_assoc] + simp_rw [← NatTrans.comp_app] + simp only [Cat.comp_obj, NatTrans.comp_app, Category.assoc] + set Y := ((S.map (mkHom (op (𝟙 U)))).obj X) + + simp_rw [← NatTrans.comp_app_assoc] + simp_rw [← NatTrans.comp_app] + let α : S.map (mkHom ((pullback.fst (𝟙 U) (𝟙 U)).op)) ≅ + S.map (𝟙 _) ≫ S.map (mkHom (Quiver.Hom.op + (by apply (IsPullback.id_vert (𝟙 U)).lift (pullback.fst (𝟙 U) (𝟙 U)) (pullback.snd (𝟙 U) (𝟙 U)) (by simp only [Category.comp_id]; exact fst_eq_snd_of_mono_eq (𝟙 U))))) := by + apply _ ≪≫ S.mapComp _ _ + apply S.map₂Iso + apply _ ≪≫ whiskerRightIso (LocallyDiscrete.idIso _) _ + apply _ ≪≫ (LocallyDiscrete.compIso _ _ _) + apply Discrete.eqToIso' _ + apply congrArg op + have := (IsPullback.id_vert (𝟙 U)).lift_fst (pullback.fst (𝟙 U) (𝟙 U)) (pullback.snd (𝟙 U) (𝟙 U)) sorry + apply this.symm + dsimp at α + rw [Functor.app_hom] + erw [PrelaxFunctor.mapFunctor_map] + simp_rw [← NatTrans.comp_app_assoc] + simp_rw [← NatTrans.comp_app] + repeat rw [← eqToHom_app] + simp only [- eqToHom_app, Category.assoc] + repeat erw [← NatTrans.comp_app_assoc] + simp [- eqToHom_app, - NatTrans.comp_app] + simp [- NatTrans.comp_app] + repeat erw [← eqToHom_app] + repeat erw [← NatTrans.comp_app] + simp only [← Category.assoc] + repeat erw [← NatTrans.comp_app] + repeat erw [← NatTrans.comp_app_assoc] + simp only [Category.assoc] + dsimp only [mkFunctor] + repeat erw [← NatTrans.comp_app] + + -- simp + -- set Y := (S.map (mkHom (op (𝟙 U)))).obj X + -- simp only [mapCompObj, Iso.app_hom, eqToHom_map, Iso.app_inv] + erw [← NatTrans.comp_app] + dsimp + + dsimp [mkFunctor, pr₀₁, pr₁₂, pr₀₂] + simp? + have h2 : pullback.snd (𝟙 U) (𝟙 U) = 𝟙 U := by apply? + simp only [Functor.map_id, Functor.id_obj, eqToHom_refl, Iso.refl_hom, Category.id_comp, + Category.comp_id, Category.assoc] + +def can (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U : C) : + DescentData S U + +end DescentData + +end Pseudofunctor + +end CategoryTheory + +end From 3fb1e33e86d9b219e67d91bd269c402029145877 Mon Sep 17 00:00:00 2001 From: Yuma Mizuno Date: Sun, 14 Sep 2025 10:36:29 +0100 Subject: [PATCH 2/6] wip --- .../Bicategory/Functor/Pseudofunctor.lean | 97 ++- .../Bicategory/LocallyDiscrete.lean | 34 + Mathlib/CategoryTheory/Category/Cat.lean | 10 + Mathlib/CategoryTheory/Stack/Basic.lean | 17 +- Mathlib/CategoryTheory/Stack/Basic2.lean | 66 ++ Mathlib/CategoryTheory/Stack/Descent.lean | 696 +++++++++++------- Mathlib/CategoryTheory/Stack/Descent2.lean | 141 ++++ 7 files changed, 805 insertions(+), 256 deletions(-) create mode 100644 Mathlib/CategoryTheory/Stack/Basic2.lean create mode 100644 Mathlib/CategoryTheory/Stack/Descent2.lean diff --git a/Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean b/Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean index 0e262a1820188b..6fecd98b8a394e 100644 --- a/Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean +++ b/Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean @@ -155,7 +155,46 @@ 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} + +#check map₂_whisker_left + +lemma map₂_whisker_left_symm (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h) : + F.map f ◁ F.map₂ η = (F.mapComp f g).inv ≫ F.map₂ (f ◁ η) ≫ (F.mapComp f h).hom := by + simp + -- Proof goes here + +@[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 + +#check map₂_right_unitor + +@[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 +224,48 @@ 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_assoc_mapComp_inv {c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : + (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).hom ≫ (F.mapComp f (g ≫ h)).hom := by + simp + +@[reassoc, to_app] +lemma mapComp_assoc_inv_mapComp_inv {c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : + 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).inv ≫ (F.mapComp (f ≫ g) h).hom := by + simp [map₂_associator_inv] + +@[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 +322,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 51a9f87745e3d8..6a8f8c689b7ed0 100644 --- a/Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean +++ b/Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean @@ -88,6 +88,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 eqToHom_eq_of_hom {X Y : LocallyDiscrete C} {f g : X ⟶ Y} (η : f ⟶ g) : + η = eqToHom (eq_of_hom η) := + Subsingleton.elim _ _ + end LocallyDiscrete namespace LocallyDiscrete @@ -128,6 +132,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 index c73e604d216796..3300446f26441b 100644 --- a/Mathlib/CategoryTheory/Stack/Basic.lean +++ b/Mathlib/CategoryTheory/Stack/Basic.lean @@ -1,9 +1,4 @@ -import Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor -import Mathlib.CategoryTheory.Bicategory.LocallyDiscrete -import Mathlib.CategoryTheory.Category.Cat -import Mathlib.CategoryTheory.Sites.Grothendieck -import Mathlib.CategoryTheory.Sites.Sheaf -import Mathlib.CategoryTheory.Sites.Over +import Mathlib.CategoryTheory.Stack.Descent universe v u v₁ u₁ @@ -56,7 +51,13 @@ def homPreSheaf (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) ( map_comp := _ +open Pseudofunctor + variable {J : GrothendieckTopology C} -structure IsStack (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) where - isSheafOfHom : ∀ (U : C) (x y : S.obj ⟨op U⟩), Presieve.IsSheaf (J.over U) (homPreSheaf S U x y) +structure IsStack [Limits.HasPullbacks C] (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) where + is_sheaf_of_hom : ∀ (U : C) (x y : S.obj ⟨op U⟩), Presieve.IsSheaf (J.over U) (homPreSheaf S U x y) + is_descent_effective : ∀ (U : C) (R : Sieve U) (_ : R ∈ J.sieves U) + (d : S.DescentData U (fun i : Σ V, { f : V ⟶ U // R f } ↦ (i.2 : i.1 ⟶ U))), + ∃ X : S.obj ⟨op U⟩, + Nonempty (d ≅ DescentData.canonical S U (fun i : Σ V, { f : V ⟶ U // R f } ↦ (i.2 : i.1 ⟶ U)) X) diff --git a/Mathlib/CategoryTheory/Stack/Basic2.lean b/Mathlib/CategoryTheory/Stack/Basic2.lean new file mode 100644 index 00000000000000..49d6c11b5cab55 --- /dev/null +++ b/Mathlib/CategoryTheory/Stack/Basic2.lean @@ -0,0 +1,66 @@ +import Mathlib.CategoryTheory.Stack.Descent2 + +universe v u v₁ u₁ + +open CategoryTheory Opposite Bicategory Pseudofunctor LocallyDiscrete +open ProofWidgets Mathlib.Tactic.Widget + +variable {C : Type u} [Category.{v} C] + +@[simps] +def homPreSheaf (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U : C) (x y : S.mkCat U) : + Opposite (Over U) ⥤ Type v₁ where + obj V := (S.mkFunctor V.unop.hom).obj x ⟶ (S.mkFunctor V.unop.hom).obj y + map {V V'} g ϕ := + eqToHom (by simp) ≫ (S.mapCompCat V.unop.hom g.unop.left).hom.app x ≫ + (S.mkFunctor g.unop.left).map ϕ ≫ + (S.mapCompCat V.unop.hom g.unop.left).inv.app y ≫ eqToHom (by simp) + map_id := by + rintro ⟨X, _, f : X ⟶ U⟩ + 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 ⟨X, _, f : X ⟶ U⟩ ⟨Y, _, g : Y ⟶ U⟩ ⟨Z, _, h : Z ⟶ U⟩ ⟨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} + +structure IsStack (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) : Prop where + is_sheaf_of_hom (U : C) (x y : S.mkCat U) : + Presieve.IsSheaf (J.over U) (homPreSheaf S U x y) + is_descent_effective (U : C) (R : Sieve U) (_ : R ∈ J.sieves U) (d : S.DescentData R) : + ∃ x : S.mkCat U, Nonempty (d ≅ DescentData.canonical S x) diff --git a/Mathlib/CategoryTheory/Stack/Descent.lean b/Mathlib/CategoryTheory/Stack/Descent.lean index 2ddbc84313099e..74d19b3a4e56de 100644 --- a/Mathlib/CategoryTheory/Stack/Descent.lean +++ b/Mathlib/CategoryTheory/Stack/Descent.lean @@ -58,13 +58,13 @@ instance : OfNat Direction 0 := ⟨Direction.left⟩ instance : OfNat Direction 1 := ⟨Direction.middle⟩ instance : OfNat Direction 2 := ⟨Direction.right⟩ -instance : Coe (ℕ × ℕ) DirectionPair where - coe d := - match d with - | (0, 1) => DirectionPair.left_middle - | (1, 2) => DirectionPair.middle_right - | (0, 2) => DirectionPair.left_right - | _ => Inhabited.default +-- instance : Coe (ℕ × ℕ) DirectionPair where +-- coe d := +-- match d with +-- | (0, 1) => DirectionPair.left_middle +-- | (1, 2) => DirectionPair.middle_right +-- | (0, 2) => DirectionPair.left_right +-- | _ => Inhabited.default @[simp] def DirectionPair.fst : DirectionPair → Direction @@ -82,7 +82,7 @@ variable {V : Direction → C} (f : (i : Direction) → V i ⟶ U) variable {HasPullback : ∀ i j : Direction, HasPullback (f i) (f j)} variable [(Presieve.ofArrows V f).HasTriplewisePullbacks] -def pr (p : DirectionPair) : triplePullback (f 0) (f 1) (f 2) ⟶ pullback (f p.fst) (f p.snd) := +def proj₂ (p : DirectionPair) : triplePullback (f 0) (f 1) (f 2) ⟶ pullback (f p.fst) (f p.snd) := match p with | .left_middle => pullback.fst (pullback.snd (f 0) (f 1)) (pullback.fst (f 1) (f 2)) | .middle_right => pullback.snd (pullback.snd (f 0) (f 1)) (pullback.fst (f 1) (f 2)) @@ -96,55 +96,67 @@ def pr (p : DirectionPair) : triplePullback (f 0) (f 1) (f 2) ⟶ pullback (f p. rw [Category.assoc, pullback.condition, ← Category.assoc, pullback.condition, Category.assoc, pullback.condition, Category.assoc] -def prToSingle (i : Direction) : +def proj₁ (i : Direction) : triplePullback (f 0) (f 1) (f 2) ⟶ V i := match i with - | 0 => pr f .left_middle ≫ pullback.fst (f 0) (f 1) - | 1 => pr f .left_middle ≫ pullback.snd (f 0) (f 1) - | 2 => pr f .middle_right ≫ pullback.snd (f 1) (f 2) + | 0 => proj₂ f .left_middle ≫ pullback.fst (f 0) (f 1) + | 1 => proj₂ f .left_middle ≫ pullback.snd (f 0) (f 1) + | 2 => proj₂ f .middle_right ≫ pullback.snd (f 1) (f 2) + +theorem proj₁_fst {ij : DirectionPair} : + proj₁ f ij.fst = proj₂ f ij ≫ pullback.fst (f ij.fst) (f ij.snd) := by + cases ij + case left_middle => rfl + case middle_right => exact pullback.condition + case left_right => simp [proj₁, proj₂] + +theorem proj₁_snd {ij : DirectionPair} : + proj₁ f ij.snd = proj₂ f ij ≫ pullback.snd (f ij.fst) (f ij.snd) := by + cases ij + all_goals simp [proj₁, proj₂] variable {U : C} {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) variable [(Presieve.ofArrows V f).HasTriplewisePullbacks] -def pr₀₁₂_₀₁ (i j k : I) : - triplePullback (f i) (f j) (f k) ⟶ pullback (f i) (f j) := - pullback.fst (pullback.snd (f i) (f j)) (pullback.fst (f j) (f k)) +-- def pr₀₁₂_₀₁ (i j k : I) : +-- triplePullback (f i) (f j) (f k) ⟶ pullback (f i) (f j) := +-- pullback.fst (pullback.snd (f i) (f j)) (pullback.fst (f j) (f k)) -def pr₀₁₂_₁₂ (i j k : I) : - triplePullback (f i) (f j) (f k) ⟶ pullback (f j) (f k) := - pullback.snd (pullback.snd (f i) (f j)) (pullback.fst (f j) (f k)) +-- def pr₀₁₂_₁₂ (i j k : I) : +-- triplePullback (f i) (f j) (f k) ⟶ pullback (f j) (f k) := +-- pullback.snd (pullback.snd (f i) (f j)) (pullback.fst (f j) (f k)) -def pr₀₁₂_₀₂ (i j k : I) : - triplePullback (f i) (f j) (f k) ⟶ pullback (f i) (f k) := - pullback.lift (pr₀₁₂_₀₁ f i j k ≫ pullback.fst (f i) (f j)) - (pr₀₁₂_₁₂ f i j k ≫ pullback.snd (f j) (f k)) <| by - dsimp only [pr₀₁₂_₀₁, pr₀₁₂_₁₂] - rw [Category.assoc, pullback.condition, ← Category.assoc, pullback.condition, - Category.assoc, pullback.condition, Category.assoc] +-- def pr₀₁₂_₀₂ (i j k : I) : +-- triplePullback (f i) (f j) (f k) ⟶ pullback (f i) (f k) := +-- pullback.lift (pr₀₁₂_₀₁ f i j k ≫ pullback.fst (f i) (f j)) +-- (pr₀₁₂_₁₂ f i j k ≫ pullback.snd (f j) (f k)) <| by +-- dsimp only [pr₀₁₂_₀₁, pr₀₁₂_₁₂] +-- rw [Category.assoc, pullback.condition, ← Category.assoc, pullback.condition, +-- Category.assoc, pullback.condition, Category.assoc] -abbrev pr₀₁_₀ (i j : I) : - pullback (f i) (f j) ⟶ V i := - pullback.fst (f i) (f j) +-- abbrev pr₀₁_₀ (i j : I) : +-- pullback (f i) (f j) ⟶ V i := +-- pullback.fst (f i) (f j) -abbrev pr₀₁_₁ (i j : I) : - pullback (f i) (f j) ⟶ V j := - pullback.snd (f i) (f j) +-- abbrev pr₀₁_₁ (i j : I) : +-- pullback (f i) (f j) ⟶ V j := +-- pullback.snd (f i) (f j) -abbrev pr₁₂_₁ (j k : I) : - pullback (f j) (f k) ⟶ V j := - pullback.fst (f j) (f k) +-- abbrev pr₁₂_₁ (j k : I) : +-- pullback (f j) (f k) ⟶ V j := +-- pullback.fst (f j) (f k) -abbrev pr₁₂_₂ (j k : I) : - pullback (f j) (f k) ⟶ V k := - pullback.snd (f j) (f k) +-- abbrev pr₁₂_₂ (j k : I) : +-- pullback (f j) (f k) ⟶ V k := +-- pullback.snd (f j) (f k) -abbrev pr₀₂_₀ (i k : I) : - pullback (f i) (f k) ⟶ V i := - pullback.fst (f i) (f k) +-- abbrev pr₀₂_₀ (i k : I) : +-- pullback (f i) (f k) ⟶ V i := +-- pullback.fst (f i) (f k) -abbrev pr₀₂_₂ (i k : I) : - pullback (f i) (f k) ⟶ V k := - pullback.snd (f i) (f k) +-- abbrev pr₀₂_₂ (i k : I) : +-- pullback (f i) (f k) ⟶ V k := +-- pullback.snd (f i) (f k) -- theorem pullback_condition₀ (i j k : I) : -- pr₀₁₂_₀₁ f i j k ≫ pr₀₁_₀ f i j = pr₀₁₂_₀₂ f i j k ≫ pr₀₂_₀ f i k := by @@ -158,40 +170,40 @@ abbrev pr₀₂_₂ (i k : I) : -- pr₀₁₂_₀₂ f i j k ≫ pr₀₂_₂ f i k = pr₀₁₂_₁₂ f i j k ≫ pr₁₂_₂ f j k := by -- simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app, pr₀₁₂_₀₂, pr₀₁₂_₀₂, pr₀₁₂_₁₂] -def pr₀₁₂_₀ (i j k : I) : triplePullback (f i) (f j) (f k) ⟶ V i := - pr₀₁₂_₀₁ f i j k ≫ pr₀₁_₀ f i j +-- def pr₀₁₂_₀ (i j k : I) : triplePullback (f i) (f j) (f k) ⟶ V i := +-- pr₀₁₂_₀₁ f i j k ≫ pr₀₁_₀ f i j -theorem pr₀₁₂_₀_def₀₁ {i j k : I} : - pr₀₁₂_₀ f i j k = pr₀₁₂_₀₁ f i j k ≫ pr₀₁_₀ f i j := - rfl +-- theorem pr₀₁₂_₀_def₀₁ {i j k : I} : +-- pr₀₁₂_₀ f i j k = pr₀₁₂_₀₁ f i j k ≫ pr₀₁_₀ f i j := +-- rfl -theorem pr₀₁₂_₀_def₀₂ {i j k : I} : - pr₀₁₂_₀ f i j k = pr₀₁₂_₀₂ f i j k ≫ pr₀₂_₀ f i k := by - simp only [pr₀₁₂_₀_def₀₁, pr₀₁₂_₀₁, pr₀₁₂_₀₂, limit.lift_π, PullbackCone.mk_pt, - PullbackCone.mk_π_app] +-- theorem pr₀₁₂_₀_def₀₂ {i j k : I} : +-- pr₀₁₂_₀ f i j k = pr₀₁₂_₀₂ f i j k ≫ pr₀₂_₀ f i k := by +-- simp only [pr₀₁₂_₀_def₀₁, pr₀₁₂_₀₁, pr₀₁₂_₀₂, limit.lift_π, PullbackCone.mk_pt, +-- PullbackCone.mk_π_app] -def pr₀₁₂_₁ (i j k : I) : triplePullback (f i) (f j) (f k) ⟶ V j := - pr₀₁₂_₀₁ f i j k ≫ pr₀₁_₁ f i j +-- def pr₀₁₂_₁ (i j k : I) : triplePullback (f i) (f j) (f k) ⟶ V j := +-- pr₀₁₂_₀₁ f i j k ≫ pr₀₁_₁ f i j -theorem pr₀₁₂_₁_def₀₁ {i j k : I} : - pr₀₁₂_₁ f i j k = pr₀₁₂_₀₁ f i j k ≫ pr₀₁_₁ f i j := - rfl +-- theorem pr₀₁₂_₁_def₀₁ {i j k : I} : +-- pr₀₁₂_₁ f i j k = pr₀₁₂_₀₁ f i j k ≫ pr₀₁_₁ f i j := +-- rfl -theorem pr₀₁₂_₁_def₁₂ {i j k : I} : - pr₀₁₂_₁ f i j k = pr₀₁₂_₁₂ f i j k ≫ pr₁₂_₁ f j k := - pullback.condition +-- theorem pr₀₁₂_₁_def₁₂ {i j k : I} : +-- pr₀₁₂_₁ f i j k = pr₀₁₂_₁₂ f i j k ≫ pr₁₂_₁ f j k := +-- pullback.condition -def pr₀₁₂_₂ (i j k : I) : triplePullback (f i) (f j) (f k) ⟶ V k := - pr₀₁₂_₁₂ f i j k ≫ pr₁₂_₂ f j k +-- def pr₀₁₂_₂ (i j k : I) : triplePullback (f i) (f j) (f k) ⟶ V k := +-- pr₀₁₂_₁₂ f i j k ≫ pr₁₂_₂ f j k -theorem pr₀₁₂_₂_def₁₂ {i j k : I} : - pr₀₁₂_₂ f i j k = pr₀₁₂_₁₂ f i j k ≫ pr₁₂_₂ f j k := - rfl +-- theorem pr₀₁₂_₂_def₁₂ {i j k : I} : +-- pr₀₁₂_₂ f i j k = pr₀₁₂_₁₂ f i j k ≫ pr₁₂_₂ f j k := +-- rfl -theorem pr₀₁₂_₂_def₀₂ {i j k : I} : - pr₀₁₂_₂ f i j k = pr₀₁₂_₀₂ f i j k ≫ pr₀₂_₂ f i k := by - simp only [pr₀₁₂_₂_def₁₂, pr₀₁₂_₁₂, pr₀₁₂_₀₂, limit.lift_π, PullbackCone.mk_pt, - PullbackCone.mk_π_app] +-- theorem pr₀₁₂_₂_def₀₂ {i j k : I} : +-- pr₀₁₂_₂ f i j k = pr₀₁₂_₀₂ f i j k ≫ pr₀₂_₂ f i k := by +-- simp only [pr₀₁₂_₂_def₁₂, pr₀₁₂_₁₂, pr₀₁₂_₀₂, limit.lift_π, PullbackCone.mk_pt, +-- PullbackCone.mk_π_app] end TriplePullback @@ -201,7 +213,7 @@ open TriplePullback -- set_option pp.universes true -def mkCat (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (X : C) : Cat := +abbrev mkCat (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (X : C) : Cat := S.obj ⟨op X⟩ -- def mkFunctor (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) {X Y : C} (f : Y ⟶ X) : @@ -213,21 +225,29 @@ def mkCat (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (X : C) abbrev mkFunctor (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) {X Y : C} (f : Y ⟶ X) : S.mkCat X ⟶ S.mkCat Y := - S.map (LocallyDiscrete.mkHom (op f)) + S.map (LocallyDiscrete.mkHom f.op) + +#check Pseudofunctor.mapComp + +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) -- @[to_app?] -- @[simps!?] -abbrev mapCompObj (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) {X Y Z : C} +abbrev mapCompCatApp (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) {X Y Z : C} (f : Y ⟶ X) (g : Z ⟶ Y) {x : S.mkCat X} : (S.mkFunctor (g ≫ f)).obj x ≅ (S.mkFunctor g).obj ((S.mkFunctor f).obj x) := - (S.mapComp (mkHom (op f)) (mkHom (op g))).app x + (mapCompCat S f g).app x structure PreDescentData (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U : C) {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) [(Presieve.ofArrows V f).HasTriplewisePullbacks] where /-- An object `Xᵢ` of `S Vᵢ` for each `i : I`. -/ X : ∀ i, S.obj ⟨op (V i)⟩ - /-- An isomorphism `φᵢⱼ : pr₀* Xᵢ ≅ pr₁* Xⱼ` for each `i j : I`. -/ + /-- An isomorphism `φᵢⱼ : pr₀* Xᵢ ≅ pr₁* Xⱼ` for each `i j : I`, where `pr₀` and `pr₁` + are the projections from the pullback. -/ φ : ∀ i j : I, (S.mkFunctor (pullback.fst (f i) (f j))).obj (X i) ≅ (S.mkFunctor (pullback.snd (f i) (f j))).obj (X j) @@ -258,84 +278,84 @@ instance {ι : Direction → I} : (Presieve.ofArrows (fun j ↦ V (ι j)) fun j ↦ f (ι j)).HasTriplewisePullbacks := sorry def cocycleMap (d : PreDescentData S U f) (ι : Direction → I) (ij : DirectionPair) : - (S.mkFunctor (prToSingle (fun j ↦ f (ι j)) ij.fst)).obj (d.X (ι ij.fst)) ≅ - (S.mkFunctor (prToSingle (fun j ↦ f (ι j)) ij.snd)).obj (d.X (ι ij.snd)) := + (S.mkFunctor (proj₁ (fun j ↦ f (ι j)) ij.fst)).obj (d.X (ι ij.fst)) ≅ + (S.mkFunctor (proj₁ (fun j ↦ f (ι j)) ij.snd)).obj (d.X (ι ij.snd)) := let f' := fun j ↦ f (ι j) let i := ij.fst let j := ij.snd calc - (S.mkFunctor (prToSingle f' i)).obj (d.X (ι i)) ≅ - (S.mkFunctor (pr f' ij ≫ pr₀₁_₀ f (ι i) (ι j))).obj (d.X (ι i)) := - (S.map₂Iso (Discrete.eqToIso' (congrArg op sorry))).app (d.X (ι i)) - _ ≅ (S.mkFunctor (pr₀₁_₀ f (ι i) (ι j)) ≫ S.mkFunctor (pr f' ij)).obj (d.X (ι i)) := - (S.mapComp (mkHom ((pr₀₁_₀ f (ι i) (ι j)).op)) (mkHom ((pr f' ij).op))).app (d.X (ι i)) - _ ≅ (S.mkFunctor (pr₀₁_₁ f (ι i) (ι j)) ≫ S.mkFunctor (pr f' ij)).obj (d.X (ι j)) := + (S.mkFunctor (proj₁ f' i)).obj (d.X (ι i)) ≅ + (S.mkFunctor (proj₂ f' ij ≫ pullback.fst (f (ι i)) (f (ι j)))).obj (d.X (ι i)) := + (S.map₂Iso (Discrete.eqToIso' (congrArg op (proj₁_fst f')))).app (d.X (ι i)) + _ ≅ (S.mkFunctor (pullback.fst (f (ι i)) (f (ι j))) ≫ S.mkFunctor (proj₂ f' ij)).obj (d.X (ι i)) := + (S.mapCompCat (pullback.fst (f (ι i)) (f (ι j))) (proj₂ f' ij)).app (d.X (ι i)) + _ ≅ (S.mkFunctor (pullback.snd (f (ι i)) (f (ι j))) ≫ S.mkFunctor (proj₂ f' ij)).obj (d.X (ι j)) := /- Here is the main part. -/ - (S.mkFunctor (pr f' ij)).mapIso (d.φ (ι i) (ι j)) - _ ≅ (S.mkFunctor ((pr f' ij) ≫ pr₀₁_₁ f (ι i) (ι j))).obj (d.X (ι j)) := - (S.mapComp (mkHom ((pr₀₁_₁ f (ι i) (ι j)).op)) (mkHom ((pr f' ij).op))).symm.app (d.X (ι j)) - _ ≅ (S.mkFunctor (prToSingle f' j)).obj (d.X (ι j)) := - (S.map₂Iso (Discrete.eqToIso' (congrArg op sorry))).symm.app (d.X (ι j)) - -def cocycleMapAux (d : PreDescentData S U f) (ι : Direction → I) (ij : DirectionPair) : - (S.mkFunctor (prToSingle (fun j ↦ f (ι j)) ij.fst)) ≅ - (S.mkFunctor (pr₀₁_₀ f (ι ij.fst) (ι ij.snd)) ≫ S.mkFunctor (pr (fun j ↦ f (ι j)) ij)) := - let f' := fun j ↦ f (ι j) - let i := ij.fst - let j := ij.snd - calc - (S.mkFunctor (prToSingle f' i)) ≅ (S.mkFunctor (pr f' ij ≫ pr₀₁_₀ f (ι i) (ι j))) := - (S.map₂Iso (Discrete.eqToIso' (congrArg op sorry))) - _ ≅ (S.mkFunctor (pr₀₁_₀ f (ι i) (ι j)) ≫ S.mkFunctor (pr f' ij)) := - (S.mapComp (mkHom ((pr₀₁_₀ f (ι i) (ι j)).op)) (mkHom ((pr f' ij).op))) - -def cocycleMap₀₁ (d : PreDescentData S U f) (i j k : I) : - (S.mkFunctor (pr₀₁₂_₀ f i j k)).obj (d.X i) ≅ (S.mkFunctor (pr₀₁₂_₁ f i j k)).obj (d.X j) := - calc - (S.mkFunctor (pr₀₁₂_₀ f i j k)).obj (d.X i) ≅ - (S.mkFunctor (pr₀₁₂_₀₁ f i j k ≫ pr₀₁_₀ f i j)).obj (d.X i) := - (S.map₂Iso (Discrete.eqToIso' (congrArg op (pr₀₁₂_₀_def₀₁ f)))).app (d.X i) - _ ≅ (S.mkFunctor (pr₀₁_₀ f i j) ≫ S.mkFunctor (pr₀₁₂_₀₁ f i j k)).obj (d.X i) := - (S.mapComp (mkHom ((pr₀₁_₀ f i j).op)) (mkHom ((pr₀₁₂_₀₁ f i j k).op))).app (d.X i) - _ ≅ (S.mkFunctor (pr₀₁_₁ f i j) ≫ S.mkFunctor (pr₀₁₂_₀₁ f i j k)).obj (d.X j) := - /- Here is the main part. -/ - (S.mkFunctor (pr₀₁₂_₀₁ f i j k)).mapIso (d.φ i j) - _ ≅ (S.mkFunctor ((pr₀₁₂_₀₁ f i j k) ≫ pr₀₁_₁ f i j)).obj (d.X j) := - (S.mapComp (mkHom ((pr₀₁_₁ f i j).op)) (mkHom ((pr₀₁₂_₀₁ f i j k).op))).symm.app (d.X j) - _ ≅ (S.mkFunctor (pr₀₁₂_₁ f i j k)).obj (d.X j) := - (S.map₂Iso (Discrete.eqToIso' (congrArg op (pr₀₁₂_₁_def₀₁ f)))).symm.app (d.X j) - -def cocycleMap₁₂ (d : PreDescentData S U f) (i j k : I) : - (S.mkFunctor (pr₀₁₂_₁ f i j k)).obj (d.X j) ≅ (S.mkFunctor (pr₀₁₂_₂ f i j k)).obj (d.X k) := - calc - (S.mkFunctor (pr₀₁₂_₁ f i j k)).obj (d.X j) ≅ - (S.mkFunctor (pr₀₁₂_₁₂ f i j k ≫ pr₁₂_₁ f j k)).obj (d.X j) := - (S.map₂Iso (Discrete.eqToIso' (congrArg op (pr₀₁₂_₁_def₁₂ f)))).app (d.X j) - _ ≅ (S.mkFunctor (pr₁₂_₁ f j k) ≫ S.mkFunctor (pr₀₁₂_₁₂ f i j k)).obj (d.X j) := - (S.mapComp (mkHom ((pr₁₂_₁ f j k).op)) (mkHom ((pr₀₁₂_₁₂ f i j k).op))).app (d.X j) - _ ≅ (S.mkFunctor (pr₁₂_₂ f j k) ≫ S.mkFunctor (pr₀₁₂_₁₂ f i j k)).obj (d.X k) := - /- Here is the main part. -/ - (S.mkFunctor (pr₀₁₂_₁₂ f i j k)).mapIso (d.φ j k) - _ ≅ (S.mkFunctor ((pr₀₁₂_₁₂ f i j k) ≫ pr₁₂_₂ f j k)).obj (d.X k) := - (S.mapComp (mkHom ((pr₁₂_₂ f j k).op)) (mkHom ((pr₀₁₂_₁₂ f i j k).op))).symm.app (d.X k) - _ ≅ (S.mkFunctor (pr₀₁₂_₂ f i j k)).obj (d.X k) := - (S.map₂Iso (Discrete.eqToIso' (congrArg op (pr₀₁₂_₂_def₁₂ f)))).symm.app (d.X k) - -def cocycleMap₀₂ (d : PreDescentData S U f) (i j k : I) : - (S.mkFunctor (pr₀₁₂_₀ f i j k)).obj (d.X i) ≅ (S.mkFunctor (pr₀₁₂_₂ f i j k)).obj (d.X k) := - calc - (S.mkFunctor (pr₀₁₂_₀ f i j k)).obj (d.X i) ≅ - (S.mkFunctor (pr₀₁₂_₀₂ f i j k ≫ pr₀₂_₀ f i k)).obj (d.X i) := - (S.map₂Iso (Discrete.eqToIso' (congrArg op (pr₀₁₂_₀_def₀₂ f)))).app (d.X i) - _ ≅ (S.mkFunctor (pr₀₂_₀ f i k) ≫ S.mkFunctor (pr₀₁₂_₀₂ f i j k)).obj (d.X i) := - (S.mapComp (mkHom ((pr₀₂_₀ f i k).op)) (mkHom ((pr₀₁₂_₀₂ f i j k).op))).app (d.X i) - _ ≅ (S.mkFunctor (pr₀₂_₂ f i k) ≫ S.mkFunctor (pr₀₁₂_₀₂ f i j k)).obj (d.X k) := - /- Here is the main part. -/ - (S.mkFunctor (pr₀₁₂_₀₂ f i j k)).mapIso (d.φ i k) - _ ≅ (S.mkFunctor ((pr₀₁₂_₀₂ f i j k) ≫ pr₀₂_₂ f i k)).obj (d.X k) := - (S.mapComp (mkHom ((pr₀₂_₂ f i k).op)) (mkHom ((pr₀₁₂_₀₂ f i j k).op))).symm.app (d.X k) - _ ≅ (S.mkFunctor (pr₀₁₂_₂ f i j k)).obj (d.X k) := - (S.map₂Iso (Discrete.eqToIso' (congrArg op (pr₀₁₂_₂_def₀₂ f)))).symm.app (d.X k) + (S.mkFunctor (proj₂ f' ij)).mapIso (d.φ (ι i) (ι j)) + _ ≅ (S.mkFunctor ((proj₂ f' ij) ≫ pullback.snd (f (ι i)) (f (ι j)))).obj (d.X (ι j)) := + (S.mapCompCat (pullback.snd (f (ι i)) (f (ι j))) (proj₂ f' ij)).symm.app (d.X (ι j)) + _ ≅ (S.mkFunctor (proj₁ f' j)).obj (d.X (ι j)) := + (S.map₂Iso (Discrete.eqToIso' (congrArg op (proj₁_snd f')))).symm.app (d.X (ι j)) + +-- def cocycleMapAux (d : PreDescentData S U f) (ι : Direction → I) (ij : DirectionPair) : +-- (S.mkFunctor (proj₁ (fun j ↦ f (ι j)) ij.fst)) ≅ +-- (S.mkFunctor (pr₀₁_₀ f (ι ij.fst) (ι ij.snd)) ≫ S.mkFunctor (proj₂ (fun j ↦ f (ι j)) ij)) := +-- let f' := fun j ↦ f (ι j) +-- let i := ij.fst +-- let j := ij.snd +-- calc +-- (S.mkFunctor (proj₁ f' i)) ≅ (S.mkFunctor (proj₂ f' ij ≫ pr₀₁_₀ f (ι i) (ι j))) := +-- (S.map₂Iso (Discrete.eqToIso' (congrArg op sorry))) +-- _ ≅ (S.mkFunctor (pr₀₁_₀ f (ι i) (ι j)) ≫ S.mkFunctor (proj₂ f' ij)) := +-- (S.mapComp (mkHom ((pr₀₁_₀ f (ι i) (ι j)).op)) (mkHom ((proj₂ f' ij).op))) + +-- def cocycleMap₀₁ (d : PreDescentData S U f) (i j k : I) : +-- (S.mkFunctor (pr₀₁₂_₀ f i j k)).obj (d.X i) ≅ (S.mkFunctor (pr₀₁₂_₁ f i j k)).obj (d.X j) := +-- calc +-- (S.mkFunctor (pr₀₁₂_₀ f i j k)).obj (d.X i) ≅ +-- (S.mkFunctor (pr₀₁₂_₀₁ f i j k ≫ pr₀₁_₀ f i j)).obj (d.X i) := +-- (S.map₂Iso (Discrete.eqToIso' (congrArg op (pr₀₁₂_₀_def₀₁ f)))).app (d.X i) +-- _ ≅ (S.mkFunctor (pr₀₁_₀ f i j) ≫ S.mkFunctor (pr₀₁₂_₀₁ f i j k)).obj (d.X i) := +-- (S.mapComp (mkHom ((pr₀₁_₀ f i j).op)) (mkHom ((pr₀₁₂_₀₁ f i j k).op))).app (d.X i) +-- _ ≅ (S.mkFunctor (pr₀₁_₁ f i j) ≫ S.mkFunctor (pr₀₁₂_₀₁ f i j k)).obj (d.X j) := +-- /- Here is the main part. -/ +-- (S.mkFunctor (pr₀₁₂_₀₁ f i j k)).mapIso (d.φ i j) +-- _ ≅ (S.mkFunctor ((pr₀₁₂_₀₁ f i j k) ≫ pr₀₁_₁ f i j)).obj (d.X j) := +-- (S.mapComp (mkHom ((pr₀₁_₁ f i j).op)) (mkHom ((pr₀₁₂_₀₁ f i j k).op))).symm.app (d.X j) +-- _ ≅ (S.mkFunctor (pr₀₁₂_₁ f i j k)).obj (d.X j) := +-- (S.map₂Iso (Discrete.eqToIso' (congrArg op (pr₀₁₂_₁_def₀₁ f)))).symm.app (d.X j) + +-- def cocycleMap₁₂ (d : PreDescentData S U f) (i j k : I) : +-- (S.mkFunctor (pr₀₁₂_₁ f i j k)).obj (d.X j) ≅ (S.mkFunctor (pr₀₁₂_₂ f i j k)).obj (d.X k) := +-- calc +-- (S.mkFunctor (pr₀₁₂_₁ f i j k)).obj (d.X j) ≅ +-- (S.mkFunctor (pr₀₁₂_₁₂ f i j k ≫ pr₁₂_₁ f j k)).obj (d.X j) := +-- (S.map₂Iso (Discrete.eqToIso' (congrArg op (pr₀₁₂_₁_def₁₂ f)))).app (d.X j) +-- _ ≅ (S.mkFunctor (pr₁₂_₁ f j k) ≫ S.mkFunctor (pr₀₁₂_₁₂ f i j k)).obj (d.X j) := +-- (S.mapComp (mkHom ((pr₁₂_₁ f j k).op)) (mkHom ((pr₀₁₂_₁₂ f i j k).op))).app (d.X j) +-- _ ≅ (S.mkFunctor (pr₁₂_₂ f j k) ≫ S.mkFunctor (pr₀₁₂_₁₂ f i j k)).obj (d.X k) := +-- /- Here is the main part. -/ +-- (S.mkFunctor (pr₀₁₂_₁₂ f i j k)).mapIso (d.φ j k) +-- _ ≅ (S.mkFunctor ((pr₀₁₂_₁₂ f i j k) ≫ pr₁₂_₂ f j k)).obj (d.X k) := +-- (S.mapComp (mkHom ((pr₁₂_₂ f j k).op)) (mkHom ((pr₀₁₂_₁₂ f i j k).op))).symm.app (d.X k) +-- _ ≅ (S.mkFunctor (pr₀₁₂_₂ f i j k)).obj (d.X k) := +-- (S.map₂Iso (Discrete.eqToIso' (congrArg op (pr₀₁₂_₂_def₁₂ f)))).symm.app (d.X k) + +-- def cocycleMap₀₂ (d : PreDescentData S U f) (i j k : I) : +-- (S.mkFunctor (pr₀₁₂_₀ f i j k)).obj (d.X i) ≅ (S.mkFunctor (pr₀₁₂_₂ f i j k)).obj (d.X k) := +-- calc +-- (S.mkFunctor (pr₀₁₂_₀ f i j k)).obj (d.X i) ≅ +-- (S.mkFunctor (pr₀₁₂_₀₂ f i j k ≫ pr₀₂_₀ f i k)).obj (d.X i) := +-- (S.map₂Iso (Discrete.eqToIso' (congrArg op (pr₀₁₂_₀_def₀₂ f)))).app (d.X i) +-- _ ≅ (S.mkFunctor (pr₀₂_₀ f i k) ≫ S.mkFunctor (pr₀₁₂_₀₂ f i j k)).obj (d.X i) := +-- (S.mapComp (mkHom ((pr₀₂_₀ f i k).op)) (mkHom ((pr₀₁₂_₀₂ f i j k).op))).app (d.X i) +-- _ ≅ (S.mkFunctor (pr₀₂_₂ f i k) ≫ S.mkFunctor (pr₀₁₂_₀₂ f i j k)).obj (d.X k) := +-- /- Here is the main part. -/ +-- (S.mkFunctor (pr₀₁₂_₀₂ f i j k)).mapIso (d.φ i k) +-- _ ≅ (S.mkFunctor ((pr₀₁₂_₀₂ f i j k) ≫ pr₀₂_₂ f i k)).obj (d.X k) := +-- (S.mapComp (mkHom ((pr₀₂_₂ f i k).op)) (mkHom ((pr₀₁₂_₀₂ f i j k).op))).symm.app (d.X k) +-- _ ≅ (S.mkFunctor (pr₀₁₂_₂ f i j k)).obj (d.X k) := +-- (S.map₂Iso (Discrete.eqToIso' (congrArg op (pr₀₁₂_₂_def₀₂ f)))).symm.app (d.X k) #check op_comp @@ -385,11 +405,11 @@ structure DescentData (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u toPreDescentData.cocycleMap (fromDirection i j k) .left_right -- let φ₁₂ := - -- (mapCompObj _ _ _).hom ≫ (S.mkFunctor (pr₁₂ f i j k)).map (φ j k).hom ≫ (mapCompObj _ _ _).inv + -- (mapCompCatApp _ _ _).hom ≫ (S.mkFunctor (pr₁₂ f i j k)).map (φ j k).hom ≫ (mapCompCatApp _ _ _).inv -- let φ₀₂ := - -- (mapCompObj _ _ _).hom ≫ (S.mkFunctor (pr₀₂ f i j k)).map (φ i k).hom ≫ (mapCompObj _ _ _).inv + -- (mapCompCatApp _ _ _).hom ≫ (S.mkFunctor (pr₀₂ f i j k)).map (φ i k).hom ≫ (mapCompCatApp _ _ _).inv -- let φ₀₁ := - -- (mapCompObj _ _ _).hom ≫ (S.mkFunctor (pr₀₁ f i j k)).map (φ i j).hom ≫ (mapCompObj _ _ _).inv + -- (mapCompCatApp _ _ _).hom ≫ (S.mkFunctor (pr₀₁ f i j k)).map (φ i j).hom ≫ (mapCompCatApp _ _ _).inv -- φ₀₁ ≫ -- (S.map₂ (Discrete.eqToHom' (by rw [pullback_condition₁]))).app (X j) ≫ φ₁₂ = -- (S.map₂ (Discrete.eqToHom' (by rw [pullback_condition₀]))).app (X i) ≫ @@ -398,11 +418,41 @@ structure DescentData (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u namespace DescentData -export PreDescentData (cocycleMap₀₁ cocycleMap₁₂ cocycleMap₀₂ cocycleMap) +export PreDescentData (cocycleMap) -- PreDescentData.cocycleMap₁₂ -- PreDescentData.cocycleMap₀₂ --- attribute [local simp] eqToHom_map +variable {S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}} {U : C} + {I : Type v₂} {V : I → C} {f : (i : I) → V i ⟶ U} + [(Presieve.ofArrows V f).HasTriplewisePullbacks] + +@[ext] +structure Hom (d₁ d₂ : DescentData S U f) where + /-- A morphism in `S Vᵢ` for each `i : I`. -/ + hom : ∀ i, d₁.X i ⟶ d₂.X i + /-- The squares involving the `φᵢⱼ` commute. -/ + comm : ∀ i j : I, + (S.mkFunctor (pullback.fst (f i) (f j))).map (hom i) ≫ (d₂.φ i j).hom = + (d₁.φ i j).hom ≫ (S.mkFunctor (pullback.snd (f i) (f j))).map (hom j) + +attribute [reassoc] Hom.comm + +@[simps] +def Hom.id (d : DescentData S U f) : Hom d d where + hom i := 𝟙 (d.X i) + comm i j := by simp + +@[simps] +def Hom.comp {d₁ d₂ d₃ : DescentData S U f} (f : Hom d₁ d₂) (g : Hom d₂ d₃) : Hom d₁ d₃ where + hom i := f.hom i ≫ g.hom i + comm i j := by simp [g.comm, f.comm_assoc] + +-- attribute [local simp] Hom.comm Hom.comm_assoc + +instance : Category (DescentData S U f) where + Hom := Hom + id d := Hom.id d + comp f g := Hom.comp f g def canonicalAux (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U : C) {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) @@ -411,44 +461,239 @@ def canonicalAux (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) X i := (S.mkFunctor (f i)).obj X φ i j := ((S.mapComp (mkHom (f i).op) (mkHom (pullback.fst (f i) (f j)).op)).symm ≪≫ - S.map₂Iso - ((compIso (f i).op (pullback.fst (f i) (f j)).op).symm ≪≫ - Discrete.eqToIso' (congrArg op pullback.condition) ≪≫ - compIso (f j).op (pullback.snd (f i) (f j)).op) ≪≫ + S.map₂Iso (Discrete.eqToIso' (congrArg op pullback.condition)) ≪≫ + -- ((compIso (f i).op (pullback.fst (f i) (f j)).op).symm ≪≫ + -- Discrete.eqToIso' (congrArg op pullback.condition) ≪≫ + -- compIso (f j).op (pullback.snd (f i) (f j)).op) ≪≫ S.mapComp (mkHom (f j).op) (mkHom (pullback.snd (f i) (f j)).op)).app X open DirectionPair #check Pseudofunctor.map₂_associator_app +example {B : Type} [Bicategory B] + (self : Pseudofunctor B Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(self.obj a)) : + (self.map₂ (α_ f g h).hom).app X = + (self.mapComp (f ≫ g) h).hom.app X ≫ + (self.map h).map ((self.mapComp f g).hom.app X) ≫ + (α_ (self.map f) (self.map g) (self.map h)).hom.app X ≫ + (self.mapComp g h).inv.app ((self.map f).obj X) ≫ (self.mapComp f (g ≫ h)).inv.app X := by + dsimp only [Cat.comp_obj] + apply Pseudofunctor.map₂_associator_app + variable {D E E' : Type} [Category D] [Category E][Category E'] variable (F G H : C ⥤ D) {G : D ⥤ E} {H : E ⥤ E'} {X : C} #check (H.obj (G.obj (F.obj X))) + example (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U : C) {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) [(Presieve.ofArrows V f).HasTriplewisePullbacks] (X : S.mkCat U) (i j k : I) (p : DirectionPair) : - (canonicalAux S U f X).cocycleMap (fromDirection i j k) .left_middle = sorry := by - apply Iso.ext - dsimp only [fromDirection_left, fromDirection_middle, fromDirection_right, fst, canonicalAux, snd, - cocycleMap, - Cat.comp_obj, - eqToIso_refl, Iso.trans_def, Iso.trans_hom, Iso.app_hom, - Functor.mapIso_hom, Iso.refl_hom, PrelaxFunctor.mapFunctor_map, Iso.symm_hom, - eqToIso.hom, - NatTrans.comp_app, Functor.mapIso_inv, Iso.refl_inv] - simp only [- eqToHom_refl, PrelaxFunctor.map₂_id, Cat.id_app, Category.id_comp, - PrelaxFunctor.map₂_comp, Cat.comp_app, Category.assoc, Functor.map_comp, - eqToIso_refl, - Iso.refl_inv] + let ι := (fun t ↦ f (fromDirection i j k t)) + ((canonicalAux S U f X).cocycleMap (fromDirection i j k) .left_middle).hom = + (S.mkFunctor (f i) ◁ S.map₂ (Discrete.eqToIso' sorry).hom ≫ + S.mkFunctor (f i) ◁ (S.mapCompCat (pullback.fst (f i) (f j)) (proj₂ ι .left_middle)).hom ≫ + (α_ _ _ _).inv ≫ + (S.mapCompCat (f i) (pullback.fst (f i) (f j))).inv ▷ S.mkFunctor (proj₂ ι .left_middle) ≫ + S.map₂ + ((compIso (f i).op (pullback.fst (f i) (f j)).op).inv ≫ + (Discrete.eqToIso' sorry).hom ≫ (compIso (f j).op (pullback.snd (f i) (f j)).op).hom) ▷ S.mkFunctor (proj₂ ι .left_middle) ≫ + (S.mapCompCat (f j) (pullback.snd (f i) (f j))).hom ▷ S.mkFunctor (proj₂ ι .left_middle) ≫ + (α_ _ _ _).hom ≫ + S.mkFunctor (f j) ◁ (S.mapCompCat (pullback.snd (f i) (f j)) (proj₂ ι .left_middle)).inv ≫ + S.mkFunctor (f j) ◁ (S.map₂Iso (Discrete.eqToIso' sorry)).inv).app X := by + dsimp only [fromDirection_left, fromDirection_middle, fromDirection_right, fst, mkFunctor, + canonicalAux, compIso, snd, cocycleMap, op_comp, Cat.comp_obj, mapCompCat, Iso.trans_def, + Iso.trans_hom, Iso.app_hom, Functor.mapIso_hom, eqToIso.hom, eqToHom_refl, + PrelaxFunctor.mapFunctor_map, Iso.symm_hom, eqToIso.inv, NatTrans.comp_app, Functor.mapIso_inv, + Cat.comp_app, Cat.whiskerLeft_app, Cat.whiskerRight_app, Lean.Elab.WF.paramLet] + simp only [Functor.map_comp, Category.assoc] + congr 2 + rw [Cat.associator_hom_app] + rw [Cat.associator_inv_app] + dsimp only [Iso.refl_inv, Cat.comp_obj] + simp only [← Category.assoc]; congr 2; simp only [Category.assoc] + simp only [eqToHom_refl, Category.id_comp, Category.comp_id] + + + +def caconicalCocycleMapAux (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U : C) + {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) + [(Presieve.ofArrows V f).HasTriplewisePullbacks] (X : S.mkCat U) (i j k : I) (p : DirectionPair) : + let ι := (fun t ↦ f (fromDirection i j k t)) + let i' := (fromDirection i j k p.fst) + let j' := (fromDirection i j k p.snd) + S.mkFunctor (f i') ≫ S.mkFunctor (proj₁ ι p.fst) ⟶ S.mkFunctor (f j') ≫ S.mkFunctor (proj₁ ι p.snd) := by + sorry + +theorem canonical_cocycle_aux₁ (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U : C) + {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) + [(Presieve.ofArrows V f).HasTriplewisePullbacks] (X : S.mkCat U) (i j k : I) (p : DirectionPair) : + let ι := (fun t ↦ f (fromDirection i j k t)) + let i' := (fromDirection i j k p.fst) + let j' := (fromDirection i j k p.snd) + ((canonicalAux S U f X).cocycleMap (fromDirection i j k) p).hom = + (S.mkFunctor (f i') ◁ S.map₂ (Discrete.eqToIso' sorry).hom ≫ + S.mkFunctor (f i') ◁ (S.mapCompCat (pullback.fst (f i') (f j')) (proj₂ ι p)).hom ≫ + (α_ _ _ _).inv ≫ + (S.mapCompCat (f i') (pullback.fst (f i') (f j'))).inv ▷ S.mkFunctor (proj₂ ι p) ≫ + S.map₂ + ((compIso (f i').op (pullback.fst (f i') (f j')).op).inv ≫ + (Discrete.eqToIso' sorry).hom ≫ (compIso (f j').op (pullback.snd (f i') (f j')).op).hom) ▷ S.mkFunctor (proj₂ ι p) ≫ + (S.mapCompCat (f j') (pullback.snd (f i') (f j'))).hom ▷ S.mkFunctor (proj₂ ι p) ≫ + (α_ _ _ _).hom ≫ + S.mkFunctor (f j') ◁ (S.mapCompCat (pullback.snd (f i') (f j')) (proj₂ ι p)).inv ≫ + S.mkFunctor (f j') ◁ (S.map₂Iso (Discrete.eqToIso' sorry)).inv).app X := by + dsimp only [fromDirection_left, fromDirection_middle, fromDirection_right, fst, mkFunctor, + canonicalAux, compIso, snd, cocycleMap, op_comp, Cat.comp_obj, mapCompCat, Iso.trans_def, + Iso.trans_hom, Iso.app_hom, Functor.mapIso_hom, eqToIso.hom, eqToHom_refl, + PrelaxFunctor.mapFunctor_map, Iso.symm_hom, eqToIso.inv, NatTrans.comp_app, Functor.mapIso_inv, + Cat.comp_app, Cat.whiskerLeft_app, Cat.whiskerRight_app, Lean.Elab.WF.paramLet] + simp only [Functor.map_comp, Category.assoc] + congr 2 + rw [Cat.associator_hom_app] + rw [Cat.associator_inv_app] + dsimp only [Iso.refl_inv, Cat.comp_obj] + simp only [← Category.assoc]; congr 2; simp only [Category.assoc] + simp only [eqToHom_refl, Category.id_comp, Category.comp_id] + +-- example (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U : C) +-- {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) +-- [(Presieve.ofArrows V f).HasTriplewisePullbacks] (X : S.mkCat U) (i j k : I) (p : DirectionPair) : +-- let ι := (fun t ↦ f (fromDirection i j k t)) +-- ((canonicalAux S U f X).cocycleMap (fromDirection i j k) .left_middle).hom = +-- (S.mkFunctor (f i) ◁ S.map₂ (Discrete.eqToIso' sorry).hom ≫ +-- S.mkFunctor (f i) ◁ (S.mapCompCat (pullback.fst (f i) (f j)) (proj₂ ι .left_middle)).hom ≫ +-- (α_ _ _ _).inv ≫ +-- (S.mapCompCat (f i) (pullback.fst (f i) (f j))).inv ▷ S.mkFunctor (proj₂ ι .left_middle) ≫ +-- S.map₂ +-- ((compIso (f i).op (pullback.fst (f i) (f j)).op).inv ≫ +-- (Discrete.eqToIso' sorry).hom ≫ (compIso (f j).op (pullback.snd (f i) (f j)).op).hom) ▷ S.mkFunctor (proj₂ ι .left_middle) ≫ +-- (S.mapCompCat (f j) (pullback.snd (f i) (f j))).hom ▷ S.mkFunctor (proj₂ ι .left_middle) ≫ +-- (α_ _ _ _).hom ≫ +-- S.mkFunctor (f j) ◁ (S.mapCompCat (pullback.snd (f i) (f j)) (proj₂ ι .left_middle)).inv ≫ +-- S.mkFunctor (f j) ◁ (S.map₂Iso (Discrete.eqToIso' sorry)).inv).app X := by +-- dsimp only [mkFunctor] +-- rw [S.mapComp_assoc_mapComp_inv_assoc] +-- rw [S.mapComp_assoc_inv_mapComp_inv_assoc] +-- rw [← S.map₂_whisker_right_assoc] +-- rw [← S.map₂_comp_assoc] +-- rw [← S.map₂_comp_assoc] +-- rw [LocallyDiscrete.associator_hom] +-- rw [LocallyDiscrete.associator_inv] +-- dsimp only [compIso, Discrete.eqToIso', Discrete.eqToIso] +-- dsimp only [eqToIso.hom, eqToIso.inv] +-- simp only [fromDirection_left, fromDirection_middle, fromDirection_right, fst, snd, op_comp, +-- - eqToHom_refl, Category.comp_id, Category.id_comp, Category.assoc, -PrelaxFunctor.map₂_comp, +-- map₂_whisker_right, - eqToIso_refl, - Functor.mapIso_refl, PrelaxFunctor.mapFunctor_obj, +-- Iso.refl_inv, -Cat.comp_app, Cat.comp_obj, Cat.whiskerLeft_app, Cat.whiskerRight_app, Cat.id_app] +-- simp only [eqToHom_trans, eqToHom_whiskerRight] +-- simp [- Cat.comp_app, Cat.comp_obj, Cat.whiskerLeft_app, Cat.id_app] +-- simp only [Cat.comp_app, Cat.comp_obj, Cat.whiskerLeft_app, Cat.id_app] +-- -- simp only [fromDirection_left, fromDirection_middle, fromDirection_right, fst, snd, op_comp, +-- -- -eqToHom_refl, -eqToIso_refl, Functor.mapIso_inv, Iso.refl_inv, -PrelaxFunctor.mapFunctor_map, +-- -- -Cat.comp_app, -Cat.comp_obj, -Cat.whiskerLeft_app] +-- -- rw [Cat.associator_hom_app] +-- dsimp +-- simp +-- -- simp only [fromDirection_left, fromDirection_middle, fromDirection_right, fst, snd, op_comp, +-- -- eqToIso_refl, Iso.refl_hom, eqToIso.hom, PrelaxFunctor.map₂_comp, comp_whiskerRight, +-- -- Functor.mapIso_refl, PrelaxFunctor.mapFunctor_obj, Iso.refl_inv, Category.assoc, Cat.comp_app, +-- -- Cat.comp_obj, Cat.whiskerLeft_app, Cat.whiskerRight_app, Cat.id_app] +-- -- rw? +-- sorry + + +theorem cocycle_aux (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U : C) + {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) + [(Presieve.ofArrows V f).HasTriplewisePullbacks] + (X : S.mkCat U) (i j k : I) (p : DirectionPair) : + let ι := (fun t ↦ f (fromDirection i j k t)) + let i' := (fromDirection i j k p.fst) + let j' := (fromDirection i j k p.snd) + ((canonicalAux S U f X).cocycleMap (fromDirection i j k) p).hom = + (S.map (mkHom (f i').op) ◁ S.map₂ (eqToHom sorry) ≫ + (S.mapComp (mkHom (f i').op) + (mkHom (pullback.fst (f i') (f j')).op ≫ + mkHom (proj₂ ι p).op)).inv ≫ + S.map₂ (eqToHom sorry) ≫ + (S.mapComp (mkHom (f j').op) + (mkHom (pullback.snd (f i') (f j')).op ≫ + mkHom (proj₂ ι p).op)).hom ≫ + S.map (mkHom (f j').op) ◁ (S.map₂Iso (eqToIso sorry)).inv).app X := by + rw [canonical_cocycle_aux₁] + congr 1 dsimp only [mkFunctor] - set pr₀₁ := (pr (fun j_1 ↦ f (fromDirection i j k j_1)) left_middle) - slice_lhs 2 3 => - change (S.map (mkHom (op (f i))) ◁ ((S.mapComp (mkHom (pr₀₁_₀ f i j).op) (mkHom pr₀₁.op)).hom)).app X ≫ - (((S.mapComp (mkHom (f i).op) (mkHom (pullback.fst (f i) (f j)).op)).inv ▷ S.map (mkHom (pr₀₁.op))).app X) - - simp only [PrelaxFunctor.map₂_id, Cat.id_app, Category.id_comp, PrelaxFunctor.map₂_comp, - Cat.comp_app, Category.assoc, Functor.map_comp] - set f' := (fun j_1 ↦ f (fromDirection i j k j_1)) - -- set S' := S.mkFunctor - simp - -- sorry + rw [S.mapComp_assoc_mapComp_inv_assoc] + rw [S.mapComp_assoc_inv_mapComp_inv_assoc] + rw [← S.map₂_whisker_right_assoc] + rw [← S.map₂_comp_assoc] + rw [← S.map₂_comp_assoc] + rw [LocallyDiscrete.associator_hom] + rw [LocallyDiscrete.associator_inv] + dsimp only [fromDirection_left, fromDirection_middle, fromDirection_right, fst, snd, op_comp, + -eqToIso_refl, Iso.refl_hom, eqToIso.hom, Functor.mapIso_inv, Iso.refl_inv, + PrelaxFunctor.mapFunctor_map, -eqToHom_refl] + simp only [-eqToHom_refl, comp_whiskerRight, Category.assoc, PrelaxFunctor.map₂_comp, + -map₂_whisker_right, Iso.inv_hom_id_assoc, -eqToIso_refl, Iso.refl_inv, PrelaxFunctor.map₂_id, + whiskerLeft_id, Category.id_comp] + congr 2 + simp only [← Category.assoc] + congr + simp only [Category.assoc] + rw [← S.map₂_comp_assoc] + rw [← S.map₂_comp_assoc] + rw [← S.map₂_comp_assoc] + rw [← S.map₂_comp] + congr 1 + apply Subsingleton.elim + -- dsimp [mkFunctor, canonicalAux, cocycleMap] + -- simp only [PrelaxFunctor.map₂_comp, Cat.comp_app, Category.assoc, Functor.map_comp, + -- mapCompCat] + -- -- simp only [← NatTrans.comp_app] + -- rw [S.mapComp_assoc_mapComp_inv_assoc] + -- rw [S.mapComp_assoc_inv_mapComp_inv_assoc] + -- simp only [- map₂_associator_inv, comp_whiskerRight, map₂_associator, Category.assoc, + -- Iso.inv_hom_id_assoc, PrelaxFunctor.map₂_id, whiskerLeft_id, Category.id_comp] + -- rw [← S.map₂_whisker_right_assoc] + -- rw [← S.map₂_comp_assoc] + -- rw [← S.map₂_comp_assoc] + -- rw [LocallyDiscrete.associator_hom] + -- rw [LocallyDiscrete.associator_inv] + +-- theorem cocycle_aux' (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U : C) +-- {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) +-- [(Presieve.ofArrows V f).HasTriplewisePullbacks] +-- (X : S.mkCat U) (i j k : I) (p : DirectionPair) : +-- let ι := (fun t ↦ f (fromDirection i j k t)) +-- let i' := (fromDirection i j k p.fst) +-- let j' := (fromDirection i j k p.snd) +-- ((canonicalAux S U f X).cocycleMap (fromDirection i j k) p).hom = +-- (S.map (mkHom (f i').op) ◁ S.map₂ (eqToHom sorry) ≫ +-- (S.mapComp (mkHom (f i').op) +-- (mkHom (pullback.fst (f i') (f j')).op ≫ +-- mkHom (proj₂ ι p).op)).inv ≫ +-- S.map₂ (eqToHom sorry) ≫ +-- (S.mapComp (mkHom (f j').op) +-- (mkHom (pullback.snd (f i') (f j')).op ≫ +-- mkHom (proj₂ ι p).op)).hom ≫ +-- S.map (mkHom (f j').op) ◁ (S.map₂Iso (eqToIso sorry)).inv).app X := by +-- dsimp [mkFunctor, canonicalAux, cocycleMap] +-- simp only [PrelaxFunctor.map₂_comp, Cat.comp_app, Category.assoc, Functor.map_comp] +-- rw [S.mapComp_assoc_mapComp_inv_assoc] +-- rw [S.mapComp_assoc_inv_mapComp_inv_assoc] +-- rw [← S.map₂_whisker_right_assoc] +-- rw [← S.map₂_comp_assoc] +-- rw [← S.map₂_comp_assoc] +-- rw [LocallyDiscrete.associator_hom] +-- rw [LocallyDiscrete.associator_inv] +-- dsimp only [compIso, Discrete.eqToIso', Discrete.eqToIso] +-- dsimp only [eqToIso.hom, eqToIso.inv] +-- simp only [fromDirection_left, fromDirection_middle, fromDirection_right, fst, snd, op_comp, +-- - eqToHom_refl, Category.comp_id, Category.id_comp, Category.assoc, -PrelaxFunctor.map₂_comp, +-- map₂_whisker_right, - eqToIso_refl, - Functor.mapIso_refl, PrelaxFunctor.mapFunctor_obj, +-- Iso.refl_inv, -Cat.comp_app, Cat.comp_obj, Cat.whiskerLeft_app, Cat.whiskerRight_app, Cat.id_app] + def canonical (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U : C) {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) (X : S.mkCat U) @@ -458,22 +703,33 @@ def canonical (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U cocycle_condition i j k := by apply Iso.ext dsimp only [Iso.trans_hom] - dsimp [canonicalAux, cocycleMap₀₁, cocycleMap₁₂, cocycleMap₀₂] - dsimp [PreDescentData.cocycleMap] - simp only [PrelaxFunctor.map₂_id, Cat.id_app, Category.id_comp, PrelaxFunctor.map₂_comp, - Cat.comp_app, Category.assoc, Functor.map_comp] - simp? - sorry - -- cocycle_condition i j k := by - -- -- intro i j k - -- dsimp - -- simp only [PrelaxFunctor.map₂_comp, Cat.comp_app, Category.assoc, Functor.map_comp] - -- -- dsimp [mapCompObj] - -- simp_rw [← Functor.map_comp_assoc] - -- simp_rw [← NatTrans.comp_app_assoc] - -- simp_rw [← S.map₂_comp_assoc] - - -- sorry + rw [cocycle_aux _ _ _ _ _ _ _ DirectionPair.left_middle] + rw [cocycle_aux _ _ _ _ _ _ _ DirectionPair.middle_right] + rw [cocycle_aux _ _ _ _ _ _ _ DirectionPair.left_right] + simp only [← NatTrans.comp_app] + apply congrFun (congrArg _ _) + simp only [Category.assoc] + dsimp only [fromDirection_left, fromDirection_middle, fromDirection_right, fst, snd] + rw [S.map₂Iso_inv] + dsimp only [eqToIso.inv] + slice_lhs 5 6 => + rw [← whiskerLeft_comp] + rw [← S.map₂_comp] + rw [eqToHom_trans] + slice_lhs 4 6 => + rw [← map₂_whisker_left] + rw [whiskerLeft_eqToHom] + simp only [Category.assoc] + rw [← S.map₂_comp_assoc] + rw [← S.map₂_comp_assoc] + simp only [eqToHom_trans] + rw [S.map₂Iso_inv, S.map₂Iso_inv] + simp only [eqToIso.inv] + simp only [map₂_whisker_left_symm, Category.assoc] + simp only [whiskerLeft_eqToHom] + simp only [Iso.hom_inv_id_assoc] + simp only [S.map₂_eqToHom] + simp only [eqToHom_refl, Category.id_comp, eqToHom_trans_assoc] instance (U : C) : (Presieve.ofArrows (fun (_ : Unit) ↦ U) (fun _ ↦ 𝟙 U)).HasTriplewisePullbacks where @@ -498,61 +754,7 @@ def trivial (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U : -- ext x intro ⟨⟩ ⟨⟩ ⟨⟩ - dsimp only [Iso.app_hom, Lean.Elab.WF.paramLet, mapCompObj] - dsimp only [mkFunctor] - simp only [Functor.mapIso_hom, eqToIso.hom, PrelaxFunctor.mapFunctor_map, Iso.app_inv, - Category.assoc] - simp_rw [← NatTrans.comp_app_assoc] - simp_rw [← NatTrans.comp_app] - simp only [Cat.comp_obj, NatTrans.comp_app, Category.assoc] - set Y := ((S.map (mkHom (op (𝟙 U)))).obj X) - - simp_rw [← NatTrans.comp_app_assoc] - simp_rw [← NatTrans.comp_app] - let α : S.map (mkHom ((pullback.fst (𝟙 U) (𝟙 U)).op)) ≅ - S.map (𝟙 _) ≫ S.map (mkHom (Quiver.Hom.op - (by apply (IsPullback.id_vert (𝟙 U)).lift (pullback.fst (𝟙 U) (𝟙 U)) (pullback.snd (𝟙 U) (𝟙 U)) (by simp only [Category.comp_id]; exact fst_eq_snd_of_mono_eq (𝟙 U))))) := by - apply _ ≪≫ S.mapComp _ _ - apply S.map₂Iso - apply _ ≪≫ whiskerRightIso (LocallyDiscrete.idIso _) _ - apply _ ≪≫ (LocallyDiscrete.compIso _ _ _) - apply Discrete.eqToIso' _ - apply congrArg op - have := (IsPullback.id_vert (𝟙 U)).lift_fst (pullback.fst (𝟙 U) (𝟙 U)) (pullback.snd (𝟙 U) (𝟙 U)) sorry - apply this.symm - dsimp at α - rw [Functor.app_hom] - erw [PrelaxFunctor.mapFunctor_map] - simp_rw [← NatTrans.comp_app_assoc] - simp_rw [← NatTrans.comp_app] - repeat rw [← eqToHom_app] - simp only [- eqToHom_app, Category.assoc] - repeat erw [← NatTrans.comp_app_assoc] - simp [- eqToHom_app, - NatTrans.comp_app] - simp [- NatTrans.comp_app] - repeat erw [← eqToHom_app] - repeat erw [← NatTrans.comp_app] - simp only [← Category.assoc] - repeat erw [← NatTrans.comp_app] - repeat erw [← NatTrans.comp_app_assoc] - simp only [Category.assoc] - dsimp only [mkFunctor] - repeat erw [← NatTrans.comp_app] - - -- simp - -- set Y := (S.map (mkHom (op (𝟙 U)))).obj X - -- simp only [mapCompObj, Iso.app_hom, eqToHom_map, Iso.app_inv] - erw [← NatTrans.comp_app] - dsimp - - dsimp [mkFunctor, pr₀₁, pr₁₂, pr₀₂] - simp? - have h2 : pullback.snd (𝟙 U) (𝟙 U) = 𝟙 U := by apply? - simp only [Functor.map_id, Functor.id_obj, eqToHom_refl, Iso.refl_hom, Category.id_comp, - Category.comp_id, Category.assoc] - -def can (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U : C) : - DescentData S U + sorry end DescentData diff --git a/Mathlib/CategoryTheory/Stack/Descent2.lean b/Mathlib/CategoryTheory/Stack/Descent2.lean new file mode 100644 index 00000000000000..95e5d7d3141ead --- /dev/null +++ b/Mathlib/CategoryTheory/Stack/Descent2.lean @@ -0,0 +1,141 @@ +import Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor +import Mathlib.CategoryTheory.Bicategory.LocallyDiscrete +import Mathlib.CategoryTheory.Category.Cat +import Mathlib.CategoryTheory.Sites.Grothendieck +import Mathlib.CategoryTheory.Sites.Sheaf +import Mathlib.CategoryTheory.Sites.Over + +import Mathlib.Tactic.Widget.StringDiagram + +noncomputable section + +universe v u v₁ u₁ v₂ + +open CategoryTheory Opposite Bicategory +open CategoryTheory.Limits LocallyDiscrete +open ProofWidgets Mathlib.Tactic.Widget + + +variable {C : Type u} [Category.{v} C] + +namespace CategoryTheory + +namespace Pseudofunctor + +open Category Opposite Limits + +abbrev mkCat (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (X : C) : Cat := + S.obj ⟨op X⟩ + +abbrev mkFunctor (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) {X Y : C} (f : Y ⟶ X) : + S.mkCat X ⟶ S.mkCat Y := + S.map (LocallyDiscrete.mkHom f.op) + +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) + +variable {B : Type} [Bicategory B] + +structure PreDescentData (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) + {a : C} (P : Presieve a) where + obj : ∀ {b : C} (f : b ⟶ a) (_ : P f := by cat_disch), S.obj ⟨op b⟩ + 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) + +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.mapId ⟨op 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} + +@[ext] +structure Hom (𝒟₁ 𝒟₂ : DescentData S P) where + 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 + +@[simps] +def Hom.id (𝒟 : DescentData S P) : Hom 𝒟 𝒟 where + hom f _ := 𝟙 (𝒟.obj f) + +@[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, assoc] + rw [η₂.comm f g, η₁.comm_assoc f g] + +instance : Category (DescentData S P) where + Hom := Hom + id := Hom.id + comp := Hom.comp + +@[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 [assoc] + rw [Cat.rightUnitor_eqToIso, LocallyDiscrete.rightUnitor_inv, S.map₂_eqToHom] + simp only [eqToIso_refl, Iso.refl_hom, comp_id, eqToHom_naturality_assoc, 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 + this 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, 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 [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 From 13f9d3ce03662c49c9dbf7c39a15c928bb95de88 Mon Sep 17 00:00:00 2001 From: Yuma Mizuno Date: Sun, 14 Sep 2025 13:11:09 +0100 Subject: [PATCH 3/6] update --- Mathlib/CategoryTheory/Stack/Basic.lean | 138 ++-- Mathlib/CategoryTheory/Stack/Basic2.lean | 66 -- Mathlib/CategoryTheory/Stack/Descent.lean | 849 ++++----------------- Mathlib/CategoryTheory/Stack/Descent2.lean | 141 ---- 4 files changed, 222 insertions(+), 972 deletions(-) delete mode 100644 Mathlib/CategoryTheory/Stack/Basic2.lean delete mode 100644 Mathlib/CategoryTheory/Stack/Descent2.lean diff --git a/Mathlib/CategoryTheory/Stack/Basic.lean b/Mathlib/CategoryTheory/Stack/Basic.lean index 3300446f26441b..0189d47be39652 100644 --- a/Mathlib/CategoryTheory/Stack/Basic.lean +++ b/Mathlib/CategoryTheory/Stack/Basic.lean @@ -1,63 +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 +open CategoryTheory Opposite Bicategory Pseudofunctor LocallyDiscrete -variable {C : Type u} [Category.{v} C] +namespace CategoryTheory -def homPreSheaf (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U : C) (x y : S.obj ⟨op U⟩) : - Opposite (Over U) ⥤ Type v₁ where - obj V := (S.map ⟨V.unop.hom.op⟩).obj x ⟶ (S.map ⟨V.unop.hom.op⟩).obj y - map {V V'} g := by - let f : Discrete (op U ⟶ op (unop V).left) := ⟨V.unop.hom.op⟩ - let f' : Discrete (op U ⟶ op (unop V').left) := ⟨V'.unop.hom.op⟩ - let g' : Discrete (op (unop V).left ⟶ op (unop V').left) := ⟨g.unop.left.op⟩ - have w : f.as ≫ g'.as = f'.as := by - simp [f, f', g'] - rw [← op_comp]; simp - let α := S.mapComp f g' - intro ϕ - let gϕ := (S.map g').map ϕ - let eq : ∀ x, (S.map f').obj x ≅ (S.map (f ≫ g')).obj x := - fun x ↦ eqToIso (by congr; apply Discrete.ext; simp [w]) - exact (eq x).hom ≫ α.hom.app x ≫ gϕ ≫ α.inv.app y ≫ (eq y).inv +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⟩⟩ + rintro ⟨x, _, f : x ⟶ a⟩ ext g - simp only [Functor.id_obj, Functor.const_obj_obj, unop_id, Over.id_left, op_id, eqToIso.hom, - Cat.comp_obj, eqToIso.inv, types_id_apply] - dsimp at f g - erw [Pseudofunctor.mapComp_id_right_hom] - dsimp only [Cat.comp_app, Cat.comp_obj, Cat.id_obj, Cat.whiskerLeft_app] - simp only [Category.assoc] - erw [Pseudofunctor.mapComp_id_right_inv] - dsimp only [Cat.comp_app, Cat.comp_obj, Cat.id_obj, Cat.whiskerLeft_app] - simp only [Category.assoc, NatTrans.naturality_assoc, Cat.id_obj, Cat.id_map, - Iso.inv_hom_id_app_assoc] - rw [Cat.rightUnitor_inv_app] - rw [Cat.rightUnitor_hom_app] - simp only [Cat.comp_obj, Cat.id_obj, eqToHom_refl, Category.id_comp] - simp only [Pseudofunctor.map₂_right_unitor, Cat.comp_app, Cat.comp_obj, Cat.id_obj, - Cat.whiskerLeft_app, Category.assoc] - -- rw [Cat.rightUnitor_inv_app] - rw [Cat.rightUnitor_hom_app] - simp only [Cat.comp_obj, Cat.id_obj, eqToHom_refl, Category.id_comp] - have : (S.map₂ (ρ_ (⟨f.op⟩ : Discrete (op U ⟶ op X))).hom).app x ≫ (ρ_ (S.map (⟨f.op⟩ : Discrete (op U ⟶ op X)))).inv.app x = sorry := by - rw [Cat.rightUnitor_inv_app] - sorry - -- let _ := g.w - - map_comp := _ + 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} -structure IsStack [Limits.HasPullbacks C] (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) where - is_sheaf_of_hom : ∀ (U : C) (x y : S.obj ⟨op U⟩), Presieve.IsSheaf (J.over U) (homPreSheaf S U x y) - is_descent_effective : ∀ (U : C) (R : Sieve U) (_ : R ∈ J.sieves U) - (d : S.DescentData U (fun i : Σ V, { f : V ⟶ U // R f } ↦ (i.2 : i.1 ⟶ U))), - ∃ X : S.obj ⟨op U⟩, - Nonempty (d ≅ DescentData.canonical S U (fun i : Σ V, { f : V ⟶ U // R f } ↦ (i.2 : i.1 ⟶ U)) X) +/-- 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/Basic2.lean b/Mathlib/CategoryTheory/Stack/Basic2.lean deleted file mode 100644 index 49d6c11b5cab55..00000000000000 --- a/Mathlib/CategoryTheory/Stack/Basic2.lean +++ /dev/null @@ -1,66 +0,0 @@ -import Mathlib.CategoryTheory.Stack.Descent2 - -universe v u v₁ u₁ - -open CategoryTheory Opposite Bicategory Pseudofunctor LocallyDiscrete -open ProofWidgets Mathlib.Tactic.Widget - -variable {C : Type u} [Category.{v} C] - -@[simps] -def homPreSheaf (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U : C) (x y : S.mkCat U) : - Opposite (Over U) ⥤ Type v₁ where - obj V := (S.mkFunctor V.unop.hom).obj x ⟶ (S.mkFunctor V.unop.hom).obj y - map {V V'} g ϕ := - eqToHom (by simp) ≫ (S.mapCompCat V.unop.hom g.unop.left).hom.app x ≫ - (S.mkFunctor g.unop.left).map ϕ ≫ - (S.mapCompCat V.unop.hom g.unop.left).inv.app y ≫ eqToHom (by simp) - map_id := by - rintro ⟨X, _, f : X ⟶ U⟩ - 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 ⟨X, _, f : X ⟶ U⟩ ⟨Y, _, g : Y ⟶ U⟩ ⟨Z, _, h : Z ⟶ U⟩ ⟨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} - -structure IsStack (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) : Prop where - is_sheaf_of_hom (U : C) (x y : S.mkCat U) : - Presieve.IsSheaf (J.over U) (homPreSheaf S U x y) - is_descent_effective (U : C) (R : Sieve U) (_ : R ∈ J.sieves U) (d : S.DescentData R) : - ∃ x : S.mkCat U, Nonempty (d ≅ DescentData.canonical S x) diff --git a/Mathlib/CategoryTheory/Stack/Descent.lean b/Mathlib/CategoryTheory/Stack/Descent.lean index 74d19b3a4e56de..7c42788f3cb622 100644 --- a/Mathlib/CategoryTheory/Stack/Descent.lean +++ b/Mathlib/CategoryTheory/Stack/Descent.lean @@ -1,760 +1,177 @@ +/- +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.Category.Cat -import Mathlib.CategoryTheory.Sites.Grothendieck -import Mathlib.CategoryTheory.Sites.Sheaf -import Mathlib.CategoryTheory.Sites.Over +import Mathlib.CategoryTheory.Sites.Sieves -noncomputable section +/-! +# Descent data -universe v u v₁ u₁ v₂ +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. -open CategoryTheory Opposite Bicategory -open CategoryTheory.Limits LocallyDiscrete +The set of descent data on `P` forms a category `DescentData S P`. +-/ -variable {C : Type u} [Category.{v} C] - -namespace CategoryTheory - -namespace Presieve - -variable {X : C} - -class HasTriplewisePullbacks (R : Presieve X) extends HasPairwisePullbacks R where - -- has_pairwise_pullbacks : ∀ {Y Z} {f : Y ⟶ X} (_ : R f) {g : Z ⟶ X} (_ : R g), HasPullback f g - has_triplewise_pullbacks : - ∀ {X₁ X₂ X₃} {f₁ : X₁ ⟶ X} (_ : R f₁) {f₂ : X₂ ⟶ X} (_ : R f₂) {f₃ : X₃ ⟶ X} (_ : R f₃) - [HasPullback f₁ f₂] [HasPullback f₂ f₃], HasPullback (pullback.snd f₁ f₂) (pullback.fst f₂ f₃) - -instance (R : Presieve X) [HasPullbacks C] : R.HasTriplewisePullbacks := ⟨inferInstance⟩ - -instance {α : Type v₂} {X : α → C} {B : C} (π : (a : α) → X a ⟶ B) - [(Presieve.ofArrows X π).HasTriplewisePullbacks] (a b c : α) : - HasPullback (pullback.snd (π a) (π b)) (pullback.fst (π b) (π c)) := - Presieve.HasTriplewisePullbacks.has_triplewise_pullbacks - (Presieve.ofArrows.mk _) (Presieve.ofArrows.mk _) (Presieve.ofArrows.mk _) - -end Presieve - -namespace TriplePullback - -variable {U V₁ V₂ V₃ : C} - -abbrev triplePullback (f₁ : V₁ ⟶ U) (f₂ : V₂ ⟶ U) (f₃ : V₃ ⟶ U) - [HasPullback f₁ f₂] [HasPullback f₂ f₃] - [HasPullback (pullback.snd f₁ f₂) (pullback.fst f₂ f₃)] : C := - pullback (pullback.snd f₁ f₂) (pullback.fst f₂ f₃) - -inductive Direction | left | middle | right - -inductive DirectionPair - | left_middle : DirectionPair - | middle_right : DirectionPair - | left_right : DirectionPair - deriving Inhabited - -instance : OfNat Direction 0 := ⟨Direction.left⟩ -instance : OfNat Direction 1 := ⟨Direction.middle⟩ -instance : OfNat Direction 2 := ⟨Direction.right⟩ - --- instance : Coe (ℕ × ℕ) DirectionPair where --- coe d := --- match d with --- | (0, 1) => DirectionPair.left_middle --- | (1, 2) => DirectionPair.middle_right --- | (0, 2) => DirectionPair.left_right --- | _ => Inhabited.default - -@[simp] -def DirectionPair.fst : DirectionPair → Direction - | DirectionPair.left_middle => 0 - | DirectionPair.middle_right => 1 - | DirectionPair.left_right => 0 - -@[simp] -def DirectionPair.snd : DirectionPair → Direction - | DirectionPair.left_middle => 1 - | DirectionPair.middle_right => 2 - | DirectionPair.left_right => 2 - -variable {V : Direction → C} (f : (i : Direction) → V i ⟶ U) -variable {HasPullback : ∀ i j : Direction, HasPullback (f i) (f j)} -variable [(Presieve.ofArrows V f).HasTriplewisePullbacks] - -def proj₂ (p : DirectionPair) : triplePullback (f 0) (f 1) (f 2) ⟶ pullback (f p.fst) (f p.snd) := - match p with - | .left_middle => pullback.fst (pullback.snd (f 0) (f 1)) (pullback.fst (f 1) (f 2)) - | .middle_right => pullback.snd (pullback.snd (f 0) (f 1)) (pullback.fst (f 1) (f 2)) - | .left_right => - pullback.lift - (pullback.fst (pullback.snd (f 0) (f 1)) (pullback.fst (f 1) (f 2)) ≫ - pullback.fst (f 0) (f 1)) - (pullback.snd (pullback.snd (f 0) (f 1)) (pullback.fst (f 1) (f 2)) ≫ - pullback.snd (f 1) (f 2)) <| by - dsimp only [DirectionPair.fst, DirectionPair.snd] - rw [Category.assoc, pullback.condition, ← Category.assoc, pullback.condition, - Category.assoc, pullback.condition, Category.assoc] - -def proj₁ (i : Direction) : - triplePullback (f 0) (f 1) (f 2) ⟶ V i := - match i with - | 0 => proj₂ f .left_middle ≫ pullback.fst (f 0) (f 1) - | 1 => proj₂ f .left_middle ≫ pullback.snd (f 0) (f 1) - | 2 => proj₂ f .middle_right ≫ pullback.snd (f 1) (f 2) - -theorem proj₁_fst {ij : DirectionPair} : - proj₁ f ij.fst = proj₂ f ij ≫ pullback.fst (f ij.fst) (f ij.snd) := by - cases ij - case left_middle => rfl - case middle_right => exact pullback.condition - case left_right => simp [proj₁, proj₂] - -theorem proj₁_snd {ij : DirectionPair} : - proj₁ f ij.snd = proj₂ f ij ≫ pullback.snd (f ij.fst) (f ij.snd) := by - cases ij - all_goals simp [proj₁, proj₂] - -variable {U : C} {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) -variable [(Presieve.ofArrows V f).HasTriplewisePullbacks] +universe v u v₁ u₁ --- def pr₀₁₂_₀₁ (i j k : I) : --- triplePullback (f i) (f j) (f k) ⟶ pullback (f i) (f j) := --- pullback.fst (pullback.snd (f i) (f j)) (pullback.fst (f j) (f k)) +open CategoryTheory Opposite Bicategory Limits LocallyDiscrete --- def pr₀₁₂_₁₂ (i j k : I) : --- triplePullback (f i) (f j) (f k) ⟶ pullback (f j) (f k) := --- pullback.snd (pullback.snd (f i) (f j)) (pullback.fst (f j) (f k)) - --- def pr₀₁₂_₀₂ (i j k : I) : --- triplePullback (f i) (f j) (f k) ⟶ pullback (f i) (f k) := --- pullback.lift (pr₀₁₂_₀₁ f i j k ≫ pullback.fst (f i) (f j)) --- (pr₀₁₂_₁₂ f i j k ≫ pullback.snd (f j) (f k)) <| by --- dsimp only [pr₀₁₂_₀₁, pr₀₁₂_₁₂] --- rw [Category.assoc, pullback.condition, ← Category.assoc, pullback.condition, --- Category.assoc, pullback.condition, Category.assoc] - --- abbrev pr₀₁_₀ (i j : I) : --- pullback (f i) (f j) ⟶ V i := --- pullback.fst (f i) (f j) - --- abbrev pr₀₁_₁ (i j : I) : --- pullback (f i) (f j) ⟶ V j := --- pullback.snd (f i) (f j) - --- abbrev pr₁₂_₁ (j k : I) : --- pullback (f j) (f k) ⟶ V j := --- pullback.fst (f j) (f k) - --- abbrev pr₁₂_₂ (j k : I) : --- pullback (f j) (f k) ⟶ V k := --- pullback.snd (f j) (f k) - --- abbrev pr₀₂_₀ (i k : I) : --- pullback (f i) (f k) ⟶ V i := --- pullback.fst (f i) (f k) - --- abbrev pr₀₂_₂ (i k : I) : --- pullback (f i) (f k) ⟶ V k := --- pullback.snd (f i) (f k) - --- theorem pullback_condition₀ (i j k : I) : --- pr₀₁₂_₀₁ f i j k ≫ pr₀₁_₀ f i j = pr₀₁₂_₀₂ f i j k ≫ pr₀₂_₀ f i k := by --- simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app, pr₀₁₂_₀₁, pr₀₁₂_₀₂] - --- theorem pullback_condition₁ (i j k : I) : --- pr₀₁₂_₀₁ f i j k ≫ pr₀₁_₁ f i j = pr₀₁₂_₁₂ f i j k ≫ pr₁₂_₁ f j k := --- pullback.condition - --- theorem pullback_condition₂ (i j k : I) : --- pr₀₁₂_₀₂ f i j k ≫ pr₀₂_₂ f i k = pr₀₁₂_₁₂ f i j k ≫ pr₁₂_₂ f j k := by --- simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app, pr₀₁₂_₀₂, pr₀₁₂_₀₂, pr₀₁₂_₁₂] - --- def pr₀₁₂_₀ (i j k : I) : triplePullback (f i) (f j) (f k) ⟶ V i := --- pr₀₁₂_₀₁ f i j k ≫ pr₀₁_₀ f i j - --- theorem pr₀₁₂_₀_def₀₁ {i j k : I} : --- pr₀₁₂_₀ f i j k = pr₀₁₂_₀₁ f i j k ≫ pr₀₁_₀ f i j := --- rfl - --- theorem pr₀₁₂_₀_def₀₂ {i j k : I} : --- pr₀₁₂_₀ f i j k = pr₀₁₂_₀₂ f i j k ≫ pr₀₂_₀ f i k := by --- simp only [pr₀₁₂_₀_def₀₁, pr₀₁₂_₀₁, pr₀₁₂_₀₂, limit.lift_π, PullbackCone.mk_pt, --- PullbackCone.mk_π_app] - --- def pr₀₁₂_₁ (i j k : I) : triplePullback (f i) (f j) (f k) ⟶ V j := --- pr₀₁₂_₀₁ f i j k ≫ pr₀₁_₁ f i j - --- theorem pr₀₁₂_₁_def₀₁ {i j k : I} : --- pr₀₁₂_₁ f i j k = pr₀₁₂_₀₁ f i j k ≫ pr₀₁_₁ f i j := --- rfl - --- theorem pr₀₁₂_₁_def₁₂ {i j k : I} : --- pr₀₁₂_₁ f i j k = pr₀₁₂_₁₂ f i j k ≫ pr₁₂_₁ f j k := --- pullback.condition - --- def pr₀₁₂_₂ (i j k : I) : triplePullback (f i) (f j) (f k) ⟶ V k := --- pr₀₁₂_₁₂ f i j k ≫ pr₁₂_₂ f j k - --- theorem pr₀₁₂_₂_def₁₂ {i j k : I} : --- pr₀₁₂_₂ f i j k = pr₀₁₂_₁₂ f i j k ≫ pr₁₂_₂ f j k := --- rfl - --- theorem pr₀₁₂_₂_def₀₂ {i j k : I} : --- pr₀₁₂_₂ f i j k = pr₀₁₂_₀₂ f i j k ≫ pr₀₂_₂ f i k := by --- simp only [pr₀₁₂_₂_def₁₂, pr₀₁₂_₁₂, pr₀₁₂_₀₂, limit.lift_π, PullbackCone.mk_pt, --- PullbackCone.mk_π_app] +variable {C : Type u} [Category.{v} C] -end TriplePullback +namespace CategoryTheory namespace Pseudofunctor -open TriplePullback - --- set_option pp.universes true - +/-- 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 ⟨op X⟩ - --- def mkFunctor (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) {X Y : C} (f : Y ⟶ X) : --- S.mkCat X ⟶ S.mkCat Y := --- S.map ⟨op f⟩ - --- def mkCat' (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (X : C) : Type u₁ := --- S.obj ⟨op X⟩ + 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 (LocallyDiscrete.mkHom f.op) + S.map (mkHom f.op) -#check Pseudofunctor.mapComp +/-- 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) --- @[to_app?] --- @[simps!?] -abbrev mapCompCatApp (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) {X Y Z : C} - (f : Y ⟶ X) (g : Z ⟶ Y) {x : S.mkCat X} : - (S.mkFunctor (g ≫ f)).obj x ≅ (S.mkFunctor g).obj ((S.mkFunctor f).obj x) := - (mapCompCat S f g).app x - +/-- An auxiliary structure for descent data: it contains only data, with no conditions. -/ structure PreDescentData (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) - (U : C) {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) - [(Presieve.ofArrows V f).HasTriplewisePullbacks] where - /-- An object `Xᵢ` of `S Vᵢ` for each `i : I`. -/ - X : ∀ i, S.obj ⟨op (V i)⟩ - /-- An isomorphism `φᵢⱼ : pr₀* Xᵢ ≅ pr₁* Xⱼ` for each `i j : I`, where `pr₀` and `pr₁` - are the projections from the pullback. -/ - φ : ∀ i j : I, - (S.mkFunctor (pullback.fst (f i) (f j))).obj (X i) ≅ - (S.mkFunctor (pullback.snd (f i) (f j))).obj (X j) - -namespace PreDescentData - -variable {S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}} - {U : C} {I : Type v₂} {V : I → C} {f : (i : I) → V i ⟶ U} - [(Presieve.ofArrows V f).HasTriplewisePullbacks] - -@[simp] -def objAtDirection (V : I → C) (i j k : I) : Direction → C - | 0 => V i - | 1 => V j - | 2 => V k - -@[simp] -def morAtDirection (f : (i : I) → V i ⟶ U) (i j k : I) : (d : Direction) → objAtDirection V i j k d ⟶ U - | 0 => f i - | 1 => f j - | 2 => f k - -instance {i j k : I} : - (Presieve.ofArrows (objAtDirection V i j k) (morAtDirection f i j k)).HasTriplewisePullbacks := - sorry - -instance {ι : Direction → I} : - (Presieve.ofArrows (fun j ↦ V (ι j)) fun j ↦ f (ι j)).HasTriplewisePullbacks := sorry - -def cocycleMap (d : PreDescentData S U f) (ι : Direction → I) (ij : DirectionPair) : - (S.mkFunctor (proj₁ (fun j ↦ f (ι j)) ij.fst)).obj (d.X (ι ij.fst)) ≅ - (S.mkFunctor (proj₁ (fun j ↦ f (ι j)) ij.snd)).obj (d.X (ι ij.snd)) := - let f' := fun j ↦ f (ι j) - let i := ij.fst - let j := ij.snd - calc - (S.mkFunctor (proj₁ f' i)).obj (d.X (ι i)) ≅ - (S.mkFunctor (proj₂ f' ij ≫ pullback.fst (f (ι i)) (f (ι j)))).obj (d.X (ι i)) := - (S.map₂Iso (Discrete.eqToIso' (congrArg op (proj₁_fst f')))).app (d.X (ι i)) - _ ≅ (S.mkFunctor (pullback.fst (f (ι i)) (f (ι j))) ≫ S.mkFunctor (proj₂ f' ij)).obj (d.X (ι i)) := - (S.mapCompCat (pullback.fst (f (ι i)) (f (ι j))) (proj₂ f' ij)).app (d.X (ι i)) - _ ≅ (S.mkFunctor (pullback.snd (f (ι i)) (f (ι j))) ≫ S.mkFunctor (proj₂ f' ij)).obj (d.X (ι j)) := - /- Here is the main part. -/ - (S.mkFunctor (proj₂ f' ij)).mapIso (d.φ (ι i) (ι j)) - _ ≅ (S.mkFunctor ((proj₂ f' ij) ≫ pullback.snd (f (ι i)) (f (ι j)))).obj (d.X (ι j)) := - (S.mapCompCat (pullback.snd (f (ι i)) (f (ι j))) (proj₂ f' ij)).symm.app (d.X (ι j)) - _ ≅ (S.mkFunctor (proj₁ f' j)).obj (d.X (ι j)) := - (S.map₂Iso (Discrete.eqToIso' (congrArg op (proj₁_snd f')))).symm.app (d.X (ι j)) - --- def cocycleMapAux (d : PreDescentData S U f) (ι : Direction → I) (ij : DirectionPair) : --- (S.mkFunctor (proj₁ (fun j ↦ f (ι j)) ij.fst)) ≅ --- (S.mkFunctor (pr₀₁_₀ f (ι ij.fst) (ι ij.snd)) ≫ S.mkFunctor (proj₂ (fun j ↦ f (ι j)) ij)) := --- let f' := fun j ↦ f (ι j) --- let i := ij.fst --- let j := ij.snd --- calc --- (S.mkFunctor (proj₁ f' i)) ≅ (S.mkFunctor (proj₂ f' ij ≫ pr₀₁_₀ f (ι i) (ι j))) := --- (S.map₂Iso (Discrete.eqToIso' (congrArg op sorry))) --- _ ≅ (S.mkFunctor (pr₀₁_₀ f (ι i) (ι j)) ≫ S.mkFunctor (proj₂ f' ij)) := --- (S.mapComp (mkHom ((pr₀₁_₀ f (ι i) (ι j)).op)) (mkHom ((proj₂ f' ij).op))) - --- def cocycleMap₀₁ (d : PreDescentData S U f) (i j k : I) : --- (S.mkFunctor (pr₀₁₂_₀ f i j k)).obj (d.X i) ≅ (S.mkFunctor (pr₀₁₂_₁ f i j k)).obj (d.X j) := --- calc --- (S.mkFunctor (pr₀₁₂_₀ f i j k)).obj (d.X i) ≅ --- (S.mkFunctor (pr₀₁₂_₀₁ f i j k ≫ pr₀₁_₀ f i j)).obj (d.X i) := --- (S.map₂Iso (Discrete.eqToIso' (congrArg op (pr₀₁₂_₀_def₀₁ f)))).app (d.X i) --- _ ≅ (S.mkFunctor (pr₀₁_₀ f i j) ≫ S.mkFunctor (pr₀₁₂_₀₁ f i j k)).obj (d.X i) := --- (S.mapComp (mkHom ((pr₀₁_₀ f i j).op)) (mkHom ((pr₀₁₂_₀₁ f i j k).op))).app (d.X i) --- _ ≅ (S.mkFunctor (pr₀₁_₁ f i j) ≫ S.mkFunctor (pr₀₁₂_₀₁ f i j k)).obj (d.X j) := --- /- Here is the main part. -/ --- (S.mkFunctor (pr₀₁₂_₀₁ f i j k)).mapIso (d.φ i j) --- _ ≅ (S.mkFunctor ((pr₀₁₂_₀₁ f i j k) ≫ pr₀₁_₁ f i j)).obj (d.X j) := --- (S.mapComp (mkHom ((pr₀₁_₁ f i j).op)) (mkHom ((pr₀₁₂_₀₁ f i j k).op))).symm.app (d.X j) --- _ ≅ (S.mkFunctor (pr₀₁₂_₁ f i j k)).obj (d.X j) := --- (S.map₂Iso (Discrete.eqToIso' (congrArg op (pr₀₁₂_₁_def₀₁ f)))).symm.app (d.X j) - --- def cocycleMap₁₂ (d : PreDescentData S U f) (i j k : I) : --- (S.mkFunctor (pr₀₁₂_₁ f i j k)).obj (d.X j) ≅ (S.mkFunctor (pr₀₁₂_₂ f i j k)).obj (d.X k) := --- calc --- (S.mkFunctor (pr₀₁₂_₁ f i j k)).obj (d.X j) ≅ --- (S.mkFunctor (pr₀₁₂_₁₂ f i j k ≫ pr₁₂_₁ f j k)).obj (d.X j) := --- (S.map₂Iso (Discrete.eqToIso' (congrArg op (pr₀₁₂_₁_def₁₂ f)))).app (d.X j) --- _ ≅ (S.mkFunctor (pr₁₂_₁ f j k) ≫ S.mkFunctor (pr₀₁₂_₁₂ f i j k)).obj (d.X j) := --- (S.mapComp (mkHom ((pr₁₂_₁ f j k).op)) (mkHom ((pr₀₁₂_₁₂ f i j k).op))).app (d.X j) --- _ ≅ (S.mkFunctor (pr₁₂_₂ f j k) ≫ S.mkFunctor (pr₀₁₂_₁₂ f i j k)).obj (d.X k) := --- /- Here is the main part. -/ --- (S.mkFunctor (pr₀₁₂_₁₂ f i j k)).mapIso (d.φ j k) --- _ ≅ (S.mkFunctor ((pr₀₁₂_₁₂ f i j k) ≫ pr₁₂_₂ f j k)).obj (d.X k) := --- (S.mapComp (mkHom ((pr₁₂_₂ f j k).op)) (mkHom ((pr₀₁₂_₁₂ f i j k).op))).symm.app (d.X k) --- _ ≅ (S.mkFunctor (pr₀₁₂_₂ f i j k)).obj (d.X k) := --- (S.map₂Iso (Discrete.eqToIso' (congrArg op (pr₀₁₂_₂_def₁₂ f)))).symm.app (d.X k) - --- def cocycleMap₀₂ (d : PreDescentData S U f) (i j k : I) : --- (S.mkFunctor (pr₀₁₂_₀ f i j k)).obj (d.X i) ≅ (S.mkFunctor (pr₀₁₂_₂ f i j k)).obj (d.X k) := --- calc --- (S.mkFunctor (pr₀₁₂_₀ f i j k)).obj (d.X i) ≅ --- (S.mkFunctor (pr₀₁₂_₀₂ f i j k ≫ pr₀₂_₀ f i k)).obj (d.X i) := --- (S.map₂Iso (Discrete.eqToIso' (congrArg op (pr₀₁₂_₀_def₀₂ f)))).app (d.X i) --- _ ≅ (S.mkFunctor (pr₀₂_₀ f i k) ≫ S.mkFunctor (pr₀₁₂_₀₂ f i j k)).obj (d.X i) := --- (S.mapComp (mkHom ((pr₀₂_₀ f i k).op)) (mkHom ((pr₀₁₂_₀₂ f i j k).op))).app (d.X i) --- _ ≅ (S.mkFunctor (pr₀₂_₂ f i k) ≫ S.mkFunctor (pr₀₁₂_₀₂ f i j k)).obj (d.X k) := --- /- Here is the main part. -/ --- (S.mkFunctor (pr₀₁₂_₀₂ f i j k)).mapIso (d.φ i k) --- _ ≅ (S.mkFunctor ((pr₀₁₂_₀₂ f i j k) ≫ pr₀₂_₂ f i k)).obj (d.X k) := --- (S.mapComp (mkHom ((pr₀₂_₂ f i k).op)) (mkHom ((pr₀₁₂_₀₂ f i j k).op))).symm.app (d.X k) --- _ ≅ (S.mkFunctor (pr₀₁₂_₂ f i j k)).obj (d.X k) := --- (S.map₂Iso (Discrete.eqToIso' (congrArg op (pr₀₁₂_₂_def₀₂ f)))).symm.app (d.X k) - -#check op_comp - -end PreDescentData - -example (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) - (U : C) {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) - [(Presieve.ofArrows V f).HasTriplewisePullbacks] (d : PreDescentData S U f) : Prop := - ∀ i j k : I, - let ι : Direction → I - | .left => i - | .middle => j - | .right => k - d.cocycleMap ι .left_middle ≪≫ d.cocycleMap ι .middle_right = d.cocycleMap ι .left_right - --- @[simp] -def fromDirection {I : Type v₂} (i j k : I) : Direction → I - | .left => i - | .middle => j - | .right => k - -@[simp] -theorem fromDirection_left {I : Type v₂} (i j k : I) : fromDirection i j k 0 = i := rfl - -@[simp] -theorem fromDirection_middle {I : Type v₂} (i j k : I) : fromDirection i j k 1 = j := rfl - -@[simp] -theorem fromDirection_right {I : Type v₂} (i j k : I) : fromDirection i j k 2 = k := rfl - - -def cocycleMap' {S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}} - {U : C} {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) - [(Presieve.ofArrows V f).HasTriplewisePullbacks] (d : PreDescentData S U f) (i j k : I) := - d.cocycleMap (fromDirection i j k) - + {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₁}) - (U : C) {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) - [(Presieve.ofArrows V f).HasTriplewisePullbacks] extends PreDescentData S U f where - /-- The cocycle condition for `φᵢⱼ`. -/ - cocycle_condition : ∀ i j k : I, - -- PreDescentData.cocycleMap₀₁ toPreDescentData i j k ≪≫ - -- PreDescentData.cocycleMap₁₂ toPreDescentData i j k = - -- PreDescentData.cocycleMap₀₂ toPreDescentData i j k - toPreDescentData.cocycleMap (fromDirection i j k) .left_middle ≪≫ - toPreDescentData.cocycleMap (fromDirection i j k) .middle_right = - toPreDescentData.cocycleMap (fromDirection i j k) .left_right - - -- let φ₁₂ := - -- (mapCompCatApp _ _ _).hom ≫ (S.mkFunctor (pr₁₂ f i j k)).map (φ j k).hom ≫ (mapCompCatApp _ _ _).inv - -- let φ₀₂ := - -- (mapCompCatApp _ _ _).hom ≫ (S.mkFunctor (pr₀₂ f i j k)).map (φ i k).hom ≫ (mapCompCatApp _ _ _).inv - -- let φ₀₁ := - -- (mapCompCatApp _ _ _).hom ≫ (S.mkFunctor (pr₀₁ f i j k)).map (φ i j).hom ≫ (mapCompCatApp _ _ _).inv - -- φ₀₁ ≫ - -- (S.map₂ (Discrete.eqToHom' (by rw [pullback_condition₁]))).app (X j) ≫ φ₁₂ = - -- (S.map₂ (Discrete.eqToHom' (by rw [pullback_condition₀]))).app (X i) ≫ - -- φ₀₂ ≫ - -- (S.map₂ (Discrete.eqToHom' (by rw [pullback_condition₂]))).app (X k) + {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 -export PreDescentData (cocycleMap) - -- PreDescentData.cocycleMap₁₂ - -- PreDescentData.cocycleMap₀₂ - -variable {S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}} {U : C} - {I : Type v₂} {V : I → C} {f : (i : I) → V i ⟶ U} - [(Presieve.ofArrows V f).HasTriplewisePullbacks] +variable {S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}} {a : C} {P : Presieve a} +/-- The homomorphism between two descent data. -/ @[ext] -structure Hom (d₁ d₂ : DescentData S U f) where - /-- A morphism in `S Vᵢ` for each `i : I`. -/ - hom : ∀ i, d₁.X i ⟶ d₂.X i - /-- The squares involving the `φᵢⱼ` commute. -/ - comm : ∀ i j : I, - (S.mkFunctor (pullback.fst (f i) (f j))).map (hom i) ≫ (d₂.φ i j).hom = - (d₁.φ i j).hom ≫ (S.mkFunctor (pullback.snd (f i) (f j))).map (hom j) +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 (d : DescentData S U f) : Hom d d where - hom i := 𝟙 (d.X i) - comm i j := by simp +def Hom.id (𝒟 : DescentData S P) : Hom 𝒟 𝒟 where + hom f _ := 𝟙 (𝒟.obj f) +/-- The composition of morphisms between descent data. -/ @[simps] -def Hom.comp {d₁ d₂ d₃ : DescentData S U f} (f : Hom d₁ d₂) (g : Hom d₂ d₃) : Hom d₁ d₃ where - hom i := f.hom i ≫ g.hom i - comm i j := by simp [g.comm, f.comm_assoc] - --- attribute [local simp] Hom.comm Hom.comm_assoc +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 U f) where +instance : Category (DescentData S P) where Hom := Hom - id d := Hom.id d - comp f g := Hom.comp f g - -def canonicalAux (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U : C) - {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) - [(Presieve.ofArrows V f).HasTriplewisePullbacks] (X : S.mkCat U) : - PreDescentData S U f where - X i := (S.mkFunctor (f i)).obj X - φ i j := - ((S.mapComp (mkHom (f i).op) (mkHom (pullback.fst (f i) (f j)).op)).symm ≪≫ - S.map₂Iso (Discrete.eqToIso' (congrArg op pullback.condition)) ≪≫ - -- ((compIso (f i).op (pullback.fst (f i) (f j)).op).symm ≪≫ - -- Discrete.eqToIso' (congrArg op pullback.condition) ≪≫ - -- compIso (f j).op (pullback.snd (f i) (f j)).op) ≪≫ - S.mapComp (mkHom (f j).op) (mkHom (pullback.snd (f i) (f j)).op)).app X - -open DirectionPair - -#check Pseudofunctor.map₂_associator_app - -example {B : Type} [Bicategory B] - (self : Pseudofunctor B Cat) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(self.obj a)) : - (self.map₂ (α_ f g h).hom).app X = - (self.mapComp (f ≫ g) h).hom.app X ≫ - (self.map h).map ((self.mapComp f g).hom.app X) ≫ - (α_ (self.map f) (self.map g) (self.map h)).hom.app X ≫ - (self.mapComp g h).inv.app ((self.map f).obj X) ≫ (self.mapComp f (g ≫ h)).inv.app X := by - dsimp only [Cat.comp_obj] - apply Pseudofunctor.map₂_associator_app - -variable {D E E' : Type} [Category D] [Category E][Category E'] -variable (F G H : C ⥤ D) {G : D ⥤ E} {H : E ⥤ E'} {X : C} -#check (H.obj (G.obj (F.obj X))) - - -example (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U : C) - {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) - [(Presieve.ofArrows V f).HasTriplewisePullbacks] (X : S.mkCat U) (i j k : I) (p : DirectionPair) : - let ι := (fun t ↦ f (fromDirection i j k t)) - ((canonicalAux S U f X).cocycleMap (fromDirection i j k) .left_middle).hom = - (S.mkFunctor (f i) ◁ S.map₂ (Discrete.eqToIso' sorry).hom ≫ - S.mkFunctor (f i) ◁ (S.mapCompCat (pullback.fst (f i) (f j)) (proj₂ ι .left_middle)).hom ≫ - (α_ _ _ _).inv ≫ - (S.mapCompCat (f i) (pullback.fst (f i) (f j))).inv ▷ S.mkFunctor (proj₂ ι .left_middle) ≫ - S.map₂ - ((compIso (f i).op (pullback.fst (f i) (f j)).op).inv ≫ - (Discrete.eqToIso' sorry).hom ≫ (compIso (f j).op (pullback.snd (f i) (f j)).op).hom) ▷ S.mkFunctor (proj₂ ι .left_middle) ≫ - (S.mapCompCat (f j) (pullback.snd (f i) (f j))).hom ▷ S.mkFunctor (proj₂ ι .left_middle) ≫ - (α_ _ _ _).hom ≫ - S.mkFunctor (f j) ◁ (S.mapCompCat (pullback.snd (f i) (f j)) (proj₂ ι .left_middle)).inv ≫ - S.mkFunctor (f j) ◁ (S.map₂Iso (Discrete.eqToIso' sorry)).inv).app X := by - dsimp only [fromDirection_left, fromDirection_middle, fromDirection_right, fst, mkFunctor, - canonicalAux, compIso, snd, cocycleMap, op_comp, Cat.comp_obj, mapCompCat, Iso.trans_def, - Iso.trans_hom, Iso.app_hom, Functor.mapIso_hom, eqToIso.hom, eqToHom_refl, - PrelaxFunctor.mapFunctor_map, Iso.symm_hom, eqToIso.inv, NatTrans.comp_app, Functor.mapIso_inv, - Cat.comp_app, Cat.whiskerLeft_app, Cat.whiskerRight_app, Lean.Elab.WF.paramLet] - simp only [Functor.map_comp, Category.assoc] - congr 2 - rw [Cat.associator_hom_app] - rw [Cat.associator_inv_app] - dsimp only [Iso.refl_inv, Cat.comp_obj] - simp only [← Category.assoc]; congr 2; simp only [Category.assoc] - simp only [eqToHom_refl, Category.id_comp, Category.comp_id] - - - -def caconicalCocycleMapAux (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U : C) - {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) - [(Presieve.ofArrows V f).HasTriplewisePullbacks] (X : S.mkCat U) (i j k : I) (p : DirectionPair) : - let ι := (fun t ↦ f (fromDirection i j k t)) - let i' := (fromDirection i j k p.fst) - let j' := (fromDirection i j k p.snd) - S.mkFunctor (f i') ≫ S.mkFunctor (proj₁ ι p.fst) ⟶ S.mkFunctor (f j') ≫ S.mkFunctor (proj₁ ι p.snd) := by - sorry + id := Hom.id + comp := Hom.comp -theorem canonical_cocycle_aux₁ (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U : C) - {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) - [(Presieve.ofArrows V f).HasTriplewisePullbacks] (X : S.mkCat U) (i j k : I) (p : DirectionPair) : - let ι := (fun t ↦ f (fromDirection i j k t)) - let i' := (fromDirection i j k p.fst) - let j' := (fromDirection i j k p.snd) - ((canonicalAux S U f X).cocycleMap (fromDirection i j k) p).hom = - (S.mkFunctor (f i') ◁ S.map₂ (Discrete.eqToIso' sorry).hom ≫ - S.mkFunctor (f i') ◁ (S.mapCompCat (pullback.fst (f i') (f j')) (proj₂ ι p)).hom ≫ - (α_ _ _ _).inv ≫ - (S.mapCompCat (f i') (pullback.fst (f i') (f j'))).inv ▷ S.mkFunctor (proj₂ ι p) ≫ - S.map₂ - ((compIso (f i').op (pullback.fst (f i') (f j')).op).inv ≫ - (Discrete.eqToIso' sorry).hom ≫ (compIso (f j').op (pullback.snd (f i') (f j')).op).hom) ▷ S.mkFunctor (proj₂ ι p) ≫ - (S.mapCompCat (f j') (pullback.snd (f i') (f j'))).hom ▷ S.mkFunctor (proj₂ ι p) ≫ - (α_ _ _ _).hom ≫ - S.mkFunctor (f j') ◁ (S.mapCompCat (pullback.snd (f i') (f j')) (proj₂ ι p)).inv ≫ - S.mkFunctor (f j') ◁ (S.map₂Iso (Discrete.eqToIso' sorry)).inv).app X := by - dsimp only [fromDirection_left, fromDirection_middle, fromDirection_right, fst, mkFunctor, - canonicalAux, compIso, snd, cocycleMap, op_comp, Cat.comp_obj, mapCompCat, Iso.trans_def, - Iso.trans_hom, Iso.app_hom, Functor.mapIso_hom, eqToIso.hom, eqToHom_refl, - PrelaxFunctor.mapFunctor_map, Iso.symm_hom, eqToIso.inv, NatTrans.comp_app, Functor.mapIso_inv, - Cat.comp_app, Cat.whiskerLeft_app, Cat.whiskerRight_app, Lean.Elab.WF.paramLet] - simp only [Functor.map_comp, Category.assoc] - congr 2 - rw [Cat.associator_hom_app] - rw [Cat.associator_inv_app] - dsimp only [Iso.refl_inv, Cat.comp_obj] - simp only [← Category.assoc]; congr 2; simp only [Category.assoc] - simp only [eqToHom_refl, Category.id_comp, Category.comp_id] - --- example (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U : C) --- {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) --- [(Presieve.ofArrows V f).HasTriplewisePullbacks] (X : S.mkCat U) (i j k : I) (p : DirectionPair) : --- let ι := (fun t ↦ f (fromDirection i j k t)) --- ((canonicalAux S U f X).cocycleMap (fromDirection i j k) .left_middle).hom = --- (S.mkFunctor (f i) ◁ S.map₂ (Discrete.eqToIso' sorry).hom ≫ --- S.mkFunctor (f i) ◁ (S.mapCompCat (pullback.fst (f i) (f j)) (proj₂ ι .left_middle)).hom ≫ --- (α_ _ _ _).inv ≫ --- (S.mapCompCat (f i) (pullback.fst (f i) (f j))).inv ▷ S.mkFunctor (proj₂ ι .left_middle) ≫ --- S.map₂ --- ((compIso (f i).op (pullback.fst (f i) (f j)).op).inv ≫ --- (Discrete.eqToIso' sorry).hom ≫ (compIso (f j).op (pullback.snd (f i) (f j)).op).hom) ▷ S.mkFunctor (proj₂ ι .left_middle) ≫ --- (S.mapCompCat (f j) (pullback.snd (f i) (f j))).hom ▷ S.mkFunctor (proj₂ ι .left_middle) ≫ --- (α_ _ _ _).hom ≫ --- S.mkFunctor (f j) ◁ (S.mapCompCat (pullback.snd (f i) (f j)) (proj₂ ι .left_middle)).inv ≫ --- S.mkFunctor (f j) ◁ (S.map₂Iso (Discrete.eqToIso' sorry)).inv).app X := by --- dsimp only [mkFunctor] --- rw [S.mapComp_assoc_mapComp_inv_assoc] --- rw [S.mapComp_assoc_inv_mapComp_inv_assoc] --- rw [← S.map₂_whisker_right_assoc] --- rw [← S.map₂_comp_assoc] --- rw [← S.map₂_comp_assoc] --- rw [LocallyDiscrete.associator_hom] --- rw [LocallyDiscrete.associator_inv] --- dsimp only [compIso, Discrete.eqToIso', Discrete.eqToIso] --- dsimp only [eqToIso.hom, eqToIso.inv] --- simp only [fromDirection_left, fromDirection_middle, fromDirection_right, fst, snd, op_comp, --- - eqToHom_refl, Category.comp_id, Category.id_comp, Category.assoc, -PrelaxFunctor.map₂_comp, --- map₂_whisker_right, - eqToIso_refl, - Functor.mapIso_refl, PrelaxFunctor.mapFunctor_obj, --- Iso.refl_inv, -Cat.comp_app, Cat.comp_obj, Cat.whiskerLeft_app, Cat.whiskerRight_app, Cat.id_app] --- simp only [eqToHom_trans, eqToHom_whiskerRight] --- simp [- Cat.comp_app, Cat.comp_obj, Cat.whiskerLeft_app, Cat.id_app] --- simp only [Cat.comp_app, Cat.comp_obj, Cat.whiskerLeft_app, Cat.id_app] --- -- simp only [fromDirection_left, fromDirection_middle, fromDirection_right, fst, snd, op_comp, --- -- -eqToHom_refl, -eqToIso_refl, Functor.mapIso_inv, Iso.refl_inv, -PrelaxFunctor.mapFunctor_map, --- -- -Cat.comp_app, -Cat.comp_obj, -Cat.whiskerLeft_app] --- -- rw [Cat.associator_hom_app] --- dsimp --- simp --- -- simp only [fromDirection_left, fromDirection_middle, fromDirection_right, fst, snd, op_comp, --- -- eqToIso_refl, Iso.refl_hom, eqToIso.hom, PrelaxFunctor.map₂_comp, comp_whiskerRight, --- -- Functor.mapIso_refl, PrelaxFunctor.mapFunctor_obj, Iso.refl_inv, Category.assoc, Cat.comp_app, --- -- Cat.comp_obj, Cat.whiskerLeft_app, Cat.whiskerRight_app, Cat.id_app] --- -- rw? --- sorry - - -theorem cocycle_aux (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U : C) - {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) - [(Presieve.ofArrows V f).HasTriplewisePullbacks] - (X : S.mkCat U) (i j k : I) (p : DirectionPair) : - let ι := (fun t ↦ f (fromDirection i j k t)) - let i' := (fromDirection i j k p.fst) - let j' := (fromDirection i j k p.snd) - ((canonicalAux S U f X).cocycleMap (fromDirection i j k) p).hom = - (S.map (mkHom (f i').op) ◁ S.map₂ (eqToHom sorry) ≫ - (S.mapComp (mkHom (f i').op) - (mkHom (pullback.fst (f i') (f j')).op ≫ - mkHom (proj₂ ι p).op)).inv ≫ - S.map₂ (eqToHom sorry) ≫ - (S.mapComp (mkHom (f j').op) - (mkHom (pullback.snd (f i') (f j')).op ≫ - mkHom (proj₂ ι p).op)).hom ≫ - S.map (mkHom (f j').op) ◁ (S.map₂Iso (eqToIso sorry)).inv).app X := by - rw [canonical_cocycle_aux₁] - congr 1 - dsimp only [mkFunctor] - rw [S.mapComp_assoc_mapComp_inv_assoc] - rw [S.mapComp_assoc_inv_mapComp_inv_assoc] - rw [← S.map₂_whisker_right_assoc] - rw [← S.map₂_comp_assoc] - rw [← S.map₂_comp_assoc] - rw [LocallyDiscrete.associator_hom] - rw [LocallyDiscrete.associator_inv] - dsimp only [fromDirection_left, fromDirection_middle, fromDirection_right, fst, snd, op_comp, - -eqToIso_refl, Iso.refl_hom, eqToIso.hom, Functor.mapIso_inv, Iso.refl_inv, - PrelaxFunctor.mapFunctor_map, -eqToHom_refl] - simp only [-eqToHom_refl, comp_whiskerRight, Category.assoc, PrelaxFunctor.map₂_comp, - -map₂_whisker_right, Iso.inv_hom_id_assoc, -eqToIso_refl, Iso.refl_inv, PrelaxFunctor.map₂_id, - whiskerLeft_id, Category.id_comp] - congr 2 - simp only [← Category.assoc] - congr - simp only [Category.assoc] - rw [← S.map₂_comp_assoc] - rw [← S.map₂_comp_assoc] - rw [← S.map₂_comp_assoc] - rw [← S.map₂_comp] - congr 1 - apply Subsingleton.elim - -- dsimp [mkFunctor, canonicalAux, cocycleMap] - -- simp only [PrelaxFunctor.map₂_comp, Cat.comp_app, Category.assoc, Functor.map_comp, - -- mapCompCat] - -- -- simp only [← NatTrans.comp_app] - -- rw [S.mapComp_assoc_mapComp_inv_assoc] - -- rw [S.mapComp_assoc_inv_mapComp_inv_assoc] - -- simp only [- map₂_associator_inv, comp_whiskerRight, map₂_associator, Category.assoc, - -- Iso.inv_hom_id_assoc, PrelaxFunctor.map₂_id, whiskerLeft_id, Category.id_comp] - -- rw [← S.map₂_whisker_right_assoc] - -- rw [← S.map₂_comp_assoc] - -- rw [← S.map₂_comp_assoc] - -- rw [LocallyDiscrete.associator_hom] - -- rw [LocallyDiscrete.associator_inv] - --- theorem cocycle_aux' (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U : C) --- {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) --- [(Presieve.ofArrows V f).HasTriplewisePullbacks] --- (X : S.mkCat U) (i j k : I) (p : DirectionPair) : --- let ι := (fun t ↦ f (fromDirection i j k t)) --- let i' := (fromDirection i j k p.fst) --- let j' := (fromDirection i j k p.snd) --- ((canonicalAux S U f X).cocycleMap (fromDirection i j k) p).hom = --- (S.map (mkHom (f i').op) ◁ S.map₂ (eqToHom sorry) ≫ --- (S.mapComp (mkHom (f i').op) --- (mkHom (pullback.fst (f i') (f j')).op ≫ --- mkHom (proj₂ ι p).op)).inv ≫ --- S.map₂ (eqToHom sorry) ≫ --- (S.mapComp (mkHom (f j').op) --- (mkHom (pullback.snd (f i') (f j')).op ≫ --- mkHom (proj₂ ι p).op)).hom ≫ --- S.map (mkHom (f j').op) ◁ (S.map₂Iso (eqToIso sorry)).inv).app X := by --- dsimp [mkFunctor, canonicalAux, cocycleMap] --- simp only [PrelaxFunctor.map₂_comp, Cat.comp_app, Category.assoc, Functor.map_comp] --- rw [S.mapComp_assoc_mapComp_inv_assoc] --- rw [S.mapComp_assoc_inv_mapComp_inv_assoc] --- rw [← S.map₂_whisker_right_assoc] --- rw [← S.map₂_comp_assoc] --- rw [← S.map₂_comp_assoc] --- rw [LocallyDiscrete.associator_hom] --- rw [LocallyDiscrete.associator_inv] --- dsimp only [compIso, Discrete.eqToIso', Discrete.eqToIso] --- dsimp only [eqToIso.hom, eqToIso.inv] --- simp only [fromDirection_left, fromDirection_middle, fromDirection_right, fst, snd, op_comp, --- - eqToHom_refl, Category.comp_id, Category.id_comp, Category.assoc, -PrelaxFunctor.map₂_comp, --- map₂_whisker_right, - eqToIso_refl, - Functor.mapIso_refl, PrelaxFunctor.mapFunctor_obj, --- Iso.refl_inv, -Cat.comp_app, Cat.comp_obj, Cat.whiskerLeft_app, Cat.whiskerRight_app, Cat.id_app] - - -def canonical (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U : C) - {I : Type v₂} {V : I → C} (f : (i : I) → V i ⟶ U) (X : S.mkCat U) - [(Presieve.ofArrows V f).HasTriplewisePullbacks] : - DescentData S U f where - toPreDescentData := canonicalAux S U f X - cocycle_condition i j k := by - apply Iso.ext - dsimp only [Iso.trans_hom] - rw [cocycle_aux _ _ _ _ _ _ _ DirectionPair.left_middle] - rw [cocycle_aux _ _ _ _ _ _ _ DirectionPair.middle_right] - rw [cocycle_aux _ _ _ _ _ _ _ DirectionPair.left_right] - simp only [← NatTrans.comp_app] - apply congrFun (congrArg _ _) +/-- 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] - dsimp only [fromDirection_left, fromDirection_middle, fromDirection_right, fst, snd] - rw [S.map₂Iso_inv] - dsimp only [eqToIso.inv] - slice_lhs 5 6 => - rw [← whiskerLeft_comp] - rw [← S.map₂_comp] - rw [eqToHom_trans] - slice_lhs 4 6 => - rw [← map₂_whisker_left] - rw [whiskerLeft_eqToHom] + 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 [← S.map₂_comp_assoc] - rw [← S.map₂_comp_assoc] - simp only [eqToHom_trans] - rw [S.map₂Iso_inv, S.map₂Iso_inv] - simp only [eqToIso.inv] - simp only [map₂_whisker_left_symm, Category.assoc] - simp only [whiskerLeft_eqToHom] - simp only [Iso.hom_inv_id_assoc] - simp only [S.map₂_eqToHom] - simp only [eqToHom_refl, Category.id_comp, eqToHom_trans_assoc] - -instance (U : C) : - (Presieve.ofArrows (fun (_ : Unit) ↦ U) (fun _ ↦ 𝟙 U)).HasTriplewisePullbacks where - has_pullbacks := by - intro Y Z f hf g hg - rw [Presieve.ofArrows_pUnit] at hf - cases hf - exact hasPullback_of_left_iso (𝟙 U) g - has_triplewise_pullbacks := by - intro X₁ X₂ X₃ f₁ hf₁ f₂ hf₂ f₃ hf₃ _ _ - rw [Presieve.ofArrows_pUnit] at hf₁ hf₂ hf₃ - cases hf₁; cases hf₂; cases hf₃ - exact hasPullback_of_right_iso (pullback.snd (𝟙 U) (𝟙 U)) (pullback.fst (𝟙 U) (𝟙 U)) - -def trivial (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (U : C) (X : S.mkCat U) : - DescentData S U (fun (_ : Unit) ↦ 𝟙 U) where - X _ := (S.mkFunctor (𝟙 U)).obj X - φ _ _ := - (S.map₂Iso (Discrete.eqToIso' (by rw [fst_eq_snd_of_mono_eq (𝟙 U)]))).app ((S.mkFunctor (𝟙 U)).obj X) - -- Iso.refl _ - cocycle_condition := by - -- ext x - intro ⟨⟩ ⟨⟩ ⟨⟩ - - sorry + 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 @@ -762,4 +179,4 @@ end Pseudofunctor end CategoryTheory -end +#lint diff --git a/Mathlib/CategoryTheory/Stack/Descent2.lean b/Mathlib/CategoryTheory/Stack/Descent2.lean deleted file mode 100644 index 95e5d7d3141ead..00000000000000 --- a/Mathlib/CategoryTheory/Stack/Descent2.lean +++ /dev/null @@ -1,141 +0,0 @@ -import Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor -import Mathlib.CategoryTheory.Bicategory.LocallyDiscrete -import Mathlib.CategoryTheory.Category.Cat -import Mathlib.CategoryTheory.Sites.Grothendieck -import Mathlib.CategoryTheory.Sites.Sheaf -import Mathlib.CategoryTheory.Sites.Over - -import Mathlib.Tactic.Widget.StringDiagram - -noncomputable section - -universe v u v₁ u₁ v₂ - -open CategoryTheory Opposite Bicategory -open CategoryTheory.Limits LocallyDiscrete -open ProofWidgets Mathlib.Tactic.Widget - - -variable {C : Type u} [Category.{v} C] - -namespace CategoryTheory - -namespace Pseudofunctor - -open Category Opposite Limits - -abbrev mkCat (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) (X : C) : Cat := - S.obj ⟨op X⟩ - -abbrev mkFunctor (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) {X Y : C} (f : Y ⟶ X) : - S.mkCat X ⟶ S.mkCat Y := - S.map (LocallyDiscrete.mkHom f.op) - -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) - -variable {B : Type} [Bicategory B] - -structure PreDescentData (S : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat.{v₁, u₁}) - {a : C} (P : Presieve a) where - obj : ∀ {b : C} (f : b ⟶ a) (_ : P f := by cat_disch), S.obj ⟨op b⟩ - 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) - -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.mapId ⟨op 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} - -@[ext] -structure Hom (𝒟₁ 𝒟₂ : DescentData S P) where - 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 - -@[simps] -def Hom.id (𝒟 : DescentData S P) : Hom 𝒟 𝒟 where - hom f _ := 𝟙 (𝒟.obj f) - -@[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, assoc] - rw [η₂.comm f g, η₁.comm_assoc f g] - -instance : Category (DescentData S P) where - Hom := Hom - id := Hom.id - comp := Hom.comp - -@[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 [assoc] - rw [Cat.rightUnitor_eqToIso, LocallyDiscrete.rightUnitor_inv, S.map₂_eqToHom] - simp only [eqToIso_refl, Iso.refl_hom, comp_id, eqToHom_naturality_assoc, 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 - this 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, 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 [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 From 1ae7d745d8f79e3b24efa6dfed2eb2f05e897185 Mon Sep 17 00:00:00 2001 From: Yuma Mizuno Date: Sun, 14 Sep 2025 13:17:36 +0100 Subject: [PATCH 4/6] tidy up --- .../Bicategory/Functor/Pseudofunctor.lean | 23 ------------------- .../Bicategory/LocallyDiscrete.lean | 19 +-------------- Mathlib/CategoryTheory/Stack/Descent.lean | 2 -- 3 files changed, 1 insertion(+), 43 deletions(-) diff --git a/Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean b/Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean index 6fecd98b8a394e..9177a94d7ed33c 100644 --- a/Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean +++ b/Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean @@ -157,13 +157,6 @@ section variable (F : Pseudofunctor B C) {a b c d : B} -#check map₂_whisker_left - -lemma map₂_whisker_left_symm (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h) : - F.map f ◁ F.map₂ η = (F.mapComp f g).inv ≫ F.map₂ (f ◁ η) ≫ (F.mapComp f h).hom := by - simp - -- Proof goes here - @[reassoc, to_app] lemma map₂_associator_inv (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : F.map₂ (α_ f g h).inv = @@ -176,8 +169,6 @@ lemma map₂_associator_inv (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : rw [← F.map₂_inv] simp -#check map₂_right_unitor - @[reassoc, to_app] lemma map₂_left_unitor_inv (f : a ⟶ b) : F.map₂ (λ_ f).inv = @@ -224,20 +215,6 @@ 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_assoc_mapComp_inv {c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : - (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).hom ≫ (F.mapComp f (g ≫ h)).hom := by - simp - -@[reassoc, to_app] -lemma mapComp_assoc_inv_mapComp_inv {c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : - 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).inv ≫ (F.mapComp (f ≫ g) h).hom := by - simp [map₂_associator_inv] - @[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 ≫ diff --git a/Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean b/Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean index 6a8f8c689b7ed0..0bd1fe8a4b3dd3 100644 --- a/Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean +++ b/Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean @@ -55,9 +55,6 @@ instance [DecidableEq C] : DecidableEq (LocallyDiscrete C) := instance [Inhabited C] : Inhabited (LocallyDiscrete C) := ⟨⟨default⟩⟩ --- abbrev Hom [CategoryStruct.{v} C] (a b : LocallyDiscrete C) : Type v := --- Discrete (a.as ⟶ b.as) - instance categoryStruct [CategoryStruct.{v} C] : CategoryStruct (LocallyDiscrete C) where Hom a b := Discrete (a.as ⟶ b.as) id a := ⟨𝟙 a.as⟩ @@ -88,26 +85,12 @@ 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 eqToHom_eq_of_hom {X Y : LocallyDiscrete C} {f g : X ⟶ Y} (η : f ⟶ g) : +theorem eq_eqToHom {X Y : LocallyDiscrete C} {f g : X ⟶ Y} (η : f ⟶ g) : η = eqToHom (eq_of_hom η) := Subsingleton.elim _ _ end LocallyDiscrete -namespace LocallyDiscrete - -variable [Category.{v} C] - -def idIso (a : C) : - mkHom (𝟙 a) ≅ 𝟙 (mk a) := - eqToIso rfl - -def compIso {a b c : C} (f : a ⟶ b) (g : b ⟶ c) : - mkHom (f ≫ g) ≅ mkHom f ≫ mkHom g := - eqToIso rfl - -end LocallyDiscrete - variable (C) variable [Category.{v} C] diff --git a/Mathlib/CategoryTheory/Stack/Descent.lean b/Mathlib/CategoryTheory/Stack/Descent.lean index 7c42788f3cb622..5e5f0dd5c735b6 100644 --- a/Mathlib/CategoryTheory/Stack/Descent.lean +++ b/Mathlib/CategoryTheory/Stack/Descent.lean @@ -178,5 +178,3 @@ end DescentData end Pseudofunctor end CategoryTheory - -#lint From 931abdf3ae58af249c930be43fceaef44498c695 Mon Sep 17 00:00:00 2001 From: Yuma Mizuno Date: Sun, 14 Sep 2025 13:22:31 +0100 Subject: [PATCH 5/6] `lake exe mk_all` --- Mathlib.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Mathlib.lean b/Mathlib.lean index 99a6180240091f..89ff9f248b23bb 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2771,6 +2771,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 From 11140407c72622a97f59b5b4eefa0ccf31a62390 Mon Sep 17 00:00:00 2001 From: Yuma Mizuno Date: Sun, 14 Sep 2025 14:13:12 +0100 Subject: [PATCH 6/6] docs --- Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean b/Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean index 0bd1fe8a4b3dd3..118c7cd230aecf 100644 --- a/Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean +++ b/Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean @@ -62,6 +62,7 @@ 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⟩