feat(category_theory/sites): generate lemmas (#4840)

A couple of simple lemmas about the sieve generated by certain presieves.

Author: b-mehta

src/category_theory/sites/pretopology.lean

@@ -167,12 +167,7 @@ See [MM92] Chapter III, Section 2, Equations (3,4).
 -/
 def of_grothendieck (J : grothendieck_topology C) : pretopology C :=
 { coverings := λ X R, sieve.generate R ∈ J X,
-  has_isos := λ X Y f i,
-  begin
-    apply J.covering_of_eq_top,
-    rw [← sieve.id_mem_iff_eq_top],
-    exactI ⟨_, inv f, f, by simp⟩,
-  end,
+  has_isos := λ X Y f i, by exactI J.covering_of_eq_top (by simp),
   pullbacks := λ X Y f R hR,
   begin
     rw [set.mem_def, pullback_arrows_comm],
@@ -197,14 +192,12 @@ def gi : galois_insertion (to_grothendieck C) (of_grothendieck C) :=
   begin
     split,
     { intros h X R hR,
-      apply h,
-      refine ⟨_, hR, _⟩,
-      apply sieve.gi_generate.gc.le_u_l },
+      exact h _ ⟨_, hR, sieve.le_generate R⟩ },
     { rintro h X S ⟨R, hR, RS⟩,
       apply J.superset_covering _ (h _ hR),
       rwa sieve.gi_generate.gc }
   end,
-  le_l_u := λ J X S hS, ⟨S, J.superset_covering (sieve.gi_generate.gc.le_u_l _) hS, le_refl _⟩,
+  le_l_u := λ J X S hS, ⟨S, J.superset_covering S.le_generate hS, le_refl _⟩,
   choice := λ x hx, to_grothendieck C x,
   choice_eq := λ _ _, rfl }
 
@@ -224,8 +217,7 @@ def trivial : pretopology C :=
     refine ⟨pullback (eq_to_hom (eq.refl _) ≫ g) f, pullback.snd, _, _⟩,
     { refine ⟨pullback.lift (f ≫ inv g) (𝟙 _) (by simp), _, _⟩,
       { apply pullback.hom_ext,
-        { rw [assoc, pullback.lift_fst],
-          rw ← pullback.condition_assoc,
+        { rw [assoc, pullback.lift_fst, ← pullback.condition_assoc],
           simp },
         { simp } },
       { simp } },

src/category_theory/sites/sieves.lean

@@ -219,6 +219,31 @@ def gi_generate : galois_insertion (generate : presieve X → sieve X) arrows :=
   choice_eq := λ _ _, rfl,
   le_l_u := λ S Y f hf, ⟨_, 𝟙 _, _, hf, category.id_comp _⟩ }
 
+lemma le_generate (R : presieve X) : R ≤ generate R :=
+gi_generate.gc.le_u_l R
+
+/-- If the identity arrow is in a sieve, the sieve is maximal. -/
+lemma id_mem_iff_eq_top : S (𝟙 X) ↔ S = ⊤ :=
+⟨λ h, top_unique $ λ Y f _, by simpa using downward_closed _ h f,
+ λ h, h.symm ▸ trivial⟩
+
+/-- If an arrow set contains a split epi, it generates the maximal sieve. -/
+lemma generate_of_contains_split_epi {R : presieve X} (f : Y ⟶ X) [split_epi f]
+  (hf : R f) : generate R = ⊤ :=
+begin
+  rw ← id_mem_iff_eq_top,
+  exact ⟨_, section_ f, f, hf, by simp⟩,
+end
+
+@[simp]
+lemma generate_of_singleton_split_epi (f : Y ⟶ X) [split_epi f] :
+  generate (presieve.singleton f) = ⊤ :=
+generate_of_contains_split_epi f (presieve.singleton_self _)
+
+@[simp]
+lemma generate_top : generate (⊤ : presieve X) = ⊤ :=
+generate_of_contains_split_epi (𝟙 _) ⟨⟩
+
 /-- Given a morphism `h : Y ⟶ X`, send a sieve S on X to a sieve on Y
     as the inverse image of S with `_ ≫ h`.
     That is, `sieve.pullback S h := (≫ h) '⁻¹ S`. -/
@@ -246,11 +271,6 @@ lemma pullback_inter {f : Y ⟶ X} (S R : sieve X) :
  (S ⊓ R).pullback f = S.pullback f ⊓ R.pullback f :=
 by simp [sieve.ext_iff]
 
-/-- If the identity arrow is in a sieve, the sieve is maximal. -/
-lemma id_mem_iff_eq_top : S (𝟙 X) ↔ S = ⊤ :=
-⟨λ h, top_unique $ λ Y f _, by simpa using downward_closed _ h f,
- λ h, h.symm ▸ trivial⟩
-
 lemma pullback_eq_top_iff_mem (f : Y ⟶ X) : S f ↔ S.pullback f = ⊤ :=
 by rw [← id_mem_iff_eq_top, mem_pullback, category.id_comp]