From 738f9b7270755f96c459d3fba57d00b044cca99a Mon Sep 17 00:00:00 2001 From: Christian Merten Date: Mon, 13 Apr 2026 19:22:00 +0200 Subject: [PATCH] limits under --- Mathlib/CategoryTheory/Limits/Comma.lean | 9 ++ .../Limits/Constructions/Over/Basic.lean | 14 +++- .../Limits/Constructions/Over/Connected.lean | 46 ++++++++++- Mathlib/CategoryTheory/Limits/Opposites.lean | 82 ++++++++++++++++++- 4 files changed, 147 insertions(+), 4 deletions(-) diff --git a/Mathlib/CategoryTheory/Limits/Comma.lean b/Mathlib/CategoryTheory/Limits/Comma.lean index 608ea1f9d9ab61..eb96984ed717f6 100644 --- 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 index dffa5d9d8e6c02..a7e4295e6cdf07 100644 --- 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 index be3afb7e07be3d..fc04268734e34b 100644 --- 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 index 0de70d2d51197b..c3e0cbc600ad75 100644 --- 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