feat(category_theory/sites): The pushforward pullback adjunction (#11273)

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Author: erdOne

src/category_theory/sites/cover_preserving.lean

@@ -3,7 +3,10 @@ Copyright (c) 2021 Andrew Yang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
-import category_theory.sites.sheaf
+import category_theory.sites.limits
+import category_theory.flat_functors
+import category_theory.limits.preserves.filtered
+import category_theory.sites.left_exact
 
 /-!
 # Cover-preserving functors between sites.
@@ -18,9 +21,13 @@ sheaves on `D` back to sheaves on `C` via `G.op ⋙ -`.
 pushes covering sieves to covering sieves
 * `category_theory.compatible_preserving`: a functor between sites is compatible-preserving
 if it pushes compatible families of elements to compatible families.
-* `category_theory.pullback_sheaf` : the pullback of a sheaf along a cover-preserving and
+* `category_theory.pullback_sheaf`: the pullback of a sheaf along a cover-preserving and
 compatible-preserving functor.
-* `category_theory.sites.pullback` : the induced functor `Sheaf K A ⥤ Sheaf J A` for a
+* `category_theory.sites.pullback`: the induced functor `Sheaf K A ⥤ Sheaf J A` for a
+cover-preserving and compatible-preserving functor `G : (C, J) ⥤ (D, K)`.
+* `category_theory.sites.pushforward`: the induced functor `Sheaf J A ⥤ Sheaf K A` for a
+cover-preserving and compatible-preserving functor `G : (C, J) ⥤ (D, K)`.
+* `category_theory.sites.pushforward`: the induced functor `Sheaf J A ⥤ Sheaf K A` for a
 cover-preserving and compatible-preserving functor `G : (C, J) ⥤ (D, K)`.
 
 ## Main results
@@ -118,6 +125,43 @@ end
 
 omit h hG
 
+open limits.walking_cospan
+
+lemma compatible_preserving_of_flat {C : Type u₁} [category.{v₁} C] {D : Type u₁} [category.{v₁} D]
+  (K : grothendieck_topology D) (G : C ⥤ D) [representably_flat G] : compatible_preserving K G :=
+begin
+  constructor,
+  intros ℱ Z T x hx Y₁ Y₂ X f₁ f₂ g₁ g₂ hg₁ hg₂ e,
+
+  /- First, `f₁` and `f₂` form a cone over `cospan g₁ g₂ ⋙ u`. -/
+  let c : cone (cospan g₁ g₂ ⋙ G) :=
+    (cones.postcompose (diagram_iso_cospan (cospan g₁ g₂ ⋙ G)).inv).obj
+      (pullback_cone.mk f₁ f₂ e),
+
+  /-
+  This can then be viewed as a cospan of structured arrows, and we may obtain an arbitrary cone
+  over it since `structured_arrow W u` is cofiltered.
+  Then, it suffices to prove that it is compatible when restricted onto `u(c'.X.right)`.
+  -/
+  let c' := is_cofiltered.cone (structured_arrow_cone.to_diagram c ⋙ structured_arrow.pre _ _ _),
+  have eq₁ : f₁ = (c'.X.hom ≫ G.map (c'.π.app left).right) ≫ eq_to_hom (by simp),
+  { erw ← (c'.π.app left).w, dsimp, simp },
+  have eq₂ : f₂ = (c'.X.hom ≫ G.map (c'.π.app right).right) ≫ eq_to_hom (by simp),
+  { erw ← (c'.π.app right).w, dsimp, simp },
+  conv_lhs { rw eq₁ },
+  conv_rhs { rw eq₂ },
+  simp only [op_comp, functor.map_comp, types_comp_apply, eq_to_hom_op, eq_to_hom_map],
+  congr' 1,
+
+  /-
+  Since everything now falls in the image of `u`,
+  the result follows from the compatibility of `x` in the image of `u`.
+  -/
+  injection c'.π.naturality walking_cospan.hom.inl with _ e₁,
+  injection c'.π.naturality walking_cospan.hom.inr with _ e₂,
+  exact hx (c'.π.app left).right (c'.π.app right).right hg₁ hg₂ (e₁.symm.trans e₂)
+end
+
 /--
 If `G` is cover-preserving and compatible-preserving,
 then `G.op ⋙ _` pulls sheaves back to sheaves.
@@ -168,3 +212,48 @@ if `G` is cover-preserving and compatible-preserving.
   map_comp' := λ _ _ _ f g, by { ext1, apply (((whiskering_left _ _ _).obj G.op)).map_comp } }
 
 end category_theory
+
+namespace category_theory
+
+variables {C : Type v₁} [small_category C] {D : Type v₁} [small_category D]
+variables (A : Type u₂) [category.{v₁} A]
+variables (J : grothendieck_topology C) (K : grothendieck_topology D)
+
+instance [has_limits A] : creates_limits (Sheaf_to_presheaf J A) :=
+category_theory.Sheaf.category_theory.Sheaf_to_presheaf.category_theory.creates_limits.{u₂ v₁ v₁}
+
+-- The assumptions so that we have sheafification
+variables [concrete_category.{v₁} A] [preserves_limits (forget A)] [has_colimits A] [has_limits A]
+variables [preserves_filtered_colimits (forget A)] [reflects_isomorphisms (forget A)]
+
+local attribute [instance] reflects_limits_of_reflects_isomorphisms
+
+instance {X : C} : is_cofiltered (J.cover X) := infer_instance
+
+/-- The pushforward functor `Sheaf J A ⥤ Sheaf K A` associated to a functor `G : C ⥤ D` in the
+same direction as `G`. -/
+@[simps] def sites.pushforward (G : C ⥤ D) : Sheaf J A ⥤ Sheaf K A :=
+Sheaf_to_presheaf J A ⋙ Lan G.op ⋙ presheaf_to_Sheaf K A
+
+instance (G : C ⥤ D) [representably_flat G] :
+  preserves_finite_limits (sites.pushforward A J K G) :=
+begin
+  apply_with comp_preserves_finite_limits { instances := ff },
+  { apply_instance },
+  apply_with comp_preserves_finite_limits { instances := ff },
+  { apply category_theory.Lan_preserves_finite_limits_of_flat },
+  { apply category_theory.presheaf_to_Sheaf.limits.preserves_finite_limits.{u₂ v₁ v₁},
+    apply_instance }
+end
+
+/-- The pushforward functor is left adjoint to the pullback functor. -/
+def sites.pullback_pushforward_adjunction {G : C ⥤ D} (hG₁ : compatible_preserving K G)
+  (hG₂ : cover_preserving J K G) : sites.pushforward A J K G ⊣ sites.pullback A hG₁ hG₂ :=
+((Lan.adjunction A G.op).comp _ _ (sheafification_adjunction K A)).restrict_fully_faithful
+  (Sheaf_to_presheaf J A) (𝟭 _)
+  (nat_iso.of_components (λ _, iso.refl _)
+    (λ _ _ _,(category.comp_id _).trans (category.id_comp _).symm))
+  (nat_iso.of_components (λ _, iso.refl _)
+    (λ _ _ _,(category.comp_id _).trans (category.id_comp _).symm))
+
+end category_theory