diff --git a/Mathlib/Algebra/Category/ModuleCat/AB.lean b/Mathlib/Algebra/Category/ModuleCat/AB.lean index 85340e179340bd..599e1c7d296600 100644 --- a/Mathlib/Algebra/Category/ModuleCat/AB.lean +++ b/Mathlib/Algebra/Category/ModuleCat/AB.lean @@ -36,11 +36,11 @@ instance : AB4Star (ModuleCat.{u} R) where lemma ModuleCat.isSeparator [Small.{v} R] : IsSeparator (ModuleCat.of.{v} R (Shrink.{v} R)) := fun X Y f g h ↦ by - simp only [Set.mem_singleton_iff, forall_eq, ModuleCat.hom_ext_iff, LinearMap.ext_iff] at h + simp only [ObjectProperty.singleton_iff, ModuleCat.hom_ext_iff, hom_comp, + LinearMap.ext_iff, LinearMap.coe_comp, Function.comp_apply, forall_eq'] at h ext x - simpa [Shrink.linearEquiv, Equiv.linearEquiv] using - h (ModuleCat.ofHom ((LinearMap.toSpanSingleton R X x).comp - (Shrink.linearEquiv R R : Shrink R →ₗ[R] R))) 1 + simpa using h (ModuleCat.ofHom ((LinearMap.toSpanSingleton R X x).comp + (Shrink.linearEquiv R R : Shrink R →ₗ[R] R))) 1 instance [Small.{v} R] : HasSeparator (ModuleCat.{v} R) where hasSeparator := ⟨ModuleCat.of R (Shrink.{v} R), ModuleCat.isSeparator R⟩ diff --git a/Mathlib/Algebra/Category/ModuleCat/Presheaf/Generator.lean b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Generator.lean index 624fbfffa33fd0..85e2df00afe01e 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Presheaf/Generator.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Generator.lean @@ -69,24 +69,23 @@ lemma freeYonedaEquiv_comp {M N : PresheafOfModules.{v} R} {X : C} variable (R) in /-- The set of `PresheafOfModules.{v} R` consisting of objects of the form `(free R).obj (yoneda.obj X)` for some `X`. -/ -def freeYoneda : Set (PresheafOfModules.{v} R) := Set.range (yoneda ⋙ free R).obj +def freeYoneda : ObjectProperty (PresheafOfModules.{v} R) := .ofObj (yoneda ⋙ free R).obj namespace freeYoneda -instance : Small.{u} (freeYoneda R) := by - let π : C → freeYoneda R := fun X ↦ ⟨_, ⟨X, rfl⟩⟩ - have hπ : Function.Surjective π := by rintro ⟨_, ⟨X, rfl⟩⟩; exact ⟨X, rfl⟩ - exact small_of_surjective hπ +instance : ObjectProperty.Small.{u} (freeYoneda R) := by + dsimp [freeYoneda] + infer_instance variable (R) -lemma isSeparating : IsSeparating (freeYoneda R) := by +lemma isSeparating : ObjectProperty.IsSeparating (freeYoneda R) := by intro M N f₁ f₂ h ext ⟨X⟩ m obtain ⟨g, rfl⟩ := freeYonedaEquiv.surjective m - exact congr_arg freeYonedaEquiv (h _ ⟨X, rfl⟩ g) + exact congr_arg freeYonedaEquiv (h _ ⟨X⟩ g) -lemma isDetecting : IsDetecting (freeYoneda R) := +lemma isDetecting : ObjectProperty.IsDetecting (freeYoneda R) := (isSeparating R).isDetecting end freeYoneda diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean index 3a323a14d4dae5..7d922e8e2acae7 100644 --- a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean +++ b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean @@ -111,8 +111,8 @@ lemma exists_pushouts ∃ (X' : C) (i : X ⟶ X') (p' : X' ⟶ Y) (_ : (generatingMonomorphisms G).pushouts i) (_ : ¬ IsIso i) (_ : Mono p'), i ≫ p' = p := by rw [hG.isDetector.isIso_iff_of_mono] at hp - simp only [coyoneda_obj_obj, coyoneda_obj_map, Set.mem_singleton_iff, forall_eq, - Function.Surjective, not_forall, not_exists] at hp + simp only [ObjectProperty.singleton_iff, Function.Surjective, coyoneda_obj_obj, + coyoneda_obj_map, forall_eq', not_forall, not_exists] at hp -- `f : G ⟶ Y` is a monomorphism the image of which is not contained in `X` obtain ⟨f, hf⟩ := hp -- we use the subobject `X'` of `Y` that is generated by the images of `p : X ⟶ Y` diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/GabrielPopescu.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/GabrielPopescu.lean index d65dd4bc03c818..1a99e5b1c10c09 100644 --- a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/GabrielPopescu.lean +++ b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ModuleEmbedding/GabrielPopescu.lean @@ -40,7 +40,7 @@ namespace CategoryTheory.IsGrothendieckAbelian variable {C : Type u} [Category.{v} C] [Abelian C] [IsGrothendieckAbelian.{v} C] instance {G : C} : (preadditiveCoyonedaObj G).IsRightAdjoint := - isRightAdjoint_of_preservesLimits_of_isCoseparating (isCoseparator_coseparator _) _ + isRightAdjoint_of_preservesLimits_of_isCoseparating.{v} (isCoseparator_coseparator _) _ /-- The left adjoint of the functor `Hom(G, ·)`, which can be thought of as `· ⊗ G`. -/ noncomputable def tensorObj (G : C) : ModuleCat (End G)ᵐᵒᵖ ⥤ C := diff --git a/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean b/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean index 70462aa2882952..070991b00e932f 100644 --- a/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean +++ b/Mathlib/CategoryTheory/Adjunction/AdjointFunctorTheorems.lean @@ -101,20 +101,22 @@ variable {D : Type u'} [Category.{v} D] well-powered and has a small coseparating set, then `G` has a left adjoint. -/ lemma isRightAdjoint_of_preservesLimits_of_isCoseparating [HasLimits D] [WellPowered.{v} D] - {𝒢 : Set D} [Small.{v} 𝒢] (h𝒢 : IsCoseparating 𝒢) (G : D ⥤ C) [PreservesLimits G] : - G.IsRightAdjoint := - have : ∀ A, HasInitial (StructuredArrow A G) := fun A => - hasInitial_of_isCoseparating (StructuredArrow.isCoseparating_proj_preimage A G h𝒢) - isRightAdjointOfStructuredArrowInitials _ + {P : ObjectProperty D} [ObjectProperty.Small.{v} P] + (hP : P.IsCoseparating) (G : D ⥤ C) [PreservesLimits G] : + G.IsRightAdjoint := by + have : ∀ A, HasInitial (StructuredArrow A G) := fun A ↦ + hasInitial_of_isCoseparating (StructuredArrow.isCoseparating_inverseImage_proj A G hP) + exact isRightAdjointOfStructuredArrowInitials _ /-- The special adjoint functor theorem: if `F : C ⥤ D` preserves colimits and `C` is cocomplete, well-copowered and has a small separating set, then `F` has a right adjoint. -/ lemma isLeftAdjoint_of_preservesColimits_of_isSeparating [HasColimits C] [WellPowered.{v} Cᵒᵖ] - {𝒢 : Set C} [Small.{v} 𝒢] (h𝒢 : IsSeparating 𝒢) (F : C ⥤ D) [PreservesColimits F] : + {P : ObjectProperty C} [ObjectProperty.Small.{v} P] + (h𝒢 : P.IsSeparating) (F : C ⥤ D) [PreservesColimits F] : F.IsLeftAdjoint := have : ∀ A, HasTerminal (CostructuredArrow F A) := fun A => - hasTerminal_of_isSeparating (CostructuredArrow.isSeparating_proj_preimage F A h𝒢) + hasTerminal_of_isSeparating (CostructuredArrow.isSeparating_inverseImage_proj F A h𝒢) isLeftAdjoint_of_costructuredArrowTerminals _ end SpecialAdjointFunctorTheorem @@ -123,19 +125,19 @@ namespace Limits /-- A consequence of the special adjoint functor theorem: if `C` is complete, well-powered and has a small coseparating set, then it is cocomplete. -/ -theorem hasColimits_of_hasLimits_of_isCoseparating [HasLimits C] [WellPowered.{v} C] {𝒢 : Set C} - [Small.{v} 𝒢] (h𝒢 : IsCoseparating 𝒢) : HasColimits C := +theorem hasColimits_of_hasLimits_of_isCoseparating [HasLimits C] [WellPowered.{v} C] + {P : ObjectProperty C} [ObjectProperty.Small.{v} P] (hP : P.IsCoseparating) : HasColimits C := { has_colimits_of_shape := fun _ _ => hasColimitsOfShape_iff_isRightAdjoint_const.2 - (isRightAdjoint_of_preservesLimits_of_isCoseparating h𝒢 _) } + (isRightAdjoint_of_preservesLimits_of_isCoseparating hP _) } /-- A consequence of the special adjoint functor theorem: if `C` is cocomplete, well-copowered and has a small separating set, then it is complete. -/ -theorem hasLimits_of_hasColimits_of_isSeparating [HasColimits C] [WellPowered.{v} Cᵒᵖ] {𝒢 : Set C} - [Small.{v} 𝒢] (h𝒢 : IsSeparating 𝒢) : HasLimits C := +theorem hasLimits_of_hasColimits_of_isSeparating [HasColimits C] [WellPowered.{v} Cᵒᵖ] + {P : ObjectProperty C} [ObjectProperty.Small.{v} P] (hP : P.IsSeparating) : HasLimits C := { has_limits_of_shape := fun _ _ => hasLimitsOfShape_iff_isLeftAdjoint_const.2 - (isLeftAdjoint_of_preservesColimits_of_isSeparating h𝒢 _) } + (isLeftAdjoint_of_preservesColimits_of_isSeparating hP _) } /-- A consequence of the special adjoint functor theorem: if `C` is complete, well-powered and has a separator, then it is complete. -/ diff --git a/Mathlib/CategoryTheory/Comma/StructuredArrow/Small.lean b/Mathlib/CategoryTheory/Comma/StructuredArrow/Small.lean index 1cd9473c266109..ea569695d60868 100644 --- a/Mathlib/CategoryTheory/Comma/StructuredArrow/Small.lean +++ b/Mathlib/CategoryTheory/Comma/StructuredArrow/Small.lean @@ -5,7 +5,7 @@ Authors: Markus Himmel -/ import Mathlib.CategoryTheory.Comma.StructuredArrow.Basic import Mathlib.CategoryTheory.EssentiallySmall -import Mathlib.Logic.Small.Set +import Mathlib.CategoryTheory.ObjectProperty.Small /-! # Small sets in the category of structured arrows @@ -25,12 +25,19 @@ namespace StructuredArrow variable {S : D} {T : C ⥤ D} -instance small_proj_preimage_of_locallySmall {𝒢 : Set C} [Small.{v₁} 𝒢] [LocallySmall.{v₁} D] : - Small.{v₁} ((proj S T).obj ⁻¹' 𝒢) := by - suffices (proj S T).obj ⁻¹' 𝒢 = Set.range fun f : Σ G : 𝒢, S ⟶ T.obj G => mk f.2 by +instance small_inverseImage_proj_of_locallySmall + {P : ObjectProperty C} [ObjectProperty.Small.{v₁} P] [LocallySmall.{v₁} D] : + ObjectProperty.Small.{v₁} (P.inverseImage (proj S T)) := by + suffices P.inverseImage (proj S T) = .ofObj fun f : Σ (G : Subtype P), S ⟶ T.obj G => mk f.2 by rw [this] infer_instance - exact Set.ext fun X => ⟨fun h => ⟨⟨⟨_, h⟩, X.hom⟩, (eq_mk _).symm⟩, by cat_disch⟩ + ext X + simp only [ObjectProperty.prop_inverseImage_iff, proj_obj, ObjectProperty.ofObj_iff, + Sigma.exists, Subtype.exists, exists_prop] + exact ⟨fun h ↦ ⟨_, h, _, rfl⟩, by rintro ⟨_, h, _, rfl⟩; exact h⟩ + +@[deprecated (since := "2025-10-07")] alias small_proj_preimage_of_locallySmall := + small_inverseImage_proj_of_locallySmall end StructuredArrow @@ -38,13 +45,19 @@ namespace CostructuredArrow variable {S : C ⥤ D} {T : D} -instance small_proj_preimage_of_locallySmall {𝒢 : Set C} [Small.{v₁} 𝒢] [LocallySmall.{v₁} D] : - Small.{v₁} ((proj S T).obj ⁻¹' 𝒢) := by - suffices (proj S T).obj ⁻¹' 𝒢 = Set.range fun f : Σ G : 𝒢, S.obj G ⟶ T => mk f.2 by +instance small_inverseImage_proj_of_locallySmall + {P : ObjectProperty C} [ObjectProperty.Small.{v₁} P] [LocallySmall.{v₁} D] : + ObjectProperty.Small.{v₁} (P.inverseImage (proj S T)) := by + suffices P.inverseImage (proj S T) = .ofObj fun f : Σ (G : Subtype P), S.obj G ⟶ T => mk f.2 by rw [this] infer_instance - exact Set.ext fun X => ⟨fun h => ⟨⟨⟨_, h⟩, X.hom⟩, (eq_mk _).symm⟩, by cat_disch⟩ + ext X + simp only [ObjectProperty.prop_inverseImage_iff, proj_obj, ObjectProperty.ofObj_iff, + Sigma.exists, Subtype.exists, exists_prop] + exact ⟨fun h ↦ ⟨_, h, _, rfl⟩, by rintro ⟨_, h, _, rfl⟩; exact h⟩ +@[deprecated (since := "2025-10-07")] alias small_proj_preimage_of_locallySmall := + small_inverseImage_proj_of_locallySmall end CostructuredArrow end CategoryTheory diff --git a/Mathlib/CategoryTheory/Generator/Basic.lean b/Mathlib/CategoryTheory/Generator/Basic.lean index 65a605c444466d..f9b79a3af6a063 100644 --- a/Mathlib/CategoryTheory/Generator/Basic.lean +++ b/Mathlib/CategoryTheory/Generator/Basic.lean @@ -6,7 +6,7 @@ Authors: Markus Himmel import Mathlib.CategoryTheory.Limits.EssentiallySmall import Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers import Mathlib.CategoryTheory.Subobject.Lattice -import Mathlib.Data.Set.Opposite +import Mathlib.CategoryTheory.ObjectProperty.Small /-! # Separating and detecting sets @@ -14,10 +14,12 @@ import Mathlib.Data.Set.Opposite There are several non-equivalent notions of a generator of a category. Here, we consider two of them: -* We say that `𝒢` is a separating set if the functors `C(G, -)` for `G ∈ 𝒢` are collectively - faithful, i.e., if `h ≫ f = h ≫ g` for all `h` with domain in `𝒢` implies `f = g`. -* We say that `𝒢` is a detecting set if the functors `C(G, -)` collectively reflect isomorphisms, - i.e., if any `h` with domain in `𝒢` uniquely factors through `f`, then `f` is an isomorphism. +* We say that `P : ObjectProperty C` is a separating set if the functors `C(G, -)` + for `G` such that `P G` are collectively faithful, i.e., if + `h ≫ f = h ≫ g` for all `h` with domain satisfying `P` implies `f = g`. +* We say that `P : ObjectProperty C` is a detecting set if the functors `C(G, -)` + collectively reflect isomorphisms, i.e., if any `h` with domain satisfying `P` + uniquely factors through `f`, then `f` is an isomorphism. There are, of course, also the dual notions of coseparating and codetecting sets. @@ -25,7 +27,7 @@ There are, of course, also the dual notions of coseparating and codetecting sets We * define predicates `IsSeparating`, `IsCoseparating`, `IsDetecting` and `IsCodetecting` on - sets of objects; + `ObjectProperty C`; * show that equivalences of categories preserves these notions; * show that separating and coseparating are dual notions; * show that detecting and codetecting are dual notions; @@ -45,9 +47,9 @@ We * define corresponding typeclasses `HasSeparator`, `HasCoseparator`, `HasDetector` and `HasCodetector` on categories and prove analogous results for these. -## Future work +## Examples -* We currently don't have any examples yet. +See the files `CategoryTheory.Generator.Presheaf` and `CategoryTheory.Generator.Sheaf`. -/ @@ -60,143 +62,161 @@ namespace CategoryTheory variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D] -/-- We say that `𝒢` is a separating set if the functors `C(G, -)` for `G ∈ 𝒢` are collectively - faithful, i.e., if `h ≫ f = h ≫ g` for all `h` with domain in `𝒢` implies `f = g`. -/ -def IsSeparating (𝒢 : Set C) : Prop := - ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ G ∈ 𝒢, ∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g - -/-- We say that `𝒢` is a coseparating set if the functors `C(-, G)` for `G ∈ 𝒢` are collectively - faithful, i.e., if `f ≫ h = g ≫ h` for all `h` with codomain in `𝒢` implies `f = g`. -/ -def IsCoseparating (𝒢 : Set C) : Prop := - ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ G ∈ 𝒢, ∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g - -/-- We say that `𝒢` is a detecting set if the functors `C(G, -)` collectively reflect isomorphisms, - i.e., if any `h` with domain in `𝒢` uniquely factors through `f`, then `f` is an isomorphism. -/ -def IsDetecting (𝒢 : Set C) : Prop := - ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ G ∈ 𝒢, ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h) → IsIso f - -/-- We say that `𝒢` is a codetecting set if the functors `C(-, G)` collectively reflect - isomorphisms, i.e., if any `h` with codomain in `G` uniquely factors through `f`, then `f` is - an isomorphism. -/ -def IsCodetecting (𝒢 : Set C) : Prop := - ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ G ∈ 𝒢, ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h) → IsIso f +namespace ObjectProperty + +variable (P : ObjectProperty C) + +/-- We say that `P : ObjectProperty C` is a separating set if the functors `C(G, -)` +for `G : C` such that `P G` are collectively faithful, +i.e., if `h ≫ f = h ≫ g` for all `h` with domain in `𝒢` implies `f = g`. -/ +def IsSeparating : Prop := + ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (G : C) (_ : P G) (h : G ⟶ X), h ≫ f = h ≫ g) → f = g + +/-- We say that `P : ObjectProperty C` is a coseparating set if the functors `C(-, G)` +for `G : C` such that `P G` are collectively faithful, +i.e., if `f ≫ h = g ≫ h` for all `h` with codomain in `𝒢` implies `f = g`. -/ +def IsCoseparating : Prop := + ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (G : C) (_ : P G) (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g + +/-- We say that `P : ObjectProperty C` is a detecting set if the functors `C(G, -)` +for `G : C` such that `P G` collectively reflect isomorphisms, +i.e., if any `h` with domain `G` that `P G` uniquely factors through `f`, +then `f` is an isomorphism. -/ +def IsDetecting : Prop := + ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (G : C) (_ : P G), + ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h) → IsIso f + +/-- We say that `P : ObjectProperty C` is a codetecting set if the functors `C(-, G)` +for `G : C` such that `P G` collectively reflect isomorphisms, +i.e., if any `h` with codomain `G` such that `P G` uniquely factors through `f`, +then `f` is an isomorphism. -/ +def IsCodetecting : Prop := + ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (G : C) (_ : P G), + ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h) → IsIso f section Equivalence +variable {P} + lemma IsSeparating.of_equivalence - {𝒢 : Set C} (h : IsSeparating 𝒢) {D : Type*} [Category D] (α : C ≌ D) : - IsSeparating (α.functor.obj '' 𝒢) := fun X Y f g H => - α.inverse.map_injective (h _ _ (fun Z hZ h => by + (h : IsSeparating P) {D : Type*} [Category D] (α : C ≌ D) : + IsSeparating (P.strictMap α.functor) := fun X Y f g H => + α.inverse.map_injective (h _ _ (fun Z hZ h ↦ by obtain ⟨h', rfl⟩ := (α.toAdjunction.homEquiv _ _).surjective h simp only [Adjunction.homEquiv_unit, Category.assoc, ← Functor.map_comp, - H (α.functor.obj Z) (Set.mem_image_of_mem _ hZ) h'])) + H _ (P.strictMap_obj _ hZ) h'])) lemma IsCoseparating.of_equivalence - {𝒢 : Set C} (h : IsCoseparating 𝒢) {D : Type*} [Category D] (α : C ≌ D) : - IsCoseparating (α.functor.obj '' 𝒢) := fun X Y f g H => - α.inverse.map_injective (h _ _ (fun Z hZ h => by + (h : IsCoseparating P) {D : Type*} [Category D] (α : C ≌ D) : + IsCoseparating (P.strictMap α.functor) := fun X Y f g H => + α.inverse.map_injective (h _ _ (fun Z hZ h ↦ by obtain ⟨h', rfl⟩ := (α.symm.toAdjunction.homEquiv _ _).symm.surjective h - simp only [Adjunction.homEquiv_symm_apply, ← Category.assoc, ← Functor.map_comp, - Equivalence.symm_functor, H (α.functor.obj Z) (Set.mem_image_of_mem _ hZ) h'])) + simp only [Equivalence.symm_inverse, Equivalence.symm_functor, + Adjunction.homEquiv_counit, ← Functor.map_comp_assoc, + H _ (P.strictMap_obj _ hZ) h'])) end Equivalence section Dual -theorem isSeparating_op_iff (𝒢 : Set C) : IsSeparating 𝒢.op ↔ IsCoseparating 𝒢 := by - refine ⟨fun h𝒢 X Y f g hfg => ?_, fun h𝒢 X Y f g hfg => ?_⟩ - · refine Quiver.Hom.op_inj (h𝒢 _ _ fun G hG h => Quiver.Hom.unop_inj ?_) - simpa only [unop_comp, Quiver.Hom.unop_op] using hfg _ (Set.mem_op.1 hG) _ - · refine Quiver.Hom.unop_inj (h𝒢 _ _ fun G hG h => Quiver.Hom.op_inj ?_) - simpa only [op_comp, Quiver.Hom.op_unop] using hfg _ (Set.op_mem_op.2 hG) _ - -theorem isCoseparating_op_iff (𝒢 : Set C) : IsCoseparating 𝒢.op ↔ IsSeparating 𝒢 := by - refine ⟨fun h𝒢 X Y f g hfg => ?_, fun h𝒢 X Y f g hfg => ?_⟩ - · refine Quiver.Hom.op_inj (h𝒢 _ _ fun G hG h => Quiver.Hom.unop_inj ?_) - simpa only [unop_comp, Quiver.Hom.unop_op] using hfg _ (Set.mem_op.1 hG) _ - · refine Quiver.Hom.unop_inj (h𝒢 _ _ fun G hG h => Quiver.Hom.op_inj ?_) - simpa only [op_comp, Quiver.Hom.op_unop] using hfg _ (Set.op_mem_op.2 hG) _ - -theorem isCoseparating_unop_iff (𝒢 : Set Cᵒᵖ) : IsCoseparating 𝒢.unop ↔ IsSeparating 𝒢 := by - rw [← isSeparating_op_iff, Set.unop_op] - -theorem isSeparating_unop_iff (𝒢 : Set Cᵒᵖ) : IsSeparating 𝒢.unop ↔ IsCoseparating 𝒢 := by - rw [← isCoseparating_op_iff, Set.unop_op] - -theorem isDetecting_op_iff (𝒢 : Set C) : IsDetecting 𝒢.op ↔ IsCodetecting 𝒢 := by - refine ⟨fun h𝒢 X Y f hf => ?_, fun h𝒢 X Y f hf => ?_⟩ - · refine (isIso_op_iff _).1 (h𝒢 _ fun G hG h => ?_) - obtain ⟨t, ht, ht'⟩ := hf (unop G) (Set.mem_op.1 hG) h.unop +theorem isSeparating_op_iff : IsSeparating P.op ↔ IsCoseparating P := by + refine ⟨fun hP X Y f g hfg => ?_, fun hP X Y f g hfg => ?_⟩ + · refine Quiver.Hom.op_inj (hP _ _ fun G hG h => Quiver.Hom.unop_inj ?_) + simpa only [unop_comp, Quiver.Hom.unop_op] using hfg _ hG _ + · refine Quiver.Hom.unop_inj (hP _ _ fun G hG h => Quiver.Hom.op_inj ?_) + simpa only [op_comp, Quiver.Hom.op_unop] using hfg _ hG _ + +theorem isCoseparating_op_iff : IsCoseparating P.op ↔ IsSeparating P := by + refine ⟨fun hP X Y f g hfg => ?_, fun hP X Y f g hfg => ?_⟩ + · refine Quiver.Hom.op_inj (hP _ _ fun G hG h => Quiver.Hom.unop_inj ?_) + simpa only [unop_comp, Quiver.Hom.unop_op] using hfg _ hG _ + · refine Quiver.Hom.unop_inj (hP _ _ fun G hG h => Quiver.Hom.op_inj ?_) + simpa only [op_comp, Quiver.Hom.op_unop] using hfg _ hG _ + +theorem isCoseparating_unop_iff (P : ObjectProperty Cᵒᵖ) : + IsCoseparating P.unop ↔ IsSeparating P := + P.unop.isSeparating_op_iff.symm + +theorem isSeparating_unop_iff (P : ObjectProperty Cᵒᵖ) : + IsSeparating P.unop ↔ IsCoseparating P := + P.unop.isCoseparating_op_iff.symm + +theorem isDetecting_op_iff : IsDetecting P.op ↔ IsCodetecting P := by + refine ⟨fun hP X Y f hf => ?_, fun hP X Y f hf => ?_⟩ + · refine (isIso_op_iff _).1 (hP _ fun G hG h => ?_) + obtain ⟨t, ht, ht'⟩ := hf (unop G) hG h.unop exact ⟨t.op, Quiver.Hom.unop_inj ht, fun y hy => Quiver.Hom.unop_inj (ht' _ (Quiver.Hom.op_inj hy))⟩ - · refine (isIso_unop_iff _).1 (h𝒢 _ fun G hG h => ?_) - obtain ⟨t, ht, ht'⟩ := hf (op G) (Set.op_mem_op.2 hG) h.op + · refine (isIso_unop_iff _).1 (hP _ fun G hG h => ?_) + obtain ⟨t, ht, ht'⟩ := hf (op G) hG h.op refine ⟨t.unop, Quiver.Hom.op_inj ht, fun y hy => Quiver.Hom.op_inj (ht' _ ?_)⟩ exact Quiver.Hom.unop_inj (by simpa only using hy) -theorem isCodetecting_op_iff (𝒢 : Set C) : IsCodetecting 𝒢.op ↔ IsDetecting 𝒢 := by - refine ⟨fun h𝒢 X Y f hf => ?_, fun h𝒢 X Y f hf => ?_⟩ - · refine (isIso_op_iff _).1 (h𝒢 _ fun G hG h => ?_) - obtain ⟨t, ht, ht'⟩ := hf (unop G) (Set.mem_op.1 hG) h.unop +theorem isCodetecting_op_iff : IsCodetecting P.op ↔ IsDetecting P := by + refine ⟨fun hP X Y f hf => ?_, fun hP X Y f hf => ?_⟩ + · refine (isIso_op_iff _).1 (hP _ fun G hG h => ?_) + obtain ⟨t, ht, ht'⟩ := hf (unop G) hG h.unop exact ⟨t.op, Quiver.Hom.unop_inj ht, fun y hy => Quiver.Hom.unop_inj (ht' _ (Quiver.Hom.op_inj hy))⟩ - · refine (isIso_unop_iff _).1 (h𝒢 _ fun G hG h => ?_) - obtain ⟨t, ht, ht'⟩ := hf (op G) (Set.op_mem_op.2 hG) h.op + · refine (isIso_unop_iff _).1 (hP _ fun G hG h => ?_) + obtain ⟨t, ht, ht'⟩ := hf (op G) hG h.op refine ⟨t.unop, Quiver.Hom.op_inj ht, fun y hy => Quiver.Hom.op_inj (ht' _ ?_)⟩ exact Quiver.Hom.unop_inj (by simpa only using hy) -theorem isDetecting_unop_iff (𝒢 : Set Cᵒᵖ) : IsDetecting 𝒢.unop ↔ IsCodetecting 𝒢 := by - rw [← isCodetecting_op_iff, Set.unop_op] +theorem isDetecting_unop_iff (P : ObjectProperty Cᵒᵖ) : IsDetecting P.unop ↔ IsCodetecting P := + P.unop.isCodetecting_op_iff.symm -theorem isCodetecting_unop_iff {𝒢 : Set Cᵒᵖ} : IsCodetecting 𝒢.unop ↔ IsDetecting 𝒢 := by - rw [← isDetecting_op_iff, Set.unop_op] +theorem isCodetecting_unop_iff (P : ObjectProperty Cᵒᵖ) : IsCodetecting P.unop ↔ IsDetecting P := + P.unop.isDetecting_op_iff.symm end Dual -theorem IsDetecting.isSeparating [HasEqualizers C] {𝒢 : Set C} (h𝒢 : IsDetecting 𝒢) : - IsSeparating 𝒢 := fun _ _ f g hfg => - have : IsIso (equalizer.ι f g) := h𝒢 _ fun _ hG _ => equalizer.existsUnique _ (hfg _ hG _) +variable {P} + +theorem IsDetecting.isSeparating [HasEqualizers C] (hP : IsDetecting P) : + IsSeparating P := fun _ _ f g hfg => + have : IsIso (equalizer.ι f g) := hP _ fun _ hG _ => equalizer.existsUnique _ (hfg _ hG _) eq_of_epi_equalizer -theorem IsCodetecting.isCoseparating [HasCoequalizers C] {𝒢 : Set C} : - IsCodetecting 𝒢 → IsCoseparating 𝒢 := by +theorem IsCodetecting.isCoseparating [HasCoequalizers C] : + IsCodetecting P → IsCoseparating P := by simpa only [← isSeparating_op_iff, ← isDetecting_op_iff] using IsDetecting.isSeparating -theorem IsSeparating.isDetecting [Balanced C] {𝒢 : Set C} (h𝒢 : IsSeparating 𝒢) : - IsDetecting 𝒢 := by +theorem IsSeparating.isDetecting [Balanced C] (hP : IsSeparating P) : + IsDetecting P := by intro X Y f hf refine - (isIso_iff_mono_and_epi _).2 ⟨⟨fun g h hgh => h𝒢 _ _ fun G hG i => ?_⟩, ⟨fun g h hgh => ?_⟩⟩ + (isIso_iff_mono_and_epi _).2 ⟨⟨fun g h hgh => hP _ _ fun G hG i => ?_⟩, ⟨fun g h hgh => ?_⟩⟩ · obtain ⟨t, -, ht⟩ := hf G hG (i ≫ g ≫ f) rw [ht (i ≫ g) (Category.assoc _ _ _), ht (i ≫ h) (hgh.symm ▸ Category.assoc _ _ _)] - · refine h𝒢 _ _ fun G hG i => ?_ + · refine hP _ _ fun G hG i => ?_ obtain ⟨t, rfl, -⟩ := hf G hG i rw [Category.assoc, hgh, Category.assoc] -lemma IsDetecting.isIso_iff_of_mono {𝒢 : Set C} (h𝒢 : IsDetecting 𝒢) +lemma IsDetecting.isIso_iff_of_mono (hP : IsDetecting P) {X Y : C} (f : X ⟶ Y) [Mono f] : - IsIso f ↔ ∀ s ∈ 𝒢, Function.Surjective ((coyoneda.obj (op s)).map f) := by + IsIso f ↔ ∀ (G : C) (_ : P G), Function.Surjective ((coyoneda.obj (op G)).map f) := by constructor · intro h rw [isIso_iff_yoneda_map_bijective] at h intro A _ exact (h A).2 · intro hf - refine h𝒢 _ (fun A hA g ↦ existsUnique_of_exists_of_unique ?_ ?_) + refine hP _ (fun A hA g ↦ existsUnique_of_exists_of_unique ?_ ?_) · exact hf A hA g · intro l₁ l₂ h₁ h₂ rw [← cancel_mono f, h₁, h₂] -lemma IsCodetecting.isIso_iff_of_epi {𝒢 : Set C} (h𝒢 : IsCodetecting 𝒢) +lemma IsCodetecting.isIso_iff_of_epi (hP : IsCodetecting P) {X Y : C} (f : X ⟶ Y) [Epi f] : - IsIso f ↔ ∀ s ∈ 𝒢, Function.Surjective ((yoneda.obj s).map f.op) := by + IsIso f ↔ ∀ (G : C) (_ : P G), Function.Surjective ((yoneda.obj G).map f.op) := by constructor · intro h rw [isIso_iff_coyoneda_map_bijective] at h intro A _ exact (h A).2 · intro hf - refine h𝒢 _ (fun A hA g ↦ existsUnique_of_exists_of_unique ?_ ?_) + refine hP _ (fun A hA g ↦ existsUnique_of_exists_of_unique ?_ ?_) · exact hf A hA g · intro l₁ l₂ h₁ h₂ rw [← cancel_epi f, h₁, h₂] @@ -205,84 +225,96 @@ section attribute [local instance] balanced_opposite -theorem IsCoseparating.isCodetecting [Balanced C] {𝒢 : Set C} : - IsCoseparating 𝒢 → IsCodetecting 𝒢 := by +theorem IsCoseparating.isCodetecting [Balanced C] : + IsCoseparating P → IsCodetecting P := by simpa only [← isDetecting_op_iff, ← isSeparating_op_iff] using IsSeparating.isDetecting end -theorem isDetecting_iff_isSeparating [HasEqualizers C] [Balanced C] (𝒢 : Set C) : - IsDetecting 𝒢 ↔ IsSeparating 𝒢 := +theorem isDetecting_iff_isSeparating [HasEqualizers C] [Balanced C] : + IsDetecting P ↔ IsSeparating P := ⟨IsDetecting.isSeparating, IsSeparating.isDetecting⟩ -theorem isCodetecting_iff_isCoseparating [HasCoequalizers C] [Balanced C] {𝒢 : Set C} : - IsCodetecting 𝒢 ↔ IsCoseparating 𝒢 := +theorem isCodetecting_iff_isCoseparating [HasCoequalizers C] [Balanced C] : + IsCodetecting P ↔ IsCoseparating P := ⟨IsCodetecting.isCoseparating, IsCoseparating.isCodetecting⟩ section Mono -theorem IsSeparating.mono {𝒢 : Set C} (h𝒢 : IsSeparating 𝒢) {ℋ : Set C} (h𝒢ℋ : 𝒢 ⊆ ℋ) : - IsSeparating ℋ := fun _ _ _ _ hfg => h𝒢 _ _ fun _ hG _ => hfg _ (h𝒢ℋ hG) _ +theorem IsSeparating.of_le (hP : IsSeparating P) {Q : ObjectProperty C} (h : P ≤ Q) : + IsSeparating Q := fun _ _ _ _ hfg => hP _ _ fun _ hG _ => hfg _ (h _ hG) _ -theorem IsCoseparating.mono {𝒢 : Set C} (h𝒢 : IsCoseparating 𝒢) {ℋ : Set C} (h𝒢ℋ : 𝒢 ⊆ ℋ) : - IsCoseparating ℋ := fun _ _ _ _ hfg => h𝒢 _ _ fun _ hG _ => hfg _ (h𝒢ℋ hG) _ +theorem IsCoseparating.of_le (hP : IsCoseparating P) {Q : ObjectProperty C} (h : P ≤ Q) : + IsCoseparating Q := fun _ _ _ _ hfg => hP _ _ fun _ hG _ => hfg _ (h _ hG) _ -theorem IsDetecting.mono {𝒢 : Set C} (h𝒢 : IsDetecting 𝒢) {ℋ : Set C} (h𝒢ℋ : 𝒢 ⊆ ℋ) : - IsDetecting ℋ := fun _ _ _ hf => h𝒢 _ fun _ hG _ => hf _ (h𝒢ℋ hG) _ +theorem IsDetecting.of_le (hP : IsDetecting P) {Q : ObjectProperty C} (h : P ≤ Q) : + IsDetecting Q := fun _ _ _ hf => hP _ fun _ hG _ => hf _ (h _ hG) _ -theorem IsCodetecting.mono {𝒢 : Set C} (h𝒢 : IsCodetecting 𝒢) {ℋ : Set C} (h𝒢ℋ : 𝒢 ⊆ ℋ) : - IsCodetecting ℋ := fun _ _ _ hf => h𝒢 _ fun _ hG _ => hf _ (h𝒢ℋ hG) _ +theorem IsCodetecting.of_le (h𝒢 : IsCodetecting P) {Q : ObjectProperty C} (h : P ≤ Q) : + IsCodetecting Q := fun _ _ _ hf => h𝒢 _ fun _ hG _ => hf _ (h _ hG) _ end Mono section Empty -theorem thin_of_isSeparating_empty (h : IsSeparating (∅ : Set C)) : Quiver.IsThin C := fun _ _ => - ⟨fun _ _ => h _ _ fun _ => False.elim⟩ +lemma isThin_of_isSeparating_bot (h : IsSeparating (⊥ : ObjectProperty C)) : + Quiver.IsThin C := fun _ _ ↦ ⟨fun _ _ ↦ h _ _ (by simp)⟩ -theorem isSeparating_empty_of_thin [Quiver.IsThin C] : IsSeparating (∅ : Set C) := - fun _ _ _ _ _ => Subsingleton.elim _ _ +lemma isSeparating_bot_of_isThin [Quiver.IsThin C] : IsSeparating (⊥ : ObjectProperty C) := + fun _ _ _ _ _ ↦ Subsingleton.elim _ _ -theorem thin_of_isCoseparating_empty (h : IsCoseparating (∅ : Set C)) : Quiver.IsThin C := - fun _ _ => ⟨fun _ _ => h _ _ fun _ => False.elim⟩ +lemma isThin_of_isCoseparating_bot (h : IsCoseparating (⊥ : ObjectProperty C)) : + Quiver.IsThin C := fun _ _ ↦ ⟨fun _ _ ↦ h _ _ (by simp)⟩ -theorem isCoseparating_empty_of_thin [Quiver.IsThin C] : IsCoseparating (∅ : Set C) := - fun _ _ _ _ _ => Subsingleton.elim _ _ +lemma isCoseparating_bot_of_isThin [Quiver.IsThin C] : IsCoseparating (⊥ : ObjectProperty C) := + fun _ _ _ _ _ ↦ Subsingleton.elim _ _ -theorem groupoid_of_isDetecting_empty (h : IsDetecting (∅ : Set C)) {X Y : C} (f : X ⟶ Y) : - IsIso f := - h _ fun _ => False.elim +lemma isGroupoid_of_isDetecting_bot (h : IsDetecting (⊥ : ObjectProperty C)) : + IsGroupoid C where + all_isIso f := h _ (by simp) -theorem isDetecting_empty_of_groupoid [∀ {X Y : C} (f : X ⟶ Y), IsIso f] : - IsDetecting (∅ : Set C) := fun _ _ _ _ => inferInstance +lemma isDetecting_bot_of_isGroupoid [IsGroupoid C] : + IsDetecting (⊥ : ObjectProperty C) := + fun _ _ _ _ ↦ inferInstance -theorem groupoid_of_isCodetecting_empty (h : IsCodetecting (∅ : Set C)) {X Y : C} (f : X ⟶ Y) : - IsIso f := - h _ fun _ => False.elim +lemma isGroupoid_of_isCodetecting_bot (h : IsCodetecting (⊥ : ObjectProperty C)) : + IsGroupoid C where + all_isIso f := h _ (by simp) -theorem isCodetecting_empty_of_groupoid [∀ {X Y : C} (f : X ⟶ Y), IsIso f] : - IsCodetecting (∅ : Set C) := fun _ _ _ _ => inferInstance +lemma isCodetecting_bot_of_isGroupoid [IsGroupoid C] : + IsCodetecting (⊥ : ObjectProperty C) := + fun _ _ _ _ ↦ inferInstance end Empty -theorem isSeparating_iff_epi (𝒢 : Set C) - [∀ A : C, HasCoproduct fun f : Σ G : 𝒢, (G : C) ⟶ A => (f.1 : C)] : - IsSeparating 𝒢 ↔ ∀ A : C, Epi (Sigma.desc (@Sigma.snd 𝒢 fun G => (G : C) ⟶ A)) := by - refine ⟨fun h A => ⟨fun u v huv => h _ _ fun G hG f => ?_⟩, fun h X Y f g hh => ?_⟩ - · simpa using Sigma.ι (fun f : Σ G : 𝒢, (G : C) ⟶ A => (f.1 : C)) ⟨⟨G, hG⟩, f⟩ ≫= huv - · haveI := h X - refine - (cancel_epi (Sigma.desc (@Sigma.snd 𝒢 fun G => (G : C) ⟶ X))).1 (colimit.hom_ext fun j => ?_) - simpa using hh j.as.1.1 j.as.1.2 j.as.2 - -theorem isCoseparating_iff_mono (𝒢 : Set C) - [∀ A : C, HasProduct fun f : Σ G : 𝒢, A ⟶ (G : C) => (f.1 : C)] : - IsCoseparating 𝒢 ↔ ∀ A : C, Mono (Pi.lift (@Sigma.snd 𝒢 fun G => A ⟶ (G : C))) := by - refine ⟨fun h A => ⟨fun u v huv => h _ _ fun G hG f => ?_⟩, fun h X Y f g hh => ?_⟩ - · simpa using huv =≫ Pi.π (fun f : Σ G : 𝒢, A ⟶ (G : C) => (f.1 : C)) ⟨⟨G, hG⟩, f⟩ - · haveI := h Y - refine (cancel_mono (Pi.lift (@Sigma.snd 𝒢 fun G => Y ⟶ (G : C)))).1 (limit.hom_ext fun j => ?_) - simpa using hh j.as.1.1 j.as.1.2 j.as.2 +variable (P) + +theorem isSeparating_iff_epi + [∀ A : C, HasCoproduct fun f : Σ G : Subtype P, G.1 ⟶ A ↦ f.1.1] : + IsSeparating P ↔ + ∀ A : C, Epi (Sigma.desc (Sigma.snd (β := fun (G : Subtype P) ↦ G.1 ⟶ A))) := by + let β (A : C) (G : Subtype P) := G.1 ⟶ A + let b (A : C) (x : Σ G, β A G) := x.1.1 + refine ⟨fun h A ↦ ⟨fun u v huv ↦ h _ _ fun G hG f ↦ ?_⟩, fun h X Y f g hh ↦ ?_⟩ + · simpa [β, b] using Sigma.ι (b A) ⟨⟨G, hG⟩, f⟩ ≫= huv + · rw [← cancel_epi (Sigma.desc (Sigma.snd (β := β X)))] + ext ⟨⟨_, hG⟩, _⟩ + simpa using hh _ hG _ + +theorem isCoseparating_iff_mono + [∀ A : C, HasProduct fun f : Σ G : Subtype P, A ⟶ G.1 ↦ f.1.1] : + IsCoseparating P ↔ + ∀ A : C, Mono (Pi.lift (Sigma.snd (β := fun (G : Subtype P) ↦ A ⟶ G.1))) := by + let β (A : C) (G : Subtype P) := A ⟶ G.1 + let b (A : C) (x : Σ G, β A G) := x.1.1 + refine ⟨fun h A ↦ ⟨fun u v huv ↦ h _ _ fun G hG f ↦ ?_⟩, fun h X Y f g hh ↦ ?_⟩ + · simpa [β, b] using huv =≫ Pi.π (b A) ⟨⟨G, hG⟩, f⟩ + · rw [← cancel_mono (Pi.lift (Sigma.snd (β := β Y)))] + ext ⟨⟨_, hG⟩, _⟩ + simp + simpa using hh _ hG _ + +end ObjectProperty /-- An ingredient of the proof of the Special Adjoint Functor Theorem: a complete well-powered category with a small coseparating set has an initial object. @@ -290,18 +322,18 @@ theorem isCoseparating_iff_mono (𝒢 : Set C) In fact, it follows from the Special Adjoint Functor Theorem that `C` is already cocomplete, see `hasColimits_of_hasLimits_of_isCoseparating`. -/ theorem hasInitial_of_isCoseparating [LocallySmall.{w} C] [WellPowered.{w} C] - [HasLimitsOfSize.{w, w} C] {𝒢 : Set C} [Small.{w} 𝒢] - (h𝒢 : IsCoseparating 𝒢) : HasInitial C := by + [HasLimitsOfSize.{w, w} C] {P : ObjectProperty C} [ObjectProperty.Small.{w} P] + (hP : P.IsCoseparating) : HasInitial C := by have := hasFiniteLimits_of_hasLimitsOfSize C - haveI : HasProductsOfShape 𝒢 C := hasProductsOfShape_of_small C 𝒢 - haveI := fun A => hasProductsOfShape_of_small.{w} C (Σ G : 𝒢, A ⟶ (G : C)) - letI := completeLatticeOfCompleteSemilatticeInf (Subobject (piObj (Subtype.val : 𝒢 → C))) - suffices ∀ A : C, Unique (((⊥ : Subobject (piObj (Subtype.val : 𝒢 → C))) : C) ⟶ A) by - exact hasInitial_of_unique ((⊥ : Subobject (piObj (Subtype.val : 𝒢 → C))) : C) + haveI : HasProductsOfShape (Subtype P) C := hasProductsOfShape_of_small C (Subtype P) + haveI := fun A => hasProductsOfShape_of_small.{w} C (Σ G : Subtype P, A ⟶ (G : C)) + letI := completeLatticeOfCompleteSemilatticeInf (Subobject (piObj (Subtype.val : Subtype P → C))) + suffices ∀ A : C, Unique (((⊥ : Subobject (piObj (Subtype.val : Subtype P → C))) : C) ⟶ A) by + exact hasInitial_of_unique ((⊥ : Subobject (piObj (Subtype.val : Subtype P → C))) : C) refine fun A => ⟨⟨?_⟩, fun f => ?_⟩ - · let s := Pi.lift fun f : Σ G : 𝒢, A ⟶ (G : C) => id (Pi.π (Subtype.val : 𝒢 → C)) f.1 - let t := Pi.lift (@Sigma.snd 𝒢 fun G => A ⟶ (G : C)) - haveI : Mono t := (isCoseparating_iff_mono 𝒢).1 h𝒢 A + · let s := Pi.lift fun f : Σ G : Subtype P, A ⟶ (G : C) => Pi.π (Subtype.val : Subtype P → C) f.1 + let t := Pi.lift (@Sigma.snd (Subtype P) fun G => A ⟶ (G : C)) + haveI : Mono t := P.isCoseparating_iff_mono.1 hP A exact Subobject.ofLEMk _ (pullback.fst _ _ : pullback s t ⟶ _) bot_le ≫ pullback.snd _ _ · suffices ∀ (g : Subobject.underlying.obj ⊥ ⟶ A), f = g by apply this @@ -317,18 +349,18 @@ theorem hasInitial_of_isCoseparating [LocallySmall.{w} C] [WellPowered.{w} C] In fact, it follows from the Special Adjoint Functor Theorem that `C` is already complete, see `hasLimits_of_hasColimits_of_isSeparating`. -/ theorem hasTerminal_of_isSeparating [LocallySmall.{w} Cᵒᵖ] [WellPowered.{w} Cᵒᵖ] - [HasColimitsOfSize.{w, w} C] {𝒢 : Set C} [Small.{w} 𝒢] - (h𝒢 : IsSeparating 𝒢) : HasTerminal C := by - haveI : Small.{w} 𝒢.op := small_of_injective (Set.opEquiv_self 𝒢).injective - haveI : HasInitial Cᵒᵖ := hasInitial_of_isCoseparating ((isCoseparating_op_iff _).2 h𝒢) + [HasColimitsOfSize.{w, w} C] {P : ObjectProperty C} [ObjectProperty.Small.{w} P] + (hP : P.IsSeparating) : HasTerminal C := by + haveI : HasInitial Cᵒᵖ := hasInitial_of_isCoseparating (P.isCoseparating_op_iff.2 hP) exact hasTerminal_of_hasInitial_op section WellPowered namespace Subobject -theorem eq_of_le_of_isDetecting {𝒢 : Set C} (h𝒢 : IsDetecting 𝒢) {X : C} (P Q : Subobject X) - (h₁ : P ≤ Q) (h₂ : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f) : P = Q := by +theorem eq_of_le_of_isDetecting {𝒢 : ObjectProperty C} (h𝒢 : 𝒢.IsDetecting) {X : C} + (P Q : Subobject X) (h₁ : P ≤ Q) + (h₂ : ∀ (G : C) (_ : 𝒢 G), ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f) : P = Q := by suffices IsIso (ofLE _ _ h₁) by exact le_antisymm h₁ (le_of_comm (inv (ofLE _ _ h₁)) (by simp)) refine h𝒢 _ fun G hG f => ?_ have : P.Factors (f ≫ Q.arrow) := h₂ _ hG ((factors_iff _ _).2 ⟨_, rfl⟩) @@ -337,13 +369,15 @@ theorem eq_of_le_of_isDetecting {𝒢 : Set C} (h𝒢 : IsDetecting 𝒢) {X : C · simp only [← cancel_mono (Subobject.ofLE _ _ h₁), ← cancel_mono Q.arrow, hg, Category.assoc, ofLE_arrow, factorThru_arrow] -theorem inf_eq_of_isDetecting [HasPullbacks C] {𝒢 : Set C} (h𝒢 : IsDetecting 𝒢) {X : C} - (P Q : Subobject X) (h : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, P.Factors f → Q.Factors f) : P ⊓ Q = P := +theorem inf_eq_of_isDetecting [HasPullbacks C] {𝒢 : ObjectProperty C} (h𝒢 : 𝒢.IsDetecting) {X : C} + (P Q : Subobject X) (h : ∀ (G : C) (_ : 𝒢 G), ∀ {f : G ⟶ X}, P.Factors f → Q.Factors f) : + P ⊓ Q = P := eq_of_le_of_isDetecting h𝒢 _ _ _root_.inf_le_left fun _ hG _ hf => (inf_factors _).2 ⟨hf, h _ hG hf⟩ -theorem eq_of_isDetecting [HasPullbacks C] {𝒢 : Set C} (h𝒢 : IsDetecting 𝒢) {X : C} - (P Q : Subobject X) (h : ∀ G ∈ 𝒢, ∀ {f : G ⟶ X}, P.Factors f ↔ Q.Factors f) : P = Q := +theorem eq_of_isDetecting [HasPullbacks C] {𝒢 : ObjectProperty C} (h𝒢 : 𝒢.IsDetecting) {X : C} + (P Q : Subobject X) (h : ∀ (G : C) (_ : 𝒢 G), + ∀ {f : G ⟶ X}, P.Factors f ↔ Q.Factors f) : P = Q := calc P = P ⊓ Q := Eq.symm <| inf_eq_of_isDetecting h𝒢 _ _ fun G hG _ hf => (h G hG).1 hf _ = Q ⊓ P := inf_comm .. @@ -352,12 +386,13 @@ theorem eq_of_isDetecting [HasPullbacks C] {𝒢 : Set C} (h𝒢 : IsDetecting end Subobject /-- A category with pullbacks and a small detecting set is well-powered. -/ -theorem wellPowered_of_isDetecting [HasPullbacks C] {𝒢 : Set C} [Small.{w} 𝒢] - [LocallySmall.{w} C] (h𝒢 : IsDetecting 𝒢) : WellPowered.{w} C := - ⟨fun X => - @small_of_injective _ _ _ (fun P : Subobject X => { f : Σ G : 𝒢, G.1 ⟶ X | P.Factors f.2 }) +theorem wellPowered_of_isDetecting [HasPullbacks C] {𝒢 : ObjectProperty C} + [ObjectProperty.Small.{w} 𝒢] [LocallySmall.{w} C] + (h𝒢 : 𝒢.IsDetecting) : WellPowered.{w} C where + subobject_small X := small_of_injective + (f := fun P : Subobject X => { f : Σ G : Subtype 𝒢, G.1 ⟶ X | P.Factors f.2 }) fun P Q h => Subobject.eq_of_isDetecting h𝒢 _ _ - (by simpa [Set.ext_iff, Sigma.forall] using h)⟩ + (by simpa [Set.ext_iff, Sigma.forall] using h) end WellPowered @@ -365,9 +400,9 @@ namespace StructuredArrow variable (S : D) (T : C ⥤ D) -theorem isCoseparating_proj_preimage {𝒢 : Set C} (h𝒢 : IsCoseparating 𝒢) : - IsCoseparating ((proj S T).obj ⁻¹' 𝒢) := by - refine fun X Y f g hfg => ext _ _ (h𝒢 _ _ fun G hG h => ?_) +theorem isCoseparating_inverseImage_proj {P : ObjectProperty C} (hP : P.IsCoseparating) : + (P.inverseImage (proj S T)).IsCoseparating := by + refine fun X Y f g hfg => ext _ _ (hP _ _ fun G hG h => ?_) exact congr_arg CommaMorphism.right (hfg (mk (Y.hom ≫ T.map h)) hG (homMk h rfl)) end StructuredArrow @@ -376,87 +411,90 @@ namespace CostructuredArrow variable (S : C ⥤ D) (T : D) -theorem isSeparating_proj_preimage {𝒢 : Set C} (h𝒢 : IsSeparating 𝒢) : - IsSeparating ((proj S T).obj ⁻¹' 𝒢) := by - refine fun X Y f g hfg => ext _ _ (h𝒢 _ _ fun G hG h => ?_) +theorem isSeparating_inverseImage_proj {P : ObjectProperty C} (hP : P.IsSeparating) : + (P.inverseImage (proj S T)).IsSeparating := by + refine fun X Y f g hfg => ext _ _ (hP _ _ fun G hG h => ?_) exact congr_arg CommaMorphism.left (hfg (mk (S.map h ≫ X.hom)) hG (homMk h rfl)) end CostructuredArrow /-- We say that `G` is a separator if the functor `C(G, -)` is faithful. -/ def IsSeparator (G : C) : Prop := - IsSeparating ({G} : Set C) + ObjectProperty.IsSeparating (.singleton G) /-- We say that `G` is a coseparator if the functor `C(-, G)` is faithful. -/ def IsCoseparator (G : C) : Prop := - IsCoseparating ({G} : Set C) + ObjectProperty.IsCoseparating (.singleton G) /-- We say that `G` is a detector if the functor `C(G, -)` reflects isomorphisms. -/ def IsDetector (G : C) : Prop := - IsDetecting ({G} : Set C) + ObjectProperty.IsDetecting (.singleton G) /-- We say that `G` is a codetector if the functor `C(-, G)` reflects isomorphisms. -/ def IsCodetector (G : C) : Prop := - IsCodetecting ({G} : Set C) - + ObjectProperty.IsCodetecting (.singleton G) section Equivalence theorem IsSeparator.of_equivalence {G : C} (h : IsSeparator G) (α : C ≌ D) : - IsSeparator (α.functor.obj G) := by simpa using IsSeparating.of_equivalence h α + IsSeparator (α.functor.obj G) := by + simpa using ObjectProperty.IsSeparating.of_equivalence h α theorem IsCoseparator.of_equivalence {G : C} (h : IsCoseparator G) (α : C ≌ D) : - IsCoseparator (α.functor.obj G) := by simpa using IsCoseparating.of_equivalence h α + IsCoseparator (α.functor.obj G) := by + simpa using ObjectProperty.IsCoseparating.of_equivalence h α end Equivalence section Dual +open ObjectProperty + theorem isSeparator_op_iff (G : C) : IsSeparator (op G) ↔ IsCoseparator G := by - rw [IsSeparator, IsCoseparator, ← isSeparating_op_iff, Set.singleton_op] + rw [IsSeparator, IsCoseparator, ← isSeparating_op_iff, op_singleton] theorem isCoseparator_op_iff (G : C) : IsCoseparator (op G) ↔ IsSeparator G := by - rw [IsSeparator, IsCoseparator, ← isCoseparating_op_iff, Set.singleton_op] + rw [IsSeparator, IsCoseparator, ← isCoseparating_op_iff, op_singleton] theorem isCoseparator_unop_iff (G : Cᵒᵖ) : IsCoseparator (unop G) ↔ IsSeparator G := by - rw [IsSeparator, IsCoseparator, ← isCoseparating_unop_iff, Set.singleton_unop] + rw [IsSeparator, IsCoseparator, ← isCoseparating_unop_iff, unop_singleton] theorem isSeparator_unop_iff (G : Cᵒᵖ) : IsSeparator (unop G) ↔ IsCoseparator G := by - rw [IsSeparator, IsCoseparator, ← isSeparating_unop_iff, Set.singleton_unop] + rw [IsSeparator, IsCoseparator, ← isSeparating_unop_iff, unop_singleton] theorem isDetector_op_iff (G : C) : IsDetector (op G) ↔ IsCodetector G := by - rw [IsDetector, IsCodetector, ← isDetecting_op_iff, Set.singleton_op] + rw [IsDetector, IsCodetector, ← isDetecting_op_iff, op_singleton] theorem isCodetector_op_iff (G : C) : IsCodetector (op G) ↔ IsDetector G := by - rw [IsDetector, IsCodetector, ← isCodetecting_op_iff, Set.singleton_op] + rw [IsDetector, IsCodetector, ← isCodetecting_op_iff, op_singleton] theorem isCodetector_unop_iff (G : Cᵒᵖ) : IsCodetector (unop G) ↔ IsDetector G := by - rw [IsDetector, IsCodetector, ← isCodetecting_unop_iff, Set.singleton_unop] + rw [IsDetector, IsCodetector, ← isCodetecting_unop_iff, unop_singleton] theorem isDetector_unop_iff (G : Cᵒᵖ) : IsDetector (unop G) ↔ IsCodetector G := by - rw [IsDetector, IsCodetector, ← isDetecting_unop_iff, Set.singleton_unop] + rw [IsDetector, IsCodetector, ← isDetecting_unop_iff, unop_singleton] end Dual theorem IsDetector.isSeparator [HasEqualizers C] {G : C} : IsDetector G → IsSeparator G := - IsDetecting.isSeparating + ObjectProperty.IsDetecting.isSeparating theorem IsCodetector.isCoseparator [HasCoequalizers C] {G : C} : IsCodetector G → IsCoseparator G := - IsCodetecting.isCoseparating + ObjectProperty.IsCodetecting.isCoseparating theorem IsSeparator.isDetector [Balanced C] {G : C} : IsSeparator G → IsDetector G := - IsSeparating.isDetecting + ObjectProperty.IsSeparating.isDetecting theorem IsCoseparator.isCodetector [Balanced C] {G : C} : IsCoseparator G → IsCodetector G := - IsCoseparating.isCodetecting + ObjectProperty.IsCoseparating.isCodetecting theorem isSeparator_def (G : C) : IsSeparator G ↔ ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ h : G ⟶ X, h ≫ f = h ≫ g) → f = g := ⟨fun hG X Y f g hfg => hG _ _ fun H hH h => by - obtain rfl := Set.mem_singleton_iff.1 hH + obtain rfl := (ObjectProperty.singleton_iff _ _).1 hH exact hfg h, - fun hG _ _ _ _ hfg => hG _ _ fun _ => hfg _ (Set.mem_singleton _) _⟩ + fun hG _ _ _ _ hfg => hG _ _ fun _ => hfg _ (by simp) _⟩ theorem IsSeparator.def {G : C} : IsSeparator G → ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ h : G ⟶ X, h ≫ f = h ≫ g) → f = g := @@ -466,9 +504,9 @@ theorem isCoseparator_def (G : C) : IsCoseparator G ↔ ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ h : Y ⟶ G, f ≫ h = g ≫ h) → f = g := ⟨fun hG X Y f g hfg => hG _ _ fun H hH h => by - obtain rfl := Set.mem_singleton_iff.1 hH + obtain rfl := (ObjectProperty.singleton_iff _ _).1 hH exact hfg h, - fun hG _ _ _ _ hfg => hG _ _ fun _ => hfg _ (Set.mem_singleton _) _⟩ + fun hG _ _ _ _ hfg => hG _ _ fun _ => hfg _ (by simp) _⟩ theorem IsCoseparator.def {G : C} : IsCoseparator G → ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ h : Y ⟶ G, f ≫ h = g ≫ h) → f = g := @@ -478,9 +516,9 @@ theorem isDetector_def (G : C) : IsDetector G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ h : G ⟶ Y, ∃! h', h' ≫ f = h) → IsIso f := ⟨fun hG X Y f hf => hG _ fun H hH h => by - obtain rfl := Set.mem_singleton_iff.1 hH + obtain rfl := (ObjectProperty.singleton_iff _ _).1 hH exact hf h, - fun hG _ _ _ hf => hG _ fun _ => hf _ (Set.mem_singleton _) _⟩ + fun hG _ _ _ hf => hG _ fun _ => hf _ (by simp) _⟩ theorem IsDetector.def {G : C} : IsDetector G → ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ h : G ⟶ Y, ∃! h', h' ≫ f = h) → IsIso f := @@ -490,9 +528,9 @@ theorem isCodetector_def (G : C) : IsCodetector G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ h : X ⟶ G, ∃! h', f ≫ h' = h) → IsIso f := ⟨fun hG X Y f hf => hG _ fun H hH h => by - obtain rfl := Set.mem_singleton_iff.1 hH + obtain rfl := (ObjectProperty.singleton_iff _ _).1 hH exact hf h, - fun hG _ _ _ hf => hG _ fun _ => hf _ (Set.mem_singleton _) _⟩ + fun hG _ _ _ hf => hG _ fun _ => hf _ (by simp) _⟩ theorem IsCodetector.def {G : C} : IsCodetector G → ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ h : X ⟶ G, ∃! h', f ≫ h' = h) → IsIso f := @@ -530,81 +568,92 @@ section ZeroMorphisms variable [HasZeroMorphisms C] +lemma isSeparator_of_isColimit_cofan {β : Type w} {f : β → C} + (hf : ObjectProperty.IsSeparating (.ofObj f)) {c : Cofan f} (hc : IsColimit c) : + IsSeparator c.pt := by + rw [isSeparator_def] + refine fun _ _ _ _ huv ↦ hf _ _ (fun _ h g ↦ ?_) + obtain ⟨b⟩ := h + classical simpa using c.inj b ≫= huv (hc.desc (Cofan.mk _ (Pi.single b g))) + +lemma isSeparator_iff_of_isColimit_cofan {β : Type w} {f : β → C} + {c : Cofan f} (hc : IsColimit c) : + IsSeparator c.pt ↔ ObjectProperty.IsSeparating (.ofObj f) := by + refine ⟨fun h X Y u v huv => ?_, fun h => isSeparator_of_isColimit_cofan h hc⟩ + refine h.def _ _ fun g => hc.hom_ext fun b => ?_ + simpa using huv (f b.as) (by simp) (c.inj _ ≫ g) + +theorem isSeparator_sigma {β : Type w} (f : β → C) [HasCoproduct f] : + IsSeparator (∐ f) ↔ ObjectProperty.IsSeparating (.ofObj f) := + isSeparator_iff_of_isColimit_cofan (hc := colimit.isColimit _) + theorem isSeparator_coprod (G H : C) [HasBinaryCoproduct G H] : - IsSeparator (G ⨿ H) ↔ IsSeparating ({G, H} : Set C) := by - refine - ⟨fun h X Y u v huv => ?_, fun h => - (isSeparator_def _).2 fun X Y u v huv => h _ _ fun Z hZ g => ?_⟩ - · refine h.def _ _ fun g => coprod.hom_ext ?_ ?_ - · simpa using huv G (by simp) (coprod.inl ≫ g) - · simpa using huv H (by simp) (coprod.inr ≫ g) - · simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hZ - rcases hZ with (rfl | rfl) - · simpa using coprod.inl ≫= huv (coprod.desc g 0) - · simpa using coprod.inr ≫= huv (coprod.desc 0 g) + IsSeparator (G ⨿ H) ↔ ObjectProperty.IsSeparating (.pair G H) := by + refine (isSeparator_iff_of_isColimit_cofan (coprodIsCoprod G H)).trans ?_ + convert Iff.rfl + ext X + simp only [ObjectProperty.pair_iff, ObjectProperty.ofObj_iff] + constructor + · rintro (rfl | rfl); exacts [⟨.left, rfl⟩, ⟨.right, rfl⟩] + · rintro ⟨⟨_ | _⟩, rfl⟩ <;> tauto theorem isSeparator_coprod_of_isSeparator_left (G H : C) [HasBinaryCoproduct G H] (hG : IsSeparator G) : IsSeparator (G ⨿ H) := - (isSeparator_coprod _ _).2 <| IsSeparating.mono hG <| by simp + (isSeparator_coprod _ _).2 <| ObjectProperty.IsSeparating.of_le hG <| by simp theorem isSeparator_coprod_of_isSeparator_right (G H : C) [HasBinaryCoproduct G H] (hH : IsSeparator H) : IsSeparator (G ⨿ H) := - (isSeparator_coprod _ _).2 <| IsSeparating.mono hH <| by simp - -lemma isSeparator_of_isColimit_cofan {β : Type w} {f : β → C} - (hf : IsSeparating (Set.range f)) {c : Cofan f} (hc : IsColimit c) : IsSeparator c.pt := by - refine (isSeparator_def _).2 fun X Y u v huv => hf _ _ fun Z hZ g => ?_ - obtain ⟨b, rfl⟩ := Set.mem_range.1 hZ - classical simpa using c.ι.app ⟨b⟩ ≫= huv (hc.desc (Cofan.mk _ (Pi.single b g))) - -theorem isSeparator_sigma {β : Type w} (f : β → C) [HasCoproduct f] : - IsSeparator (∐ f) ↔ IsSeparating (Set.range f) := by - refine ⟨fun h X Y u v huv => ?_, fun h => isSeparator_of_isColimit_cofan h (colimit.isColimit _)⟩ - refine h.def _ _ fun g => colimit.hom_ext fun b => ?_ - simpa using huv (f b.as) (by simp) (colimit.ι (Discrete.functor f) _ ≫ g) + (isSeparator_coprod _ _).2 <| ObjectProperty.IsSeparating.of_le hH <| by simp -theorem IsSeparating.isSeparator_coproduct {β : Type w} {f : β → C} [HasCoproduct f] - (hS : IsSeparating (Set.range f)) : IsSeparator (∐ f) := +theorem ObjectProperty.IsSeparating.isSeparator_coproduct + {β : Type w} {f : β → C} [HasCoproduct f] + (hS : ObjectProperty.IsSeparating (.ofObj f)) : IsSeparator (∐ f) := (isSeparator_sigma _).2 hS theorem isSeparator_sigma_of_isSeparator {β : Type w} (f : β → C) [HasCoproduct f] (b : β) (hb : IsSeparator (f b)) : IsSeparator (∐ f) := - (isSeparator_sigma _).2 <| IsSeparating.mono hb <| by simp + (isSeparator_sigma _).2 <| ObjectProperty.IsSeparating.of_le hb <| by simp + +lemma isCoseparator_of_isLimit_fan {β : Type w} {f : β → C} + (hf : ObjectProperty.IsCoseparating (.ofObj f)) {c : Fan f} (hc : IsLimit c) : + IsCoseparator c.pt := by + rw [isCoseparator_def] + refine fun _ _ _ _ huv ↦ hf _ _ (fun _ h g ↦ ?_) + obtain ⟨b⟩ := h + classical simpa using huv (hc.lift (Fan.mk _ (Pi.single b g))) =≫ c.proj b + +lemma isCoseparator_iff_of_isLimit_fan {β : Type w} {f : β → C} + {c : Fan f} (hc : IsLimit c) : + IsCoseparator c.pt ↔ ObjectProperty.IsCoseparating (.ofObj f) := by + refine ⟨fun h X Y u v huv => ?_, fun h => isCoseparator_of_isLimit_fan h hc⟩ + refine h.def _ _ fun g => hc.hom_ext fun b => ?_ + simpa using huv (f b.as) (by simp) (g ≫ c.proj _) + +theorem isCoseparator_pi {β : Type w} (f : β → C) [HasProduct f] : + IsCoseparator (∏ᶜ f) ↔ ObjectProperty.IsCoseparating (.ofObj f) := + isCoseparator_iff_of_isLimit_fan (hc := limit.isLimit _) theorem isCoseparator_prod (G H : C) [HasBinaryProduct G H] : - IsCoseparator (G ⨯ H) ↔ IsCoseparating ({G, H} : Set C) := by - refine - ⟨fun h X Y u v huv => ?_, fun h => - (isCoseparator_def _).2 fun X Y u v huv => h _ _ fun Z hZ g => ?_⟩ - · refine h.def _ _ fun g => Limits.prod.hom_ext ?_ ?_ - · simpa using huv G (by simp) (g ≫ Limits.prod.fst) - · simpa using huv H (by simp) (g ≫ Limits.prod.snd) - · simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hZ - rcases hZ with (rfl | rfl) - · simpa using huv (prod.lift g 0) =≫ Limits.prod.fst - · simpa using huv (prod.lift 0 g) =≫ Limits.prod.snd + IsCoseparator (G ⨯ H) ↔ ObjectProperty.IsCoseparating (.pair G H) := by + refine (isCoseparator_iff_of_isLimit_fan (prodIsProd G H)).trans ?_ + convert Iff.rfl + ext X + simp only [ObjectProperty.pair_iff, ObjectProperty.ofObj_iff] + constructor + · rintro (rfl | rfl); exacts [⟨.left, rfl⟩, ⟨.right, rfl⟩] + · rintro ⟨⟨_ | _⟩, rfl⟩ <;> tauto theorem isCoseparator_prod_of_isCoseparator_left (G H : C) [HasBinaryProduct G H] (hG : IsCoseparator G) : IsCoseparator (G ⨯ H) := - (isCoseparator_prod _ _).2 <| IsCoseparating.mono hG <| by simp + (isCoseparator_prod _ _).2 <| ObjectProperty.IsCoseparating.of_le hG <| by simp theorem isCoseparator_prod_of_isCoseparator_right (G H : C) [HasBinaryProduct G H] (hH : IsCoseparator H) : IsCoseparator (G ⨯ H) := - (isCoseparator_prod _ _).2 <| IsCoseparating.mono hH <| by simp - -theorem isCoseparator_pi {β : Type w} (f : β → C) [HasProduct f] : - IsCoseparator (∏ᶜ f) ↔ IsCoseparating (Set.range f) := by - refine - ⟨fun h X Y u v huv => ?_, fun h => - (isCoseparator_def _).2 fun X Y u v huv => h _ _ fun Z hZ g => ?_⟩ - · refine h.def _ _ fun g => limit.hom_ext fun b => ?_ - simpa using huv (f b.as) (by simp) (g ≫ limit.π (Discrete.functor f) _) - · obtain ⟨b, rfl⟩ := Set.mem_range.1 hZ - classical simpa using huv (Pi.lift (Pi.single b g)) =≫ Pi.π f b + (isCoseparator_prod _ _).2 <| ObjectProperty.IsCoseparating.of_le hH <| by simp theorem isCoseparator_pi_of_isCoseparator {β : Type w} (f : β → C) [HasProduct f] (b : β) (hb : IsCoseparator (f b)) : IsCoseparator (∏ᶜ f) := - (isCoseparator_pi _).2 <| IsCoseparating.mono hb <| by simp + (isCoseparator_pi _).2 <| ObjectProperty.IsCoseparating.of_le hb <| by simp end ZeroMorphisms @@ -820,4 +869,79 @@ end Dual end HasGenerator +@[deprecated (since := "2025-10-06")] alias IsSeparating := ObjectProperty.IsSeparating +@[deprecated (since := "2025-10-06")] alias IsCoseparating := ObjectProperty.IsCoseparating +@[deprecated (since := "2025-10-06")] alias IsDetecting := ObjectProperty.IsDetecting +@[deprecated (since := "2025-10-06")] alias IsCodetecting := ObjectProperty.IsCodetecting +@[deprecated (since := "2025-10-06")] alias IsSeparating.of_equivalence := + ObjectProperty.IsSeparating.of_equivalence +@[deprecated (since := "2025-10-06")] alias IsCoseparating.of_equivalence := + ObjectProperty.IsCoseparating.of_equivalence +@[deprecated (since := "2025-10-06")] alias isSeparating_op_iff := + ObjectProperty.isSeparating_op_iff +@[deprecated (since := "2025-10-06")] alias isCoseparating_op_iff := + ObjectProperty.isCoseparating_op_iff +@[deprecated (since := "2025-10-06")] alias isSeparating_unop_iff := + ObjectProperty.isSeparating_op_iff +@[deprecated (since := "2025-10-06")] alias isCoseparating_unop_iff := + ObjectProperty.isCoseparating_op_iff +@[deprecated (since := "2025-10-06")] alias isDetecting_op_iff := + ObjectProperty.isDetecting_op_iff +@[deprecated (since := "2025-10-06")] alias isCodetecting_op_iff := + ObjectProperty.isCodetecting_op_iff +@[deprecated (since := "2025-10-06")] alias isDetecting_unop_iff := + ObjectProperty.isDetecting_op_iff +@[deprecated (since := "2025-10-06")] alias isCodetecting_unop_iff := + ObjectProperty.isCodetecting_op_iff +@[deprecated (since := "2025-10-06")] alias IsDetecting.isSeparating := + ObjectProperty.IsDetecting.isSeparating +@[deprecated (since := "2025-10-06")] alias IsCodetecting.isCoseparating := + ObjectProperty.IsCodetecting.isCoseparating +@[deprecated (since := "2025-10-06")] alias IsSeparating.isDetecting := + ObjectProperty.IsSeparating.isDetecting +@[deprecated (since := "2025-10-06")] alias IsDetecting.isIso_iff_of_mono := + ObjectProperty.IsDetecting.isIso_iff_of_mono +@[deprecated (since := "2025-10-06")] alias IsCodetecting.isIso_iff_of_epi := + ObjectProperty.IsCodetecting.isIso_iff_of_epi +@[deprecated (since := "2025-10-06")] alias IsCoseparating.isCodetecting := + ObjectProperty.IsCoseparating.isCodetecting +@[deprecated (since := "2025-10-06")] alias isDetecting_iff_isSeparating := + ObjectProperty.isDetecting_iff_isSeparating +@[deprecated (since := "2025-10-06")] alias isCodetecting_iff_isCoseparating := + ObjectProperty.isCodetecting_iff_isCoseparating +@[deprecated (since := "2025-10-06")] alias IsSeparating.mono := + ObjectProperty.IsSeparating.of_le +@[deprecated (since := "2025-10-06")] alias IsCoseparating.mono := + ObjectProperty.IsCoseparating.of_le +@[deprecated (since := "2025-10-06")] alias IsDetecting.mono := + ObjectProperty.IsDetecting.of_le +@[deprecated (since := "2025-10-06")] alias IsCodetecting.mono := + ObjectProperty.IsCodetecting.of_le +@[deprecated (since := "2025-10-06")] alias thin_of_isSeparating_empty := + ObjectProperty.isThin_of_isSeparating_bot +@[deprecated (since := "2025-10-06")] alias isSeparating_empty_of_thin := + ObjectProperty.isSeparating_bot_of_isThin +@[deprecated (since := "2025-10-06")] alias thin_of_isCoseparating_empty := + ObjectProperty.isThin_of_isCoseparating_bot +@[deprecated (since := "2025-10-06")] alias isCoseparating_empty_of_thin := + ObjectProperty.isCoseparating_bot_of_isThin +@[deprecated (since := "2025-10-06")] alias groupoid_of_isDetecting_empty := + ObjectProperty.isGroupoid_of_isDetecting_bot +@[deprecated (since := "2025-10-06")] alias isDetecting_empty_of_groupoid := + ObjectProperty.isDetecting_bot_of_isGroupoid +@[deprecated (since := "2025-10-06")] alias groupoid_of_isCodetecting_empty := + ObjectProperty.isGroupoid_of_isCodetecting_bot +@[deprecated (since := "2025-10-06")] alias isCodetecting_empty_of_groupoid := + ObjectProperty.isCodetecting_bot_of_isGroupoid +@[deprecated (since := "2025-10-07")] alias isSeparating_iff_epi := + ObjectProperty.isSeparating_iff_epi +@[deprecated (since := "2025-10-07")] alias isCoseparating_iff_mono := + ObjectProperty.isCoseparating_iff_mono +@[deprecated (since := "2025-10-07")] alias IsSeparating.isSeparator_coproduct := + ObjectProperty.IsSeparating.isSeparator_coproduct +@[deprecated (since := "2025-10-07")] alias StructuredArrow.isCoseparating_proj_preimage := + StructuredArrow.isCoseparating_inverseImage_proj +@[deprecated (since := "2025-10-07")] alias CostructuredArrow.isSeparating_proj_preimage := + CostructuredArrow.isSeparating_inverseImage_proj + end CategoryTheory diff --git a/Mathlib/CategoryTheory/Generator/HomologicalComplex.lean b/Mathlib/CategoryTheory/Generator/HomologicalComplex.lean index cd3b90df9e64ef..0c99e234af2548 100644 --- a/Mathlib/CategoryTheory/Generator/HomologicalComplex.lean +++ b/Mathlib/CategoryTheory/Generator/HomologicalComplex.lean @@ -28,7 +28,7 @@ section variable [HasZeroMorphisms C] [HasZeroObject C] -variable {α : Type t} {X : α → C} (hX : IsSeparating (Set.range X)) +variable {α : Type t} {X : α → C} (hX : ObjectProperty.IsSeparating (.ofObj X)) variable (X) in /-- If `X : α → C` is a separating family, and `c : ComplexShape ι` has no loop, @@ -40,14 +40,15 @@ noncomputable def separatingFamily (j : α × ι) : HomologicalComplex C c := include hX in lemma isSeparating_separatingFamily : - IsSeparating (Set.range (separatingFamily c X)) := by + ObjectProperty.IsSeparating (.ofObj (separatingFamily c X)) := by intro K L f g h ext j apply hX - rintro _ ⟨a, rfl⟩ p + rintro _ ⟨a⟩ p have H := evalCompCoyonedaCorepresentable c (X a) j apply H.homEquiv.symm.injective - simpa only [H.homEquiv_symm_comp] using h _ ⟨⟨a, j⟩, rfl⟩ (H.homEquiv.symm p) + simpa only [H.homEquiv_symm_comp] using h _ + (ObjectProperty.ofObj_apply _ ⟨a, j⟩) (H.homEquiv.symm p) end diff --git a/Mathlib/CategoryTheory/Generator/Indization.lean b/Mathlib/CategoryTheory/Generator/Indization.lean index 370e9ed144d900..21a5ad8435b28c 100644 --- a/Mathlib/CategoryTheory/Generator/Indization.lean +++ b/Mathlib/CategoryTheory/Generator/Indization.lean @@ -25,7 +25,8 @@ section variable {C : Type u} [Category.{v} C] -theorem Ind.isSeparating_range_yoneda : IsSeparating (Set.range (Ind.yoneda : C ⥤ _).obj) := by +theorem Ind.isSeparating_range_yoneda : + ObjectProperty.IsSeparating (.ofObj (Ind.yoneda : C ⥤ _).obj) := by refine fun X Y f g h => (cancel_epi (Ind.colimitPresentationCompYoneda X).hom).1 ?_ exact colimit.hom_ext (fun i => by simp [← Category.assoc, h]) diff --git a/Mathlib/CategoryTheory/Generator/Preadditive.lean b/Mathlib/CategoryTheory/Generator/Preadditive.lean index 8e30fa00586bfa..c948742f130c8f 100644 --- a/Mathlib/CategoryTheory/Generator/Preadditive.lean +++ b/Mathlib/CategoryTheory/Generator/Preadditive.lean @@ -17,19 +17,21 @@ preadditive categories. universe v u -open CategoryTheory Opposite +open CategoryTheory Opposite ObjectProperty namespace CategoryTheory variable {C : Type u} [Category.{v} C] [Preadditive C] -theorem Preadditive.isSeparating_iff (𝒢 : Set C) : - IsSeparating 𝒢 ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ G ∈ 𝒢, ∀ (h : G ⟶ X), h ≫ f = 0) → f = 0 := +theorem Preadditive.isSeparating_iff (P : ObjectProperty C) : + P.IsSeparating ↔ + ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (G : C) (_ : P G), ∀ (h : G ⟶ X), h ≫ f = 0) → f = 0 := ⟨fun h𝒢 X Y f hf => h𝒢 _ _ (by simpa only [Limits.comp_zero] using hf), fun h𝒢 X Y f g hfg => sub_eq_zero.1 <| h𝒢 _ (by simpa only [Preadditive.comp_sub, sub_eq_zero] using hfg)⟩ -theorem Preadditive.isCoseparating_iff (𝒢 : Set C) : - IsCoseparating 𝒢 ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ G ∈ 𝒢, ∀ (h : Y ⟶ G), f ≫ h = 0) → f = 0 := +theorem Preadditive.isCoseparating_iff (P : ObjectProperty C) : + P.IsCoseparating ↔ + ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (G : C) (_ : P G), ∀ (h : Y ⟶ G), f ≫ h = 0) → f = 0 := ⟨fun h𝒢 X Y f hf => h𝒢 _ _ (by simpa only [Limits.zero_comp] using hf), fun h𝒢 X Y f g hfg => sub_eq_zero.1 <| h𝒢 _ (by simpa only [Preadditive.sub_comp, sub_eq_zero] using hfg)⟩ diff --git a/Mathlib/CategoryTheory/Generator/Presheaf.lean b/Mathlib/CategoryTheory/Generator/Presheaf.lean index 61042589d44a2e..8fc01993932da9 100644 --- a/Mathlib/CategoryTheory/Generator/Presheaf.lean +++ b/Mathlib/CategoryTheory/Generator/Presheaf.lean @@ -63,17 +63,17 @@ lemma freeYonedaHomEquiv_symm_comp {X : C} {M : A} {F G : Cᵒᵖ ⥤ A} (α : M variable (C) -lemma isSeparating {ι : Type w} {S : ι → A} (hS : IsSeparating (Set.range S)) : - IsSeparating (Set.range (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda X (S i))) := by +lemma isSeparating {ι : Type w} {S : ι → A} (hS : ObjectProperty.IsSeparating (.ofObj S)) : + ObjectProperty.IsSeparating (.ofObj (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda X (S i))) := by intro F G f g h ext ⟨X⟩ refine hS _ _ ?_ - rintro _ ⟨i, rfl⟩ α + rintro _ ⟨i⟩ α apply freeYonedaHomEquiv.symm.injective simpa only [freeYonedaHomEquiv_symm_comp] using - h _ ⟨⟨X, i⟩, rfl⟩ (freeYonedaHomEquiv.symm α) + h _ (ObjectProperty.ofObj_apply _ ⟨X, i⟩) (freeYonedaHomEquiv.symm α) -lemma isSeparator {ι : Type w} {S : ι → A} (hS : IsSeparating (Set.range S)) +lemma isSeparator {ι : Type w} {S : ι → A} (hS : ObjectProperty.IsSeparating (.ofObj S)) [HasCoproduct (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda X (S i))] [HasZeroMorphisms A] : IsSeparator (∐ (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda X (S i))) := diff --git a/Mathlib/CategoryTheory/Generator/Sheaf.lean b/Mathlib/CategoryTheory/Generator/Sheaf.lean index 5539908fff9819..bd7f0862ce4c53 100644 --- a/Mathlib/CategoryTheory/Generator/Sheaf.lean +++ b/Mathlib/CategoryTheory/Generator/Sheaf.lean @@ -40,16 +40,17 @@ noncomputable def freeYonedaHomEquiv {X : C} {M : A} {F : Sheaf J A} : (freeYoneda J X M ⟶ F) ≃ (M ⟶ F.val.obj (op X)) := ((sheafificationAdjunction J A).homEquiv _ _).trans Presheaf.freeYonedaHomEquiv -lemma isSeparating {ι : Type w} {S : ι → A} (hS : IsSeparating (Set.range S)) : - IsSeparating (Set.range (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda J X (S i))) := by +lemma isSeparating {ι : Type w} {S : ι → A} (hS : ObjectProperty.IsSeparating (.ofObj S)) : + ObjectProperty.IsSeparating (.ofObj (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda J X (S i))) := by intro F G f g hfg refine (sheafToPresheaf J A).map_injective (Presheaf.isSeparating C hS _ _ ?_) - rintro _ ⟨⟨X, i⟩, rfl⟩ a + rintro _ ⟨X, i⟩ a apply ((sheafificationAdjunction _ _).homEquiv _ _).symm.injective simpa only [← Adjunction.homEquiv_naturality_right_symm] using - hfg _ ⟨⟨X, i⟩, rfl⟩ (((sheafificationAdjunction _ _).homEquiv _ _).symm a) + hfg _ (ObjectProperty.ofObj_apply _ ⟨X, i⟩) + (((sheafificationAdjunction _ _).homEquiv _ _).symm a) -lemma isSeparator {ι : Type w} {S : ι → A} (hS : IsSeparating (Set.range S)) +lemma isSeparator {ι : Type w} {S : ι → A} (hS : ObjectProperty.IsSeparating (.ofObj S)) [HasCoproduct (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda J X (S i))] [Preadditive A] : IsSeparator (∐ (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda J X (S i))) := (isSeparating J hS).isSeparator_coproduct