From 9a0751d25533db972f207d423eb054f6e3e9e7c9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Mon, 6 Oct 2025 15:59:30 +0200 Subject: [PATCH 01/14] refactor(CategoryTheory/Generator): use ObjectProperty --- Mathlib.lean | 1 + Mathlib/CategoryTheory/Generator/Basic.lean | 324 +++++++++++------- .../CategoryTheory/ObjectProperty/Basic.lean | 36 ++ .../ObjectProperty/Opposite.lean | 76 ++++ 4 files changed, 320 insertions(+), 117 deletions(-) create mode 100644 Mathlib/CategoryTheory/ObjectProperty/Opposite.lean diff --git a/Mathlib.lean b/Mathlib.lean index 985f244b4c64f4..afc86a026ab940 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2668,6 +2668,7 @@ import Mathlib.CategoryTheory.ObjectProperty.Extensions import Mathlib.CategoryTheory.ObjectProperty.FullSubcategory import Mathlib.CategoryTheory.ObjectProperty.Ind import Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape +import Mathlib.CategoryTheory.ObjectProperty.Opposite import Mathlib.CategoryTheory.ObjectProperty.Retract import Mathlib.CategoryTheory.ObjectProperty.Shift import Mathlib.CategoryTheory.ObjectProperty.Small diff --git a/Mathlib/CategoryTheory/Generator/Basic.lean b/Mathlib/CategoryTheory/Generator/Basic.lean index 6e3bc206804f39..f74bc6ae173673 100644 --- a/Mathlib/CategoryTheory/Generator/Basic.lean +++ b/Mathlib/CategoryTheory/Generator/Basic.lean @@ -6,6 +6,7 @@ Authors: Markus Himmel import Mathlib.CategoryTheory.Limits.EssentiallySmall import Mathlib.CategoryTheory.Limits.Opposites import Mathlib.CategoryTheory.Subobject.Lattice +import Mathlib.CategoryTheory.ObjectProperty.Opposite import Mathlib.Data.Set.Opposite /-! @@ -14,10 +15,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 +28,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 +48,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 +63,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 => + (h : IsSeparating P) {D : Type*} [Category D] (α : C ≌ D) : + IsSeparating (P.map α.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.prop_map_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 => + (h : IsCoseparating P) {D : Type*} [Category D] (α : C ≌ D) : + IsCoseparating (P.map α.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.prop_map_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,63 +226,65 @@ 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 @@ -820,4 +843,71 @@ end Dual end HasGenerator +end ObjectProperty + +@[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 + end CategoryTheory diff --git a/Mathlib/CategoryTheory/ObjectProperty/Basic.lean b/Mathlib/CategoryTheory/ObjectProperty/Basic.lean index 7cf7a47eb945ba..210309b1408ea0 100644 --- a/Mathlib/CategoryTheory/ObjectProperty/Basic.lean +++ b/Mathlib/CategoryTheory/ObjectProperty/Basic.lean @@ -66,6 +66,42 @@ lemma prop_of_is (P : ObjectProperty C) (X : C) [P.Is X] : P X := by rwa [← P. lemma is_of_prop (P : ObjectProperty C) {X : C} (hX : P X) : P.Is X := by rwa [P.is_iff] +section + +variable {ι : Type u'} (X : ι → C) + +/-- The property of objects that is satisfied by the `X i` for a family +of objects `X : ι : C`. -/ +inductive ofObj : ObjectProperty C + | mk (i : ι) : ofObj (X i) + +@[simp] +lemma prop_ofObj (i : ι) : ofObj X (X i) := ⟨i⟩ + +lemma ofObj_iff (Y : C) : ofObj X Y ↔ ∃ i, X i = Y := by + constructor + · rintro ⟨i⟩ + exact ⟨i, rfl⟩ + · rintro ⟨i, rfl⟩ + exact ⟨i⟩ + +lemma ofObj_le_iff (P : ObjectProperty C) : + ofObj X ≤ P ↔ ∀ i, P (X i) := + ⟨fun h i ↦ h _ (by simp), fun h ↦ by rintro _ ⟨i⟩; exact h i⟩ + +end + +/-- The property of objects in a category that is satisfying by a single object `X : C`. -/ +abbrev singleton (X : C) : ObjectProperty C := ofObj (fun (_ : Unit) ↦ X) + +@[simp] +lemma singleton_iff (X Y : C) : singleton X Y ↔ X = Y := by simp [ofObj_iff] + +@[simp] +lemma singleton_le_iff {X : C} {P : ObjectProperty C} : + singleton X ≤ P ↔ P X := by + simp [ofObj_le_iff] + end ObjectProperty end CategoryTheory diff --git a/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean b/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean new file mode 100644 index 00000000000000..a29ff32316363e --- /dev/null +++ b/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean @@ -0,0 +1,76 @@ +/- +Copyright (c) 2025 Joël Riou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joël Riou +-/ +import Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms +import Mathlib.CategoryTheory.Opposites + +/-! +# The opposite of a property of objects + +-/ + +universe v u + +namespace CategoryTheory.ObjectProperty + +open Opposite + +variable {C : Type u} [Category.{v} C] + +/-- The property of objects of `Cᵒᵖ` corresponding to `P : ObjectProperty C`. -/ +protected def op (P : ObjectProperty C) : ObjectProperty Cᵒᵖ := + fun X ↦ P X.unop + +/-- The property of objects of `C` corresponding to `P : ObjectProperty Cᵒᵖ`. -/ +protected def unop (P : ObjectProperty Cᵒᵖ) : ObjectProperty C := + fun X ↦ P (op X) + +@[simp] +lemma op_iff (P : ObjectProperty C) (X : Cᵒᵖ) : + P.op X ↔ P X.unop := Iff.rfl + +@[simp] +lemma unop_iff (P : ObjectProperty Cᵒᵖ) (X : C) : + P.unop X ↔ P (op X) := Iff.rfl + +@[simp] +lemma op_unop (P : ObjectProperty Cᵒᵖ) : P.unop.op = P := rfl + +@[simp] +lemma unop_op (P : ObjectProperty C) : P.op.unop = P := rfl + +lemma op_injective {P Q : ObjectProperty C} (h : P.op = Q.op) : P = Q := by + rw [← P.unop_op, ← Q.unop_op, h] + +lemma unop_injective {P Q : ObjectProperty Cᵒᵖ} (h : P.unop = Q.unop) : P = Q := by + rw [← P.op_unop, ← Q.op_unop, h] + +lemma op_injective_iff {P Q : ObjectProperty C} : + P.op = Q.op ↔ P = Q := + ⟨op_injective, by rintro rfl; rfl⟩ + +lemma unop_injective_iff {P Q : ObjectProperty Cᵒᵖ} : + P.unop = Q.unop ↔ P = Q := + ⟨unop_injective, by rintro rfl; rfl⟩ + +instance (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] : + P.op.IsClosedUnderIsomorphisms where + of_iso e hX := P.prop_of_iso e.symm.unop hX + +instance (P : ObjectProperty Cᵒᵖ) [P.IsClosedUnderIsomorphisms] : + P.unop.IsClosedUnderIsomorphisms where + of_iso e hX := P.prop_of_iso e.symm.op hX + +lemma isoClosure_op (P : ObjectProperty C) : + P.isoClosure.op = P.op.isoClosure := by + ext ⟨X⟩ + exact ⟨fun ⟨Y, h, ⟨e⟩⟩ ↦ ⟨op Y, h, ⟨e.op.symm⟩⟩, + fun ⟨Y, h, ⟨e⟩⟩ ↦ ⟨Y.unop, h, ⟨e.unop.symm⟩⟩⟩ + +lemma isoClosure_unop (P : ObjectProperty Cᵒᵖ) : + P.isoClosure.unop = P.unop.isoClosure := by + rw [← op_injective_iff, P.unop.isoClosure_op, op_unop, op_unop] + +end CategoryTheory.ObjectProperty From 13098da6ea4d70783760110dbd392b18370c944e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Tue, 7 Oct 2025 10:32:27 +0200 Subject: [PATCH 02/14] fix --- Mathlib/CategoryTheory/Generator/Basic.lean | 307 ++++++++++-------- .../CategoryTheory/ObjectProperty/Basic.lean | 41 ++- .../ObjectProperty/Opposite.lean | 30 ++ .../CategoryTheory/ObjectProperty/Small.lean | 17 + 4 files changed, 255 insertions(+), 140 deletions(-) diff --git a/Mathlib/CategoryTheory/Generator/Basic.lean b/Mathlib/CategoryTheory/Generator/Basic.lean index f74bc6ae173673..521c1c73de800c 100644 --- a/Mathlib/CategoryTheory/Generator/Basic.lean +++ b/Mathlib/CategoryTheory/Generator/Basic.lean @@ -6,8 +6,7 @@ Authors: Markus Himmel import Mathlib.CategoryTheory.Limits.EssentiallySmall import Mathlib.CategoryTheory.Limits.Opposites import Mathlib.CategoryTheory.Subobject.Lattice -import Mathlib.CategoryTheory.ObjectProperty.Opposite -import Mathlib.Data.Set.Opposite +import Mathlib.CategoryTheory.ObjectProperty.Small /-! # Separating and detecting sets @@ -101,20 +100,20 @@ variable {P} lemma IsSeparating.of_equivalence (h : IsSeparating P) {D : Type*} [Category D] (α : C ≌ D) : - IsSeparating (P.map α.functor) := fun X Y f g H => - α.inverse.map_injective (h _ _ (fun Z hZ h => by + 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 _ (P.prop_map_obj _ hZ) h'])) + H _ (P.prop_strictMap_obj _ hZ) h'])) lemma IsCoseparating.of_equivalence (h : IsCoseparating P) {D : Type*} [Category D] (α : C ≌ D) : - IsCoseparating (P.map α.functor) := fun X Y f g H => - α.inverse.map_injective (h _ _ (fun Z hZ h => by + 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 [Equivalence.symm_inverse, Equivalence.symm_functor, Adjunction.homEquiv_counit, ← Functor.map_comp_assoc, - H _ (P.prop_map_obj _ hZ) h'])) + H _ (P.prop_strictMap_obj _ hZ) h'])) end Equivalence @@ -288,24 +287,34 @@ lemma isCodetecting_bot_of_isGroupoid [IsGroupoid C] : 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 _ + +variable {P} /-- 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. @@ -313,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] [ObjectProperty.Small.{w} P] + (hP : IsCoseparating P) : 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 := (isCoseparating_iff_mono P).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 @@ -340,18 +349,20 @@ 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] [ObjectProperty.Small.{w} P] + (hP : IsSeparating P) : HasTerminal C := by + haveI : HasInitial Cᵒᵖ := hasInitial_of_isCoseparating ((isCoseparating_op_iff _).2 hP) exact hasTerminal_of_hasInitial_op +end ObjectProperty + 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⟩) @@ -360,13 +371,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 .. @@ -375,12 +388,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 @@ -388,9 +402,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_proj_preimage {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 @@ -399,87 +413,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_proj_preimage {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.prop_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 := @@ -489,9 +506,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.prop_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 := @@ -501,9 +518,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.prop_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 := @@ -513,9 +530,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.prop_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 := @@ -553,81 +570,91 @@ 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.prop_pair_iff, ObjectProperty.prop_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) := + (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.prop_pair_iff, ObjectProperty.prop_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 @@ -843,8 +870,6 @@ end Dual end HasGenerator -end ObjectProperty - @[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 @@ -909,5 +934,13 @@ end ObjectProperty 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 hasInitial_of_isCoseparating := + ObjectProperty.hasInitial_of_isCoseparating +@[deprecated (since := "2025-10-07")] alias hasTerminal_of_isSeparating := + ObjectProperty.hasTerminal_of_isSeparating end CategoryTheory diff --git a/Mathlib/CategoryTheory/ObjectProperty/Basic.lean b/Mathlib/CategoryTheory/ObjectProperty/Basic.lean index 210309b1408ea0..6f9454ea250227 100644 --- a/Mathlib/CategoryTheory/ObjectProperty/Basic.lean +++ b/Mathlib/CategoryTheory/ObjectProperty/Basic.lean @@ -57,6 +57,18 @@ lemma prop_map_obj (P : ObjectProperty C) (F : C ⥤ D) {X : C} (hX : P X) : P.map F (F.obj X) := ⟨X, hX, ⟨Iso.refl _⟩⟩ +/-- The strict image of a property of objects by a functor. -/ +inductive strictMap (P : ObjectProperty C) (F : C ⥤ D) : ObjectProperty D + | mk (X : C) (hX : P X) : strictMap P F (F.obj X) + +lemma prop_strictMap_iff (P : ObjectProperty C) (F : C ⥤ D) (Y : D) : + P.strictMap F Y ↔ ∃ (X : C), P X ∧ F.obj X = Y := + ⟨by rintro ⟨X, hX⟩; exact ⟨X, hX, rfl⟩, by rintro ⟨X, hX, rfl⟩; exact ⟨X, hX⟩⟩ + +lemma prop_strictMap_obj (P : ObjectProperty C) (F : C ⥤ D) {X : C} (hX : P X) : + P.strictMap F (F.obj X) := + ⟨X, hX⟩ + /-- The typeclass associated to `P : ObjectProperty C`. -/ @[mk_iff] class Is (P : ObjectProperty C) (X : C) : Prop where @@ -78,7 +90,7 @@ inductive ofObj : ObjectProperty C @[simp] lemma prop_ofObj (i : ι) : ofObj X (X i) := ⟨i⟩ -lemma ofObj_iff (Y : C) : ofObj X Y ↔ ∃ i, X i = Y := by +lemma prop_ofObj_iff (Y : C) : ofObj X Y ↔ ∃ i, X i = Y := by constructor · rintro ⟨i⟩ exact ⟨i, rfl⟩ @@ -89,19 +101,42 @@ lemma ofObj_le_iff (P : ObjectProperty C) : ofObj X ≤ P ↔ ∀ i, P (X i) := ⟨fun h i ↦ h _ (by simp), fun h ↦ by rintro _ ⟨i⟩; exact h i⟩ +@[simp] +lemma strictMap_ofObj (F : C ⥤ D) : + (ofObj X).strictMap F = ofObj (F.obj ∘ X) := by + ext Y + simp [prop_ofObj_iff, prop_strictMap_iff] + end -/-- The property of objects in a category that is satisfying by a single object `X : C`. -/ +/-- The property of objects in a category that is satisfied by a single object `X : C`. -/ abbrev singleton (X : C) : ObjectProperty C := ofObj (fun (_ : Unit) ↦ X) @[simp] -lemma singleton_iff (X Y : C) : singleton X Y ↔ X = Y := by simp [ofObj_iff] +lemma prop_singleton_iff (X Y : C) : singleton X Y ↔ X = Y := by simp [prop_ofObj_iff] @[simp] lemma singleton_le_iff {X : C} {P : ObjectProperty C} : singleton X ≤ P ↔ P X := by simp [ofObj_le_iff] +@[simp high] +lemma strictMap_singleton (X : C) (F : C ⥤ D) : + (singleton X).strictMap F = singleton (F.obj X) := by + ext + simp [prop_strictMap_iff] + +/-- The property of objects in a category that is satisfied by `X : C` and `Y : C`. -/ +def pair (X Y : C) : ObjectProperty C := + ofObj (Sum.elim (fun (_ : Unit) ↦ X) (fun (_ : Unit) ↦ Y)) + +@[simp] +lemma prop_pair_iff (X Y Z : C) : + pair X Y Z ↔ X = Z ∨ Y = Z := by + constructor + · rintro ⟨_ | _⟩ <;> tauto + · rintro (rfl | rfl); exacts [⟨Sum.inl .unit⟩, ⟨Sum.inr .unit⟩] + end ObjectProperty end CategoryTheory diff --git a/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean b/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean index a29ff32316363e..90344e9f12b61f 100644 --- a/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean +++ b/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean @@ -73,4 +73,34 @@ lemma isoClosure_unop (P : ObjectProperty Cᵒᵖ) : P.isoClosure.unop = P.unop.isoClosure := by rw [← op_injective_iff, P.unop.isoClosure_op, op_unop, op_unop] +/-- The bijection `Subtype P.op ≃ Subtype P` for `P : ObjectProperty C`. -/ +def subtypeOpEquiv (P : ObjectProperty C) : + Subtype P.op ≃ Subtype P where + toFun x := ⟨x.1.unop, x.2⟩ + invFun x := ⟨op x.1, x.2⟩ + +@[simp] +lemma op_ofObj {ι : Type*} (X : ι → C) : (ofObj X).op = ofObj (fun i ↦ op (X i)) := by + ext Z + simp only [op_iff, prop_ofObj_iff] + constructor + · rintro ⟨i, hi⟩ + exact ⟨i, by rw [hi]⟩ + · rintro ⟨i, hi⟩ + exact ⟨i, by rw [← hi]⟩ + +@[simp] +lemma unop_ofObj {ι : Type*} (X : ι → Cᵒᵖ) : (ofObj X).unop = ofObj (fun i ↦ (X i).unop) := + op_injective ((op_ofObj _).symm) + +@[simp high] +lemma op_singleton (X : C) : + (singleton X).op = singleton (op X) := by + simp + +@[simp high] +lemma unop_singleton (X : Cᵒᵖ) : + (singleton X).unop = singleton X.unop := by + simp + end CategoryTheory.ObjectProperty diff --git a/Mathlib/CategoryTheory/ObjectProperty/Small.lean b/Mathlib/CategoryTheory/ObjectProperty/Small.lean index b1aeaff273e6f8..ba9e6a5736dbd7 100644 --- a/Mathlib/CategoryTheory/ObjectProperty/Small.lean +++ b/Mathlib/CategoryTheory/ObjectProperty/Small.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joël Riou -/ import Mathlib.CategoryTheory.ObjectProperty.FullSubcategory +import Mathlib.CategoryTheory.ObjectProperty.Opposite import Mathlib.Logic.Small.Basic /-! @@ -33,4 +34,20 @@ lemma Small.of_le {P Q : ObjectProperty C} [ObjectProperty.Small.{w} Q] (h : P ObjectProperty.Small.{w} P := small_of_injective (Subtype.map_injective h Function.injective_id) +instance (P : ObjectProperty C) [ObjectProperty.Small.{w} P] : + ObjectProperty.Small.{w} P.op := + small_of_injective P.subtypeOpEquiv.injective + +instance (P : ObjectProperty Cᵒᵖ) [ObjectProperty.Small.{w} P] : + ObjectProperty.Small.{w} P.unop := by + simpa only [← small_congr P.unop.subtypeOpEquiv] + +instance {ι : Type*} (X : ι → C) [Small.{w} ι] : + ObjectProperty.Small.{w} (ofObj X) := + small_of_surjective (f := fun i ↦ ⟨X i, by simp⟩) (by rintro ⟨_, ⟨i⟩⟩;simp ) + +instance (X Y : C) : ObjectProperty.Small.{w} (.pair X Y) := by + dsimp [pair] + infer_instance + end CategoryTheory.ObjectProperty From 8189bf8d1d955f2d14a448a9233bd8a20bda0c72 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Tue, 7 Oct 2025 10:48:10 +0200 Subject: [PATCH 03/14] fix --- Mathlib/CategoryTheory/Generator/Basic.lean | 25 ++++++++----------- .../Generator/HomologicalComplex.lean | 9 ++++--- .../CategoryTheory/Generator/Indization.lean | 3 ++- .../CategoryTheory/Generator/Preadditive.lean | 12 +++++---- .../CategoryTheory/Generator/Presheaf.lean | 10 ++++---- Mathlib/CategoryTheory/Generator/Sheaf.lean | 11 ++++---- 6 files changed, 36 insertions(+), 34 deletions(-) diff --git a/Mathlib/CategoryTheory/Generator/Basic.lean b/Mathlib/CategoryTheory/Generator/Basic.lean index 521c1c73de800c..8c134f34534683 100644 --- a/Mathlib/CategoryTheory/Generator/Basic.lean +++ b/Mathlib/CategoryTheory/Generator/Basic.lean @@ -314,7 +314,7 @@ theorem isCoseparating_iff_mono simp simpa using hh _ hG _ -variable {P} +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. @@ -322,8 +322,8 @@ variable {P} 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] [ObjectProperty.Small.{w} P] - (hP : IsCoseparating P) : 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 (Subtype P) C := hasProductsOfShape_of_small C (Subtype P) haveI := fun A => hasProductsOfShape_of_small.{w} C (Σ G : Subtype P, A ⟶ (G : C)) @@ -333,7 +333,7 @@ theorem hasInitial_of_isCoseparating [LocallySmall.{w} C] [WellPowered.{w} C] refine fun A => ⟨⟨?_⟩, fun f => ?_⟩ · 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 := (isCoseparating_iff_mono P).1 hP A + 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 @@ -349,13 +349,11 @@ 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] [ObjectProperty.Small.{w} P] - (hP : IsSeparating P) : HasTerminal C := by - haveI : HasInitial Cᵒᵖ := hasInitial_of_isCoseparating ((isCoseparating_op_iff _).2 hP) + [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 -end ObjectProperty - section WellPowered namespace Subobject @@ -607,7 +605,8 @@ theorem isSeparator_coprod_of_isSeparator_right (G H : C) [HasBinaryCoproduct G (hH : IsSeparator H) : IsSeparator (G ⨿ H) := (isSeparator_coprod _ _).2 <| ObjectProperty.IsSeparating.of_le hH <| by simp -theorem IsSeparating.isSeparator_coproduct {β : Type w} {f : β → C} [HasCoproduct f] +theorem ObjectProperty.IsSeparating.isSeparator_coproduct + {β : Type w} {f : β → C} [HasCoproduct f] (hS : ObjectProperty.IsSeparating (.ofObj f)) : IsSeparator (∐ f) := (isSeparator_sigma _).2 hS @@ -938,9 +937,7 @@ end HasGenerator ObjectProperty.isSeparating_iff_epi @[deprecated (since := "2025-10-07")] alias isCoseparating_iff_mono := ObjectProperty.isCoseparating_iff_mono -@[deprecated (since := "2025-10-07")] alias hasInitial_of_isCoseparating := - ObjectProperty.hasInitial_of_isCoseparating -@[deprecated (since := "2025-10-07")] alias hasTerminal_of_isSeparating := - ObjectProperty.hasTerminal_of_isSeparating +@[deprecated (since := "2025-10-07")] alias IsSeparating.isSeparator_coproduct := + ObjectProperty.IsSeparating.isSeparator_coproduct end CategoryTheory diff --git a/Mathlib/CategoryTheory/Generator/HomologicalComplex.lean b/Mathlib/CategoryTheory/Generator/HomologicalComplex.lean index cd3b90df9e64ef..65cc55e20f01ad 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.prop_ofObj _ ⟨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 4df5b3357d3bbc..b0020c7e4e234f 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..4b3aabd0aba800 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.prop_ofObj _ ⟨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..28452ee8575e94 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.prop_ofObj _ ⟨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 From 4c41a3a9b28a1c0560f1570526278c9ee6c783a6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Tue, 7 Oct 2025 11:21:41 +0200 Subject: [PATCH 04/14] fix --- .../ModuleCat/Presheaf/Generator.lean | 15 +++++----- .../Adjunction/AdjointFunctorTheorems.lean | 28 +++++++++-------- .../Comma/StructuredArrow/Small.lean | 30 ++++++++++++++----- Mathlib/CategoryTheory/Generator/Basic.lean | 8 +++-- 4 files changed, 50 insertions(+), 31 deletions(-) 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/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 85d468129e6558..80040b58ee5d96 100644 --- a/Mathlib/CategoryTheory/Comma/StructuredArrow/Small.lean +++ b/Mathlib/CategoryTheory/Comma/StructuredArrow/Small.lean @@ -5,6 +5,7 @@ Authors: Markus Himmel -/ import Mathlib.CategoryTheory.Comma.StructuredArrow.Basic import Mathlib.CategoryTheory.EssentiallySmall +import Mathlib.CategoryTheory.ObjectProperty.Small import Mathlib.Logic.Small.Set /-! @@ -25,12 +26,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.prop_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 +46,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.prop_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 8c134f34534683..152068fd649a0a 100644 --- a/Mathlib/CategoryTheory/Generator/Basic.lean +++ b/Mathlib/CategoryTheory/Generator/Basic.lean @@ -400,7 +400,7 @@ namespace StructuredArrow variable (S : D) (T : C ⥤ D) -theorem isCoseparating_proj_preimage {P : ObjectProperty C} (hP : P.IsCoseparating) : +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)) @@ -411,7 +411,7 @@ namespace CostructuredArrow variable (S : C ⥤ D) (T : D) -theorem isSeparating_proj_preimage {P : ObjectProperty C} (hP : P.IsSeparating) : +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)) @@ -939,5 +939,9 @@ end HasGenerator 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 From 8c8bf906b018660f6110b06c569ec48ce53b4d21 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Tue, 7 Oct 2025 11:31:54 +0200 Subject: [PATCH 05/14] fix --- Mathlib/Algebra/Category/ModuleCat/AB.lean | 8 ++++---- .../Abelian/GrothendieckCategory/EnoughInjectives.lean | 4 ++-- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/AB.lean b/Mathlib/Algebra/Category/ModuleCat/AB.lean index 300c83cf121c7a..6aec76bedd4562 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.prop_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/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean index 3a323a14d4dae5..090828e8c3df38 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.prop_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` From bf53e9de3c245deecc90789d7536eb7f0c801e68 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Tue, 7 Oct 2025 11:38:10 +0200 Subject: [PATCH 06/14] fix --- .../GrothendieckCategory/ModuleEmbedding/GabrielPopescu.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 := From 03da717014c10806db11755f8c2d1949b738a7f0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Tue, 7 Oct 2025 11:42:13 +0200 Subject: [PATCH 07/14] feat(CategoryTheory): the opposite of a property of objects --- Mathlib.lean | 1 + .../CategoryTheory/ObjectProperty/Basic.lean | 71 ++++++++++++ .../ObjectProperty/Opposite.lean | 106 ++++++++++++++++++ .../CategoryTheory/ObjectProperty/Small.lean | 17 +++ 4 files changed, 195 insertions(+) create mode 100644 Mathlib/CategoryTheory/ObjectProperty/Opposite.lean diff --git a/Mathlib.lean b/Mathlib.lean index 985f244b4c64f4..afc86a026ab940 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2668,6 +2668,7 @@ import Mathlib.CategoryTheory.ObjectProperty.Extensions import Mathlib.CategoryTheory.ObjectProperty.FullSubcategory import Mathlib.CategoryTheory.ObjectProperty.Ind import Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape +import Mathlib.CategoryTheory.ObjectProperty.Opposite import Mathlib.CategoryTheory.ObjectProperty.Retract import Mathlib.CategoryTheory.ObjectProperty.Shift import Mathlib.CategoryTheory.ObjectProperty.Small diff --git a/Mathlib/CategoryTheory/ObjectProperty/Basic.lean b/Mathlib/CategoryTheory/ObjectProperty/Basic.lean index 7cf7a47eb945ba..6f9454ea250227 100644 --- a/Mathlib/CategoryTheory/ObjectProperty/Basic.lean +++ b/Mathlib/CategoryTheory/ObjectProperty/Basic.lean @@ -57,6 +57,18 @@ lemma prop_map_obj (P : ObjectProperty C) (F : C ⥤ D) {X : C} (hX : P X) : P.map F (F.obj X) := ⟨X, hX, ⟨Iso.refl _⟩⟩ +/-- The strict image of a property of objects by a functor. -/ +inductive strictMap (P : ObjectProperty C) (F : C ⥤ D) : ObjectProperty D + | mk (X : C) (hX : P X) : strictMap P F (F.obj X) + +lemma prop_strictMap_iff (P : ObjectProperty C) (F : C ⥤ D) (Y : D) : + P.strictMap F Y ↔ ∃ (X : C), P X ∧ F.obj X = Y := + ⟨by rintro ⟨X, hX⟩; exact ⟨X, hX, rfl⟩, by rintro ⟨X, hX, rfl⟩; exact ⟨X, hX⟩⟩ + +lemma prop_strictMap_obj (P : ObjectProperty C) (F : C ⥤ D) {X : C} (hX : P X) : + P.strictMap F (F.obj X) := + ⟨X, hX⟩ + /-- The typeclass associated to `P : ObjectProperty C`. -/ @[mk_iff] class Is (P : ObjectProperty C) (X : C) : Prop where @@ -66,6 +78,65 @@ lemma prop_of_is (P : ObjectProperty C) (X : C) [P.Is X] : P X := by rwa [← P. lemma is_of_prop (P : ObjectProperty C) {X : C} (hX : P X) : P.Is X := by rwa [P.is_iff] +section + +variable {ι : Type u'} (X : ι → C) + +/-- The property of objects that is satisfied by the `X i` for a family +of objects `X : ι : C`. -/ +inductive ofObj : ObjectProperty C + | mk (i : ι) : ofObj (X i) + +@[simp] +lemma prop_ofObj (i : ι) : ofObj X (X i) := ⟨i⟩ + +lemma prop_ofObj_iff (Y : C) : ofObj X Y ↔ ∃ i, X i = Y := by + constructor + · rintro ⟨i⟩ + exact ⟨i, rfl⟩ + · rintro ⟨i, rfl⟩ + exact ⟨i⟩ + +lemma ofObj_le_iff (P : ObjectProperty C) : + ofObj X ≤ P ↔ ∀ i, P (X i) := + ⟨fun h i ↦ h _ (by simp), fun h ↦ by rintro _ ⟨i⟩; exact h i⟩ + +@[simp] +lemma strictMap_ofObj (F : C ⥤ D) : + (ofObj X).strictMap F = ofObj (F.obj ∘ X) := by + ext Y + simp [prop_ofObj_iff, prop_strictMap_iff] + +end + +/-- The property of objects in a category that is satisfied by a single object `X : C`. -/ +abbrev singleton (X : C) : ObjectProperty C := ofObj (fun (_ : Unit) ↦ X) + +@[simp] +lemma prop_singleton_iff (X Y : C) : singleton X Y ↔ X = Y := by simp [prop_ofObj_iff] + +@[simp] +lemma singleton_le_iff {X : C} {P : ObjectProperty C} : + singleton X ≤ P ↔ P X := by + simp [ofObj_le_iff] + +@[simp high] +lemma strictMap_singleton (X : C) (F : C ⥤ D) : + (singleton X).strictMap F = singleton (F.obj X) := by + ext + simp [prop_strictMap_iff] + +/-- The property of objects in a category that is satisfied by `X : C` and `Y : C`. -/ +def pair (X Y : C) : ObjectProperty C := + ofObj (Sum.elim (fun (_ : Unit) ↦ X) (fun (_ : Unit) ↦ Y)) + +@[simp] +lemma prop_pair_iff (X Y Z : C) : + pair X Y Z ↔ X = Z ∨ Y = Z := by + constructor + · rintro ⟨_ | _⟩ <;> tauto + · rintro (rfl | rfl); exacts [⟨Sum.inl .unit⟩, ⟨Sum.inr .unit⟩] + end ObjectProperty end CategoryTheory diff --git a/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean b/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean new file mode 100644 index 00000000000000..90344e9f12b61f --- /dev/null +++ b/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean @@ -0,0 +1,106 @@ +/- +Copyright (c) 2025 Joël Riou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joël Riou +-/ +import Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms +import Mathlib.CategoryTheory.Opposites + +/-! +# The opposite of a property of objects + +-/ + +universe v u + +namespace CategoryTheory.ObjectProperty + +open Opposite + +variable {C : Type u} [Category.{v} C] + +/-- The property of objects of `Cᵒᵖ` corresponding to `P : ObjectProperty C`. -/ +protected def op (P : ObjectProperty C) : ObjectProperty Cᵒᵖ := + fun X ↦ P X.unop + +/-- The property of objects of `C` corresponding to `P : ObjectProperty Cᵒᵖ`. -/ +protected def unop (P : ObjectProperty Cᵒᵖ) : ObjectProperty C := + fun X ↦ P (op X) + +@[simp] +lemma op_iff (P : ObjectProperty C) (X : Cᵒᵖ) : + P.op X ↔ P X.unop := Iff.rfl + +@[simp] +lemma unop_iff (P : ObjectProperty Cᵒᵖ) (X : C) : + P.unop X ↔ P (op X) := Iff.rfl + +@[simp] +lemma op_unop (P : ObjectProperty Cᵒᵖ) : P.unop.op = P := rfl + +@[simp] +lemma unop_op (P : ObjectProperty C) : P.op.unop = P := rfl + +lemma op_injective {P Q : ObjectProperty C} (h : P.op = Q.op) : P = Q := by + rw [← P.unop_op, ← Q.unop_op, h] + +lemma unop_injective {P Q : ObjectProperty Cᵒᵖ} (h : P.unop = Q.unop) : P = Q := by + rw [← P.op_unop, ← Q.op_unop, h] + +lemma op_injective_iff {P Q : ObjectProperty C} : + P.op = Q.op ↔ P = Q := + ⟨op_injective, by rintro rfl; rfl⟩ + +lemma unop_injective_iff {P Q : ObjectProperty Cᵒᵖ} : + P.unop = Q.unop ↔ P = Q := + ⟨unop_injective, by rintro rfl; rfl⟩ + +instance (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] : + P.op.IsClosedUnderIsomorphisms where + of_iso e hX := P.prop_of_iso e.symm.unop hX + +instance (P : ObjectProperty Cᵒᵖ) [P.IsClosedUnderIsomorphisms] : + P.unop.IsClosedUnderIsomorphisms where + of_iso e hX := P.prop_of_iso e.symm.op hX + +lemma isoClosure_op (P : ObjectProperty C) : + P.isoClosure.op = P.op.isoClosure := by + ext ⟨X⟩ + exact ⟨fun ⟨Y, h, ⟨e⟩⟩ ↦ ⟨op Y, h, ⟨e.op.symm⟩⟩, + fun ⟨Y, h, ⟨e⟩⟩ ↦ ⟨Y.unop, h, ⟨e.unop.symm⟩⟩⟩ + +lemma isoClosure_unop (P : ObjectProperty Cᵒᵖ) : + P.isoClosure.unop = P.unop.isoClosure := by + rw [← op_injective_iff, P.unop.isoClosure_op, op_unop, op_unop] + +/-- The bijection `Subtype P.op ≃ Subtype P` for `P : ObjectProperty C`. -/ +def subtypeOpEquiv (P : ObjectProperty C) : + Subtype P.op ≃ Subtype P where + toFun x := ⟨x.1.unop, x.2⟩ + invFun x := ⟨op x.1, x.2⟩ + +@[simp] +lemma op_ofObj {ι : Type*} (X : ι → C) : (ofObj X).op = ofObj (fun i ↦ op (X i)) := by + ext Z + simp only [op_iff, prop_ofObj_iff] + constructor + · rintro ⟨i, hi⟩ + exact ⟨i, by rw [hi]⟩ + · rintro ⟨i, hi⟩ + exact ⟨i, by rw [← hi]⟩ + +@[simp] +lemma unop_ofObj {ι : Type*} (X : ι → Cᵒᵖ) : (ofObj X).unop = ofObj (fun i ↦ (X i).unop) := + op_injective ((op_ofObj _).symm) + +@[simp high] +lemma op_singleton (X : C) : + (singleton X).op = singleton (op X) := by + simp + +@[simp high] +lemma unop_singleton (X : Cᵒᵖ) : + (singleton X).unop = singleton X.unop := by + simp + +end CategoryTheory.ObjectProperty diff --git a/Mathlib/CategoryTheory/ObjectProperty/Small.lean b/Mathlib/CategoryTheory/ObjectProperty/Small.lean index b1aeaff273e6f8..ba9e6a5736dbd7 100644 --- a/Mathlib/CategoryTheory/ObjectProperty/Small.lean +++ b/Mathlib/CategoryTheory/ObjectProperty/Small.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joël Riou -/ import Mathlib.CategoryTheory.ObjectProperty.FullSubcategory +import Mathlib.CategoryTheory.ObjectProperty.Opposite import Mathlib.Logic.Small.Basic /-! @@ -33,4 +34,20 @@ lemma Small.of_le {P Q : ObjectProperty C} [ObjectProperty.Small.{w} Q] (h : P ObjectProperty.Small.{w} P := small_of_injective (Subtype.map_injective h Function.injective_id) +instance (P : ObjectProperty C) [ObjectProperty.Small.{w} P] : + ObjectProperty.Small.{w} P.op := + small_of_injective P.subtypeOpEquiv.injective + +instance (P : ObjectProperty Cᵒᵖ) [ObjectProperty.Small.{w} P] : + ObjectProperty.Small.{w} P.unop := by + simpa only [← small_congr P.unop.subtypeOpEquiv] + +instance {ι : Type*} (X : ι → C) [Small.{w} ι] : + ObjectProperty.Small.{w} (ofObj X) := + small_of_surjective (f := fun i ↦ ⟨X i, by simp⟩) (by rintro ⟨_, ⟨i⟩⟩;simp ) + +instance (X Y : C) : ObjectProperty.Small.{w} (.pair X Y) := by + dsimp [pair] + infer_instance + end CategoryTheory.ObjectProperty From 079c5abecb2159a451a2254bae0c8702e7bd2ff6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Tue, 7 Oct 2025 11:50:52 +0200 Subject: [PATCH 08/14] fix --- Mathlib/CategoryTheory/Comma/StructuredArrow/Small.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/CategoryTheory/Comma/StructuredArrow/Small.lean b/Mathlib/CategoryTheory/Comma/StructuredArrow/Small.lean index 80040b58ee5d96..f9e87398ce41b9 100644 --- a/Mathlib/CategoryTheory/Comma/StructuredArrow/Small.lean +++ b/Mathlib/CategoryTheory/Comma/StructuredArrow/Small.lean @@ -6,7 +6,6 @@ Authors: Markus Himmel import Mathlib.CategoryTheory.Comma.StructuredArrow.Basic import Mathlib.CategoryTheory.EssentiallySmall import Mathlib.CategoryTheory.ObjectProperty.Small -import Mathlib.Logic.Small.Set /-! # Small sets in the category of structured arrows From be9237b0e57ed8e8f4baf93e43137347555a81e1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <37772949+joelriou@users.noreply.github.com> Date: Tue, 7 Oct 2025 21:17:33 +0200 Subject: [PATCH 09/14] Apply suggestion from @chrisflav Co-authored-by: Christian Merten <136261474+chrisflav@users.noreply.github.com> --- Mathlib/CategoryTheory/ObjectProperty/Opposite.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean b/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean index 90344e9f12b61f..f942ed28789b8c 100644 --- a/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean +++ b/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean @@ -69,7 +69,7 @@ lemma isoClosure_op (P : ObjectProperty C) : exact ⟨fun ⟨Y, h, ⟨e⟩⟩ ↦ ⟨op Y, h, ⟨e.op.symm⟩⟩, fun ⟨Y, h, ⟨e⟩⟩ ↦ ⟨Y.unop, h, ⟨e.unop.symm⟩⟩⟩ -lemma isoClosure_unop (P : ObjectProperty Cᵒᵖ) : +lemma unop_isoClosure (P : ObjectProperty Cᵒᵖ) : P.isoClosure.unop = P.unop.isoClosure := by rw [← op_injective_iff, P.unop.isoClosure_op, op_unop, op_unop] From 9a5146daea82d4ab5351c2e36a9225b6fbc506ad Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <37772949+joelriou@users.noreply.github.com> Date: Tue, 7 Oct 2025 21:17:41 +0200 Subject: [PATCH 10/14] Apply suggestion from @chrisflav Co-authored-by: Christian Merten <136261474+chrisflav@users.noreply.github.com> --- Mathlib/CategoryTheory/ObjectProperty/Opposite.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean b/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean index f942ed28789b8c..11d830d9bc906b 100644 --- a/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean +++ b/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean @@ -63,7 +63,7 @@ instance (P : ObjectProperty Cᵒᵖ) [P.IsClosedUnderIsomorphisms] : P.unop.IsClosedUnderIsomorphisms where of_iso e hX := P.prop_of_iso e.symm.op hX -lemma isoClosure_op (P : ObjectProperty C) : +lemma op_isoClosure (P : ObjectProperty C) : P.isoClosure.op = P.op.isoClosure := by ext ⟨X⟩ exact ⟨fun ⟨Y, h, ⟨e⟩⟩ ↦ ⟨op Y, h, ⟨e.op.symm⟩⟩, From 3a0923c5736c6af63f6c50c4cf87fe6d48b62025 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Tue, 7 Oct 2025 21:23:37 +0200 Subject: [PATCH 11/14] op_monotone --- .../CategoryTheory/ObjectProperty/Opposite.lean | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean b/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean index 11d830d9bc906b..dc7de2ffe4f269 100644 --- a/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean +++ b/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean @@ -55,6 +55,20 @@ lemma unop_injective_iff {P Q : ObjectProperty Cᵒᵖ} : P.unop = Q.unop ↔ P = Q := ⟨unop_injective, by rintro rfl; rfl⟩ +lemma op_monotone {P Q : ObjectProperty C} (h : P ≤ Q) : P.op ≤ Q.op := + fun _ hX ↦ h _ hX + +lemma unop_monotone {P Q : ObjectProperty Cᵒᵖ} (h : P ≤ Q) : P.unop ≤ Q.unop := + fun _ hX ↦ h _ hX + +@[simp] +lemma op_monotone_iff {P Q : ObjectProperty C} : P.op ≤ Q.op ↔ P ≤ Q := + ⟨unop_monotone, op_monotone⟩ + +@[simp] +lemma unop_monotone_iff {P Q : ObjectProperty Cᵒᵖ} : P.unop ≤ Q.unop ↔ P ≤ Q := + ⟨op_monotone, unop_monotone⟩ + instance (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] : P.op.IsClosedUnderIsomorphisms where of_iso e hX := P.prop_of_iso e.symm.unop hX @@ -71,7 +85,7 @@ lemma op_isoClosure (P : ObjectProperty C) : lemma unop_isoClosure (P : ObjectProperty Cᵒᵖ) : P.isoClosure.unop = P.unop.isoClosure := by - rw [← op_injective_iff, P.unop.isoClosure_op, op_unop, op_unop] + rw [← op_injective_iff, P.unop.op_isoClosure, op_unop, op_unop] /-- The bijection `Subtype P.op ≃ Subtype P` for `P : ObjectProperty C`. -/ def subtypeOpEquiv (P : ObjectProperty C) : From f2cbc1bb2ba6e6c418e9161f2c1a5a36fe84d788 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Tue, 7 Oct 2025 21:29:00 +0200 Subject: [PATCH 12/14] better names --- Mathlib/CategoryTheory/ObjectProperty/Basic.lean | 16 ++++++++-------- .../CategoryTheory/ObjectProperty/Opposite.lean | 2 +- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/Mathlib/CategoryTheory/ObjectProperty/Basic.lean b/Mathlib/CategoryTheory/ObjectProperty/Basic.lean index 6f9454ea250227..01c6f8ab89f8a2 100644 --- a/Mathlib/CategoryTheory/ObjectProperty/Basic.lean +++ b/Mathlib/CategoryTheory/ObjectProperty/Basic.lean @@ -61,11 +61,11 @@ lemma prop_map_obj (P : ObjectProperty C) (F : C ⥤ D) {X : C} (hX : P X) : inductive strictMap (P : ObjectProperty C) (F : C ⥤ D) : ObjectProperty D | mk (X : C) (hX : P X) : strictMap P F (F.obj X) -lemma prop_strictMap_iff (P : ObjectProperty C) (F : C ⥤ D) (Y : D) : +lemma strictMap_iff (P : ObjectProperty C) (F : C ⥤ D) (Y : D) : P.strictMap F Y ↔ ∃ (X : C), P X ∧ F.obj X = Y := ⟨by rintro ⟨X, hX⟩; exact ⟨X, hX, rfl⟩, by rintro ⟨X, hX, rfl⟩; exact ⟨X, hX⟩⟩ -lemma prop_strictMap_obj (P : ObjectProperty C) (F : C ⥤ D) {X : C} (hX : P X) : +lemma strictMap_obj (P : ObjectProperty C) (F : C ⥤ D) {X : C} (hX : P X) : P.strictMap F (F.obj X) := ⟨X, hX⟩ @@ -88,9 +88,9 @@ inductive ofObj : ObjectProperty C | mk (i : ι) : ofObj (X i) @[simp] -lemma prop_ofObj (i : ι) : ofObj X (X i) := ⟨i⟩ +lemma ofObj_apply (i : ι) : ofObj X (X i) := ⟨i⟩ -lemma prop_ofObj_iff (Y : C) : ofObj X Y ↔ ∃ i, X i = Y := by +lemma ofObj_iff (Y : C) : ofObj X Y ↔ ∃ i, X i = Y := by constructor · rintro ⟨i⟩ exact ⟨i, rfl⟩ @@ -105,7 +105,7 @@ lemma ofObj_le_iff (P : ObjectProperty C) : lemma strictMap_ofObj (F : C ⥤ D) : (ofObj X).strictMap F = ofObj (F.obj ∘ X) := by ext Y - simp [prop_ofObj_iff, prop_strictMap_iff] + simp [ofObj_iff, strictMap_iff] end @@ -113,7 +113,7 @@ end abbrev singleton (X : C) : ObjectProperty C := ofObj (fun (_ : Unit) ↦ X) @[simp] -lemma prop_singleton_iff (X Y : C) : singleton X Y ↔ X = Y := by simp [prop_ofObj_iff] +lemma singleton_iff (X Y : C) : singleton X Y ↔ X = Y := by simp [ofObj_iff] @[simp] lemma singleton_le_iff {X : C} {P : ObjectProperty C} : @@ -124,14 +124,14 @@ lemma singleton_le_iff {X : C} {P : ObjectProperty C} : lemma strictMap_singleton (X : C) (F : C ⥤ D) : (singleton X).strictMap F = singleton (F.obj X) := by ext - simp [prop_strictMap_iff] + simp [strictMap_iff] /-- The property of objects in a category that is satisfied by `X : C` and `Y : C`. -/ def pair (X Y : C) : ObjectProperty C := ofObj (Sum.elim (fun (_ : Unit) ↦ X) (fun (_ : Unit) ↦ Y)) @[simp] -lemma prop_pair_iff (X Y Z : C) : +lemma pair_iff (X Y Z : C) : pair X Y Z ↔ X = Z ∨ Y = Z := by constructor · rintro ⟨_ | _⟩ <;> tauto diff --git a/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean b/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean index dc7de2ffe4f269..d0de958f69c5d2 100644 --- a/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean +++ b/Mathlib/CategoryTheory/ObjectProperty/Opposite.lean @@ -96,7 +96,7 @@ def subtypeOpEquiv (P : ObjectProperty C) : @[simp] lemma op_ofObj {ι : Type*} (X : ι → C) : (ofObj X).op = ofObj (fun i ↦ op (X i)) := by ext Z - simp only [op_iff, prop_ofObj_iff] + simp only [op_iff, ofObj_iff] constructor · rintro ⟨i, hi⟩ exact ⟨i, by rw [hi]⟩ From 6ce7bc49286e16cb955a28b225848f75fecd397d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 8 Oct 2025 00:06:27 +0200 Subject: [PATCH 13/14] fix --- .../Comma/StructuredArrow/Small.lean | 4 ++-- Mathlib/CategoryTheory/Generator/Basic.lean | 16 ++++++++-------- .../Generator/HomologicalComplex.lean | 2 +- Mathlib/CategoryTheory/Generator/Presheaf.lean | 2 +- Mathlib/CategoryTheory/Generator/Sheaf.lean | 2 +- 5 files changed, 13 insertions(+), 13 deletions(-) diff --git a/Mathlib/CategoryTheory/Comma/StructuredArrow/Small.lean b/Mathlib/CategoryTheory/Comma/StructuredArrow/Small.lean index f9e87398ce41b9..2b8fd923ce0bc9 100644 --- a/Mathlib/CategoryTheory/Comma/StructuredArrow/Small.lean +++ b/Mathlib/CategoryTheory/Comma/StructuredArrow/Small.lean @@ -32,7 +32,7 @@ instance small_inverseImage_proj_of_locallySmall rw [this] infer_instance ext X - simp only [ObjectProperty.prop_inverseImage_iff, proj_obj, ObjectProperty.prop_ofObj_iff, + 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⟩ @@ -52,7 +52,7 @@ instance small_inverseImage_proj_of_locallySmall rw [this] infer_instance ext X - simp only [ObjectProperty.prop_inverseImage_iff, proj_obj, ObjectProperty.prop_ofObj_iff, + 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⟩ diff --git a/Mathlib/CategoryTheory/Generator/Basic.lean b/Mathlib/CategoryTheory/Generator/Basic.lean index 152068fd649a0a..e8e8b91593f551 100644 --- a/Mathlib/CategoryTheory/Generator/Basic.lean +++ b/Mathlib/CategoryTheory/Generator/Basic.lean @@ -104,7 +104,7 @@ lemma IsSeparating.of_equivalence α.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 _ (P.prop_strictMap_obj _ hZ) h'])) + H _ (P.strictMap_obj _ hZ) h'])) lemma IsCoseparating.of_equivalence (h : IsCoseparating P) {D : Type*} [Category D] (α : C ≌ D) : @@ -113,7 +113,7 @@ lemma IsCoseparating.of_equivalence obtain ⟨h', rfl⟩ := (α.symm.toAdjunction.homEquiv _ _).symm.surjective h simp only [Equivalence.symm_inverse, Equivalence.symm_functor, Adjunction.homEquiv_counit, ← Functor.map_comp_assoc, - H _ (P.prop_strictMap_obj _ hZ) h'])) + H _ (P.strictMap_obj _ hZ) h'])) end Equivalence @@ -492,7 +492,7 @@ 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 := (ObjectProperty.prop_singleton_iff _ _).1 hH + obtain rfl := (ObjectProperty.singleton_iff _ _).1 hH exact hfg h, fun hG _ _ _ _ hfg => hG _ _ fun _ => hfg _ (by simp) _⟩ @@ -504,7 +504,7 @@ 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 := (ObjectProperty.prop_singleton_iff _ _).1 hH + obtain rfl := (ObjectProperty.singleton_iff _ _).1 hH exact hfg h, fun hG _ _ _ _ hfg => hG _ _ fun _ => hfg _ (by simp) _⟩ @@ -516,7 +516,7 @@ 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 := (ObjectProperty.prop_singleton_iff _ _).1 hH + obtain rfl := (ObjectProperty.singleton_iff _ _).1 hH exact hf h, fun hG _ _ _ hf => hG _ fun _ => hf _ (by simp) _⟩ @@ -528,7 +528,7 @@ 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 := (ObjectProperty.prop_singleton_iff _ _).1 hH + obtain rfl := (ObjectProperty.singleton_iff _ _).1 hH exact hf h, fun hG _ _ _ hf => hG _ fun _ => hf _ (by simp) _⟩ @@ -592,7 +592,7 @@ theorem isSeparator_coprod (G H : C) [HasBinaryCoproduct G H] : refine (isSeparator_iff_of_isColimit_cofan (coprodIsCoprod G H)).trans ?_ convert Iff.rfl ext X - simp only [ObjectProperty.prop_pair_iff, ObjectProperty.prop_ofObj_iff] + simp only [ObjectProperty.pair_iff, ObjectProperty.ofObj_iff] constructor · rintro (rfl | rfl); exacts [⟨.left, rfl⟩, ⟨.right, rfl⟩] · rintro ⟨⟨_ | _⟩, rfl⟩ <;> tauto @@ -638,7 +638,7 @@ theorem isCoseparator_prod (G H : C) [HasBinaryProduct G H] : refine (isCoseparator_iff_of_isLimit_fan (prodIsProd G H)).trans ?_ convert Iff.rfl ext X - simp only [ObjectProperty.prop_pair_iff, ObjectProperty.prop_ofObj_iff] + simp only [ObjectProperty.pair_iff, ObjectProperty.ofObj_iff] constructor · rintro (rfl | rfl); exacts [⟨.left, rfl⟩, ⟨.right, rfl⟩] · rintro ⟨⟨_ | _⟩, rfl⟩ <;> tauto diff --git a/Mathlib/CategoryTheory/Generator/HomologicalComplex.lean b/Mathlib/CategoryTheory/Generator/HomologicalComplex.lean index 65cc55e20f01ad..0c99e234af2548 100644 --- a/Mathlib/CategoryTheory/Generator/HomologicalComplex.lean +++ b/Mathlib/CategoryTheory/Generator/HomologicalComplex.lean @@ -48,7 +48,7 @@ lemma isSeparating_separatingFamily : have H := evalCompCoyonedaCorepresentable c (X a) j apply H.homEquiv.symm.injective simpa only [H.homEquiv_symm_comp] using h _ - (ObjectProperty.prop_ofObj _ ⟨a, j⟩) (H.homEquiv.symm p) + (ObjectProperty.ofObj_apply _ ⟨a, j⟩) (H.homEquiv.symm p) end diff --git a/Mathlib/CategoryTheory/Generator/Presheaf.lean b/Mathlib/CategoryTheory/Generator/Presheaf.lean index 4b3aabd0aba800..8fc01993932da9 100644 --- a/Mathlib/CategoryTheory/Generator/Presheaf.lean +++ b/Mathlib/CategoryTheory/Generator/Presheaf.lean @@ -71,7 +71,7 @@ lemma isSeparating {ι : Type w} {S : ι → A} (hS : ObjectProperty.IsSeparatin rintro _ ⟨i⟩ α apply freeYonedaHomEquiv.symm.injective simpa only [freeYonedaHomEquiv_symm_comp] using - h _ (ObjectProperty.prop_ofObj _ ⟨X, i⟩) (freeYonedaHomEquiv.symm α) + h _ (ObjectProperty.ofObj_apply _ ⟨X, i⟩) (freeYonedaHomEquiv.symm α) lemma isSeparator {ι : Type w} {S : ι → A} (hS : ObjectProperty.IsSeparating (.ofObj S)) [HasCoproduct (fun (⟨X, i⟩ : C × ι) ↦ freeYoneda X (S i))] diff --git a/Mathlib/CategoryTheory/Generator/Sheaf.lean b/Mathlib/CategoryTheory/Generator/Sheaf.lean index 28452ee8575e94..bd7f0862ce4c53 100644 --- a/Mathlib/CategoryTheory/Generator/Sheaf.lean +++ b/Mathlib/CategoryTheory/Generator/Sheaf.lean @@ -47,7 +47,7 @@ lemma isSeparating {ι : Type w} {S : ι → A} (hS : ObjectProperty.IsSeparatin rintro _ ⟨X, i⟩ a apply ((sheafificationAdjunction _ _).homEquiv _ _).symm.injective simpa only [← Adjunction.homEquiv_naturality_right_symm] using - hfg _ (ObjectProperty.prop_ofObj _ ⟨X, i⟩) + hfg _ (ObjectProperty.ofObj_apply _ ⟨X, i⟩) (((sheafificationAdjunction _ _).homEquiv _ _).symm a) lemma isSeparator {ι : Type w} {S : ι → A} (hS : ObjectProperty.IsSeparating (.ofObj S)) From 63524b26ff7fde9e5c0ae7697775eb226c5fccf0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 8 Oct 2025 00:11:18 +0200 Subject: [PATCH 14/14] fix --- Mathlib/Algebra/Category/ModuleCat/AB.lean | 2 +- .../Abelian/GrothendieckCategory/EnoughInjectives.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/Category/ModuleCat/AB.lean b/Mathlib/Algebra/Category/ModuleCat/AB.lean index 6aec76bedd4562..8be6e655c045e6 100644 --- a/Mathlib/Algebra/Category/ModuleCat/AB.lean +++ b/Mathlib/Algebra/Category/ModuleCat/AB.lean @@ -36,7 +36,7 @@ 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 [ObjectProperty.prop_singleton_iff, ModuleCat.hom_ext_iff, hom_comp, + 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 using h (ModuleCat.ofHom ((LinearMap.toSpanSingleton R X x).comp diff --git a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean index 090828e8c3df38..7d922e8e2acae7 100644 --- a/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean +++ b/Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean @@ -111,7 +111,7 @@ 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 [ObjectProperty.prop_singleton_iff, Function.Surjective, coyoneda_obj_obj, + 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