feat(CategoryTheory/Limits/Comma): comma categories have finite (co)limits (leanprover-community#40896)

The original file proves the existence of limits and colimits in comma categories under suitable conditions, and prove that the forgetful functors from (co)structured arrows preserve (co)limits. This adds the specific instances for finite (co)limits.

Co-authored-by: morel <sophie.morel@ens-lyon.fr>

Author: smorel394

Mathlib/CategoryTheory/Limits/Comma.lean

@@ -10,6 +10,8 @@ public import Mathlib.CategoryTheory.Comma.Over.Basic
 public import Mathlib.CategoryTheory.Limits.Constructions.EpiMono
 public import Mathlib.CategoryTheory.Limits.Creates
 public import Mathlib.CategoryTheory.Limits.Unit
+public import Mathlib.CategoryTheory.Limits.Preserves.Finite
+public import Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
 
 /-!
 # Limits and colimits in comma categories
@@ -150,6 +152,10 @@ instance hasLimitsOfSize [HasLimitsOfSize.{w, w'} A] [HasLimitsOfSize.{w, w'} B]
     [PreservesLimitsOfSize.{w, w'} R] : HasLimitsOfSize.{w, w'} (Comma L R) :=
   ⟨fun _ _ => inferInstance⟩
 
+instance hasFiniteLimits [HasFiniteLimits A] [HasFiniteLimits B]
+    [PreservesFiniteLimits R] : HasFiniteLimits (Comma L R) where
+      out _ _ _ := inferInstance
+
 instance hasColimit (F : J ⥤ Comma L R) [HasColimit (F ⋙ fst L R)] [HasColimit (F ⋙ snd L R)]
     [PreservesColimit (F ⋙ fst L R) L] : HasColimit F :=
   HasColimit.mk ⟨_, coconeOfPreservesIsColimit _ (colimit.isColimit _) (colimit.isColimit _)⟩
@@ -161,6 +167,10 @@ instance hasColimitsOfSize [HasColimitsOfSize.{w, w'} A] [HasColimitsOfSize.{w,
     [PreservesColimitsOfSize.{w, w'} L] : HasColimitsOfSize.{w, w'} (Comma L R) :=
   ⟨fun _ _ => inferInstance⟩
 
+instance hasFiniteColimits [HasFiniteColimits A] [HasFiniteColimits B]
+    [PreservesFiniteColimits L] : HasFiniteColimits (Comma L R) where
+      out _ _ _ := inferInstance
+
 instance preservesColimitsOfShape_fst [HasColimitsOfShape J A] [HasColimitsOfShape J B]
     [PreservesColimitsOfShape J L] : PreservesColimitsOfShape J (Comma.fst L R) where
   preservesColimit :=
@@ -188,6 +198,9 @@ instance hasLimit (F : J ⥤ Arrow T) [i₁ : HasLimit (F ⋙ leftFunc)] [i₂ :
 
 instance hasLimitsOfShape [HasLimitsOfShape J T] : HasLimitsOfShape J (Arrow T) where
 
+instance hasFiniteLimits [HasFiniteLimits T] : HasFiniteLimits (Arrow T) where
+  out _ _ _ := inferInstance
+
 instance hasLimits [HasLimits T] : HasLimits (Arrow T) :=
   ⟨fun _ _ => inferInstance⟩
 
@@ -200,6 +213,9 @@ instance hasColimit (F : J ⥤ Arrow T) [i₁ : HasColimit (F ⋙ leftFunc)]
 
 instance hasColimitsOfShape [HasColimitsOfShape J T] : HasColimitsOfShape J (Arrow T) where
 
+instance hasFiniteColimits [HasFiniteColimits T] : HasFiniteColimits (Arrow T) where
+  out _ _ _ := inferInstance
+
 instance hasColimits [HasColimits T] : HasColimits (Arrow T) :=
   ⟨fun _ _ => inferInstance⟩
 
@@ -230,6 +246,10 @@ instance hasLimit [i₁ : HasLimit (F ⋙ proj X G)] [i₂ : PreservesLimit (F 
 instance hasLimitsOfShape [HasLimitsOfShape J A] [PreservesLimitsOfShape J G] :
     HasLimitsOfShape J (StructuredArrow X G) where
 
+instance hasFiniteLimits [HasFiniteLimits A] [PreservesFiniteLimits G] :
+    HasFiniteLimits (StructuredArrow X G) where
+      out _ _ _ := inferInstance
+
 instance hasLimitsOfSize [HasLimitsOfSize.{w, w'} A] [PreservesLimitsOfSize.{w, w'} G] :
     HasLimitsOfSize.{w, w'} (StructuredArrow X G) :=
   ⟨fun J hJ => by infer_instance⟩
@@ -246,6 +266,10 @@ noncomputable instance createsLimit [i : PreservesLimit (F ⋙ proj X G) G] :
 noncomputable instance createsLimitsOfShape [PreservesLimitsOfShape J G] :
     CreatesLimitsOfShape J (proj X G) where
 
+noncomputable instance createsFiniteLimits [PreservesFiniteLimits G] :
+    CreatesFiniteLimits (proj X G) where
+      createsFiniteLimits _ _ _ := inferInstance
+
 noncomputable instance createsLimitsOfSize [PreservesLimitsOfSize.{w, w'} G] :
     CreatesLimitsOfSize.{w, w'} (proj X G :) where
 
@@ -277,6 +301,10 @@ instance hasColimit [i₁ : HasColimit (F ⋙ proj G X)] [i₂ : PreservesColimi
 instance hasColimitsOfShape [HasColimitsOfShape J A] [PreservesColimitsOfShape J G] :
     HasColimitsOfShape J (CostructuredArrow G X) where
 
+instance hasFiniteColimits [HasFiniteColimits A] [PreservesFiniteColimits G] :
+    HasFiniteColimits (CostructuredArrow G X) where
+      out _ _ _ := inferInstance
+
 instance hasColimitsOfSize [HasColimitsOfSize.{w, w'} A] [PreservesColimitsOfSize.{w, w'} G] :
     HasColimitsOfSize.{w, w'} (CostructuredArrow G X) :=
   ⟨fun _ _ => inferInstance⟩
@@ -293,6 +321,10 @@ noncomputable instance createsColimit [i : PreservesColimit (F ⋙ proj G X) G]
 noncomputable instance createsColimitsOfShape [PreservesColimitsOfShape J G] :
     CreatesColimitsOfShape J (proj G X) where
 
+noncomputable instance createsFiniteColimits [PreservesFiniteColimits G] :
+    CreatesFiniteColimits (proj G X) where
+      createsFiniteColimits _ _ _ := inferInstance
+
 noncomputable instance createsColimitsOfSize [PreservesColimitsOfSize.{w, w'} G] :
     CreatesColimitsOfSize.{w, w'} (proj G X :) where