feat(CategoryTheory/Sites): the equalizer sheaf condition for a singleton (leanprover-community#25839)

Co-authored-by: Christian Merten <136261474+chrisflav@users.noreply.github.com>

Author: chrisflav

Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean

@@ -367,6 +367,32 @@ theorem sheaf_condition : (Presieve.ofArrows X π).IsSheafFor P ↔
 
 end Arrows
 
+/-- The sheaf condition for a single morphism is the same as the canonical fork diagram being
+limiting. -/
+lemma isSheafFor_singleton_iff {F : Cᵒᵖ ⥤ Type*} {X Y : C} {f : X ⟶ Y}
+    (c : PullbackCone f f) (hc : IsLimit c) :
+    Presieve.IsSheafFor F (.singleton f) ↔
+      Nonempty
+        (IsLimit (Fork.ofι (F.map f.op) (f := F.map c.fst.op) (g := F.map c.snd.op)
+          (by simp [← Functor.map_comp, ← op_comp, c.condition]))) := by
+  have h (x : F.obj (op X)) : (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
+      p₁ ≫ f = p₂ ≫ f → F.map p₁.op x = F.map p₂.op x) ↔ F.map c.fst.op x = F.map c.snd.op x := by
+    refine ⟨fun H ↦ H _ _ c.condition, fun H Z p₁ p₂ h ↦ ?_⟩
+    rw [← PullbackCone.IsLimit.lift_fst hc _ _ h, op_comp, FunctorToTypes.map_comp_apply, H]
+    simp [← FunctorToTypes.map_comp_apply, ← op_comp]
+  rw [Types.type_equalizer_iff_unique, Presieve.isSheafFor_singleton]
+  simp_rw [h]
+
+/-- Special case of `isSheafFor_singleton_iff` with `c = pullback.cone f f`. -/
+lemma isSheafFor_singleton_iff_of_hasPullback {F : Cᵒᵖ ⥤ Type*} {X Y : C} {f : X ⟶ Y}
+    [HasPullback f f] :
+    Presieve.IsSheafFor F (.singleton f) ↔
+      Nonempty
+        (IsLimit (Fork.ofι (F.map f.op) (f := F.map (pullback.fst f f).op)
+          (g := F.map (pullback.snd f f).op)
+          (by simp [← Functor.map_comp, ← op_comp, pullback.condition]))) :=
+  isSheafFor_singleton_iff (pullback.cone f f) (pullback.isLimit f f)
+
 end Presieve
 
 end

Mathlib/CategoryTheory/Sites/IsSheafFor.lean

@@ -93,6 +93,13 @@ def FamilyOfElements (P : Cᵒᵖ ⥤ Type w) (R : Presieve X) :=
 instance : Inhabited (FamilyOfElements P (⊥ : Presieve X)) :=
   ⟨fun _ _ => False.elim⟩
 
+@[ext]
+lemma FamilyOfElements.ext {R : Presieve X} {x y : R.FamilyOfElements P}
+    (H : ∀ {Y : C} (f : Y ⟶ X) (hf : R f), x f hf = y f hf) :
+    x = y := by
+  funext Z f hf
+  exact H f hf
+
 /-- A family of elements for a presheaf on the presieve `R₂` can be restricted to a smaller presieve
 `R₁`.
 -/
@@ -113,6 +120,21 @@ lemma FamilyOfElements.restrict_map
     (p : FamilyOfElements P R) (φ : P ⟶ Q) {R' : Presieve X} (h : R' ≤ R) :
     (p.restrict h).map φ = (p.map φ).restrict h := rfl
 
+variable (P) in
+/-- A family of elements on `{ f : X ⟶ Y }` is an element of `F(X)`. -/
+@[simps apply, simps -isSimp symm_apply]
+def FamilyOfElements.singletonEquiv {X Y : C} (f : X ⟶ Y) :
+    (singleton f).FamilyOfElements P ≃ P.obj (op X) where
+  toFun x := x f (by simp)
+  invFun x Z g hg := P.map (eqToHom <| by cases hg; rfl).op x
+  left_inv x := by ext _ _ ⟨rfl⟩; simp
+  right_inv x := by simp
+
+@[simp]
+lemma FamilyOfElements.singletonEquiv_symm_apply_self {X Y : C} (f : X ⟶ Y) (x : P.obj (op X)) :
+    (singletonEquiv P f).symm x f ⟨⟩ = x := by
+  simp [singletonEquiv_symm_apply]
+
 /-- A family of elements for the arrow set `R` is *compatible* if for any `f₁ : Y₁ ⟶ X` and
 `f₂ : Y₂ ⟶ X` in `R`, and any `g₁ : Z ⟶ Y₁` and `g₂ : Z ⟶ Y₂`, if the square `g₁ ≫ f₁ = g₂ ≫ f₂`
 commutes then the elements of `P Z` obtained by restricting the element of `P Y₁` along `g₁` and
@@ -267,6 +289,14 @@ theorem FamilyOfElements.comp_of_compatible (S : Sieve X) {x : FamilyOfElements
     x (g ≫ f) (S.downward_closed hf g) = P.map g.op (x f hf) := by
   simpa using t (𝟙 _) g (S.downward_closed hf g) hf (id_comp _)
 
+lemma FamilyOfElements.compatible_singleton_iff
+    {X Y : C} (f : X ⟶ Y) (x : (singleton f).FamilyOfElements P) :
+    x.Compatible ↔ ∀ {Z : C} (p₁ p₂ : Z ⟶ X), p₁ ≫ f = p₂ ≫ f →
+      P.map p₁.op (x f ⟨⟩) = P.map p₂.op (x f ⟨⟩) := by
+  refine ⟨fun H Z p₁ p₂ h ↦ H _ _ _ _ h, fun H Y₁ Y₂ Z g₁ g₂ f₁ f₂ ↦ ?_⟩
+  rintro ⟨rfl⟩ ⟨rfl⟩ h
+  exact H _ _ h
+
 section FunctorPullback
 
 variable {D : Type u₂} [Category.{v₂} D] (F : D ⥤ C) {Z : D}
@@ -372,6 +402,14 @@ theorem isAmalgamation_sieveExtend {R : Presieve X} (x : FamilyOfElements P R) (
   dsimp [FamilyOfElements.sieveExtend]
   rw [← ht _, ← FunctorToTypes.map_comp_apply, ← op_comp, hf.choose_spec.choose_spec.choose_spec.2]
 
+@[simp]
+lemma FamilyOfElements.isAmalgamation_singleton_iff {X Y : C} (f : X ⟶ Y)
+    (x : (singleton f).FamilyOfElements P) (y : P.obj (op Y)) :
+    x.IsAmalgamation y ↔ P.map f.op y = x f ⟨⟩ := by
+  refine ⟨fun H ↦ H _ _, ?_⟩
+  rintro H Y g ⟨rfl⟩
+  exact H
+
 /-- A presheaf is separated for a presieve if there is at most one amalgamation. -/
 def IsSeparatedFor (P : Cᵒᵖ ⥤ Type w) (R : Presieve X) : Prop :=
   ∀ (x : FamilyOfElements P R) (t₁ t₂), x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂
@@ -757,6 +795,24 @@ theorem isSheafFor_arrows_iff_pullbacks : (ofArrows X π).IsSheafFor P ↔
 
 end Arrows
 
+@[simp]
+lemma isSeparatedFor_singleton {X Y : C} {f : X ⟶ Y} :
+    Presieve.IsSeparatedFor P (.singleton f) ↔
+      Function.Injective (P.map f.op) := by
+  rw [IsSeparatedFor, Equiv.forall_congr_left (Presieve.FamilyOfElements.singletonEquiv P f)]
+  simp_rw [FamilyOfElements.isAmalgamation_singleton_iff,
+    FamilyOfElements.singletonEquiv_symm_apply_self, Function.Injective]
+  aesop
+
+lemma isSheafFor_singleton {X Y : C} {f : X ⟶ Y} :
+    Presieve.IsSheafFor P (.singleton f) ↔
+      ∀ (x : P.obj (op X)),
+        (∀ {Z : C} (p₁ p₂ : Z ⟶ X), p₁ ≫ f = p₂ ≫ f → P.map p₁.op x = P.map p₂.op x) →
+        ∃! y, P.map f.op y = x := by
+  rw [IsSheafFor, Equiv.forall_congr_left (Presieve.FamilyOfElements.singletonEquiv P f)]
+  simp_rw [FamilyOfElements.compatible_singleton_iff,
+    FamilyOfElements.isAmalgamation_singleton_iff, FamilyOfElements.singletonEquiv_symm_apply_self]
+
 end Presieve
 
 end CategoryTheory