chore(CategoryTheory): make MorphismProperty.IsStableUnderColimitsOfShape a class (#24773)

Author: joelriou

Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Colim.lean

@@ -138,18 +138,16 @@ open Limits
 open MorphismProperty
 
 variable (J C) in
-lemma isStableUnderColimitsOfShape_monomorphisms
+instance isStableUnderColimitsOfShape_monomorphisms
     [HasColimitsOfShape J C] [(colim : (J ⥤ C) ⥤ C).PreservesMonomorphisms] :
-    (monomorphisms C).IsStableUnderColimitsOfShape J := by
-  intro X₁ X₂ c₁ c₂ hc₁ hc₂ f hf
-  have (j : J) : Mono (f.app j) := hf _
-  have := NatTrans.mono_of_mono_app f
-  exact colim.map_mono' f hc₁ hc₂ _ (by simp)
+    (monomorphisms C).IsStableUnderColimitsOfShape J where
+  condition X₁ X₂ c₁ c₂ hc₁ hc₂ f hf φ hφ := by
+    have (j : J) : Mono (f.app j) := hf _
+    have := NatTrans.mono_of_mono_app f
+    apply colim.map_mono' f hc₁ hc₂ φ (by simp [hφ])
 
 instance [HasCoproducts.{u'} C] [AB4OfSize.{u'} C] :
     IsStableUnderCoproducts.{u'} (monomorphisms C) where
-  isStableUnderCoproductsOfShape _ :=
-    isStableUnderColimitsOfShape_monomorphisms _ _
 
 end MorphismProperty
 

Mathlib/CategoryTheory/Localization/FiniteProducts.lean

@@ -28,30 +28,28 @@ open Limits
 namespace Localization
 
 variable {C : Type u₁} {D : Type u₂} [Category.{v₁} C] [Category.{v₂} D] (L : C ⥤ D)
-  {W : MorphismProperty C} [L.IsLocalization W]
+  (W : MorphismProperty C) [L.IsLocalization W]
 
 namespace HasProductsOfShapeAux
 
-variable {J : Type} [HasProductsOfShape J C]
-  (hW : W.IsStableUnderProductsOfShape J)
-include hW
+variable (J : Type) [HasProductsOfShape J C] [W.IsStableUnderProductsOfShape J]
 
 lemma inverts :
     (W.functorCategory (Discrete J)).IsInvertedBy (lim ⋙ L) :=
-  fun _ _ f hf => Localization.inverts L W _ (hW.limMap f hf)
+  fun _ _ f hf => Localization.inverts L W _ (MorphismProperty.limMap f hf)
 
 variable [W.ContainsIdentities] [Finite J]
 
 /-- The (candidate) limit functor for the localized category.
 It is induced by `lim ⋙ L : (Discrete J ⥤ C) ⥤ D`. -/
 noncomputable abbrev limitFunctor :
     (Discrete J ⥤ D) ⥤ D :=
-  Localization.lift _ (inverts L hW)
+  Localization.lift _ (inverts L W J)
     ((whiskeringRight (Discrete J) C D).obj L)
 
-/-- The functor `limitFunctor L hW` is induced by `lim ⋙ L`. -/
+/-- The functor `limitFunctor L W J` is induced by `lim ⋙ L`. -/
 noncomputable def compLimitFunctorIso :
-    ((whiskeringRight (Discrete J) C D).obj L) ⋙ limitFunctor L hW ≅
+    ((whiskeringRight (Discrete J) C D).obj L) ⋙ limitFunctor L W J ≅
       lim ⋙ L := by
   apply Localization.fac
 
@@ -61,56 +59,54 @@ instance :
   iso' := (Functor.compConstIso _ _).symm
 
 noncomputable instance :
-    CatCommSq lim ((whiskeringRight (Discrete J) C D).obj L) L (limitFunctor L hW) where
-  iso' := (compLimitFunctorIso L hW).symm
+    CatCommSq lim ((whiskeringRight (Discrete J) C D).obj L) L (limitFunctor L W J) where
+  iso' := (compLimitFunctorIso L W J).symm
 
 /-- The adjunction between the constant functor `D ⥤ (Discrete J ⥤ D)`
-and `limitFunctor L hW`. -/
+and `limitFunctor L W J`. -/
 noncomputable def adj :
-    Functor.const _ ⊣ limitFunctor L hW :=
+    Functor.const _ ⊣ limitFunctor L W J :=
   constLimAdj.localization L W ((whiskeringRight (Discrete J) C D).obj L)
-    (W.functorCategory (Discrete J)) (Functor.const _) (limitFunctor L hW)
+    (W.functorCategory (Discrete J)) (Functor.const _) (limitFunctor L W J)
 
 lemma adj_counit_app (F : Discrete J ⥤ C) :
-    (adj L hW).counit.app (F ⋙ L) =
-      (Functor.const (Discrete J)).map ((compLimitFunctorIso L hW).hom.app F) ≫
+    (adj L W J).counit.app (F ⋙ L) =
+      (Functor.const (Discrete J)).map ((compLimitFunctorIso L W J).hom.app F) ≫
         (Functor.compConstIso (Discrete J) L).hom.app (lim.obj F) ≫
         whiskerRight (constLimAdj.counit.app F) L := by
   apply constLimAdj.localization_counit_app
 
 /-- Auxiliary definition for `Localization.preservesProductsOfShape`. -/
 noncomputable def isLimitMapCone (F : Discrete J ⥤ C) :
     IsLimit (L.mapCone (limit.cone F)) :=
-  IsLimit.ofIsoLimit (isLimitConeOfAdj (adj L hW) (F ⋙ L))
-    (Cones.ext ((compLimitFunctorIso L hW).app F) (by simp [adj_counit_app, constLimAdj]))
+  IsLimit.ofIsoLimit (isLimitConeOfAdj (adj L W J) (F ⋙ L))
+    (Cones.ext ((compLimitFunctorIso L W J).app F) (by simp [adj_counit_app, constLimAdj]))
 
 end HasProductsOfShapeAux
 
-variable (W)
 variable [W.ContainsIdentities]
 
 include L
 lemma hasProductsOfShape (J : Type) [Finite J] [HasProductsOfShape J C]
-    (hW : W.IsStableUnderProductsOfShape J) :
+    [W.IsStableUnderProductsOfShape J] :
     HasProductsOfShape J D :=
   hasLimitsOfShape_iff_isLeftAdjoint_const.2
-    (HasProductsOfShapeAux.adj L hW).isLeftAdjoint
+    (HasProductsOfShapeAux.adj L W J).isLeftAdjoint
 
 /-- When `C` has finite products indexed by `J`, `W : MorphismProperty C` contains
 identities and is stable by products indexed by `J`,
 then any localization functor for `W` preserves finite products indexed by `J`. -/
 lemma preservesProductsOfShape (J : Type) [Finite J]
-    [HasProductsOfShape J C] (hW : W.IsStableUnderProductsOfShape J) :
+    [HasProductsOfShape J C] [W.IsStableUnderProductsOfShape J] :
     PreservesLimitsOfShape (Discrete J) L where
   preservesLimit {F} := preservesLimit_of_preserves_limit_cone (limit.isLimit F)
-    (HasProductsOfShapeAux.isLimitMapCone L hW F)
+    (HasProductsOfShapeAux.isLimitMapCone L W J F)
 
 variable [HasFiniteProducts C] [W.IsStableUnderFiniteProducts]
 
 include W in
 lemma hasFiniteProducts : HasFiniteProducts D :=
-  ⟨fun _ => hasProductsOfShape L W _
-    (W.isStableUnderProductsOfShape_of_isStableUnderFiniteProducts _)⟩
+  ⟨fun _ => hasProductsOfShape L W _⟩
 
 include W in
 /-- When `C` has finite products and `W : MorphismProperty C` contains
@@ -119,7 +115,6 @@ then any localization functor for `W` preserves finite products. -/
 lemma preservesFiniteProducts :
     PreservesFiniteProducts L where
   preserves _ := preservesProductsOfShape L W _
-      (W.isStableUnderProductsOfShape_of_isStableUnderFiniteProducts _)
 
 instance : HasFiniteProducts (W.Localization) := hasFiniteProducts W.Q W
 

Mathlib/CategoryTheory/MorphismProperty/FunctorCategory.lean

@@ -37,39 +37,25 @@ instance [W.IsStableUnderRetracts] (J : Type u'') [Category.{v''} J] :
 
 variable {W}
 
-lemma IsStableUnderLimitsOfShape.functorCategory
-    {K : Type u'} [Category.{v'} K]
-    (hW : W.IsStableUnderLimitsOfShape K)
-    (J : Type u'') [Category.{v''} J]
-    [HasLimitsOfShape K C] :
-    (W.functorCategory J).IsStableUnderLimitsOfShape K := by
-  intro X₁ X₂ c₁ c₂ hc₁ hc₂ f hf j
-  convert hW (X₁ ⋙ (evaluation _ _ ).obj j) (X₂ ⋙ (evaluation _ _ ).obj j)
-    _ _ (isLimitOfPreserves _ hc₁) (isLimitOfPreserves _ hc₂) (whiskerRight f _)
-    (fun k ↦ hf k j)
-  apply (isLimitOfPreserves ((evaluation J C).obj j) hc₂).hom_ext
-  intro k
-  rw [IsLimit.fac]
-  dsimp
-  rw [← NatTrans.comp_app, IsLimit.fac]
-  dsimp
-
-lemma IsStableUnderColimitsOfShape.functorCategory
-    {K : Type u'} [Category.{v'} K]
-    (hW : W.IsStableUnderColimitsOfShape K)
-    (J : Type u'') [Category.{v''} J]
-    [HasColimitsOfShape K C] :
-    (W.functorCategory J).IsStableUnderColimitsOfShape K := by
-  intro X₁ X₂ c₁ c₂ hc₁ hc₂ f hf j
-  convert hW (X₁ ⋙ (evaluation _ _ ).obj j) (X₂ ⋙ (evaluation _ _ ).obj j)
-    _ _ (isColimitOfPreserves _ hc₁) (isColimitOfPreserves _ hc₂) (whiskerRight f _)
-    (fun k ↦ hf k j)
-  apply (isColimitOfPreserves ((evaluation J C).obj j) hc₁).hom_ext
-  intro k
-  rw [IsColimit.fac]
-  dsimp
-  rw [← NatTrans.comp_app, IsColimit.fac]
-  dsimp
+instance IsStableUnderLimitsOfShape.functorCategory
+    {K : Type u'} [Category.{v'} K] [W.IsStableUnderLimitsOfShape K]
+    (J : Type u'') [Category.{v''} J] [HasLimitsOfShape K C] :
+    (W.functorCategory J).IsStableUnderLimitsOfShape K where
+  condition X₁ X₂ _ _ hc₁ hc₂ f hf φ hφ j :=
+    MorphismProperty.limitsOfShape_le _
+      (limitsOfShape.mk' (X₁ ⋙ (evaluation _ _ ).obj j) (X₂ ⋙ (evaluation _ _ ).obj j)
+      _ _ (isLimitOfPreserves _ hc₁) (isLimitOfPreserves _ hc₂) (whiskerRight f _)
+      (fun k ↦ hf k j) (φ.app j) (fun k ↦ congr_app (hφ k) j))
+
+instance IsStableUnderColimitsOfShape.functorCategory
+    {K : Type u'} [Category.{v'} K] [W.IsStableUnderColimitsOfShape K]
+    (J : Type u'') [Category.{v''} J] [HasColimitsOfShape K C] :
+    (W.functorCategory J).IsStableUnderColimitsOfShape K where
+  condition X₁ X₂ _ _ hc₁ hc₂ f hf φ hφ j :=
+    MorphismProperty.colimitsOfShape_le _
+      (colimitsOfShape.mk' (X₁ ⋙ (evaluation _ _ ).obj j) (X₂ ⋙ (evaluation _ _ ).obj j)
+      _ _ (isColimitOfPreserves _ hc₁) (isColimitOfPreserves _ hc₂) (whiskerRight f _)
+      (fun k ↦ hf k j) (φ.app j) (fun k ↦ congr_app (hφ k) j))
 
 instance [W.IsStableUnderBaseChange] (J : Type u'') [Category.{v''} J] [HasPullbacks C] :
     (W.functorCategory J).IsStableUnderBaseChange where

Mathlib/CategoryTheory/MorphismProperty/LiftingProperty.lean

@@ -79,14 +79,14 @@ instance rlp_isMultiplicative : T.rlp.IsMultiplicative where
     have := hj _ hp
     infer_instance
 
-lemma llp_isStableUnderCoproductsOfShape (J : Type*) :
+instance llp_isStableUnderCoproductsOfShape (J : Type*) :
     T.llp.IsStableUnderCoproductsOfShape J := by
   apply IsStableUnderCoproductsOfShape.mk
   intro A B _ _ f hf X Y p hp
   have := fun j ↦ hf j _ hp
   infer_instance
 
-lemma rlp_isStableUnderProductsOfShape (J : Type*) :
+instance rlp_isStableUnderProductsOfShape (J : Type*) :
     T.rlp.IsStableUnderProductsOfShape J := by
   apply IsStableUnderProductsOfShape.mk
   intro A B _ _ f hf X Y p hp
@@ -135,9 +135,7 @@ lemma rlp_pushouts : T.pushouts.rlp = T.rlp := by
 lemma colimitsOfShape_discrete_le_llp_rlp (J : Type w) :
     T.colimitsOfShape (Discrete J) ≤ T.rlp.llp := by
   intro A B i hi
-  exact (T.rlp.llp.isStableUnderColimitsOfShape_iff_colimitsOfShape_le (Discrete J)).1
-    (llp_isStableUnderCoproductsOfShape _ _) _
-      (colimitsOfShape_monotone T.le_llp_rlp _ _ hi)
+  exact MorphismProperty.colimitsOfShape_le _ (colimitsOfShape_monotone T.le_llp_rlp _ _ hi)
 
 lemma coproducts_le_llp_rlp : (coproducts.{w} T) ≤ T.rlp.llp := by
   intro A B i hi