feat(category_theory/sites/sheafification): The sheafification of a p…

…resheaf. (#10303)

We construct the sheafification of a presheaf `P` taking values in a concrete category `D` with enough (co)limits, where the forgetful functor preserves the appropriate (co)limits and reflects isomorphisms.

We follow the construction on the stacks project https://stacks.math.columbia.edu/tag/00W1

**Note:** There are two very long proofs here, so I added several comments explaining what's going on.

src/category_theory/limits/concrete_category.lean

@@ -95,6 +95,54 @@ begin
       comp_apply, comp_apply, h] }
 end
 
+/-- An auxiliary equivalence to be used in `multiequalizer_equiv` below.-/
+def concrete.multiequalizer_equiv_aux (I : multicospan_index C) :
+  (I.multicospan ⋙ (forget C)).sections ≃
+  { x : Π (i : I.L), I.left i // ∀ (i : I.R), I.fst i (x _) = I.snd i (x _) } :=
+{ to_fun := λ x, ⟨λ i, x.1 (walking_multicospan.left _), λ i, begin
+    have a := x.2 (walking_multicospan.hom.fst i),
+    have b := x.2 (walking_multicospan.hom.snd i),
+    rw ← b at a,
+    exact a,
+  end⟩,
+  inv_fun := λ x,
+  { val := λ j,
+    match j with
+    | walking_multicospan.left a := x.1 _
+    | walking_multicospan.right b := I.fst b (x.1 _)
+    end,
+    property := begin
+      rintros (a|b) (a'|b') (f|f|f),
+      { change (I.multicospan.map (𝟙 _)) _ = _, simp },
+      { refl },
+      { dsimp, erw ← x.2 b', refl },
+      { change (I.multicospan.map (𝟙 _)) _ = _, simp },
+    end },
+  left_inv := begin
+    intros x, ext (a|b),
+    { refl },
+    { change _ = x.val _,
+      rw ← x.2 (walking_multicospan.hom.fst b),
+      refl }
+  end,
+  right_inv := by { intros x, ext i, refl } }
+
+/-- The equivalence between the noncomputable multiequalizer and
+and the concrete multiequalizer. -/
+noncomputable
+def concrete.multiequalizer_equiv (I : multicospan_index C) [has_multiequalizer I]
+  [preserves_limit I.multicospan (forget C)] : (multiequalizer I : C) ≃
+    { x : Π (i : I.L), I.left i // ∀ (i : I.R), I.fst i (x _) = I.snd i (x _) } :=
+let h1 := (limit.is_limit I.multicospan),
+    h2 := (is_limit_of_preserves (forget C) h1),
+    E := h2.cone_point_unique_up_to_iso (types.limit_cone_is_limit _) in
+equiv.trans E.to_equiv (concrete.multiequalizer_equiv_aux I)
+
+@[simp]
+lemma concrete.multiequalizer_equiv_apply (I : multicospan_index C) [has_multiequalizer I]
+  [preserves_limit I.multicospan (forget C)] (x : multiequalizer I) (i : I.L) :
+  ((concrete.multiequalizer_equiv I) x : Π (i : I.L), I.left i) i = multiequalizer.ι I i x := rfl
+
 end multiequalizer
 
 -- TODO: Add analogous lemmas about products and equalizers.

src/category_theory/sites/grothendieck.lean

@@ -479,6 +479,56 @@ def pullback_comp {X Y Z : C} (S : J.cover X) (f : Z ⟶ Y) (g : Y ⟶ X) :
   S.pullback (f ≫ g) ≅ (S.pullback g).pullback f :=
 eq_to_iso $ cover.ext _ _ $ λ Y f, by simp
 
+/-- Combine a family of covers over a cover. -/
+def bind {X : C} (S : J.cover X) (T : Π (I : S.arrow), J.cover I.Y) : J.cover X :=
+⟨sieve.bind S (λ Y f hf, T ⟨Y, f, hf⟩), J.bind_covering S.condition (λ _ _ _, (T _).condition)⟩
+
+/-- The canonical moprhism from `S.bind T` to `T`. -/
+def bind_to_base {X : C} (S : J.cover X) (T : Π (I : S.arrow), J.cover I.Y) : S.bind T ⟶ S :=
+hom_of_le $ by { rintro Y f ⟨Z,e1,e2,h1,h2,h3⟩, rw ← h3, apply sieve.downward_closed, exact h1 }
+
+/-- An arrow in bind has the form `A ⟶ B ⟶ X` where `A ⟶ B` is an arrow in `T I` for some `I`.
+ and `B ⟶ X` is an arrow of `S`. This is the object `B`. -/
+noncomputable def arrow.middle {X : C} {S : J.cover X} {T : Π (I : S.arrow), J.cover I.Y}
+  (I : (S.bind T).arrow) : C :=
+I.hf.some
+
+/-- An arrow in bind has the form `A ⟶ B ⟶ X` where `A ⟶ B` is an arrow in `T I` for some `I`.
+ and `B ⟶ X` is an arrow of `S`. This is the hom `A ⟶ B`. -/
+noncomputable def arrow.to_middle_hom {X : C} {S : J.cover X} {T : Π (I : S.arrow), J.cover I.Y}
+  (I : (S.bind T).arrow) : I.Y ⟶ I.middle :=
+I.hf.some_spec.some
+
+/-- An arrow in bind has the form `A ⟶ B ⟶ X` where `A ⟶ B` is an arrow in `T I` for some `I`.
+ and `B ⟶ X` is an arrow of `S`. This is the hom `B ⟶ X`. -/
+noncomputable def arrow.from_middle_hom {X : C} {S : J.cover X} {T : Π (I : S.arrow), J.cover I.Y}
+  (I : (S.bind T).arrow) : I.middle ⟶ X :=
+I.hf.some_spec.some_spec.some
+
+lemma arrow.from_middle_condition {X : C} {S : J.cover X} {T : Π (I : S.arrow), J.cover I.Y}
+  (I : (S.bind T).arrow) : S I.from_middle_hom :=
+I.hf.some_spec.some_spec.some_spec.some
+
+/-- An arrow in bind has the form `A ⟶ B ⟶ X` where `A ⟶ B` is an arrow in `T I` for some `I`.
+ and `B ⟶ X` is an arrow of `S`. This is the hom `B ⟶ X`, as an arrow. -/
+noncomputable
+def arrow.from_middle {X : C} {S : J.cover X} {T : Π (I : S.arrow), J.cover I.Y}
+  (I : (S.bind T).arrow) : S.arrow := ⟨_, I.from_middle_hom, I.from_middle_condition⟩
+
+lemma arrow.to_middle_condition {X : C} {S : J.cover X} {T : Π (I : S.arrow), J.cover I.Y}
+  (I : (S.bind T).arrow) : (T I.from_middle) I.to_middle_hom :=
+I.hf.some_spec.some_spec.some_spec.some_spec.1
+
+/-- An arrow in bind has the form `A ⟶ B ⟶ X` where `A ⟶ B` is an arrow in `T I` for some `I`.
+ and `B ⟶ X` is an arrow of `S`. This is the hom `A ⟶ B`, as an arrow. -/
+noncomputable
+def arrow.to_middle {X : C} {S : J.cover X} {T : Π (I : S.arrow), J.cover I.Y}
+  (I : (S.bind T).arrow) : (T I.from_middle).arrow := ⟨_, I.to_middle_hom, I.to_middle_condition⟩
+
+lemma arrow.middle_spec {X : C} {S : J.cover X} {T : Π (I : S.arrow), J.cover I.Y}
+  (I : (S.bind T).arrow) : I.to_middle_hom ≫ I.from_middle_hom = I.f :=
+I.hf.some_spec.some_spec.some_spec.some_spec.2
+
 -- This is used extensively in `plus.lean`, etc.
 -- We place this definition here as it will be used in `sheaf.lean` as well.
 /-- To every `S : J.cover X` and presheaf `P`, associate a `multicospan_index`. -/

src/category_theory/sites/plus.lean

@@ -245,4 +245,49 @@ begin
   rw this, apply_instance,
 end
 
+/-- The natural isomorphism between `P` and `P⁺` when `P` is a sheaf. -/
+def iso_to_plus (hP : presheaf.is_sheaf J P) : P ≅ J.plus_obj P :=
+by letI := is_iso_to_plus_of_is_sheaf J P hP; exact as_iso (J.to_plus P)
+
+/-- Lift a morphism `P ⟶ Q` to `P⁺ ⟶ Q` when `Q` is a sheaf. -/
+def plus_lift {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (hQ : presheaf.is_sheaf J Q) :
+  J.plus_obj P ⟶ Q :=
+J.plus_map η ≫ (J.iso_to_plus Q hQ).inv
+
+lemma to_plus_plus_lift {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (hQ : presheaf.is_sheaf J Q) :
+  J.to_plus P ≫ J.plus_lift η hQ = η :=
+begin
+  dsimp [plus_lift],
+  rw ← category.assoc,
+  rw iso.comp_inv_eq,
+  dsimp only [iso_to_plus, as_iso],
+  change (J.to_plus_nat_trans D).app _ ≫ _ = _,
+  erw (J.to_plus_nat_trans D).naturality,
+  refl,
+end
+
+lemma plus_lift_unique {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (hQ : presheaf.is_sheaf J Q)
+  (γ : J.plus_obj P ⟶ Q) (hγ : J.to_plus P ≫ γ = η) : γ = J.plus_lift η hQ :=
+begin
+  dsimp only [plus_lift],
+  symmetry,
+  change (J.plus_functor D).map η ≫ _ = _,
+  rw [iso.comp_inv_eq, ← hγ, (J.plus_functor D).map_comp],
+  dsimp only [iso_to_plus, as_iso],
+  change _ = (𝟭 _).map γ ≫ (J.to_plus_nat_trans D).app _,
+  erw (J.to_plus_nat_trans D).naturality,
+  congr' 1,
+  dsimp only [plus_functor, to_plus_nat_trans],
+  rw [J.plus_map_to_plus P],
+end
+
+lemma plus_hom_ext {P Q : Cᵒᵖ ⥤ D} (η γ : J.plus_obj P ⟶ Q) (hQ : presheaf.is_sheaf J Q)
+  (h : J.to_plus P ≫ η = J.to_plus P ≫ γ) : η = γ :=
+begin
+  have : γ = J.plus_lift (J.to_plus P ≫ γ) hQ,
+  { apply plus_lift_unique, refl },
+  rw this,
+  apply plus_lift_unique, exact h
+end
+
 end category_theory.grothendieck_topology