Trigger CI for leanprover-community/batteries#1099

Mathlib.lean

@@ -1954,6 +1954,7 @@ import Mathlib.CategoryTheory.Limits.Over
 import Mathlib.CategoryTheory.Limits.Pi
 import Mathlib.CategoryTheory.Limits.Preorder
 import Mathlib.CategoryTheory.Limits.Preserves.Basic
+import Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
 import Mathlib.CategoryTheory.Limits.Preserves.Filtered
 import Mathlib.CategoryTheory.Limits.Preserves.Finite
 import Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory

Mathlib/CategoryTheory/Limits/Creates.lean

@@ -20,7 +20,7 @@ noncomputable section
 
 namespace CategoryTheory
 
-universe w' w v₁ v₂ v₃ u₁ u₂ u₃
+universe w' w'₁ w w₁ v₁ v₂ v₃ u₁ u₂ u₃
 
 variable {C : Type u₁} [Category.{v₁} C]
 
@@ -529,6 +529,19 @@ def createsLimitsOfNatIso {F G : C ⥤ D} (h : F ≅ G) [CreatesLimitsOfSize.{w,
     CreatesLimitsOfSize.{w, w'} G where
   CreatesLimitsOfShape := createsLimitsOfShapeOfNatIso h
 
+/-- If `F` creates limits of shape `J` and `J ≌ J'`, then `F` creates limits of shape `J'`. -/
+def createsLimitsOfShapeOfEquiv {J' : Type w₁} [Category.{w'₁} J'] (e : J ≌ J') (F : C ⥤ D)
+    [CreatesLimitsOfShape J F] : CreatesLimitsOfShape J' F where
+  CreatesLimit {K} :=
+    { lifts c hc := by
+        refine ⟨(Cones.whiskeringEquivalence e).inverse.obj
+          (liftLimit (hc.whiskerEquivalence e)), ?_⟩
+        letI inner := (Cones.whiskeringEquivalence (F := K ⋙ F) e).inverse.mapIso
+          (liftedLimitMapsToOriginal (K := e.functor ⋙ K) (hc.whiskerEquivalence e))
+        refine ?_ ≪≫ inner ≪≫ ((Cones.whiskeringEquivalence e).unitIso.app c).symm
+        exact Cones.ext (Iso.refl _)
+      toReflectsLimit := have := reflectsLimitsOfShape_of_equiv e F; inferInstance }
+
 /-- Transfer creation of colimits along a natural isomorphism in the diagram. -/
 def createsColimitOfIsoDiagram {K₁ K₂ : J ⥤ C} (F : C ⥤ D) (h : K₁ ≅ K₂) [CreatesColimit K₁ F] :
     CreatesColimit K₂ F :=
@@ -564,6 +577,19 @@ def createsColimitsOfNatIso {F G : C ⥤ D} (h : F ≅ G) [CreatesColimitsOfSize
     CreatesColimitsOfSize.{w, w'} G where
   CreatesColimitsOfShape := createsColimitsOfShapeOfNatIso h
 
+/-- If `F` creates colimits of shape `J` and `J ≌ J'`, then `F` creates colimits of shape `J'`. -/
+def createsColimitsOfShapeOfEquiv {J' : Type w₁} [Category.{w'₁} J'] (e : J ≌ J') (F : C ⥤ D)
+    [CreatesColimitsOfShape J F] : CreatesColimitsOfShape J' F where
+  CreatesColimit {K} :=
+    { lifts c hc := by
+        refine ⟨(Cocones.whiskeringEquivalence e).inverse.obj
+          (liftColimit (hc.whiskerEquivalence e)), ?_⟩
+        letI inner := (Cocones.whiskeringEquivalence (F := K ⋙ F) e).inverse.mapIso
+          (liftedColimitMapsToOriginal (K := e.functor ⋙ K) (hc.whiskerEquivalence e))
+        refine ?_ ≪≫ inner ≪≫ ((Cocones.whiskeringEquivalence e).unitIso.app c).symm
+        exact Cocones.ext (Iso.refl _)
+      toReflectsColimit := have := reflectsColimitsOfShape_of_equiv e F; inferInstance }
+
 -- For the inhabited linter later.
 /-- If F creates the limit of K, any cone lifts to a limit. -/
 def liftsToLimitOfCreates (K : J ⥤ C) (F : C ⥤ D) [CreatesLimit K F] (c : Cone (K ⋙ F))

Mathlib/CategoryTheory/Limits/Preserves/Creates/Finite.lean

@@ -0,0 +1,185 @@
+/-
+Copyright (c) 2025 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import Mathlib.CategoryTheory.Limits.Creates
+import Mathlib.CategoryTheory.FinCategory.AsType
+
+/-!
+# Creation of finite limits
+
+This file defines the classes `CreatesFiniteLimits`, `CreatesFiniteColimits`,
+`CreatesFiniteProducts` and `CreatesFiniteCoproducts`.
+-/
+
+namespace CategoryTheory.Limits
+
+
+universe w w' v₁ v₂ v₃ u₁ u₂ u₃
+
+variable {C : Type u₁} [Category.{v₁} C]
+variable {D : Type u₂} [Category.{v₂} D]
+variable {E : Type u₃} [Category.{v₃} E]
+
+/-- We say that a functor creates finite limits if it creates all limits of shape `J` where
+`J : Type` is a finite category. -/
+class CreatesFiniteLimits (F : C ⥤ D) where
+  /-- `F` creates all finite limits. -/
+  createsFiniteLimits :
+    ∀ (J : Type) [SmallCategory J] [FinCategory J], CreatesLimitsOfShape J F := by infer_instance
+
+attribute [instance] CreatesFiniteLimits.createsFiniteLimits
+
+noncomputable section
+
+instance (priority := 100) createsLimitsOfShapeOfCreatesFiniteLimits (F : C ⥤ D)
+    [CreatesFiniteLimits F] (J : Type w) [SmallCategory J] [FinCategory J] :
+    CreatesLimitsOfShape J F :=
+  createsLimitsOfShapeOfEquiv (FinCategory.equivAsType J) _
+
+-- Cannot be an instance because of unbound universe variables.
+/-- If `F` creates limits of any size, it creates finite limits. -/
+def CreatesLimitsOfSize.createsFiniteLimits (F : C ⥤ D)
+    [CreatesLimitsOfSize.{w, w'} F] : CreatesFiniteLimits F where
+  createsFiniteLimits J _ _ := createsLimitsOfShapeOfEquiv
+    ((ShrinkHoms.equivalence.{w} J).trans (Shrink.equivalence.{w'} _)).symm _
+
+instance (priority := 120) CreatesLimitsOfSize0.createsFiniteLimits (F : C ⥤ D)
+    [CreatesLimitsOfSize.{0, 0} F] : CreatesFiniteLimits F :=
+  CreatesLimitsOfSize.createsFiniteLimits F
+
+instance (priority := 100) CreatesLimits.createsFiniteLimits (F : C ⥤ D)
+    [CreatesLimits F] : CreatesFiniteLimits F :=
+  CreatesLimitsOfSize.createsFiniteLimits F
+
+/-- If `F` creates finite limits in any universe, then it creates finite limits. -/
+def createsFiniteLimitsOfCreatesFiniteLimitsOfSize (F : C ⥤ D)
+    (h : ∀ (J : Type w) {_ : SmallCategory J} (_ : FinCategory J), CreatesLimitsOfShape J F) :
+    CreatesFiniteLimits F where
+  createsFiniteLimits J _ _ :=
+    haveI := h (ULiftHom (ULift J)) CategoryTheory.finCategoryUlift
+    createsLimitsOfShapeOfEquiv (ULiftHomULiftCategory.equiv J).symm _
+
+instance compCreatesFiniteLimits (F : C ⥤ D) (G : D ⥤ E) [CreatesFiniteLimits F]
+    [CreatesFiniteLimits G] : CreatesFiniteLimits (F ⋙ G) where
+  createsFiniteLimits _ _ _ := compCreatesLimitsOfShape F G
+
+/-- Transfer creation of finite limits along a natural isomorphism in the functor. -/
+def createsFiniteLimitsOfNatIso {F G : C ⥤ D} {h : F ≅ G} [CreatesFiniteLimits F] :
+    CreatesFiniteLimits G where
+  createsFiniteLimits _ _ _ := createsLimitsOfShapeOfNatIso h
+
+end
+
+/-- We say that a functor creates finite products if it creates all limits of shape `Discrete J`
+where `J : Type` is finite. -/
+class CreatesFiniteProducts (F : C ⥤ D) where
+  /-- `F` creates all finite limits. -/
+  creates :
+    ∀ (J : Type) [Fintype J], CreatesLimitsOfShape (Discrete J) F := by infer_instance
+
+attribute [instance] CreatesFiniteProducts.creates
+
+noncomputable section
+
+instance (priority := 100) createsLimitsOfShapeOfCreatesFiniteProducts (F : C ⥤ D)
+    [CreatesFiniteProducts F] (J : Type w) [Finite J] : CreatesLimitsOfShape (Discrete J) F :=
+  createsLimitsOfShapeOfEquiv
+    (Discrete.equivalence (Finite.exists_equiv_fin J).choose_spec.some.symm) F
+
+instance compCreatesFiniteProducts (F : C ⥤ D) (G : D ⥤ E) [CreatesFiniteProducts F]
+    [CreatesFiniteProducts G] : CreatesFiniteProducts (F ⋙ G) where
+  creates _ _ := compCreatesLimitsOfShape _ _
+
+/-- Transfer creation of finite products along a natural isomorphism in the functor. -/
+def createsFiniteProductsOfNatIso {F G : C ⥤ D} {h : F ≅ G} [CreatesFiniteProducts F] :
+    CreatesFiniteProducts G where
+  creates _ _ := createsLimitsOfShapeOfNatIso h
+
+instance (F : C ⥤ D) [CreatesFiniteLimits F] : CreatesFiniteProducts F where
+  creates _ _ := inferInstance
+
+end
+
+/-- We say that a functor creates finite colimits if it creates all colimits of shape `J` where
+`J : Type` is a finite category. -/
+class CreatesFiniteColimits (F : C ⥤ D) where
+  /-- `F` creates all finite colimits. -/
+  createsFiniteColimits :
+    ∀ (J : Type) [SmallCategory J] [FinCategory J], CreatesColimitsOfShape J F := by infer_instance
+
+attribute [instance] CreatesFiniteColimits.createsFiniteColimits
+
+noncomputable section
+
+instance (priority := 100) createsColimitsOfShapeOfCreatesFiniteColimits (F : C ⥤ D)
+    [CreatesFiniteColimits F] (J : Type w) [SmallCategory J] [FinCategory J] :
+    CreatesColimitsOfShape J F :=
+  createsColimitsOfShapeOfEquiv (FinCategory.equivAsType J) _
+
+-- Cannot be an instance because of unbound universe variables.
+/-- If `F` creates colimits of any size, it creates finite colimits. -/
+def CreatesColimitsOfSize.createsFiniteColimits (F : C ⥤ D)
+    [CreatesColimitsOfSize.{w, w'} F] : CreatesFiniteColimits F where
+  createsFiniteColimits J _ _ := createsColimitsOfShapeOfEquiv
+    ((ShrinkHoms.equivalence.{w} J).trans (Shrink.equivalence.{w'} _)).symm _
+
+instance (priority := 120) CreatesColimitsOfSize0.createsFiniteColimits (F : C ⥤ D)
+    [CreatesColimitsOfSize.{0, 0} F] : CreatesFiniteColimits F :=
+  CreatesColimitsOfSize.createsFiniteColimits F
+
+instance (priority := 100) CreatesColimits.createsFiniteColimits (F : C ⥤ D)
+    [CreatesColimits F] : CreatesFiniteColimits F :=
+  CreatesColimitsOfSize.createsFiniteColimits F
+
+/-- If `F` creates finite colimits in any universe, then it creates finite colimits. -/
+def createsFiniteColimitsOfCreatesFiniteColimitsOfSize (F : C ⥤ D)
+    (h : ∀ (J : Type w) {_ : SmallCategory J} (_ : FinCategory J), CreatesColimitsOfShape J F) :
+    CreatesFiniteColimits F where
+  createsFiniteColimits J _ _ :=
+    haveI := h (ULiftHom (ULift J)) CategoryTheory.finCategoryUlift
+    createsColimitsOfShapeOfEquiv (ULiftHomULiftCategory.equiv J).symm _
+
+instance compCreatesFiniteColimits (F : C ⥤ D) (G : D ⥤ E) [CreatesFiniteColimits F]
+    [CreatesFiniteColimits G] : CreatesFiniteColimits (F ⋙ G) where
+  createsFiniteColimits _ _ _ := compCreatesColimitsOfShape F G
+
+/-- Transfer creation of finite colimits along a natural isomorphism in the functor. -/
+def createsFiniteColimitsOfNatIso {F G : C ⥤ D} {h : F ≅ G} [CreatesFiniteColimits F] :
+    CreatesFiniteColimits G where
+  createsFiniteColimits _ _ _ := createsColimitsOfShapeOfNatIso h
+
+end
+
+/-- We say that a functor creates finite limits if it creates all limits of shape `J` where
+`J : Type` is a finite category. -/
+class CreatesFiniteCoproducts (F : C ⥤ D) where
+  /-- `F` creates all finite limits. -/
+  creates :
+    ∀ (J : Type) [Fintype J], CreatesColimitsOfShape (Discrete J) F := by infer_instance
+
+attribute [instance] CreatesFiniteCoproducts.creates
+
+noncomputable section
+
+instance (priority := 100) createsColimitsOfShapeOfCreatesFiniteProducts (F : C ⥤ D)
+    [CreatesFiniteCoproducts F] (J : Type w) [Finite J] : CreatesColimitsOfShape (Discrete J) F :=
+  createsColimitsOfShapeOfEquiv
+    (Discrete.equivalence (Finite.exists_equiv_fin J).choose_spec.some.symm) F
+
+instance compCreatesFiniteCoproducts (F : C ⥤ D) (G : D ⥤ E) [CreatesFiniteCoproducts F]
+    [CreatesFiniteCoproducts G] : CreatesFiniteCoproducts (F ⋙ G) where
+  creates _ _ := compCreatesColimitsOfShape _ _
+
+/-- Transfer creation of finite limits along a natural isomorphism in the functor. -/
+def createsFiniteCoproductsOfNatIso {F G : C ⥤ D} {h : F ≅ G} [CreatesFiniteCoproducts F] :
+    CreatesFiniteCoproducts G where
+  creates _ _ := createsColimitsOfShapeOfNatIso h
+
+instance (F : C ⥤ D) [CreatesFiniteColimits F] : CreatesFiniteCoproducts F where
+  creates _ _ := inferInstance
+
+end
+
+end CategoryTheory.Limits

lake-manifest.json

@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c0862d0fe923069cf0e544cd5d13c5222e6fa93f",
+   "rev": "4d5ece38d480adedff34d632a4bc0ebeb9dad9de",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "fin-find",