limits under

chrisflav · chrisflav · commit 738f9b727075 · 2026-04-13T19:22:00.000+02:00
diff --git a/Mathlib/CategoryTheory/Limits/Comma.lean b/Mathlib/CategoryTheory/Limits/Comma.lean
@@ -215,6 +215,9 @@ namespace StructuredArrow
 
 variable {X : T} {G : A ⥤ T} (F : J ⥤ StructuredArrow X G)
 
+instance [G.Faithful] [G.Full] {Y : A} : HasInitial (StructuredArrow (G.obj Y) G) :=
+  StructuredArrow.mkIdInitial.hasInitial
+
 set_option backward.isDefEq.respectTransparency false in
 instance hasLimit [i₁ : HasLimit (F ⋙ proj X G)] [i₂ : PreservesLimit (F ⋙ proj X G) G] :
     HasLimit F := by
@@ -307,4 +310,10 @@ instance {X : T} : HasTerminal (Over X) := CostructuredArrow.hasTerminal
 
 end Over
 
+namespace Under
+
+instance {X : T} : HasInitial (Under X) := Under.mkIdInitial.hasInitial
+
+end Under
+
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Limits/Constructions/Over/Basic.lean b/Mathlib/CategoryTheory/Limits/Constructions/Over/Basic.lean
@@ -48,4 +48,16 @@ instance hasLimits {B : C} [HasWidePullbacks.{w} C] : HasLimitsOfSize.{w, w} (Ov
   have := ConstructProducts.over_products_of_widePullbacks (B := B)
   apply has_limits_of_hasEqualizers_and_products
 
-end CategoryTheory.Over
+end Over
+
+namespace Under
+
+instance {B : C} [HasFiniteWidePushouts C] : HasFiniteColimits (Under B) := by
+  rw [← hasFiniteLimits_opposite_iff]
+  exact hasFiniteLimits_of_hasLimitsLimits_of_createsFiniteLimits (Over.opEquivOpUnder _).inverse
+
+instance {B : C} [HasWidePushouts.{w} C] : HasColimitsOfSize.{w, w} (Under B) := by
+  rw [← hasLimitsOfSize_opposite_iff]
+  exact hasLimits_of_hasLimits_createsLimits (Over.opEquivOpUnder _).inverse
+
+end CategoryTheory.Under
diff --git a/Mathlib/CategoryTheory/Limits/Constructions/Over/Connected.lean b/Mathlib/CategoryTheory/Limits/Constructions/Over/Connected.lean
@@ -5,7 +5,7 @@ Authors: Johan Commelin, Reid Barton, Bhavik Mehta
 -/
 module
 
-public import Mathlib.CategoryTheory.Limits.Creates
+public import Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
 public import Mathlib.CategoryTheory.Comma.Over.Basic
 public import Mathlib.CategoryTheory.IsConnected
 public import Mathlib.CategoryTheory.Filtered.Final
@@ -115,6 +115,29 @@ instance hasLimitsOfShape_of_isConnected {B : D} [IsConnected J] [HasLimitsOfSha
 
 end CostructuredArrow
 
+namespace StructuredArrow
+
+/-- The projection from `StructuredArrow K B` to `C` creates any connected colimit. -/
+instance [IsConnected J] {B : D} : CreatesColimitsOfShape J (StructuredArrow.proj B K) :=
+  letI : CreatesLimitsOfShape Jᵒᵖ (proj B K).op :=
+    inferInstanceAs <| CreatesLimitsOfShape Jᵒᵖ <|
+      (structuredArrowOpEquivalence K B).functor ⋙ CostructuredArrow.proj K.op (.op B)
+  createsColimitsOfShapeOfOp _ _
+
+set_option backward.isDefEq.respectTransparency false in
+/-- The forgetful functor from `StructuredArrow K B` preserves any connected colimit. -/
+instance [IsConnected J] {B : D} : PreservesColimitsOfShape J (StructuredArrow.proj B K) := by
+  have : PreservesLimitsOfShape Jᵒᵖ (proj B K).op :=
+    inferInstanceAs <| PreservesLimitsOfShape Jᵒᵖ <|
+      (structuredArrowOpEquivalence K B).functor ⋙ CostructuredArrow.proj K.op (.op B)
+  apply preservesColimitsOfShape_of_op
+
+instance {B : D} [IsConnected J] [HasColimitsOfShape J C] :
+    HasColimitsOfShape J (StructuredArrow B K) where
+  has_colimit F := hasColimit_of_created F (StructuredArrow.proj B K)
+
+end StructuredArrow
+
 namespace Over
 
 /-- The forgetful functor from the over category creates any connected limit. -/
@@ -160,4 +183,23 @@ def isLimitConePost [IsCofilteredOrEmpty J] {F : J ⥤ C} {c : Cone F} (i : J) (
   isLimitOfReflects (Over.forget _)
     ((Functor.Initial.isLimitWhiskerEquiv (Over.forget i) c).symm hc)
 
-end CategoryTheory.Over
+end Over
+
+namespace Under
+
+/-- The forgetful functor from the under category creates any connected limit. -/
+instance createsColimitsOfShapeForgetOfIsConnected [IsConnected J] {B : C} :
+    CreatesColimitsOfShape J (forget B) :=
+  inferInstanceAs <| CreatesColimitsOfShape J (StructuredArrow.proj _ _)
+
+/-- The forgetful functor from the under category preserves any connected limit. -/
+instance preservesColimitsOfShape_forget_of_isConnected [IsConnected J] {B : C} :
+    PreservesColimitsOfShape J (forget B) :=
+  inferInstanceAs <| PreservesColimitsOfShape J (StructuredArrow.proj _ _)
+
+/-- The under category has any connected limit which the original category has. -/
+instance hasColimitsOfShape_of_isConnected {B : C} [IsConnected J] [HasColimitsOfShape J C] :
+    HasColimitsOfShape J (Under B) where
+  has_colimit F := hasColimit_of_created F (forget B)
+
+end CategoryTheory.Under
diff --git a/Mathlib/CategoryTheory/Limits/Opposites.lean b/Mathlib/CategoryTheory/Limits/Opposites.lean
@@ -18,7 +18,7 @@ We construct limits and colimits in the opposite categories.
 @[expose] public section
 
 
-universe v₁ v₂ u₁ u₂
+universe w v₁ v₂ u₁ u₂
 
 noncomputable section
 
@@ -509,12 +509,26 @@ theorem hasColimits_of_hasLimits_op [HasLimitsOfSize.{v₂, u₂} Cᵒᵖ] :
     HasColimitsOfSize.{v₂, u₂} C :=
   { has_colimits_of_shape := fun _ _ => hasColimitsOfShape_of_hasLimitsOfShape_op }
 
+lemma hasColimitsOfSize_opposite_iff :
+    HasColimitsOfSize.{v₂, u₂} Cᵒᵖ ↔ HasLimitsOfSize.{v₂, u₂} C :=
+  ⟨fun _ ↦ hasLimits_of_hasColimits_op, fun _ ↦ inferInstance⟩
+
+lemma hasLimitsOfSize_opposite_iff :
+    HasLimitsOfSize.{v₂, u₂} Cᵒᵖ ↔ HasColimitsOfSize.{v₂, u₂} C :=
+  ⟨fun _ ↦ hasColimits_of_hasLimits_op, fun _ ↦ inferInstance⟩
+
 instance hasFiniteColimits_opposite [HasFiniteLimits C] : HasFiniteColimits Cᵒᵖ :=
   ⟨fun _ _ _ => hasColimitsOfShape_op_of_hasLimitsOfShape⟩
 
 instance hasFiniteLimits_opposite [HasFiniteColimits C] : HasFiniteLimits Cᵒᵖ :=
   ⟨fun _ _ _ => hasLimitsOfShape_op_of_hasColimitsOfShape⟩
 
+lemma hasFiniteLimits_opposite_iff : HasFiniteLimits Cᵒᵖ ↔ HasFiniteColimits C :=
+  ⟨fun _ ↦ ⟨fun _ _ _ ↦ hasColimitsOfShape_of_hasLimitsOfShape_op⟩, fun _ ↦ inferInstance⟩
+
+lemma hasFiniteColimits_opposite_iff : HasFiniteColimits Cᵒᵖ ↔ HasFiniteLimits C :=
+  ⟨fun _ ↦ ⟨fun _ _ _ ↦ hasLimitsOfShape_of_hasColimitsOfShape_op⟩, fun _ ↦ inferInstance⟩
+
 lemma hasColimit_op_iff_hasLimit {F : J ⥤ C} : HasColimit F.op ↔ HasLimit F :=
   ⟨fun _ ↦ hasLimit_of_hasColimit_op F, fun _ ↦ inferInstance⟩
 
@@ -533,4 +547,70 @@ lemma hasLimit_leftOp_iff_hasColimit {F : J ⥤ Cᵒᵖ} : HasLimit F.leftOp ↔
 lemma hasLimit_rightOp_iff_hasColimit {F : Jᵒᵖ ⥤ C} : HasLimit F.rightOp ↔ HasColimit F :=
   ⟨fun _ ↦ hasColimit_of_hasLimit_rightOp F, fun _ ↦ inferInstance⟩
 
+lemma hasLimitsOfShape_opposite_iff : HasLimitsOfShape J Cᵒᵖ ↔ HasColimitsOfShape Jᵒᵖ C := by
+  refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩
+  have : HasLimitsOfShape Jᵒᵖᵒᵖ Cᵒᵖ := hasLimitsOfShape_of_equivalence (opOpEquivalence J).symm
+  exact hasColimitsOfShape_of_hasLimitsOfShape_op
+
+lemma hasColimitsOfShape_opposite_iff : HasColimitsOfShape J Cᵒᵖ ↔ HasLimitsOfShape Jᵒᵖ C := by
+  refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩
+  have : HasColimitsOfShape Jᵒᵖᵒᵖ Cᵒᵖ := hasColimitsOfShape_of_equivalence (opOpEquivalence J).symm
+  exact hasLimitsOfShape_of_hasColimitsOfShape_op
+
+lemma hasLimitsOfShape_opposite_opposite_iff :
+    HasLimitsOfShape Jᵒᵖ Cᵒᵖ ↔ HasColimitsOfShape J C := by
+  refine ⟨fun _ ↦ hasColimitsOfShape_of_hasLimitsOfShape_op, fun _ ↦ ?_⟩
+  have : HasColimitsOfShape Jᵒᵖᵒᵖ C := hasColimitsOfShape_of_equivalence (opOpEquivalence J).symm
+  exact hasLimitsOfShape_op_of_hasColimitsOfShape
+
+lemma hasColimitsOfShape_opposite_opposite_iff :
+    HasColimitsOfShape Jᵒᵖ Cᵒᵖ ↔ HasLimitsOfShape J C := by
+  refine ⟨fun _ ↦ hasLimitsOfShape_of_hasColimitsOfShape_op, fun _ ↦ ?_⟩
+  have : HasLimitsOfShape Jᵒᵖᵒᵖ C := hasLimitsOfShape_of_equivalence (opOpEquivalence J).symm
+  exact hasColimitsOfShape_op_of_hasLimitsOfShape
+
+instance [HasWidePullbacks.{w} C] : HasWidePushouts.{w} Cᵒᵖ := by
+  intro ι
+  rw [hasColimitsOfShape_opposite_iff]
+  exact hasLimitsOfShape_of_equivalence (widePushoutShapeOpEquiv _).symm
+
+instance [HasWidePushouts.{w} C] : HasWidePullbacks.{w} Cᵒᵖ := by
+  intro ι
+  rw [hasLimitsOfShape_opposite_iff]
+  exact hasColimitsOfShape_of_equivalence (widePullbackShapeOpEquiv _).symm
+
+lemma hasWidePullbacks_opposite_iff :
+    HasWidePullbacks.{w} Cᵒᵖ ↔ HasWidePushouts.{w} C := by
+  refine ⟨fun h ι ↦ ?_, fun _ ↦ inferInstance⟩
+  rw [← hasLimitsOfShape_opposite_opposite_iff]
+  exact hasLimitsOfShape_of_equivalence (widePushoutShapeOpEquiv _).symm
+
+lemma hasWidePushouts_opposite_iff :
+    HasWidePushouts.{w} Cᵒᵖ ↔ HasWidePullbacks.{w} C := by
+  refine ⟨fun h ι ↦ ?_, fun _ ↦ inferInstance⟩
+  rw [← hasColimitsOfShape_opposite_opposite_iff]
+  exact hasColimitsOfShape_of_equivalence (widePullbackShapeOpEquiv _).symm
+
+instance [HasFiniteWidePullbacks C] : HasFiniteWidePushouts Cᵒᵖ := by
+  refine ⟨fun J _ ↦ ?_⟩
+  rw [hasColimitsOfShape_opposite_iff]
+  exact hasLimitsOfShape_of_equivalence (widePushoutShapeOpEquiv _).symm
+
+instance [HasFiniteWidePushouts C] : HasFiniteWidePullbacks Cᵒᵖ := by
+  refine ⟨fun J _ ↦ ?_⟩
+  rw [hasLimitsOfShape_opposite_iff]
+  exact hasColimitsOfShape_of_equivalence (widePullbackShapeOpEquiv _).symm
+
+lemma hasFiniteWidePullbacks_opposite_iff :
+    HasFiniteWidePullbacks Cᵒᵖ ↔ HasFiniteWidePushouts C := by
+  refine ⟨fun h ↦ ⟨fun J _ ↦ ?_⟩, fun _ ↦ inferInstance⟩
+  rw [← hasLimitsOfShape_opposite_opposite_iff]
+  exact hasLimitsOfShape_of_equivalence (widePushoutShapeOpEquiv _).symm
+
+lemma hasFiniteWidePushouts_opposite_iff :
+    HasFiniteWidePushouts Cᵒᵖ ↔ HasFiniteWidePullbacks C := by
+  refine ⟨fun h ↦ ⟨fun J _ ↦ ?_⟩, fun _ ↦ inferInstance⟩
+  rw [← hasColimitsOfShape_opposite_opposite_iff]
+  exact hasColimitsOfShape_of_equivalence (widePullbackShapeOpEquiv _).symm
+
 end CategoryTheory.Limits
