feat(CategoryTheory/Sites): Over.post F preserves covers if F does (#37775)

We also show the lifting covers variant. Notably, we don't show that `Over.post F` is continuous if `F` is. This would follow for example from showing that sheaves on `Over X` are sheaves on `C` over `yoneda.obj X`, which we don't have yet.

Author: chrisflav

Mathlib/CategoryTheory/Comma/Over/Basic.lean

@@ -410,6 +410,10 @@ lemma post_comp {E : Type*} [Category* E] (F : T ⥤ D) (G : D ⥤ E) :
     post (X := X) (F ⋙ G) = post (X := X) F ⋙ post G :=
   rfl
 
+lemma post_forget_eq_forget_comp (F : T ⥤ D) (X : T) :
+    post F ⋙ forget (F.obj X) = forget X ⋙ F :=
+  rfl
+
 set_option backward.isDefEq.respectTransparency false in
 /-- `post (F ⋙ G)` is isomorphic (actually equal) to `post F ⋙ post G`. -/
 @[simps!]
@@ -897,6 +901,10 @@ lemma post_comp {E : Type*} [Category* E] (F : T ⥤ D) (G : D ⥤ E) :
     post (X := X) (F ⋙ G) = post (X := X) F ⋙ post G :=
   rfl
 
+lemma post_forget_eq_forget_comp (F : T ⥤ D) (X : T) :
+    post F ⋙ forget (F.obj X) = forget X ⋙ F :=
+  rfl
+
 set_option backward.isDefEq.respectTransparency false in
 /-- `post (F ⋙ G)` is isomorphic (actually equal) to `post F ⋙ post G`. -/
 @[simps!]

Mathlib/CategoryTheory/Sites/Over.lean

@@ -181,6 +181,29 @@ lemma overEquiv_functorPullback_map {X Y : C} (f : X ⟶ Y) (U : Over X)
   rw [Sieve.overEquiv_iff, Sieve.overEquiv_iff]
   simp [Presieve.functorPullback, heq]
 
+set_option backward.isDefEq.respectTransparency false in
+lemma overEquiv_functorPullback_post {D : Type*} [Category* D] (F : C ⥤ D) {X : C}
+    (U : Over X) (S : Sieve ((Over.post F).obj U)) :
+    (Sieve.overEquiv U) (Sieve.functorPullback (Over.post F) S) =
+      Sieve.functorPullback F ((Sieve.overEquiv ((Over.post F).obj U)) S) := by
+  refine le_antisymm ?_ ?_
+  · dsimp [Sieve.overEquiv]
+    rw [Sieve.functorPushforward_le_iff_le_functorPullback, ← Sieve.functorPullback_comp]
+    simp_rw [← CategoryTheory.Over.post_forget_eq_forget_comp, Sieve.functorPullback_comp]
+    exact Sieve.functorPullback_monotone _ _ (Sieve.le_functorPushforward_pullback _ _)
+  · intro Z g hg
+    rw [Sieve.overEquiv_iff]
+    dsimp [Presieve.functorPullback]
+    convert (Sieve.overEquiv_iff _ _).mp hg
+    simp
+
+set_option backward.isDefEq.respectTransparency false in
+lemma overEquiv_functorPushforward_post {D : Type*} [Category* D] (F : C ⥤ D) {X : C}
+    (U : Over X) (S : Sieve U) :
+    (Sieve.overEquiv _) (Sieve.functorPushforward (Over.post F) S) =
+      Sieve.functorPushforward F ((Sieve.overEquiv _) S) := by
+  simp [Sieve.overEquiv, ← Sieve.functorPushforward_comp, ← Over.post_forget_eq_forget_comp]
+
 end Sieve
 
 variable (J : GrothendieckTopology C)
@@ -273,6 +296,23 @@ instance {X Y : C} (f : X ⟶ Y) : (Over.map f).IsCocontinuous (J.over _) (J.ove
     rw [J.mem_over_iff] at hS ⊢
     rwa [Sieve.overEquiv_functorPullback_map]
 
+instance {D : Type*} [Category* D] (K : GrothendieckTopology D)
+    (F : C ⥤ D) (X : C) [F.IsCocontinuous J K] :
+    (Over.post (X := X) F).IsCocontinuous (J.over X) (K.over _) where
+  cover_lift {U} S hS := by
+    rw [GrothendieckTopology.mem_over_iff] at hS ⊢
+    rw [Sieve.overEquiv_functorPullback_post]
+    exact F.cover_lift J K hS
+
+variable {J} in
+lemma _root_.CategoryTheory.CoverPreserving.overPost {D : Type*} [Category* D]
+    {K : GrothendieckTopology D} {F : C ⥤ D} (X : C) (h : CoverPreserving J K F) :
+    CoverPreserving (J.over X) (K.over _) (Over.post (X := X) F) where
+  cover_preserve {U} S hS := by
+    rw [GrothendieckTopology.mem_over_iff] at hS ⊢
+    rw [Sieve.overEquiv_functorPushforward_post]
+    exact h.cover_preserve hS
+
 open Limits
 
 lemma coverPreserving_overPullback [HasPullbacks C] {X Y : C} (f : X ⟶ Y) :