feat(CategoryTheory/Sites): pushforward and pullback of presieves (leanprover-community#40527)

We define analogues of `Sieve.pushforward` and `Sieve.pullback` for `Presieve`s and show the Galois connection.

Author: chrisflav

Mathlib/CategoryTheory/Sites/CoproductSheafCondition.lean

@@ -86,7 +86,8 @@ lemma Presieve.isSheafFor_sigmaDesc_iff {ι : Type*} {X : ι → C} (f : ∀ i,
     [∀ i, HasPullback (f i) (Cofan.IsColimit.desc hc f)]
     (F : Cᵒᵖ ⥤ Type*)
     [PreservesLimit (Discrete.functor <| fun i ↦ op (X i)) F]
-    [PreservesLimit (Discrete.functor fun (ij : ι × ι) ↦ op (pullback (f ij.1) (f ij.2))) F] :
+    [PreservesLimit (Discrete.functor fun (ij : ι × ι) ↦
+      op (Limits.pullback (f ij.1) (f ij.2))) F] :
     Presieve.IsSheafFor F (.singleton <| Cofan.IsColimit.desc hc f) ↔
       Presieve.IsSheafFor F (.ofArrows X f) := by
   let E := PreZeroHypercover.mk _ _ f

Mathlib/CategoryTheory/Sites/Hypercover/Zero.lean

@@ -377,6 +377,56 @@ lemma Hom.sieve₀_le_sieve₀ {E F : PreZeroHypercover S} (f : E.Hom F) : E.sie
 lemma sieve₀_eq_of_iso {E F : PreZeroHypercover S} (e : E ≅ F) : E.sieve₀ = F.sieve₀ :=
   le_antisymm e.hom.sieve₀_le_sieve₀ e.inv.sieve₀_le_sieve₀
 
+/-- The equivalence on index types induced by an isomorphism of pre-`0`-hypercovers. -/
+@[simps]
+def equivOfIso {E F : PreZeroHypercover.{w} S} (e : E ≅ F) : E.I₀ ≃ F.I₀ where
+  toFun := e.hom.s₀
+  invFun := e.inv.s₀
+  left_inv _ := by simp
+  right_inv _ := by simp
+
+lemma mem_of_iso {K : Precoverage C} [K.IsStableUnderComposition] [K.HasIsos] {X : C}
+    {E F : PreZeroHypercover.{w} X} (e : E ≅ F) (hE : E.presieve₀ ∈ K X) :
+    F.presieve₀ ∈ K X := by
+  have : F.presieve₀ =
+      Presieve.ofArrows (fun (i : Σ (_ : F.I₀), Unit) ↦ _) (fun i ↦ e.inv.h₀ i.1 ≫ E.f _) := by
+    simp only [Hom.w₀]
+    refine le_antisymm ?_ ?_
+    · rw [Presieve.ofArrows_le_iff]
+      intro i
+      exact .mk (⟨i, ⟨⟩⟩ : Σ (_ : F.I₀), Unit)
+    · simp [Presieve.ofArrows_le_iff]
+  rw [this]
+  refine K.comp_mem_coverings (fun i ↦ E.f (e.inv.s₀ i)) ?_ (fun i (k : Unit) ↦ e.inv.h₀ i) ?_
+  · rwa [← E.presieve₀_reindex (PreZeroHypercover.equivOfIso e.symm)] at hE
+  · intro i
+    rw [Presieve.ofArrows_pUnit]
+    exact K.mem_coverings_of_isIso _
+
+lemma mem_iff_of_iso {K : Precoverage C} [K.IsStableUnderComposition] [K.HasIsos] {X : C}
+    {E F : PreZeroHypercover.{w} X} (e : E ≅ F) :
+    E.presieve₀ ∈ K X ↔ F.presieve₀ ∈ K X :=
+  ⟨fun h ↦ PreZeroHypercover.mem_of_iso e h, fun h ↦ PreZeroHypercover.mem_of_iso e.symm h⟩
+
+/-- Compose a pre-`0`-hypercover with a morphism on the right. -/
+@[simps]
+def pushforward {X Y : C} (f : X ⟶ Y) (E : PreZeroHypercover.{w} X) :
+    PreZeroHypercover.{w} Y where
+  I₀ := E.I₀
+  X := E.X
+  f i := E.f i ≫ f
+
+lemma presieve₀_pushforward {X Y : C} (f : X ⟶ Y) (E : PreZeroHypercover.{w} X) :
+    (E.pushforward f).presieve₀ = E.presieve₀.pushforward f := by
+  simp [presieve₀, Presieve.pushforward_ofArrows, pushforward]
+
+set_option backward.isDefEq.respectTransparency false in
+/-- Pushforward along a morphism is the same as refining the singleton pre-`0`-hypercover. -/
+@[simps!]
+def pushforwardIsoBind {X Y : C} (f : X ⟶ Y) (E : PreZeroHypercover.{w} X) :
+    E.pushforward f ≅ (singleton f).bind fun _ ↦ E :=
+  isoMk ((Equiv.uniqueSigma fun i ↦ E.I₀).symm) (fun _ ↦ Iso.refl _)
+
 end Category
 
 section Functoriality
@@ -728,6 +778,16 @@ def weaken {K L : Precoverage C} {X : C} (E : Precoverage.ZeroHypercover K X) (h
   __ := E
   mem₀ := h _ E.mem₀
 
+/-- Compose a `0`-hypercover with a morphism on the right. -/
+@[simps toPreZeroHypercover]
+def pushforward [J.IsStableUnderComposition] [J.HasIsos] {X Y : C} (f : X ⟶ Y)
+    (hf : .singleton f ∈ J _) (E : ZeroHypercover.{w} J X) :
+    ZeroHypercover.{w} J Y where
+  __ := E.toPreZeroHypercover.pushforward f
+  mem₀ := by
+    rw [PreZeroHypercover.mem_iff_of_iso (E.pushforwardIsoBind _)]
+    exact ((ZeroHypercover.singleton f hf).bind _).mem₀
+
 instance (K : Precoverage C) [K.HasPullbacks] {X Y : C} (E : K.ZeroHypercover X) (f : Y ⟶ X) :
     E.presieve₀.HasPullbacks f :=
   K.hasPullbacks_of_mem _ E.mem₀

Mathlib/CategoryTheory/Sites/IsSheafFor.lean

@@ -1062,10 +1062,10 @@ theorem isSheafFor_trans (P : Cᵒᵖ ⥤ Type*) (R S : Sieve X)
   apply Presieve.isSheafFor_subsieve_aux P this
   · apply isSheafFor_bind _ _ _ hR hS
     intro Y f hf Z g
-    rw [← pullback_comp]
+    rw [← Sieve.pullback_comp]
     apply (hS (R.downward_closed hf _)).isSeparatedFor
   · intro Y f hf
-    have : Sieve.pullback f (Sieve.bind R fun T (k : T ⟶ X) (_ : R k) => pullback k S) =
+    have : Sieve.pullback f (Sieve.bind R fun T (k : T ⟶ X) (_ : R k) => Sieve.pullback k S) =
         R.pullback f := by
       ext Z g
       constructor

Mathlib/CategoryTheory/Sites/Sieves.lean

@@ -295,6 +295,82 @@ lemma bindOfArrows_ofArrows {ι : Type*} {S : C} {X : ι → C} (f : (i : ι) 
   rintro W u ⟨i, v, ⟨j⟩⟩
   exact ⟨Sigma.mk i j⟩
 
+/-- Compose a presieve on the right with a morphism. -/
+def pushforward {X Y : C} (f : X ⟶ Y) (R : Presieve X) : Presieve Y :=
+  fun Z fg ↦ ∃ (g : Z ⟶ X), g ≫ f = fg ∧ R g
+
+@[grind .]
+lemma pushforward_apply_comp {X Y Z : C} {f : X ⟶ Y} {R : Presieve X} {g : Z ⟶ X} (hg : R g) :
+    R.pushforward f (g ≫ f) :=
+  ⟨g, rfl, hg⟩
+
+lemma pushforward_ofArrows {ι : Type*} {U : ι → C} {X Y : C} (g : ∀ i, U i ⟶ X)
+    (f : X ⟶ Y) : (ofArrows _ g).pushforward f = ofArrows _ (g · ≫ f) := by
+  refine le_antisymm ?_ ?_
+  · rintro _ _ ⟨u, rfl, ⟨i⟩⟩
+    exact ⟨i⟩
+  · rw [ofArrows_le_iff]
+    intro i
+    use g i, rfl
+    exact ⟨i⟩
+
+lemma pushforward_singleton {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
+    (singleton f).pushforward g = .singleton (f ≫ g) := by
+  rw [← ofArrows_pUnit.{_, _, 0}, pushforward_ofArrows, ofArrows_pUnit.{_, _, 0}]
+
+/-- The pullback of a presieve `R` on `Y` along a morphism `f : X ⟶ Y` is the presieve on `X`
+given by all morphisms `g : Z ⟶ X` such that `f ≫ g` is in `R`. -/
+def pullback {X Y : C} (f : X ⟶ Y) (R : Presieve Y) : Presieve X :=
+  fun _ g ↦ R (g ≫ f)
+
+variable {f} in
+@[simp, grind =]
+lemma pullback_iff {R : Presieve X} {Z : C} {g : Z ⟶ Y} :
+    R.pullback f g ↔ R (g ≫ f) :=
+  .rfl
+
+lemma pushforward_le_iff_le_pullback (R : Presieve Y) (T : Presieve X) :
+    R.pushforward f ≤ T ↔ R ≤ T.pullback f := by
+  refine ⟨fun hle Z g hg ↦ hle _ _ (pushforward_apply_comp hg), ?_⟩
+  rintro hle Z - ⟨g, rfl, hg⟩
+  exact hle _ _ hg
+
+lemma galoisConnection_pushforward_pullback :
+    GaloisConnection (pushforward f) (pullback f) :=
+  pushforward_le_iff_le_pullback f
+
+lemma monotone_pushforward : Monotone (pushforward f) :=
+  (galoisConnection_pushforward_pullback f).monotone_l
+
+lemma monotone_pullback : Monotone (pullback f) :=
+  (galoisConnection_pushforward_pullback f).monotone_u
+
+lemma pushforward_pullback_le (R : Presieve X) : (R.pullback f).pushforward f ≤ R :=
+  (galoisConnection_pushforward_pullback f).l_u_le _
+
+lemma le_pullback_pushforward (R : Presieve Y) : R ≤ (R.pushforward f).pullback f :=
+  (galoisConnection_pushforward_pullback f).le_u_l _
+
+@[simp]
+lemma pullback_id (R : Presieve X) : R.pullback (𝟙 X) = R := by
+  funext
+  simp
+
+lemma pullback_comp (R : Presieve Z) (g : X ⟶ Z) :
+    R.pullback (f ≫ g) = (R.pullback g).pullback f := by
+  funext
+  simp
+
+@[simp]
+lemma pushforward_id (R : Presieve X) : R.pushforward (𝟙 X) = R := by
+  funext
+  simp [pushforward]
+
+lemma pushforward_comp (R : Presieve Y) (g : X ⟶ Z) :
+    R.pushforward (f ≫ g) = (R.pushforward f).pushforward g := by
+  funext
+  simp [pushforward]
+
 /-- Given a presieve on `F(X)`, we can define a presieve on `X` by taking the preimage via `F`. -/
 def functorPullback (R : Presieve (F.obj X)) : Presieve X := fun _ f => R (F.map f)
 
@@ -462,7 +538,8 @@ def uncurry : Set (Σ Y, Y ⟶ X) :=
     obtain ⟨rfl, h⟩ := h; subst h; constructor
 
 @[simp] theorem uncurry_pullbackArrows [HasPullbacks C] {B : C} (b : B ⟶ X) :
-    (pullbackArrows b s).uncurry = (fun f ↦ ⟨pullback f.2 b, pullback.snd _ _⟩) '' s.uncurry := by
+    (pullbackArrows b s).uncurry =
+      (fun f ↦ ⟨Limits.pullback f.2 b, pullback.snd _ _⟩) '' s.uncurry := by
   ext ⟨Z, v⟩; constructor
   · rintro ⟨Y, u, hu⟩; exact ⟨⟨Y, u⟩, hu, rfl⟩
   · rintro ⟨⟨Y, u⟩, hu, h⟩
@@ -956,6 +1033,19 @@ theorem pullbackArrows_comm {X Y : C} (f : Y ⟶ X) (R : Presieve X) [R.HasPullb
     have := R.hasPullback f hk
     exact ⟨_, _, _, Presieve.pullbackArrows.mk _ _ hk, pullback.lift_snd _ _ comm⟩
 
+lemma pullback_arrows {X Y : C} (f : X ⟶ Y) (S : Sieve Y) :
+    (S.pullback f).arrows = S.arrows.pullback f :=
+  rfl
+
+lemma pushforward_arrows {X Y : C} (f : X ⟶ Y) (S : Sieve X) :
+    (S.pushforward f).arrows = S.arrows.pushforward f :=
+  rfl
+
+lemma generate_pushforward {X Y : C} (f : X ⟶ Y) (R : Presieve X) :
+    generate (R.pushforward f) = (generate R).pushforward f := by
+  ext
+  grind [generate_apply, Presieve.pushforward, pushforward_apply]
+
 section Functor
 
 variable {E : Type u₃} [Category.{v₃} E] (G : D ⥤ E)