feat(CategoryTheory/Sites): pullback point along flat functor (#35124)

For `F : C ⥤ D` a representably flat and cover preserving functor between sites, we construct
a point on `C` from a point on `D` by precomposing the fiber functor with `F`.

Author: chrisflav

Mathlib/CategoryTheory/Filtered/Basic.lean

@@ -324,6 +324,10 @@ theorem of_isRightAdjoint (R : C ⥤ D) [R.IsRightAdjoint] : IsFiltered D :=
 theorem of_equivalence (h : C ≌ D) : IsFiltered D :=
   of_right_adjoint h.symm.toAdjunction
 
+omit [IsFiltered C] in
+lemma iff_of_equivalence (e : C ≌ D) : IsFiltered C ↔ IsFiltered D :=
+  ⟨fun _ ↦ .of_equivalence e, fun _ ↦ .of_equivalence e.symm⟩
+
 end Nonempty
 
 section OfCocone
@@ -841,6 +845,10 @@ theorem of_isLeftAdjoint (L : C ⥤ D) [L.IsLeftAdjoint] : IsCofiltered D :=
 theorem of_equivalence (h : C ≌ D) : IsCofiltered D :=
   of_left_adjoint h.toAdjunction
 
+omit [IsCofiltered C] in
+lemma iff_of_equivalence (e : C ≌ D) : IsCofiltered C ↔ IsCofiltered D :=
+  ⟨fun _ ↦ .of_equivalence e, fun _ ↦ .of_equivalence e.symm⟩
+
 end Nonempty
 
 
@@ -935,6 +943,12 @@ lemma isCofiltered_of_isFiltered_op [IsFiltered Cᵒᵖ] : IsCofiltered C :=
 lemma isFiltered_of_isCofiltered_op [IsCofiltered Cᵒᵖ] : IsFiltered C :=
   IsFiltered.of_equivalence (opOpEquivalence _)
 
+lemma isCofiltered_op_iff_isFiltered : IsCofiltered Cᵒᵖ ↔ IsFiltered C :=
+  ⟨fun _ ↦ isFiltered_of_isCofiltered_op _, fun _ ↦ inferInstance⟩
+
+lemma isFiltered_op_iff_isCofiltered : IsFiltered Cᵒᵖ ↔ IsCofiltered C :=
+  ⟨fun _ ↦ isCofiltered_of_isFiltered_op _, fun _ ↦ inferInstance⟩
+
 end Opposite
 
 section ULift

Mathlib/CategoryTheory/Functor/Flat.lean

@@ -360,4 +360,60 @@ lemma preservesFiniteLimits_iff_lan_preservesFiniteLimits (F : C ⥤ D) :
 
 end SmallCategory
 
+section
+
+variable {C D E : Type*} [Category* C] [Category* D] [Category* E] (F : C ⥤ D) (G : D ⥤ E)
+
+attribute [local instance] IsCofiltered.isConnected IsFiltered.isConnected
+
+instance (X : E) [RepresentablyFlat F] : (StructuredArrow.pre X F G).Final :=
+  ⟨fun _ ↦ isConnected_of_equivalent (StructuredArrow.preEquivalence _ _).symm⟩
+
+instance (X : E) [RepresentablyCoflat F] : (CostructuredArrow.pre F G X).Initial :=
+  ⟨fun _ ↦ isConnected_of_equivalent (CostructuredArrow.preEquivalence _ _).symm⟩
+
+instance (X : E) [RepresentablyFlat F] [IsCofiltered (StructuredArrow X G)] :
+    IsCofiltered (StructuredArrow X (F ⋙ G)) := by
+  let T := StructuredArrow.pre X F G
+  obtain ⟨Y⟩ := IsCofiltered.nonempty (C := StructuredArrow X G)
+  obtain ⟨A⟩ := IsCofiltered.nonempty (C := StructuredArrow Y.right F)
+  have : Nonempty (StructuredArrow X (F ⋙ G)) := ⟨.mk (Y.hom ≫ G.map A.hom)⟩
+  suffices IsCofilteredOrEmpty (StructuredArrow X (F ⋙ G)) by constructor
+  refine ⟨fun A B ↦ ?_, fun A B f g ↦ ?_⟩
+  · let U := IsCofiltered.min (T.obj A) (T.obj B)
+    let A' : StructuredArrow U.right F := .mk (IsCofiltered.minToLeft (T.obj A) (T.obj B)).right
+    let B' : StructuredArrow U.right F := .mk (IsCofiltered.minToRight (T.obj A) (T.obj B)).right
+    refine ⟨.mk <| U.hom ≫ G.map (IsCofiltered.min A' B').hom, ?_, ?_, trivial⟩
+    · refine StructuredArrow.homMk (IsCofiltered.minToLeft A' B').right ?_
+      simpa [← Functor.map_comp] using StructuredArrow.w _
+    · refine StructuredArrow.homMk (IsCofiltered.minToRight A' B').right ?_
+      simpa [← Functor.map_comp] using StructuredArrow.w _
+  · let U := IsCofiltered.eq (T.map f) (T.map g)
+    let A' : StructuredArrow _ F := .mk (IsCofiltered.eqHom (T.map f) (T.map g)).right
+    let B' : StructuredArrow _ F := .mk (IsCofiltered.eqHom (T.map f) (T.map g) ≫ T.map f).right
+    let f' : A' ⟶ B' := StructuredArrow.homMk f.right rfl
+    let g' : A' ⟶ B' := StructuredArrow.homMk g.right
+      congr($(IsCofiltered.eq_condition (T.map f) (T.map g)).right).symm
+    refine ⟨.mk <| U.hom ≫ G.map (IsCofiltered.eq f' g').hom, ?_, ?_⟩
+    · refine StructuredArrow.homMk (IsCofiltered.eqHom f' g').right ?_
+      simpa [← Functor.map_comp] using StructuredArrow.w _
+    · ext
+      exact congr($(IsCofiltered.eq_condition f' g').right)
+
+instance (X : E) [RepresentablyCoflat F] [h : IsFiltered (CostructuredArrow G X)] :
+    IsFiltered (CostructuredArrow (F ⋙ G) X) := by
+  rw [← isCofiltered_op_iff_isFiltered, IsCofiltered.iff_of_equivalence
+    (costructuredArrowOpEquivalence _ _)] at h ⊢
+  exact inferInstanceAs <| IsCofiltered (StructuredArrow (op X) (F.op ⋙ G.op))
+
+instance (G : D ⥤ Type*) [RepresentablyFlat F] [IsCofiltered G.Elements] :
+    IsCofiltered (F ⋙ G).Elements := by
+  suffices h : IsCofiltered (StructuredArrow PUnit (F ⋙ G)) from
+    .of_equivalence (CategoryOfElements.structuredArrowEquivalence _).symm
+  have : IsCofiltered (StructuredArrow PUnit G) :=
+    .of_equivalence (CategoryOfElements.structuredArrowEquivalence _)
+  infer_instance
+
+end
+
 end CategoryTheory

Mathlib/CategoryTheory/Sites/Point/Basic.lean

@@ -8,7 +8,9 @@ module
 public import Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
 public import Mathlib.CategoryTheory.Filtered.FinallySmall
 public import Mathlib.CategoryTheory.Limits.Preserves.Filtered
+public import Mathlib.CategoryTheory.Sites.CoverPreserving
 public import Mathlib.CategoryTheory.Sites.LocallyBijective
+public import Mathlib.CategoryTheory.Functor.Flat
 
 /-!
 # Points of a site
@@ -310,6 +312,26 @@ noncomputable def sheafFiberCompIso [J.HasSheafCompose F] :
   Functor.isoWhiskerLeft (sheafToPresheaf J A) (Φ.presheafFiberCompIso F) ≪≫
     (Functor.associator _ _ _).symm
 
+section Comap
+
+variable {C D : Type*} [Category* C] [Category* D]
+  {J : GrothendieckTopology C} {K : GrothendieckTopology D}
+
+/-- If `F : C ⥤ D` is a representably flat and cover preserving functor between sites, then
+any point on `D` induces a point on `C` by precomposing the fiber functor with `F`. -/
+@[simps]
+def comap (F : C ⥤ D) [RepresentablyFlat F] (H : CoverPreserving J K F) (Φ : Point.{w} K)
+    [InitiallySmall (F ⋙ Φ.fiber).Elements] :
+    Point.{w} J where
+  fiber := F ⋙ Φ.fiber
+  jointly_surjective {X} {R} hR x := by
+    obtain ⟨Y, f, ⟨W, g, h, hg, rfl⟩, y, rfl⟩ :=
+      Φ.jointly_surjective (Sieve.functorPushforward F R) (H.1 hR) x
+    use W, g, hg, Φ.fiber.map h y
+    simp
+
+end Comap
+
 end Point
 
 end GrothendieckTopology