feat(CategoryTheory/Sites): a cover preserving functor that preserves pullbacks preserves 1-hypercovers (#39592)

Author: chrisflav

Mathlib/CategoryTheory/Sites/Continuous.lean

@@ -85,6 +85,58 @@ then `(E.map F).multifork P` is a limit iff `E.multifork (F.op ⋙ P)` is a limi
 def isLimitMapMultiforkEquiv {A : Type u} [Category.{t} A] (P : Dᵒᵖ ⥤ A) :
     IsLimit ((E.map F).multifork P) ≃ IsLimit (E.multifork (F.op ⋙ P)) := by rfl
 
+section
+
+variable {E} {W : C} {i₁ i₂ : E.I₀} (p₁ : W ⟶ E.X i₁) (p₂ : W ⟶ E.X i₂)
+
+lemma functorPushforward_sieve₁_map_le :
+    Sieve.functorPushforward F (E.sieve₁ p₁ p₂) ≤ (E.map F).sieve₁ (F.map p₁) (F.map p₂) := by
+  rw [Sieve.functorPushforward_le_iff_le_functorPullback]
+  intro Y f ⟨k, u, hf₁, hf₂⟩
+  exact ⟨k, F.map u, by simp [← Functor.map_comp, hf₁], by simp [← Functor.map_comp, hf₂]⟩
+
+variable (i₁ i₂) in
+set_option backward.isDefEq.respectTransparency false in
+lemma functorPushforward_sieve₁'_of_preservesLimit [HasPullback (E.f i₁) (E.f i₂)]
+    [PreservesLimit (cospan (E.f i₁) (E.f i₂)) F] :
+    Sieve.functorPushforward F (E.sieve₁' i₁ i₂) =
+      (E.map F).sieve₁ (F.map <| pullback.fst _ _) (F.map <| pullback.snd _ _) := by
+  have : HasPullback ((E.map F).f i₁) ((E.map F).f i₂) :=
+    hasPullback_of_preservesPullback F (E.f i₁) (E.f i₂)
+  refine le_antisymm ?_ ?_
+  · rw [PreOneHypercover.sieve₁'_eq_sieve₁]
+    apply PreOneHypercover.functorPushforward_sieve₁_map_le
+  · rw [PreOneHypercover.sieve₁_eq_pullback_sieve₁' _ _ _
+      (by simp [← Functor.map_comp, pullback.condition])]
+    rintro W f ⟨Z, u, v, ⟨k⟩, h⟩
+    refine ⟨E.Y k, pullback.lift (E.p₁ k) (E.p₂ k) (E.w _), u, ?_, ?_⟩
+    · use E.Y k, 𝟙 _, pullback.lift (E.p₁ k) (E.p₂ k) (E.w _), ⟨k⟩
+      simp
+    · simp only [pullback.hom_ext_iff, Category.assoc, limit.lift_π, PullbackCone.mk_π_app] at h
+      apply IsPullback.hom_ext (IsPullback.map _ (.of_hasPullback _ _)) <;>
+        simp [← h.left, ← h.right, ← Functor.map_comp]
+
+set_option backward.isDefEq.respectTransparency false in
+lemma functorPushforward_sieve₁_of_preservesPullbacks (h : p₁ ≫ E.f _ = p₂ ≫ E.f _)
+    [HasPullbacks C] [PreservesLimitsOfShape WalkingCospan F] :
+    Sieve.functorPushforward F (E.sieve₁ p₁ p₂) = (E.map F).sieve₁ (F.map p₁) (F.map p₂) := by
+  refine le_antisymm (PreOneHypercover.functorPushforward_sieve₁_map_le _ _ _) ?_
+  have : HasPullback ((E.map F).f i₁) ((E.map F).f i₂) :=
+    hasPullback_of_preservesPullback F (E.f i₁) (E.f i₂)
+  rintro T f ⟨k, u, hf₁, hf₂⟩
+  let l : W ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift p₁ p₂ h
+  have hl₁ : l ≫ pullback.fst _ _ = p₁ := by simp [l]
+  have hl₂ : l ≫ pullback.snd _ _ = p₂ := by simp [l]
+  let r : E.Y k ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift (E.p₁ _) (E.p₂ _) (E.w _)
+  refine ⟨pullback l r, pullback.fst _ _, IsPullback.lift
+    (IsPullback.map _ (.of_hasPullback _ _)) f u ?_, ?_, ?_⟩
+  · apply (IsPullback.map _ (.of_hasPullback _ _)).hom_ext <;>
+      simp [l, r, ← Functor.map_comp, hf₁, hf₂]
+  · refine ⟨k, pullback.snd _ _, ?_, ?_⟩ <;> simp [← hl₁, ← hl₂, pullback.condition_assoc, r]
+  · simp
+
+end
+
 end PreOneHypercover
 
 namespace GrothendieckTopology

Mathlib/CategoryTheory/Sites/CoverPreserving.lean

@@ -168,4 +168,21 @@ lemma Functor.isContinuous_of_coverPreserving (hF₁ : CompatiblePreserving.{max
       rintro Y _ ⟨Z, g, h, hg, rfl⟩
       simpa using congrArg _ ((hy₁ g hg).trans (hy₂ g hg).symm)
 
+/-- If `C` has pullbacks and `F : C ⥤ D` preserves pullbacks, any cover preserving
+functor preserves all `1`-hypercovers. -/
+lemma Functor.PreservesOneHypercovers.of_coverPreserving [HasPullbacks C]
+    [PreservesLimitsOfShape WalkingCospan F] (H : CoverPreserving J K F) :
+    Functor.PreservesOneHypercovers.{w} F J K := by
+  refine fun {U} E ↦ ⟨?_, fun i₁ i₂ W p₁ p₂ h ↦ ?_⟩
+  · simp [PreZeroHypercover.sieve₀_map, H.cover_preserve E.mem₀]
+  · let P : C := pullback (E.f i₁) (E.f i₂)
+    have : HasPullback ((E.toPreOneHypercover.map F).f i₁) ((E.toPreOneHypercover.map F).f i₂) :=
+      hasPullback_of_preservesPullback F (E.f i₁) (E.f i₂)
+    have := H.cover_preserve (E.mem₁ i₁ i₂ (pullback.fst (E.f i₁) (E.f i₂)) _ pullback.condition)
+    rw [PreOneHypercover.functorPushforward_sieve₁_of_preservesPullbacks _ _ _
+      pullback.condition] at this
+    refine K.superset_covering ?_
+      (K.pullback_stable (IsPullback.lift (.map _ (.of_hasPullback _ _)) p₁ p₂ h) this)
+    simp [PreOneHypercover.pullback_sieve₁]
+
 end CategoryTheory

Mathlib/CategoryTheory/Sites/Hypercover/One.lean

@@ -71,6 +71,13 @@ def sieve₁ {i₁ i₂ : E.I₀} {W : C} (p₁ : W ⟶ E.X i₁) (p₂ : W ⟶
     rintro Z Z' g ⟨j, h, fac₁, fac₂⟩ φ
     exact ⟨j, φ ≫ h, by simpa using φ ≫= fac₁, by simpa using φ ≫= fac₂⟩
 
+lemma pullback_sieve₁ {i₁ i₂ : E.I₀} {W : C} (p₁ : W ⟶ E.X i₁) (p₂ : W ⟶ E.X i₂)
+    {T : C} (f : T ⟶ W) :
+    Sieve.pullback f (E.sieve₁ p₁ p₂) = E.sieve₁ (f ≫ p₁) (f ≫ p₂) := by
+  refine le_antisymm ?_ ?_ <;>
+  · intro Z g ⟨k, u, hu₁, hu₂⟩
+    cat_disch
+
 section
 
 variable {i₁ i₂ : E.I₀} [HasPullback (E.f i₁) (E.f i₂)]
@@ -79,6 +86,14 @@ variable {i₁ i₂ : E.I₀} [HasPullback (E.f i₁) (E.f i₂)]
 noncomputable abbrev toPullback (j : E.I₁ i₁ i₂) : E.Y j ⟶ pullback (E.f i₁) (E.f i₂) :=
   pullback.lift (E.p₁ j) (E.p₂ j) (E.w j)
 
+@[reassoc (attr := simp)]
+lemma toPullback_fst (k : E.I₁ i₁ i₂) : E.toPullback k ≫ pullback.fst _ _ = E.p₁ k := by
+  rw [pullback.lift_fst]
+
+@[reassoc (attr := simp)]
+lemma toPullback_snd (k : E.I₁ i₁ i₂) : E.toPullback k ≫ pullback.snd _ _ = E.p₂ k := by
+  rw [pullback.lift_snd]
+
 variable (i₁ i₂) in
 /-- The sieve of `pullback (E.f i₁) (E.f i₂)` given by `E : PreOneHypercover S`. -/
 noncomputable def sieve₁' : Sieve (pullback (E.f i₁) (E.f i₂)) :=