feat(AlgebraicGeometry): Scheme.Hom.opensFunctor preserves 1-hypercovers (leanprover-community#40990)

We deduce this from the fact that it preserves pullbacks, which we deduce from general facts about thin categories.

Author: chrisflav

Mathlib/AlgebraicGeometry/OpenImmersion.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Geometry.RingedSpace.OpenImmersion
 public import Mathlib.AlgebraicGeometry.Scheme
 public import Mathlib.CategoryTheory.MorphismProperty.Limits
+public import Mathlib.CategoryTheory.Limits.Preorder
 
 /-!
 # Open immersions of schemes
@@ -87,6 +88,37 @@ theorem mem_opensRange {f : X ⟶ Y} [IsOpenImmersion f] {y : Y} :
 def opensFunctor : X.Opens ⥤ Y.Opens :=
   LocallyRingedSpace.IsOpenImmersion.opensFunctor f.toLRSHom
 
+/-- The adjunction image-preimage adjunction for an open immersion of schemes. -/
+def opensFunctorAdjunction : f.opensFunctor ⊣ TopologicalSpace.Opens.map f.base :=
+  IsOpenMap.adjunction ‹IsOpenImmersion f›.base_open.isOpenMap
+
+instance : f.opensFunctor.IsLeftAdjoint :=
+  f.opensFunctorAdjunction.isLeftAdjoint
+
+instance : f.opensFunctor.IsCocontinuous (Opens.grothendieckTopology _)
+    (Opens.grothendieckTopology _) := by
+  rw [f.opensFunctorAdjunction.isCocontinuous_iff_coverPreserving]
+  exact coverPreserving_opens_map f.base
+
+instance : f.opensFunctor.Full :=
+  have : Mono f.base := (TopCat.mono_iff_injective f.base).mpr f.isOpenEmbedding.injective
+  inferInstanceAs f.isOpenEmbedding.functor.Full
+
+lemma coverPreserving_opensFunctor :
+    CoverPreserving (Opens.grothendieckTopology _) (Opens.grothendieckTopology _) f.opensFunctor :=
+  f.isOpenEmbedding.isOpenMap.coverPreserving
+
+instance {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] :
+    PreservesLimitsOfShape WalkingCospan (Scheme.Hom.opensFunctor f) := by
+  dsimp [Scheme.Hom.opensFunctor]
+  infer_instance
+
+instance {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] :
+    f.opensFunctor.PreservesOneHypercovers (Opens.grothendieckTopology _)
+      (Opens.grothendieckTopology _) := by
+  refine Functor.PreservesOneHypercovers.of_coverPreserving ?_
+  exact Scheme.Hom.coverPreserving_opensFunctor f
+
 /-- `f ''ᵁ U` is notation for the image (as an open set) of `U` under an open immersion `f`.
 The preferred name in lemmas is `image` and it should be treated as an infix. -/
 scoped[AlgebraicGeometry] notation3:90 f:91 " ''ᵁ " U:90 => (Scheme.Hom.opensFunctor f).obj U
@@ -206,6 +238,13 @@ theorem appIso_hom' (U) :
     (f.appIso U).hom = f.appLE (f ''ᵁ U) U (preimage_image_eq f U).ge :=
   f.appIso_hom U
 
+set_option backward.defeqAttrib.useBackward true in
+@[reassoc (attr := simp)]
+lemma appIso_hom_naturality {U V : X.Opens} (i : op U ⟶ op V) :
+    dsimp% Y.presheaf.map (f.opensFunctor.op.map i) ≫ (f.appIso V).hom =
+      (f.appIso U).hom ≫ X.presheaf.map i := by
+  simp [← cancel_mono (f.appIso V).inv]
+
 @[reassoc (attr := simp)]
 theorem app_appIso_inv (U) :
     f.app U ≫ (f.appIso (f ⁻¹ᵁ U)).inv =

Mathlib/CategoryTheory/Discrete/Basic.lean

@@ -6,6 +6,7 @@ Authors: Stephen Morgan, Kim Morrison, Floris van Doorn
 module
 
 public import Mathlib.CategoryTheory.Pi.Basic
+public import Mathlib.Data.Set.Image
 
 /-!
 # Discrete categories
@@ -63,6 +64,9 @@ def discreteEquiv {α : Type u₁} : Discrete α ≃ α where
   left_inv := by cat_disch
   right_inv := by cat_disch
 
+lemma Discrete.as_bijective {α : Type*} : (Discrete.as (α := α)).Bijective :=
+  discreteEquiv.bijective
+
 instance {α : Type u₁} [DecidableEq α] : DecidableEq (Discrete α) :=
   discreteEquiv.decidableEq
 
@@ -179,6 +183,10 @@ theorem functor_obj_eq_as {I : Type u₁} (F : I → C) (X : Discrete I) :
     (Discrete.functor F).obj X = F X.as :=
   rfl
 
+@[simp]
+lemma range_functor {I : Type*} (X : I → C) : Set.range (Discrete.functor X).obj = Set.range X := by
+  simp [Discrete.functor, Set.range_comp, Discrete.as_bijective.surjective.range_eq]
+
 @[ext]
 lemma functor_ext {I : Type u₁} {G F : Discrete I ⥤ C} (h : (i : I) → G.obj ⟨i⟩ = F.obj ⟨i⟩) :
     G = F := by

Mathlib/CategoryTheory/Limits/Preorder.lean

@@ -6,6 +6,7 @@ Authors: Sina Hazratpour, Joël Riou, Fernando Chu
 module
 
 public import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
+public import Mathlib.CategoryTheory.Limits.Shapes.Products
 public import Mathlib.Order.Bounds.Defs
 
 /-!
@@ -211,4 +212,18 @@ instance (priority := low) [SemilatticeSup C] : HasBinaryCoproducts C where
 
 end
 
+section
+
+/-- The product of elements in a complete lattice is the infimum. -/
+def isLimitIInf [CompleteLattice C] {ι : Type*} (X : ι → C) :
+    IsLimit (Fan.mk (⨅ i, X i) fun i : ι ↦ homOfLE (iInf_le X i)) :=
+  isLimitOfIsGLB _ _ (by simp [isGLB_iInf])
+
+/-- The coproduct of elements in a complete lattice is the supremum. -/
+def isColimitISup [CompleteLattice C] {ι : Type*} (X : ι → C) :
+    IsColimit (Cofan.mk (⨆ i, X i) fun i : ι ↦ homOfLE (le_iSup X i)) :=
+  isColimitOfIsLUB _ _ (by simp [isLUB_iSup])
+
+end
+
 end Preorder

Mathlib/CategoryTheory/Limits/Shapes/Products.lean

@@ -967,6 +967,27 @@ instance [HasColimit F] [HasCoproduct F.obj] : Epi (Sigma.desc (colimit.ι F)) w
 
 end
 
+section Thin
+
+variable [Quiver.IsThin C] {J : Type*} [Category* J] {K : J ⥤ C}
+
+/-- If `K : J ⥤ C` is a diagram with `C` thin, a cone for `K` is limiting
+if and only if the cone point is the product of the components. -/
+def isLimitEquivFanOfIsThin (c : Cone K) : IsLimit c ≃ IsLimit (Fan.mk c.pt c.π.app) where
+  toFun hc := Fan.IsLimit.mk _ (fun s ↦ hc.lift { pt := s.pt, π.app j := s.proj j })
+    (by subsingleton) (by subsingleton)
+  invFun h := { lift s := Fan.IsLimit.lift h s.π.app }
+
+/-- If `K : J ⥤ C` is a diagram with `C` thin, a cone for `K` is limiting
+if and only if the cone point is the product of the components. -/
+def isColimitEquivCofanOfIsThin (c : Cocone K) :
+    IsColimit c ≃ IsColimit (Cofan.mk c.pt c.ι.app) where
+  toFun hc := Cofan.IsColimit.mk _ (fun s ↦ hc.desc { pt := s.pt, ι.app j := s.inj j })
+    (by subsingleton) (by subsingleton)
+  invFun h := { desc s := Cofan.IsColimit.desc h s.ι.app }
+
+end Thin
+
 section Fubini
 
 variable {ι ι' : Type*} {X : ι → ι' → C}

Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean

@@ -943,6 +943,54 @@ lemma IsPushout.iff_app [HasPushouts D] {F₁ F₂ F₃ F₄ : C ⥤ D}
 
 end Functor
 
+section Thin
+
+variable [Quiver.IsThin C]
+
+lemma isPullback_iff_isLimit_binaryFan_of_isThin {P X Y Z : C}
+    {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} :
+    IsPullback fst snd f g ↔ Nonempty (IsLimit (BinaryFan.mk fst snd)) := by
+  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+  · exact ⟨BinaryFan.IsLimit.mk _ (fun u v ↦ h.lift u v (by subsingleton))
+      (by subsingleton) (by subsingleton) (by subsingleton)⟩
+  · exact ⟨⟨by subsingleton⟩,
+      ⟨PullbackCone.IsLimit.mk _ (fun s ↦ BinaryFan.IsLimit.lift h.some s.fst s.snd)
+      (by subsingleton) (by subsingleton) (by subsingleton)⟩⟩
+
+lemma isPushout_iff_isColimit_binaryCofan_of_isThin {P X Y Z : C}
+    {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} :
+    IsPushout f g inl inr ↔ Nonempty (IsColimit (BinaryCofan.mk inl inr)) := by
+  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+  · exact ⟨BinaryCofan.IsColimit.mk _ (fun u v ↦ h.desc u v (by subsingleton))
+      (by subsingleton) (by subsingleton) (by subsingleton)⟩
+  · exact ⟨⟨by subsingleton⟩,
+      ⟨PushoutCocone.IsColimit.mk _ (fun s ↦ BinaryCofan.IsColimit.desc h.some s.inl s.inr)
+      (by subsingleton) (by subsingleton) (by subsingleton)⟩⟩
+
+variable {D : Type*} [Category* D] [Quiver.IsThin D] (F : C ⥤ D)
+
+instance (priority := low) [PreservesLimitsOfShape (Discrete WalkingPair) F] :
+    PreservesLimitsOfShape WalkingCospan F := by
+  refine preservesLimitsOfShape_walkingCospan_of_forall_isPullback fun X Y Z f g hfg ↦ ?_
+  use pullback f g, pullback.fst f g, pullback.snd f g, .of_hasPullback f g
+  rw [isPullback_iff_isLimit_binaryFan_of_isThin]
+  refine ⟨(BinaryFan.mk (pullback.fst f g) (pullback.snd f g)).isLimitMapConeEquiv ?_⟩
+  apply isLimitOfPreserves _ (Nonempty.some ?_)
+  rw [← CategoryTheory.isPullback_iff_isLimit_binaryFan_of_isThin (f := f) (g := g)]
+  exact .of_hasPullback f g
+
+instance (priority := low) [PreservesColimitsOfShape (Discrete WalkingPair) F] :
+    PreservesColimitsOfShape WalkingSpan F := by
+  refine preservesColimitsOfShape_walkingCospan_of_forall_isPushout fun X Y Z f g hfg ↦ ?_
+  use pushout f g, pushout.inl f g, pushout.inr f g, .of_hasPushout f g
+  rw [isPushout_iff_isColimit_binaryCofan_of_isThin]
+  refine ⟨(BinaryCofan.mk (pushout.inl f g) (pushout.inr f g)).isColimitMapConeEquiv ?_⟩
+  apply isColimitOfPreserves _ (Nonempty.some ?_)
+  rw [← CategoryTheory.isPushout_iff_isColimit_binaryCofan_of_isThin (f := f) (g := g)]
+  exact .of_hasPushout f g
+
+end Thin
+
 section IsPullbackOverPullback
 
 open Limits

Mathlib/Topology/Category/TopCat/Opens.lean

@@ -7,6 +7,8 @@ module
 
 public import Mathlib.CategoryTheory.Category.GaloisConnection
 public import Mathlib.CategoryTheory.EqToHom
+public import Mathlib.CategoryTheory.Limits.Preorder
+public import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
 public import Mathlib.Topology.Category.TopCat.EpiMono
 public import Mathlib.Topology.Sets.Opens
 
@@ -341,6 +343,15 @@ lemma Topology.IsOpenEmbedding.functor_obj_injective {X Y : TopCat.{u}} {f : X 
     (hf : IsOpenEmbedding f) : Function.Injective hf.functor.obj :=
   fun _ _ e ↦ Opens.ext (Set.image_injective.mpr hf.injective (congr_arg (↑· : Opens Y → Set Y) e))
 
+lemma Topology.IsOpenEmbedding.functor_obj_iInf {X Y : TopCat.{u}} (f : X ⟶ Y)
+    (hf : Topology.IsOpenEmbedding f) {ι : Type*} [Nonempty ι] [Finite ι]
+    (g : ι → TopologicalSpace.Opens X) :
+    hf.functor.obj (⨅ i, g i) = ⨅ i, hf.functor.obj (g i) := by
+  ext : 1
+  simp only [IsOpenMap.coe_functor_obj, TopologicalSpace.Opens.coe_iInf]
+  rw [Set.InjOn.image_iInter_eq]
+  exact hf.injective.injOn
+
 namespace Topology.IsInducing
 
 /-- Given an inducing map `X ⟶ Y` and some `U : Opens X`, this is the union of all open sets
@@ -463,4 +474,15 @@ theorem adjunction_counit_map_functor {X : TopCat.{u}} {U : Opens X} (V : Opens
       eqToHom (by dsimp; rw [map_functor_eq V]) := by
   subsingleton
 
+open Limits in
+instance {X Y : TopCat.{u}} (f : X ⟶ Y) (hf : Topology.IsOpenEmbedding f) {ι : Type*}
+    [Nonempty ι] [Finite ι] :
+    PreservesLimitsOfShape (Discrete ι) hf.functor := by
+  apply +allowSynthFailures preservesLimitsOfShape_of_discrete
+  intro g
+  refine preservesLimit_of_preserves_limit_cone (Preorder.isLimitIInf g) ?_
+  refine (Limits.Fan.isLimitMapConeEquiv _ _ _).symm (Preorder.isLimitOfIsGLB _ _ ?_)
+  simp only [Discrete.range_functor, homOfLE_leOfHom, Fan.mk_pt, hf.functor_obj_iInf]
+  apply isGLB_iInf
+
 end TopologicalSpace.Opens

Mathlib/Topology/Sets/Opens.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Mario Carneiro, Floris van Doorn
 -/
 module
 
+public import Mathlib.Data.Fintype.Option
 public import Mathlib.Order.Hom.CompleteLattice
 public import Mathlib.Topology.Compactness.Bases
 public import Mathlib.Topology.ContinuousMap.Basic
@@ -232,6 +233,13 @@ instance [Nonempty α] : Nontrivial (Opens α) where
 theorem coe_iSup {ι} (s : ι → Opens α) : ((⨆ i, s i : Opens α) : Set α) = ⋃ i, s i := by
   simp [iSup]
 
+lemma coe_iInf {ι : Type*} [Finite ι] (U : ι → TopologicalSpace.Opens α) :
+    (((⨅ i, U i) : Opens α) : Set α) = ⋂ i, U i := by
+  induction ι using Finite.induction_empty_option with
+  | of_equiv e ih => rw [← e.iInf_comp, ← e.surjective.iInter_comp, ih]
+  | h_empty => simp
+  | h_option ih => rw [iInf_option, Set.iInter_option, Opens.coe_inf, ih]
+
 theorem iSup_def {ι} (s : ι → Opens α) : ⨆ i, s i = ⟨⋃ i, s i, isOpen_iUnion fun i => (s i).2⟩ :=
   ext <| coe_iSup s