feat(CategoryTheory): PreservesLimits instances for adjoint functors (#…

…9990)

This PR adds `PreservesColimits/PreservesLimits` instances for adjoint functors.



Co-authored-by: Markus Himmel <markus@himmel-villmar.de>

Mathlib/CategoryTheory/Adjunction/Limits.lean

@@ -30,13 +30,11 @@ the functor associating to each `Y` the cocones over `K` with cone point `G.obj
 
 open Opposite
 
-namespace CategoryTheory.Adjunction
+namespace CategoryTheory
 
-open CategoryTheory
+open Functor Limits
 
-open CategoryTheory.Functor
-
-open CategoryTheory.Limits
+namespace Adjunction
 
 universe v u v₁ v₂ v₀ u₁ u₂
 
@@ -343,4 +341,23 @@ def conesIso {J : Type u} [Category.{v} J] {K : J ⥤ D} :
       inv := conesIsoComponentInv adj X }
 #align category_theory.adjunction.cones_iso CategoryTheory.Adjunction.conesIso
 
-end CategoryTheory.Adjunction
+end Adjunction
+
+namespace Functor
+
+variable {J C D : Type*} [Category J] [Category C] [Category D]
+  (F : C ⥤ D)
+
+instance [IsLeftAdjoint F] : PreservesColimitsOfShape J F :=
+  (Adjunction.ofLeftAdjoint F).leftAdjointPreservesColimits.preservesColimitsOfShape
+
+instance [IsLeftAdjoint F] : PreservesColimits F where
+
+instance [IsRightAdjoint F] : PreservesLimitsOfShape J F :=
+  (Adjunction.ofRightAdjoint F).rightAdjointPreservesLimits.preservesLimitsOfShape
+
+instance [IsRightAdjoint F] : PreservesLimits F where
+
+end Functor
+
+end CategoryTheory

Mathlib/CategoryTheory/Closed/Ideal.lean

@@ -203,9 +203,6 @@ noncomputable def bijection (A B : C) (X : D) :
 
 theorem bijection_symm_apply_id (A B : C) :
     (bijection i A B _).symm (𝟙 _) = prodComparison _ _ _ := by
-  -- Porting note: added
-  have : PreservesLimits i := (Adjunction.ofRightAdjoint i).rightAdjointPreservesLimits
-  have := preservesSmallestLimitsOfPreservesLimits i
   dsimp [bijection]
   -- Porting note: added
   erw [homEquiv_symm_apply_eq, homEquiv_symm_apply_eq, homEquiv_apply_eq, homEquiv_apply_eq]
@@ -216,8 +213,7 @@ theorem bijection_symm_apply_id (A B : C) :
   dsimp only [Functor.comp_obj]
   rw [prod.comp_lift_assoc, prod.lift_snd, prod.lift_fst_assoc, prod.lift_fst_comp_snd_comp,
     ← Adjunction.eq_homEquiv_apply, Adjunction.homEquiv_unit, Iso.comp_inv_eq, assoc]
-  -- Porting note: rw became erw
-  erw [PreservesLimitPair.iso_hom i ((leftAdjoint i).obj A) ((leftAdjoint i).obj B)]
+  rw [PreservesLimitPair.iso_hom i ((leftAdjoint i).obj A) ((leftAdjoint i).obj B)]
   apply prod.hom_ext
   · rw [Limits.prod.map_fst, assoc, assoc, prodComparison_fst, ← i.map_comp, prodComparison_fst]
     apply (Adjunction.ofRightAdjoint i).unit.naturality

Mathlib/CategoryTheory/Sites/Subsheaf.lean

@@ -8,7 +8,6 @@ import Mathlib.CategoryTheory.Adjunction.Evaluation
 import Mathlib.Tactic.CategoryTheory.Elementwise
 import Mathlib.CategoryTheory.Adhesive
 import Mathlib.CategoryTheory.Sites.ConcreteSheafification
-import Mathlib.CategoryTheory.Limits.Preserves.Filtered
 
 #align_import category_theory.sites.subsheaf from "leanprover-community/mathlib"@"70fd9563a21e7b963887c9360bd29b2393e6225a"
 

Mathlib/Topology/Category/Profinite/CofilteredLimit.lean

@@ -36,11 +36,6 @@ universe u v
 
 variable {J : Type v} [SmallCategory J] [IsCofiltered J] {F : J ⥤ ProfiniteMax.{u, v}} (C : Cone F)
 
-noncomputable
-instance preserves_smaller_limits_toTopCat :
-    PreservesLimitsOfSize.{v, v} (toTopCat : ProfiniteMax.{v, u} ⥤ TopCatMax.{v, u}) :=
-  Limits.preservesLimitsOfSizeShrink.{v, max u v, v, max u v} _
-
 -- include hC
 -- Porting note: I just add `(hC : IsLimit C)` explicitly as a hypothesis to all the theorems
 
@@ -49,7 +44,6 @@ a clopen set in one of the terms in the limit.
 -/
 theorem exists_isClopen_of_cofiltered {U : Set C.pt} (hC : IsLimit C) (hU : IsClopen U) :
     ∃ (j : J) (V : Set (F.obj j)), IsClopen V ∧ U = C.π.app j ⁻¹' V := by
-  have := preserves_smaller_limits_toTopCat.{u, v}
   -- First, we have the topological basis of the cofiltered limit obtained by pulling back
   -- clopen sets from the factors in the limit. By continuity, all such sets are again clopen.
   have hB := TopCat.isTopologicalBasis_cofiltered_limit.{u, v} (F ⋙ Profinite.toTopCat)
@@ -218,7 +212,6 @@ set_option linter.uppercaseLean3 false in
 one of the components. -/
 theorem exists_locallyConstant {α : Type*} (hC : IsLimit C) (f : LocallyConstant C.pt α) :
     ∃ (j : J) (g : LocallyConstant (F.obj j) α), f = g.comap (C.π.app _) := by
-  have := preserves_smaller_limits_toTopCat.{u, v}
   let S := f.discreteQuotient
   let ff : S → α := f.lift
   cases isEmpty_or_nonempty S

Mathlib/Topology/Sheaves/LocallySurjective.lean

@@ -5,6 +5,7 @@ Authors: Sam van Gool, Jake Levinson
 -/
 import Mathlib.Topology.Sheaves.Presheaf
 import Mathlib.Topology.Sheaves.Stalks
+import Mathlib.CategoryTheory.Limits.Preserves.Filtered
 import Mathlib.CategoryTheory.Sites.Surjective
 
 #align_import topology.sheaves.locally_surjective from "leanprover-community/mathlib"@"fb7698eb37544cbb66292b68b40e54d001f8d1a9"