feat(CategoryTheory): Limits in Subobject X (#29766)

Adds limits to `Subobject X`. Together with #29253, this will show existence of glbs in the poset of subobjects.

Co-authored-by: Christian Merten [c.j.merten@uu.nl](mailto:c.j.merten@uu.nl)

Author: FernandoChu

Mathlib/CategoryTheory/Subobject/Basic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta, Kim Morrison
 -/
+import Mathlib.CategoryTheory.Limits.Skeleton
 import Mathlib.CategoryTheory.Subobject.MonoOver
 import Mathlib.CategoryTheory.Skeletal
 import Mathlib.CategoryTheory.ConcreteCategory.Basic
@@ -69,7 +70,7 @@ In fact, in an abelian category (I'm not sure in what generality beyond that),
 -/
 
 
-universe v₁ v₂ u₁ u₂
+universe w' w v₁ v₂ v₃ u₁ u₂ u₃
 
 noncomputable section
 
@@ -516,6 +517,23 @@ def lowerEquivalence {A : C} {B : D} (e : MonoOver A ≌ MonoOver B) : Subobject
     · exact (ThinSkeleton.map_comp_eq _ _).symm
     · exact ThinSkeleton.map_id_eq.symm
 
+section Limits
+
+variable {J : Type u₃} [Category.{v₃} J]
+
+instance hasLimitsOfShape [HasLimitsOfShape J (Over X)] :
+    HasLimitsOfShape J (Subobject X) := by
+  apply hasLimitsOfShape_thinSkeleton
+
+instance hasFiniteLimits [HasFiniteLimits (Over X)] : HasFiniteLimits (Subobject X) where
+  out _ _ _ := by infer_instance
+
+instance hasLimitsOfSize [HasLimitsOfSize.{w, w'} (Over X)] :
+    HasLimitsOfSize.{w, w'} (Subobject X) where
+  has_limits_of_shape _ _ := by infer_instance
+
+end Limits
+
 section Pullback
 
 variable [HasPullbacks C]

Mathlib/CategoryTheory/Subobject/Lattice.lean

@@ -310,8 +310,7 @@ theorem bot_arrow {B : C} : (⊥ : Subobject B).arrow = 0 :=
 theorem bot_factors_iff_zero {A B : C} (f : A ⟶ B) : (⊥ : Subobject B).Factors f ↔ f = 0 :=
   ⟨by
     rintro ⟨h, rfl⟩
-    simp only [MonoOver.bot_arrow_eq_zero, Functor.id_obj, Functor.const_obj_obj,
-      MonoOver.bot_left, comp_zero],
+    simp only [MonoOver.bot_arrow_eq_zero, MonoOver.bot_left, comp_zero],
    by
     rintro rfl
     exact ⟨0, by simp⟩⟩

Mathlib/CategoryTheory/Subobject/MonoOver.lean

@@ -6,9 +6,11 @@ Authors: Bhavik Mehta, Kim Morrison
 import Mathlib.CategoryTheory.Comma.Over.Pullback
 import Mathlib.CategoryTheory.Adjunction.Reflective
 import Mathlib.CategoryTheory.Adjunction.Restrict
+import Mathlib.CategoryTheory.Limits.FullSubcategory
 import Mathlib.CategoryTheory.Limits.Shapes.Images
 import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq
 import Mathlib.CategoryTheory.Functor.ReflectsIso.Basic
+import Mathlib.CategoryTheory.WithTerminal.Cone
 
 /-!
 # Monomorphisms over a fixed object
@@ -36,7 +38,7 @@ and was ported to mathlib by Kim Morrison.
 -/
 
 
-universe v₁ v₂ u₁ u₂
+universe w' w v₁ v₂ v₃ u₁ u₂ u₃
 
 noncomputable section
 
@@ -47,13 +49,17 @@ open CategoryTheory CategoryTheory.Category CategoryTheory.Limits CategoryTheory
 variable {C : Type u₁} [Category.{v₁} C] {X Y Z : C}
 variable {D : Type u₂} [Category.{v₂} D]
 
+/-- The object property in `Over X` of the structure morphism being a monomorphism. -/
+abbrev Over.isMono (X : C) : ObjectProperty (Over X) :=
+  fun f : Over X => Mono f.hom
+
 /-- The category of monomorphisms into `X` as a full subcategory of the over category.
 This isn't skeletal, so it's not a partial order.
 
 Later we define `Subobject X` as the quotient of this by isomorphisms.
 -/
 def MonoOver (X : C) :=
-  ObjectProperty.FullSubcategory fun f : Over X => Mono f.hom
+  ObjectProperty.FullSubcategory (Over.isMono X)
 
 instance (X : C) : Category (MonoOver X) :=
   ObjectProperty.FullSubcategory.category _
@@ -202,6 +208,35 @@ def slice {A : C} {f : Over A}
     MonoOver.liftComp _ _ _ _ ≪≫
       MonoOver.liftIso _ _ f.iteratedSliceEquiv.counitIso ≪≫ MonoOver.liftId
 
+section Limits
+
+variable {J : Type u₃} [Category.{v₃} J] (X : C)
+
+lemma closedUnderLimitsOfShape_isMono :
+    ClosedUnderLimitsOfShape J (Over.isMono X) := by
+  refine fun F _ hc p ↦ ⟨fun g h e ↦ ?_⟩
+  apply IsLimit.hom_ext <| WithTerminal.isLimitEquiv.invFun hc
+  intro j; cases j with
+  | of j => have := p j; rw [← cancel_mono ((F.obj j).hom)]; simpa
+  | star => exact e
+
+instance hasLimit (F : J ⥤ MonoOver X) [HasLimit (F ⋙ (Over.isMono X).ι)] :
+    HasLimit F := by
+  apply hasLimit_of_closedUnderLimits (closedUnderLimitsOfShape_isMono X)
+
+instance hasLimitsOfShape [HasLimitsOfShape J (Over X)] :
+    HasLimitsOfShape J (MonoOver X) := by
+  apply hasLimitsOfShape_of_closedUnderLimits (closedUnderLimitsOfShape_isMono X)
+
+instance hasFiniteLimits [HasFiniteLimits (Over X)] : HasFiniteLimits (MonoOver X) where
+  out _ _ _ := by apply hasLimitsOfShape X
+
+instance hasLimitsOfSize [HasLimitsOfSize.{w, w'} (Over X)] :
+    HasLimitsOfSize.{w, w'} (MonoOver X) where
+  has_limits_of_shape _ _ := by apply hasLimitsOfShape X
+
+end Limits
+
 section Pullback
 
 variable [HasPullbacks C]

Mathlib/CategoryTheory/Subpresheaf/Subobject.lean

@@ -32,7 +32,6 @@ noncomputable def equivalenceMonoOver : Subpresheaf F ≌ MonoOver F where
   inverse :=
     { obj X := Subpresheaf.range X.arrow
       map {X Y} f := homOfLE (by
-        dsimp
         rw [← MonoOver.w f]
         apply range_comp_le ) }
   unitIso := NatIso.ofComponents (fun A ↦ eqToIso (by simp))