chore(CategoryTheory/Sites): rename Presieve.isSeparated_of_isSheaf -> Presieve.IsSheaf.isSeparated (#29088)

Rename `Presieve.isSeparated_of_isSheaf` to `Presieve.IsSheaf.isSeparated` to enable dot notation. I've also made the arguments `J` and `P` implicit, since they can be inferred from `h : IsSheaf J P`.

Co-authored-by: Ben Eltschig <b.eltschig@protonmail.com>

Author: peabrainiac

Mathlib/CategoryTheory/Sites/CoverPreserving.lean

@@ -165,8 +165,7 @@ lemma Functor.isContinuous_of_coverPreserving (hF₁ : CompatiblePreserving.{w}
         fun V f hf => (H.isAmalgamation (hx.functorPushforward hF₁) (F.map f) _).trans
           (hF₁.apply_map _ hx hf)⟩
     · intro y₁ y₂ hy₁ hy₂
-      apply (Presieve.isSeparated_of_isSheaf _ _ ((isSheaf_iff_isSheaf_of_type _ _).1 G.2) _
-        (hF₂.cover_preserve hS)).ext
+      apply (((isSheaf_iff_isSheaf_of_type _ _).1 G.2).isSeparated _ (hF₂.cover_preserve hS)).ext
       rintro Y _ ⟨Z, g, h, hg, rfl⟩
       dsimp
       simp only [Functor.map_comp, types_comp_apply]

Mathlib/CategoryTheory/Sites/CoversTop.lean

@@ -69,8 +69,7 @@ lemma sections_ext (F : Sheaf J (Type _)) {x y : F.1.sections}
     (h : ∀ (i : I), x.1 (Opposite.op (Y i)) = y.1 (Opposite.op (Y i))) :
     x = y := by
   ext W
-  apply (Presieve.isSeparated_of_isSheaf J F.1
-    ((isSheaf_iff_isSheaf_of_type _ _).1 F.2) _ (hY W.unop)).ext
+  apply (((isSheaf_iff_isSheaf_of_type _ _).1 F.2).isSeparated _ (hY W.unop)).ext
   rintro T a ⟨i, ⟨b⟩⟩
   simpa using congr_arg (F.1.map b.op) (h i)
 
@@ -140,7 +139,7 @@ lemma existsUnique_section (hx : x.IsCompatible) (hY : J.CoversTop Y) (hF : IsSh
     refine ⟨⟨fun X => s X.unop, ?_⟩, fun i => (hs i (𝟙 (Y i))).trans (by simp)⟩
     rintro ⟨Y₁⟩ ⟨Y₂⟩ ⟨f : Y₂ ⟶ Y₁⟩
     change F.map f.op (s Y₁) = s Y₂
-    apply (Presieve.isSeparated_of_isSheaf J F H _ (hY Y₂)).ext
+    apply (H.isSeparated _ (hY Y₂)).ext
     rintro Z φ ⟨i, ⟨g⟩⟩
     rw [hs' φ i g, ← hs' (φ ≫ f) i g, op_comp, F.map_comp]
     rfl

Mathlib/CategoryTheory/Sites/LocallyBijective.lean

@@ -62,8 +62,7 @@ private lemma isLocallyBijective_iff_isIso' :
       erw [← FunctorToTypes.map_comp_apply, ← FunctorToTypes.map_comp_apply]
       simp only [← op_comp, w]
     refine ⟨H.amalgamate t ht, ?_⟩
-    · apply (Presieve.isSeparated_of_isSheaf _ _
-        ((isSheaf_iff_isSheaf_of_type J G.val).1 G.cond) _
+    · apply (((isSheaf_iff_isSheaf_of_type J G.val).1 G.cond).isSeparated _
         (Presheaf.imageSieve_mem J f.val s)).ext
       intro Y g hg
       rw [← FunctorToTypes.naturality, H.valid_glue ht]

Mathlib/CategoryTheory/Sites/LocallyInjective.lean

@@ -239,7 +239,7 @@ instance isLocallyInjective_forget [IsLocallyInjective φ] :
 lemma isLocallyInjective_iff_injective :
     IsLocallyInjective φ ↔ ∀ (X : Cᵒᵖ), Function.Injective (φ.val.app X) :=
   Presheaf.isLocallyInjective_iff_injective_of_separated _ _ (by
-    apply Presieve.isSeparated_of_isSheaf
+    apply Presieve.IsSheaf.isSeparated
     rw [← isSheaf_iff_isSheaf_of_type]
     exact ((sheafCompose J (forget D)).obj F₁).2)
 

Mathlib/CategoryTheory/Sites/LocallySurjective.lean

@@ -361,7 +361,7 @@ instance epi_of_isLocallySurjective' {F₁ F₂ : Sheaf J (Type w)} (φ : F₁ 
     [IsLocallySurjective φ] : Epi φ where
   left_cancellation {Z} f₁ f₂ h := by
     ext X x
-    apply (Presieve.isSeparated_of_isSheaf J Z.1 ((isSheaf_iff_isSheaf_of_type _ _).1 Z.2) _
+    apply (((isSheaf_iff_isSheaf_of_type _ _).1 Z.2).isSeparated _
       (Presheaf.imageSieve_mem J φ.val x)).ext
     rintro Y f ⟨s : F₁.val.obj (op Y), hs : φ.val.app _ s = F₂.val.map f.op x⟩
     dsimp

Mathlib/CategoryTheory/Sites/SheafOfTypes.lean

@@ -79,9 +79,12 @@ theorem IsSheaf.isSheafFor {P : Cᵒᵖ ⥤ Type w} (hp : IsSheaf J P) (R : Pres
 theorem isSheaf_of_le (P : Cᵒᵖ ⥤ Type w) {J₁ J₂ : GrothendieckTopology C} :
     J₁ ≤ J₂ → IsSheaf J₂ P → IsSheaf J₁ P := fun h t _ S hS => t S (h _ hS)
 
-theorem isSeparated_of_isSheaf (P : Cᵒᵖ ⥤ Type w) (h : IsSheaf J P) : IsSeparated J P :=
+variable {J} in
+theorem IsSheaf.isSeparated {P : Cᵒᵖ ⥤ Type w} (h : IsSheaf J P) : IsSeparated J P :=
   fun S hS => (h S hS).isSeparatedFor
 
+@[deprecated (since := "28-08-2025")] alias isSeparated_of_isSheaf := IsSheaf.isSeparated
+
 section
 
 variable {J} {P₁ : Cᵒᵖ ⥤ Type w} {P₂ : Cᵒᵖ ⥤ Type w'}

Mathlib/CategoryTheory/Sites/Whiskering.lean

@@ -145,8 +145,8 @@ lemma Sheaf.isSeparated {FA : A → A → Type*} {CA : A → Type*}
     [∀ X Y, FunLike (FA X Y) (CA X) (CA Y)] [ConcreteCategory A FA] [J.HasSheafCompose (forget A)]
     (F : Sheaf J A) : Presheaf.IsSeparated J F.val := by
   rintro X S hS x y h
-  exact (Presieve.isSeparated_of_isSheaf _ _ ((isSheaf_iff_isSheaf_of_type _ _).1
-    ((sheafCompose J (forget A)).obj F).2) S hS).ext (fun _ _ hf => h _ _ hf)
+  exact (((isSheaf_iff_isSheaf_of_type _ _).1
+    ((sheafCompose J (forget A)).obj F).2).isSeparated S hS).ext (fun _ _ hf => h _ _ hf)
 
 lemma Presheaf.IsSheaf.isSeparated {F : Cᵒᵖ ⥤ A} {FA : A → A → Type*} {CA : A → Type*}
     [∀ X Y, FunLike (FA X Y) (CA X) (CA Y)] [ConcreteCategory A FA]