chore(category_theory/sites): nicer names (#4816)

Changes the name `arrows_with_codomain` to `presieve` which is more suggestive and shorter, and changes `singleton_arrow` to `singleton`, since it's in the presieve namespace anyway.

src/category_theory/sites/pretopology.lean

@@ -37,7 +37,7 @@ noncomputable theory
 
 namespace category_theory
 
-open category_theory category limits arrows_with_codomain
+open category_theory category limits presieve
 
 variables {C : Type u} [category.{v} C] [has_pullbacks C]
 
@@ -47,13 +47,13 @@ category.
 This is not the same as the arrow set of `sieve.pullback`, but there is a relation between them
 in `pullback_arrows_comm`.
 -/
-def pullback_arrows {X Y : C} (f : Y ⟶ X) (S : arrows_with_codomain X) :
-  arrows_with_codomain Y :=
+def pullback_arrows {X Y : C} (f : Y ⟶ X) (S : presieve X) :
+  presieve Y :=
 λ Z g, ∃ Z' (h : Z' ⟶ X), S h ∧ ∃ (H : Z = pullback h f),
   eq_to_hom H ≫ pullback.snd = g
 
 lemma pullback_arrows_comm {X Y : C} (f : Y ⟶ X)
-  (R : arrows_with_codomain X) :
+  (R : presieve X) :
   sieve.generate (pullback_arrows f R) = (sieve.generate R).pullback f :=
 begin
   ext Z g,
@@ -66,7 +66,7 @@ begin
 end
 
 lemma pullback_singleton {X Y Z : C} (f : Y ⟶ X) (g : Z ⟶ X) :
- ∃ (W : C) (k : W ⟶ Y), pullback_arrows f (singleton_arrow g) = singleton_arrow k :=
+ ∃ (W : C) (k : W ⟶ Y), pullback_arrows f (singleton g) = singleton k :=
 begin
   refine ⟨pullback (eq_to_hom (eq.refl _) ≫ g) f, pullback.snd, _⟩,
   ext W k,
@@ -99,11 +99,11 @@ a basis for a topology.
 -/
 @[ext]
 structure pretopology :=
-(coverings : Π (X : C), set (arrows_with_codomain X))
-(has_isos : ∀ ⦃X Y⦄ (f : Y ⟶ X) [is_iso f], arrows_with_codomain.singleton_arrow f ∈ coverings X)
+(coverings : Π (X : C), set (presieve X))
+(has_isos : ∀ ⦃X Y⦄ (f : Y ⟶ X) [is_iso f], presieve.singleton f ∈ coverings X)
 (pullbacks : ∀ ⦃X Y⦄ (f : Y ⟶ X) S, S ∈ coverings X → pullback_arrows f S ∈ coverings Y)
-(transitive : ∀ ⦃X : C⦄ (S : arrows_with_codomain X)
-               (Ti : Π ⦃Y⦄ (f : Y ⟶ X), S f → arrows_with_codomain Y), S ∈ coverings X →
+(transitive : ∀ ⦃X : C⦄ (S : presieve X)
+               (Ti : Π ⦃Y⦄ (f : Y ⟶ X), S f → presieve Y), S ∈ coverings X →
                (∀ ⦃Y⦄ f (H : S f), Ti f H ∈ coverings Y) → S.bind Ti ∈ coverings X)
 
 namespace pretopology
@@ -135,8 +135,8 @@ A pretopology `K` can be completed to a Grothendieck topology `J` by declaring a
 See https://stacks.math.columbia.edu/tag/00ZC, or [MM92] Chapter III, Section 2, Equation (2).
 -/
 def to_grothendieck (K : pretopology C) : grothendieck_topology C :=
-{ sieves := λ X S, ∃ R ∈ K X, R ≤ (S : arrows_with_codomain _),
-  top_mem' := λ X, ⟨arrows_with_codomain.singleton_arrow (𝟙 _), K.has_isos _, λ _ _ _, ⟨⟩⟩,
+{ sieves := λ X S, ∃ R ∈ K X, R ≤ (S : presieve _),
+  top_mem' := λ X, ⟨presieve.singleton (𝟙 _), K.has_isos _, λ _ _ _, ⟨⟩⟩,
   pullback_stable' := λ X Y S g,
   begin
     rintro ⟨R, hR, RS⟩,
@@ -155,7 +155,7 @@ def to_grothendieck (K : pretopology C) : grothendieck_topology C :=
   end }
 
 lemma mem_to_grothendieck (K : pretopology C) (X S) :
-  S ∈ to_grothendieck C K X ↔ ∃ R ∈ K X, R ≤ (S : arrows_with_codomain X) :=
+  S ∈ to_grothendieck C K X ↔ ∃ R ∈ K X, R ≤ (S : presieve X) :=
 iff.rfl
 
 /--
@@ -213,7 +213,7 @@ also known as the indiscrete, coarse, or chaotic topology.
 See https://stacks.math.columbia.edu/tag/07GE
 -/
 def trivial : pretopology C :=
-{ coverings := λ X S, ∃ Y (f : Y ⟶ X) (h : is_iso f), S = arrows_with_codomain.singleton_arrow f,
+{ coverings := λ X S, ∃ Y (f : Y ⟶ X) (h : is_iso f), S = presieve.singleton f,
   has_isos := λ X Y f i, ⟨_, _, i, rfl⟩,
   pullbacks := λ X Y f S,
   begin

src/category_theory/sites/sieves.lean

@@ -33,32 +33,33 @@ variables {X Y Z : C} (f : Y ⟶ X)
 
 /-- A set of arrows all with codomain `X`. -/
 @[derive complete_lattice]
-def arrows_with_codomain (X : C) := Π ⦃Y⦄, set (Y ⟶ X)
+def presieve (X : C) := Π ⦃Y⦄, set (Y ⟶ X)
 
-namespace arrows_with_codomain
+namespace presieve
 
-instance : inhabited (arrows_with_codomain X) := ⟨⊤⟩
+instance : inhabited (presieve X) := ⟨⊤⟩
 
 /--
 Given a set of arrows `S` all with codomain `X`, and a set of arrows with codomain `Y` for each
 `f : Y ⟶ X` in `S`, produce a set of arrows with codomain `X`:
 `{ g ≫ f | (f : Y ⟶ X) ∈ S, (g : Z ⟶ Y) ∈ R f }`.
 -/
-def bind (S : arrows_with_codomain X) (R : Π ⦃Y⦄ ⦃f : Y ⟶ X⦄, S f → arrows_with_codomain Y) :
-  arrows_with_codomain X :=
+def bind (S : presieve X) (R : Π ⦃Y⦄ ⦃f : Y ⟶ X⦄, S f → presieve Y) :
+  presieve X :=
 λ Z h, ∃ (Y : C) (g : Z ⟶ Y) (f : Y ⟶ X) (H : S f), R H g ∧ g ≫ f = h
 
 @[simp]
-lemma bind_comp {S : arrows_with_codomain X}
-  {R : Π ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S f → arrows_with_codomain Y} {g : Z ⟶ Y} (h₁ : S f) (h₂ : R h₁ g) :
+lemma bind_comp {S : presieve X}
+  {R : Π ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S f → presieve Y} {g : Z ⟶ Y} (h₁ : S f) (h₂ : R h₁ g) :
 bind S R (g ≫ f) :=
 ⟨_, _, _, h₁, h₂, rfl⟩
 
-/-- The singleton arrow set. -/
-def singleton_arrow : arrows_with_codomain X :=
+/-- The singleton presieve.  -/
+-- Note we can't make this into `has_singleton` because of the out-param.
+def singleton : presieve X :=
 λ Z g, ∃ (H : Z = Y), eq_to_hom H ≫ f = g
 
-@[simp] lemma singleton_arrow_eq_iff_domain (f g : Y ⟶ X) : singleton_arrow f g ↔ f = g :=
+@[simp] lemma singleton_eq_iff_domain (f g : Y ⟶ X) : singleton f g ↔ f = g :=
 begin
   split,
   { rintro ⟨_, rfl⟩,
@@ -67,16 +68,16 @@ begin
     exact ⟨rfl, category.id_comp _⟩ },
 end
 
-lemma singleton_arrow_self : singleton_arrow f f := (singleton_arrow_eq_iff_domain _ _).2 rfl
+lemma singleton_arrow_self : singleton f f := (singleton_eq_iff_domain _ _).2 rfl
 
-end arrows_with_codomain
+end presieve
 
 /--
 For an object `X` of a category `C`, a `sieve X` is a set of morphisms to `X` which is closed under
 left-composition.
 -/
 structure sieve {C : Type u} [category.{v} C] (X : C) :=
-(arrows : arrows_with_codomain X)
+(arrows : presieve X)
 (downward_closed' : ∀ {Y Z f} (hf : arrows f) (g : Z ⟶ Y), arrows (g ≫ f))
 
 namespace sieve
@@ -179,20 +180,20 @@ iff.rfl
 lemma mem_top (f : Y ⟶ X) : (⊤ : sieve X) f := trivial
 
 /-- Generate the smallest sieve containing the given set of arrows. -/
-def generate (R : arrows_with_codomain X) : sieve X :=
+def generate (R : presieve X) : sieve X :=
 { arrows := λ Z f, ∃ Y (h : Z ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f,
   downward_closed' :=
   begin
     rintro Y Z _ ⟨W, g, f, hf, rfl⟩ h,
     exact ⟨_, h ≫ g, _, hf, by simp⟩,
   end }
 
-lemma mem_generate (R : arrows_with_codomain X) (f : Z ⟶ X) :
+lemma mem_generate (R : presieve X) (f : Z ⟶ X) :
   generate R f ↔ ∃ (Y : C) (h : Z ⟶ Y) (g : Y ⟶ X), R g ∧ h ≫ g = f :=
 iff.rfl
 
 /-- Given a collection of arrows with fixed codomain,  -/
-def bind (S : arrows_with_codomain X) (R : Π ⦃Y⦄ ⦃f : Y ⟶ X⦄, S f → sieve Y) : sieve X :=
+def bind (S : presieve X) (R : Π ⦃Y⦄ ⦃f : Y ⟶ X⦄, S f → sieve Y) : sieve X :=
 { arrows := S.bind (λ Y f h, R h),
   downward_closed' :=
   begin
@@ -202,7 +203,7 @@ def bind (S : arrows_with_codomain X) (R : Π ⦃Y⦄ ⦃f : Y ⟶ X⦄, S f →
 
 open order lattice
 
-lemma sets_iff_generate (R : arrows_with_codomain X) (S : sieve X) :
+lemma sets_iff_generate (R : presieve X) (S : sieve X) :
   generate R ≤ S ↔ R ≤ S :=
 ⟨λ H Y g hg, H _ ⟨_, 𝟙 _, _, hg, category.id_comp _⟩,
  λ ss Y f,
@@ -212,7 +213,7 @@ lemma sets_iff_generate (R : arrows_with_codomain X) (S : sieve X) :
   end⟩
 
 /-- Show that there is a galois insertion (generate, set_over). -/
-def gi_generate : galois_insertion (generate : arrows_with_codomain X → sieve X) arrows :=
+def gi_generate : galois_insertion (generate : presieve X → sieve X) arrows :=
 { gc := sets_iff_generate,
   choice := λ 𝒢 _, generate 𝒢,
   choice_eq := λ _ _, rfl,
@@ -295,15 +296,15 @@ lemma pushforward_union {f : Y ⟶ X} (S R : sieve Y) :
   (S ⊔ R).pushforward f = S.pushforward f ⊔ R.pushforward f :=
 (galois_connection f).l_sup
 
-lemma pushforward_le_bind_of_mem (S : arrows_with_codomain X)
+lemma pushforward_le_bind_of_mem (S : presieve X)
   (R : Π ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S f → sieve Y) (f : Y ⟶ X) (h : S f) :
   (R h).pushforward f ≤ bind S R :=
 begin
   rintro Z _ ⟨g, rfl, hg⟩,
   exact ⟨_, g, f, h, hg, rfl⟩,
 end
 
-lemma le_pullback_bind (S : arrows_with_codomain X) (R : Π ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S f → sieve Y)
+lemma le_pullback_bind (S : presieve X) (R : Π ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S f → sieve Y)
   (f : Y ⟶ X) (h : S f) :
   R h ≤ (bind S R).pullback f :=
 begin