[Merged by Bors] - feat(CategoryTheory/Subpresheaf): preimage/image/range of subpresheaves

Mathlib/CategoryTheory/Sites/LocallyInjective.lean

@@ -243,8 +243,8 @@ lemma mono_of_isLocallyInjective [IsLocallyInjective φ] : Mono φ := by
   infer_instance
 
 instance {F G : Sheaf J (Type w)} (f : F ⟶ G) :
-    IsLocallyInjective (imageSheafι f) := by
-  dsimp [imageSheafι]
+    IsLocallyInjective (Sheaf.imageι f) := by
+  dsimp [Sheaf.imageι]
   infer_instance
 
 end Sheaf

Mathlib/CategoryTheory/Sites/LocallySurjective.lean

@@ -50,7 +50,7 @@ def imageSieve {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) {U : C} (s : G.obj (op U)) :
     rw [op_comp, G.map_comp, comp_apply, ← ht, elementwise_of% f.naturality]
 
 theorem imageSieve_eq_sieveOfSection {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) {U : C} (s : G.obj (op U)) :
-    imageSieve f s = (imagePresheaf (whiskerRight f (forget A))).sieveOfSection s :=
+    imageSieve f s = (Subpresheaf.range (whiskerRight f (forget A))).sieveOfSection s :=
   rfl
 
 theorem imageSieve_whisker_forget {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) {U : C} (s : G.obj (op U)) :
@@ -92,13 +92,13 @@ instance {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) [IsLocallySurjective J f] :
   imageSieve_mem s := imageSieve_mem J f s
 
 theorem isLocallySurjective_iff_imagePresheaf_sheafify_eq_top {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) :
-    IsLocallySurjective J f ↔ (imagePresheaf (whiskerRight f (forget A))).sheafify J = ⊤ := by
+    IsLocallySurjective J f ↔ (Subpresheaf.range (whiskerRight f (forget A))).sheafify J = ⊤ := by
   simp only [Subpresheaf.ext_iff, funext_iff, Set.ext_iff, top_subpresheaf_obj,
     Set.top_eq_univ, Set.mem_univ, iff_true]
   exact ⟨fun H _ => H.imageSieve_mem, fun H => ⟨H _⟩⟩
 
 theorem isLocallySurjective_iff_imagePresheaf_sheafify_eq_top' {F G : Cᵒᵖ ⥤ Type w} (f : F ⟶ G) :
-    IsLocallySurjective J f ↔ (imagePresheaf f).sheafify J = ⊤ := by
+    IsLocallySurjective J f ↔ (Subpresheaf.range f).sheafify J = ⊤ := by
   apply isLocallySurjective_iff_imagePresheaf_sheafify_eq_top
 
 theorem isLocallySurjective_iff_whisker_forget {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) :
@@ -248,7 +248,7 @@ lemma isLocallySurjective_comp_iff
     infer_instance
 
 instance {F₁ F₂ : Cᵒᵖ ⥤ Type w} (f : F₁ ⟶ F₂) :
-    IsLocallySurjective J (toImagePresheafSheafify J f) where
+    IsLocallySurjective J (Subpresheaf.toRangeSheafify J f) where
   imageSieve_mem {X} := by
     rintro ⟨s, hs⟩
     refine J.superset_covering ?_ hs
@@ -257,20 +257,20 @@ instance {F₁ F₂ : Cᵒᵖ ⥤ Type w} (f : F₁ ⟶ F₂) :
 
 /-- The image of `F` in `J.sheafify F` is isomorphic to the sheafification. -/
 noncomputable def sheafificationIsoImagePresheaf (F : Cᵒᵖ ⥤ Type max u v) :
-    J.sheafify F ≅ ((imagePresheaf (J.toSheafify F)).sheafify J).toPresheaf where
+    J.sheafify F ≅ ((Subpresheaf.range (J.toSheafify F)).sheafify J).toPresheaf where
   hom :=
-    J.sheafifyLift (toImagePresheafSheafify J _)
+    J.sheafifyLift (Subpresheaf.toRangeSheafify J _)
       ((isSheaf_iff_isSheaf_of_type J _).mpr <|
         Subpresheaf.sheafify_isSheaf _ <|
           (isSheaf_iff_isSheaf_of_type J _).mp <| GrothendieckTopology.sheafify_isSheaf J _)
   inv := Subpresheaf.ι _
   hom_inv_id :=
-    J.sheafify_hom_ext _ _ (J.sheafify_isSheaf _) (by simp [toImagePresheafSheafify])
+    J.sheafify_hom_ext _ _ (J.sheafify_isSheaf _) (by simp [Subpresheaf.toRangeSheafify])
   inv_hom_id := by
     rw [← cancel_mono (Subpresheaf.ι _), Category.id_comp, Category.assoc]
     refine Eq.trans ?_ (Category.comp_id _)
     congr 1
-    exact J.sheafify_hom_ext _ _ (J.sheafify_isSheaf _) (by simp [toImagePresheafSheafify])
+    exact J.sheafify_hom_ext _ _ (J.sheafify_isSheaf _) (by simp [Subpresheaf.toRangeSheafify])
 
 section
 
@@ -328,8 +328,8 @@ instance isLocallySurjective_of_iso [IsIso φ] : IsLocallySurjective φ := by
   infer_instance
 
 instance {F G : Sheaf J (Type w)} (f : F ⟶ G) :
-    IsLocallySurjective (toImageSheaf f) := by
-  dsimp [toImageSheaf]
+    IsLocallySurjective (Sheaf.toImage f) := by
+  dsimp [Sheaf.toImage]
   infer_instance
 
 variable [J.HasSheafCompose (forget A)]
@@ -339,11 +339,11 @@ instance [IsLocallySurjective φ] :
   (Presheaf.isLocallySurjective_iff_whisker_forget J φ.val).1 inferInstance
 
 theorem isLocallySurjective_iff_isIso {F G : Sheaf J (Type w)} (f : F ⟶ G) :
-    IsLocallySurjective f ↔ IsIso (imageSheafι f) := by
+    IsLocallySurjective f ↔ IsIso (Sheaf.imageι f) := by
   dsimp only [IsLocallySurjective]
-  rw [imageSheafι, Presheaf.isLocallySurjective_iff_imagePresheaf_sheafify_eq_top',
+  rw [Sheaf.imageι, Presheaf.isLocallySurjective_iff_imagePresheaf_sheafify_eq_top',
     Subpresheaf.eq_top_iff_isIso]
-  exact isIso_iff_of_reflects_iso (f := imageSheafι f) (F := sheafToPresheaf J (Type w))
+  exact isIso_iff_of_reflects_iso (f := Sheaf.imageι f) (F := sheafToPresheaf J (Type w))
 
 instance epi_of_isLocallySurjective' {F₁ F₂ : Sheaf J (Type w)} (φ : F₁ ⟶ F₂)
     [IsLocallySurjective φ] : Epi φ where
@@ -369,7 +369,7 @@ lemma isLocallySurjective_iff_epi {F G : Sheaf J (Type w)} (φ : F ⟶ G)
   · intro
     infer_instance
   · intro
-    have := epi_of_epi_fac (toImageSheaf_ι φ)
+    have := epi_of_epi_fac (Sheaf.toImage_ι φ)
     rw [isLocallySurjective_iff_isIso φ]
     apply isIso_of_mono_of_epi
 

Mathlib/CategoryTheory/Sites/Subsheaf.lean

@@ -194,61 +194,63 @@ variable (J)
 
 /-- A morphism factors through the sheafification of the image presheaf. -/
 @[simps!]
-def toImagePresheafSheafify (f : F' ⟶ F) : F' ⟶ ((imagePresheaf f).sheafify J).toPresheaf :=
-  toImagePresheaf f ≫ Subpresheaf.homOfLe ((imagePresheaf f).le_sheafify J)
+def Subpresheaf.toRangeSheafify (f : F' ⟶ F) : F' ⟶ ((Subpresheaf.range f).sheafify J).toPresheaf :=
+  toRange f ≫ Subpresheaf.homOfLe ((range f).le_sheafify J)
+
 
 variable {J}
 
 /-- The image sheaf of a morphism between sheaves, defined to be the sheafification of
 `image_presheaf`. -/
 @[simps]
-def imageSheaf {F F' : Sheaf J (Type w)} (f : F ⟶ F') : Sheaf J (Type w) :=
-  ⟨((imagePresheaf f.1).sheafify J).toPresheaf, by
+def Sheaf.image {F F' : Sheaf J (Type w)} (f : F ⟶ F') : Sheaf J (Type w) :=
+  ⟨((Subpresheaf.range f.1).sheafify J).toPresheaf, by
     rw [isSheaf_iff_isSheaf_of_type]
     apply Subpresheaf.sheafify_isSheaf
     rw [← isSheaf_iff_isSheaf_of_type]
     exact F'.2⟩
 
 /-- A morphism factors through the image sheaf. -/
 @[simps]
-def toImageSheaf {F F' : Sheaf J (Type w)} (f : F ⟶ F') : F ⟶ imageSheaf f :=
-  ⟨toImagePresheafSheafify J f.1⟩
+def Sheaf.toImage {F F' : Sheaf J (Type w)} (f : F ⟶ F') : F ⟶ Sheaf.image f :=
+  ⟨Subpresheaf.toRangeSheafify J f.1⟩
 
 /-- The inclusion of the image sheaf to the target. -/
 @[simps]
-def imageSheafι {F F' : Sheaf J (Type w)} (f : F ⟶ F') : imageSheaf f ⟶ F' :=
+def Sheaf.imageι {F F' : Sheaf J (Type w)} (f : F ⟶ F') : Sheaf.image f ⟶ F' :=
   ⟨Subpresheaf.ι _⟩
 
+
 @[reassoc (attr := simp)]
-theorem toImageSheaf_ι {F F' : Sheaf J (Type w)} (f : F ⟶ F') :
-    toImageSheaf f ≫ imageSheafι f = f := by
+theorem Sheaf.toImage_ι {F F' : Sheaf J (Type w)} (f : F ⟶ F') :
+    toImage f ≫ imageι f = f := by
   ext1
-  simp [toImagePresheafSheafify]
+  simp [Subpresheaf.toRangeSheafify]
 
-instance {F F' : Sheaf J (Type w)} (f : F ⟶ F') : Mono (imageSheafι f) :=
+instance {F F' : Sheaf J (Type w)} (f : F ⟶ F') : Mono (Sheaf.imageι f) :=
   (sheafToPresheaf J _).mono_of_mono_map
     (by
       dsimp
       infer_instance)
 
-instance {F F' : Sheaf J (Type w)} (f : F ⟶ F') : Epi (toImageSheaf f) := by
+instance {F F' : Sheaf J (Type w)} (f : F ⟶ F') : Epi (Sheaf.toImage f) := by
   refine ⟨@fun G' g₁ g₂ e => ?_⟩
   ext U ⟨s, hx⟩
   apply ((isSheaf_iff_isSheaf_of_type J _).mp G'.2 _ hx).isSeparatedFor.ext
   rintro V i ⟨y, e'⟩
   change (g₁.val.app _ ≫ G'.val.map _) _ = (g₂.val.app _ ≫ G'.val.map _) _
   rw [← NatTrans.naturality, ← NatTrans.naturality]
-  have E : (toImageSheaf f).val.app (op V) y = (imageSheaf f).val.map i.op ⟨s, hx⟩ :=
+  have E : (Sheaf.toImage f).val.app (op V) y = (Sheaf.image f).val.map i.op ⟨s, hx⟩ :=
     Subtype.ext e'
   have := congr_arg (fun f : F ⟶ G' => (Sheaf.Hom.val f).app _ y) e
   dsimp at this ⊢
   convert this <;> exact E.symm
 
 /-- The mono factorization given by `image_sheaf` for a morphism. -/
 def imageMonoFactorization {F F' : Sheaf J (Type w)} (f : F ⟶ F') : Limits.MonoFactorisation f where
-  I := imageSheaf f
-  m := imageSheafι f
-  e := toImageSheaf f
+  I := Sheaf.image f
+  m := Sheaf.imageι f
+  e := Sheaf.toImage f
 
 /-- The mono factorization given by `image_sheaf` for a morphism is an image. -/
 noncomputable def imageFactorization {F F' : Sheaf J (Type (max v u))} (f : F ⟶ F') :
@@ -257,14 +259,13 @@ noncomputable def imageFactorization {F F' : Sheaf J (Type (max v u))} (f : F 
   isImage :=
     { lift := fun I => by
         haveI M := (Sheaf.Hom.mono_iff_presheaf_mono J (Type (max v u)) _).mp I.m_mono
-        haveI := isIso_toImagePresheaf I.m.1
-        refine ⟨Subpresheaf.homOfLe ?_ ≫ inv (toImagePresheaf I.m.1)⟩
+        refine ⟨Subpresheaf.homOfLe ?_ ≫ inv (Subpresheaf.toRange I.m.1)⟩
         apply Subpresheaf.sheafify_le
         · conv_lhs => rw [← I.fac]
-          apply imagePresheaf_comp_le
+          apply Subpresheaf.range_comp_le
         · rw [← isSheaf_iff_isSheaf_of_type]
           exact F'.2
-        · apply Presieve.isSheaf_iso J (asIso <| toImagePresheaf I.m.1)
+        · apply Presieve.isSheaf_iso J (asIso <| Subpresheaf.toRange I.m.1)
           rw [← isSheaf_iff_isSheaf_of_type]
           exact I.I.2
       lift_fac := fun I => by
@@ -273,10 +274,17 @@ noncomputable def imageFactorization {F F' : Sheaf J (Type (max v u))} (f : F 
         generalize_proofs h
         rw [← Subpresheaf.homOfLe_ι h, Category.assoc]
         congr 1
-        rw [IsIso.inv_comp_eq, toImagePresheaf_ι] }
+        rw [IsIso.inv_comp_eq, Subpresheaf.toRange_ι] }
 
 instance : Limits.HasImages (Sheaf J (Type max v u)) :=
-  ⟨@fun _ _ f => ⟨⟨imageFactorization f⟩⟩⟩
+  ⟨fun f => ⟨⟨imageFactorization f⟩⟩⟩
+
+@[deprecated (since := "2025-01-25")] alias toImagePresheafSheafify :=
+  Subpresheaf.toRangeSheafify
+@[deprecated (since := "2025-01-25")] alias imageSheaf := Sheaf.image
+@[deprecated (since := "2025-01-25")] alias toImageSheaf := Sheaf.toImage
+@[deprecated (since := "2025-01-25")] alias imageSheafι := Sheaf.imageι
+@[deprecated (since := "2025-01-25")] alias toImageSheaf_ι := Sheaf.toImage_ι
 
 end Image
 

Mathlib/CategoryTheory/Subpresheaf/Basic.lean

@@ -6,7 +6,6 @@ Authors: Andrew Yang
 import Mathlib.CategoryTheory.Elementwise
 import Mathlib.Data.Set.Basic
 
-
 /-!
 
 # Subpresheaf of types
@@ -47,6 +46,8 @@ variable {F F' F'' : Cᵒᵖ ⥤ Type w} (G G' : Subpresheaf F)
 instance : PartialOrder (Subpresheaf F) :=
   PartialOrder.lift Subpresheaf.obj (fun _ _ => Subpresheaf.ext)
 
+lemma Subpresheaf.le_def (S T : Subpresheaf F) : S ≤ T ↔ ∀ U, S.obj U ≤ T.obj U := Iff.rfl
+
 instance : Top (Subpresheaf F) :=
   ⟨⟨fun _ => ⊤, @fun U _ _ x _ => by simp⟩⟩