|
| 1 | +/- |
| 2 | +Copyright (c) 2021 Adam Topaz. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Adam Topaz |
| 5 | +-/ |
| 6 | +import category_theory.sites.compatible_sheafification |
| 7 | +import category_theory.adjunction.whiskering |
| 8 | + |
| 9 | +/-! |
| 10 | +
|
| 11 | +In this file, we show that an adjunction `F ⊣ G` induces an adjunction between |
| 12 | +categories of sheaves, under certain hypotheses on `F` and `G`. |
| 13 | +
|
| 14 | +-/ |
| 15 | + |
| 16 | +namespace category_theory |
| 17 | + |
| 18 | +open category_theory.grothendieck_topology |
| 19 | +open category_theory |
| 20 | +open category_theory.limits |
| 21 | +open opposite |
| 22 | + |
| 23 | +universes w₁ w₂ v u |
| 24 | +variables {C : Type u} [category.{v} C] (J : grothendieck_topology C) |
| 25 | +variables {D : Type w₁} [category.{max v u} D] |
| 26 | +variables {E : Type w₂} [category.{max v u} E] |
| 27 | +variables {F : D ⥤ E} {G : E ⥤ D} |
| 28 | +variables [∀ (X : C) (S : J.cover X) (P : Cᵒᵖ ⥤ D), |
| 29 | + preserves_limit (S.index P).multicospan F] |
| 30 | + |
| 31 | +variables |
| 32 | + [concrete_category.{max v u} D] |
| 33 | + [preserves_limits (forget D)] |
| 34 | + |
| 35 | +/-- The forgetful functor from `Sheaf J D` to sheaves of types, for a concrete category `D` |
| 36 | +whose forgetful functor preserves the correct limits. -/ |
| 37 | +abbreviation Sheaf_forget : Sheaf J D ⥤ SheafOfTypes J := |
| 38 | +Sheaf_compose J (forget D) ⋙ (Sheaf_equiv_SheafOfTypes J).functor |
| 39 | + |
| 40 | +-- We need to sheafify... |
| 41 | +variables |
| 42 | + [∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.cover X), has_multiequalizer (S.index P)] |
| 43 | + [∀ (X : C), has_colimits_of_shape (J.cover X)ᵒᵖ D] |
| 44 | + [∀ (X : C), preserves_colimits_of_shape (J.cover X)ᵒᵖ (forget D)] |
| 45 | + [reflects_isomorphisms (forget D)] |
| 46 | + |
| 47 | +namespace Sheaf |
| 48 | +noncomputable theory |
| 49 | + |
| 50 | +/-- This is the functor sending a sheaf `X : Sheaf J E` to the sheafification |
| 51 | +of `X ⋙ G`. -/ |
| 52 | +abbreviation compose_and_sheafify (G : E ⥤ D) : Sheaf J E ⥤ Sheaf J D := |
| 53 | +Sheaf_to_presheaf J E ⋙ (whiskering_right _ _ _).obj G ⋙ presheaf_to_Sheaf J D |
| 54 | + |
| 55 | +/-- An auxiliary definition to be used in defining `category_theory.Sheaf.adjunction` below. -/ |
| 56 | +@[simps] |
| 57 | +def compose_equiv (adj : G ⊣ F) (X : Sheaf J E) (Y : Sheaf J D) : |
| 58 | +((compose_and_sheafify J G).obj X ⟶ Y) ≃ (X ⟶ (Sheaf_compose J F).obj Y) := |
| 59 | +let A := adj.whisker_right Cᵒᵖ in |
| 60 | +{ to_fun := λ η, A.hom_equiv _ _ (J.to_sheafify _ ≫ η), |
| 61 | + inv_fun := λ γ, J.sheafify_lift ((A.hom_equiv _ _).symm ((Sheaf_to_presheaf _ _).map γ)) Y.2, |
| 62 | + left_inv := begin |
| 63 | + intros η, |
| 64 | + symmetry, |
| 65 | + apply J.sheafify_lift_unique, |
| 66 | + erw equiv.symm_apply_apply, |
| 67 | + end, |
| 68 | + right_inv := begin |
| 69 | + intros γ, |
| 70 | + dsimp, |
| 71 | + rw [J.to_sheafify_sheafify_lift, equiv.apply_symm_apply], |
| 72 | + end } |
| 73 | + |
| 74 | +/-- An adjunction `adj : G ⊣ F` with `F : D ⥤ E` and `G : E ⥤ D` induces an adjunction |
| 75 | +between `Sheaf J D` and `Sheaf J E`, in contexts where one can sheafify `D`-valued presheaves, |
| 76 | +and `F` preserves the correct limits. -/ |
| 77 | +def adjunction (adj : G ⊣ F) : compose_and_sheafify J G ⊣ Sheaf_compose J F := |
| 78 | +adjunction.mk_of_hom_equiv |
| 79 | +{ hom_equiv := compose_equiv J adj, |
| 80 | + hom_equiv_naturality_left_symm' := begin |
| 81 | + intros X' X Y f g, |
| 82 | + symmetry, |
| 83 | + apply J.sheafify_lift_unique, |
| 84 | + dsimp [compose_equiv, adjunction.whisker_right], |
| 85 | + erw [sheafification_map_sheafify_lift, to_sheafify_sheafify_lift], |
| 86 | + ext : 2, |
| 87 | + dsimp, |
| 88 | + erw nat_trans.comp_app, |
| 89 | + simp, |
| 90 | + end, |
| 91 | + hom_equiv_naturality_right' := begin |
| 92 | + intros X Y Y' f g, |
| 93 | + dsimp [compose_equiv, adjunction.whisker_right], |
| 94 | + ext : 2, |
| 95 | + erw [nat_trans.comp_app, nat_trans.comp_app, nat_trans.comp_app, nat_trans.comp_app], |
| 96 | + dsimp, |
| 97 | + erw [nat_trans.comp_app f g], |
| 98 | + simp only [category.id_comp, category.comp_id, category.assoc, functor.map_comp], |
| 99 | + end } |
| 100 | + |
| 101 | +@[simp] |
| 102 | +lemma adjunction_hom_equiv_apply (adj : G ⊣ F) (X : Sheaf J D) (Y : Sheaf J E) |
| 103 | + (η : (compose_and_sheafify J G).obj Y ⟶ X) : (adjunction J adj).hom_equiv _ _ η = |
| 104 | + (adj.whisker_right _).hom_equiv _ _ (J.to_sheafify _ ≫ η) := rfl |
| 105 | + |
| 106 | +@[simp] |
| 107 | +lemma adjunction_hom_equiv_symm_apply (adj : G ⊣ F) (X : Sheaf J D) (Y : Sheaf J E) |
| 108 | + (η : Y ⟶ (Sheaf_compose J F).obj X) : ((adjunction J adj).hom_equiv _ _).symm η = |
| 109 | + J.sheafify_lift (((adj.whisker_right _).hom_equiv _ _).symm η) X.2 := rfl |
| 110 | + |
| 111 | +@[simp] |
| 112 | +lemma adjunction_unit_app (adj : G ⊣ F) (X : Sheaf J E) : |
| 113 | + (Sheaf_to_presheaf _ _).map ((adjunction J adj).unit.app X) = |
| 114 | + (adj.whisker_right _).unit.app _ ≫ whisker_right (J.to_sheafify _) F := |
| 115 | +begin |
| 116 | + dsimp [adjunction], |
| 117 | + erw category.comp_id, |
| 118 | + refl, |
| 119 | +end |
| 120 | + |
| 121 | +@[simp] |
| 122 | +lemma adjunction_counit_app (adj : G ⊣ F) (Y : Sheaf J D) : |
| 123 | + (Sheaf_to_presheaf _ _).map ((adjunction J adj).counit.app Y) = |
| 124 | + J.sheafify_lift ((functor.associator _ _ _).hom ≫ |
| 125 | + (adj.whisker_right _).counit.app _) Y.2 := |
| 126 | +begin |
| 127 | + dsimp [adjunction], |
| 128 | + simp only [whiskering_right_obj_map, adjunction.hom_equiv_counit], |
| 129 | + erw [whisker_right_id], |
| 130 | + refl, |
| 131 | +end |
| 132 | + |
| 133 | +instance [is_right_adjoint F] : is_right_adjoint (Sheaf_compose J F) := |
| 134 | +⟨_, adjunction J (adjunction.of_right_adjoint F)⟩ |
| 135 | + |
| 136 | +section forget_to_type |
| 137 | + |
| 138 | +/-- This is the functor sending a sheaf of types `X` to the sheafification of `X ⋙ G`. -/ |
| 139 | +abbreviation compose_and_sheafify_from_types (G : Type (max v u) ⥤ D) : |
| 140 | + SheafOfTypes J ⥤ Sheaf J D := |
| 141 | +(Sheaf_equiv_SheafOfTypes J).inverse ⋙ compose_and_sheafify _ G |
| 142 | + |
| 143 | +/-- A variant of the adjunction between sheaf categories, in the case where the right adjoint |
| 144 | +is the forgetful functor to sheaves of types. -/ |
| 145 | +def adjunction_to_types {G : Type (max v u) ⥤ D} (adj : G ⊣ forget D) : |
| 146 | + compose_and_sheafify_from_types J G ⊣ Sheaf_forget J := |
| 147 | +adjunction.comp _ _ ((Sheaf_equiv_SheafOfTypes J).symm.to_adjunction) (adjunction J adj) |
| 148 | + |
| 149 | +@[simp] |
| 150 | +lemma adjunction_to_types_hom_equiv_apply {G : Type (max v u) ⥤ D} (adj : G ⊣ forget D) |
| 151 | + (X : Sheaf J D) (Y : SheafOfTypes J) (η : (compose_and_sheafify_from_types J G).obj Y ⟶ X) : |
| 152 | + (adjunction_to_types J adj).hom_equiv _ _ η = |
| 153 | + (adj.whisker_right _).hom_equiv _ _ (J.to_sheafify _ ≫ η) := rfl |
| 154 | + |
| 155 | +@[simp] |
| 156 | +lemma adjunction_to_types_hom_equiv_symm_apply' {G : Type (max v u) ⥤ D} (adj : G ⊣ forget D) |
| 157 | + (X : Sheaf J D) (Y : SheafOfTypes J) (η : Y ⟶ (Sheaf_forget J).obj X) : |
| 158 | + ((adjunction_to_types J adj).hom_equiv _ _).symm η = |
| 159 | + J.sheafify_lift (((adj.whisker_right _).hom_equiv _ _).symm η) X.2 := rfl |
| 160 | + |
| 161 | +@[simp] |
| 162 | +lemma adjunction_to_types_unit_app {G : Type (max v u) ⥤ D} (adj : G ⊣ forget D) |
| 163 | + (Y : SheafOfTypes J) : |
| 164 | + (SheafOfTypes_to_presheaf J).map ((adjunction_to_types J adj).unit.app Y) = |
| 165 | + (adj.whisker_right _).unit.app ((SheafOfTypes_to_presheaf J).obj Y) ≫ |
| 166 | + whisker_right (J.to_sheafify _) (forget D) := |
| 167 | +begin |
| 168 | + dsimp [adjunction_to_types, adjunction.comp], |
| 169 | + rw category.comp_id, |
| 170 | + change (SheafOfTypes_to_presheaf _).map _ = _, |
| 171 | + erw [functor.map_comp, adjunction_unit_app], |
| 172 | + refl, |
| 173 | +end |
| 174 | + |
| 175 | +@[simp] |
| 176 | +lemma adjunction_to_types_counit_app {G : Type (max v u) ⥤ D} (adj : G ⊣ forget D) |
| 177 | + (X : Sheaf J D) : |
| 178 | + (Sheaf_to_presheaf _ _).map ((adjunction_to_types J adj).counit.app X) = |
| 179 | + J.sheafify_lift ((functor.associator _ _ _).hom ≫ (adj.whisker_right _).counit.app _) X.2 := |
| 180 | +begin |
| 181 | + dsimp only [adjunction_to_types, adjunction.comp], |
| 182 | + erw [functor.map_comp, functor.map_comp, adjunction_counit_app, ← category.assoc], |
| 183 | + convert category.id_comp _, |
| 184 | + dsimp only [functor.associator], |
| 185 | + erw [functor.map_id, category.id_comp, functor.map_id], |
| 186 | + refl, |
| 187 | +end |
| 188 | + |
| 189 | +instance [is_right_adjoint (forget D)] : is_right_adjoint (Sheaf_forget J) := |
| 190 | +⟨_, adjunction_to_types J (adjunction.of_right_adjoint (forget D))⟩ |
| 191 | + |
| 192 | +end forget_to_type |
| 193 | + |
| 194 | +end Sheaf |
| 195 | + |
| 196 | +end category_theory |
0 commit comments