From 9d989b7c060bcbaa914d68f637dd44660e48fd47 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Thu, 21 May 2026 13:02:44 +0200 Subject: [PATCH 01/21] =?UTF-8?q?feat(CategoryTheory):=20the=20=CE=BA-acce?= =?UTF-8?q?ssible=20category=20of=20=CE=BA-directed=20posets?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib.lean | 1 + .../Presentable/CardinalDirectedPoset.lean | 303 ++++++++++++++++++ Mathlib/Order/Category/PartOrdEmb.lean | 21 ++ 3 files changed, 325 insertions(+) create mode 100644 Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean diff --git a/Mathlib.lean b/Mathlib.lean index 8b73416360a46f..16a42b1c2d17ab 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3234,6 +3234,7 @@ public import Mathlib.CategoryTheory.Preadditive.Yoneda.Limits public import Mathlib.CategoryTheory.Preadditive.Yoneda.Projective public import Mathlib.CategoryTheory.Presentable.Adjunction public import Mathlib.CategoryTheory.Presentable.Basic +public import Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset public import Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation public import Mathlib.CategoryTheory.Presentable.ColimitPresentation public import Mathlib.CategoryTheory.Presentable.Dense diff --git a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean new file mode 100644 index 00000000000000..7cd825f760e23e --- /dev/null +++ b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean @@ -0,0 +1,303 @@ +/- +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 +-/ +module + +public import Mathlib.CategoryTheory.Limits.FullSubcategory +public import Mathlib.Order.Category.PartOrdEmb +public import Mathlib.CategoryTheory.Presentable.LocallyPresentable + +/-! +# The κ-accessible category of κ-directed posets + +Given a regular cardinal `κ : Cardinal.{u}`, we define the +category `CardinalFilteredPoset κ` of `κ`-directed partially ordered +types (with order embeddings as morphisms), and we show that it is +a `κ`-accessible category. + +-/ + +@[expose] public section + +universe u + +open CategoryTheory Limits + +namespace PartOrdEmb + +variable (κ : Cardinal.{u}) [Fact κ.IsRegular] + +/-- The property of objects in `PartOrdEmb` that are +satisfied by partially ordered types of cardinality `< κ`. -/ +abbrev isCardinalFiltered : ObjectProperty PartOrdEmb.{u} := + fun X ↦ IsCardinalFiltered X κ + +@[simp] +lemma isCardinalFiltered_iff (X : PartOrdEmb.{u}) : + isCardinalFiltered κ X ↔ IsCardinalFiltered X κ := Iff.rfl + +instance : (isCardinalFiltered κ).IsClosedUnderIsomorphisms where + of_iso e _ := .of_equivalence κ (orderIsoOfIso e).equivalence + +namespace Limits.CoconePt + +variable {κ} {J : Type u} [SmallCategory J] [IsCardinalFiltered J κ] + {F : J ⥤ PartOrdEmb.{u}} {c : Cocone (F ⋙ forget _)} (hc : IsColimit c) + +lemma isCardinalFiltered_pt (hF : ∀ j, IsCardinalFiltered (F.obj j) κ) : + letI := isFiltered_of_isCardinalFiltered J κ + IsCardinalFiltered (CoconePt hc) κ := by + letI := isFiltered_of_isCardinalFiltered J κ + refine isCardinalFiltered_preorder _ _ (fun K f hK ↦ ?_) + rw [← hasCardinalLT_iff_cardinal_mk_lt] at hK + choose j₀ x₀ hx₀ using fun k ↦ Types.jointly_surjective_of_isColimit hc (f k) + let j := IsCardinalFiltered.max j₀ hK + let x₁ (k : K) : F.obj j := F.map (IsCardinalFiltered.toMax j₀ hK k) (x₀ k) + have hx₁ (k : K) : c.ι.app j (x₁ k) = c.ι.app (j₀ k) (x₀ k) := + ConcreteCategory.congr_hom (c.w (IsCardinalFiltered.toMax j₀ hK k)) _ + refine ⟨(cocone hc).ι.app j (IsCardinalFiltered.max x₁ hK), + fun k ↦ ?_⟩ + rw [← hx₀, ← hx₁] + exact ((cocone hc).ι.app j).hom.monotone + (leOfHom (IsCardinalFiltered.toMax x₁ hK k)) + +end Limits.CoconePt + +instance (J : Type u) [SmallCategory J] [IsCardinalFiltered J κ] : + (isCardinalFiltered κ).IsClosedUnderColimitsOfShape J where + colimitsOfShape_le := by + have := isFiltered_of_isCardinalFiltered J κ + rintro X ⟨p⟩ + simp only [(isCardinalFiltered κ).prop_iff_of_iso + (p.isColimit.coconePointUniqueUpToIso + (Limits.isColimitCocone (colimit.isColimit (p.diag ⋙ forget PartOrdEmb)))), + isCardinalFiltered_iff, Limits.cocone_pt_coe] + exact Limits.CoconePt.isCardinalFiltered_pt _ p.prop_diag_obj + +end PartOrdEmb + +namespace CategoryTheory + +variable (κ : Cardinal.{u}) [Fact κ.IsRegular] + +/-- The category of `κ`-filtered partially ordered types, +with morphisms given by order embeddings. -/ +abbrev CardinalFilteredPoset := + (PartOrdEmb.isCardinalFiltered κ).FullSubcategory + +variable {κ} + +/-- The embedding of the category of `κ`-filtered +partially ordered types in the category of partially +ordered types. -/ +abbrev CardinalFilteredPoset.ι : + CardinalFilteredPoset κ ⥤ PartOrdEmb := + ObjectProperty.ι _ + +namespace CardinalFilteredPoset + +/-- Constructor for objects in `CardinalFilteredPoset κ`. -/ +abbrev of (J : PartOrdEmb.{u}) [IsCardinalFiltered J κ] : CardinalFilteredPoset κ where + obj := J + property := inferInstance + +lemma Hom.injective {J₁ J₂ : CardinalFilteredPoset κ} (f : J₁ ⟶ J₂) : + Function.Injective f := f.hom.injective + +lemma Hom.le_iff_le {J₁ J₂ : CardinalFilteredPoset κ} (f : J₁ ⟶ J₂) (x₁ x₂ : J₁.obj) : + f x₁ ≤ f x₂ ↔ x₁ ≤ x₂ := + f.hom.hom.le_iff_le + +instance (J : CardinalFilteredPoset κ) : IsCardinalFiltered J.obj κ := J.property + +instance : HasCardinalFilteredColimits (CardinalFilteredPoset κ) κ where + hasColimitsOfShape J _ _ := by + have := isFiltered_of_isCardinalFiltered J κ + infer_instance + +instance (A : Type u) [SmallCategory A] [IsCardinalFiltered A κ] : + PreservesColimitsOfShape A (forget (CardinalFilteredPoset κ)) := by + have := isFiltered_of_isCardinalFiltered A κ + change PreservesColimitsOfShape A (CardinalFilteredPoset.ι ⋙ forget _) + infer_instance + +variable (κ) in +/-- The property of posets in `CardinalFilteredPoset κ` that are +of cardinality `< κ` and have terminal object. -/ +def hasCardinalLTWithTerminal : ObjectProperty (CardinalFilteredPoset κ) := + fun J ↦ HasCardinalLT J.obj κ ∧ HasTerminal J.obj + +instance : ObjectProperty.EssentiallySmall.{u} (hasCardinalLTWithTerminal κ) where + exists_small_le' := by + obtain ⟨X, hX⟩ : ∃ (X : Type u), Cardinal.mk X = κ := ⟨κ.ord.ToType, by simp⟩ + let α : Type u := Σ (S : Set X) (_ : PartialOrder S), + ULift.{u} (PLift (IsCardinalFiltered S κ)) + let (a : α) : PartialOrder a.1 := a.2.1 + let ι (a : α) : CardinalFilteredPoset κ := + { obj := .of a.1 + property := a.2.2.1.1 } + refine ⟨.ofObj ι, inferInstance, fun J ⟨hJ, _⟩ ↦ ?_⟩ + obtain ⟨f⟩ : Cardinal.mk J.obj ≤ Cardinal.mk X := by + simpa [hX] using ((hasCardinalLT_iff_cardinal_mk_lt _ _).1 hJ).le + let e := Equiv.ofInjective _ f.injective + letI : PartialOrder (Set.range f) := PartialOrder.lift e.symm e.symm.injective + let e' : Set.range f ≃o J.obj := { toEquiv := e.symm, map_rel_iff' := by rfl } + exact ⟨_, ⟨⟨Set.range f, inferInstance, + ⟨⟨IsCardinalFiltered.of_equivalence κ e'.symm.equivalence⟩⟩⟩⟩, + ⟨CardinalFilteredPoset.ι.preimageIso (PartOrdEmb.Iso.mk (by exact e'.symm))⟩⟩ + +namespace cocone + +variable (J : CardinalFilteredPoset κ) + +/-- Given `J : CardinalFilteredPoset κ`, this is hte partially ordered set consisting +of subsets of `J.obj` that are of cardinality `< κ` and have a terminal object. -/ +def indexSet : Set (Set J.obj) := setOf (fun S ↦ HasCardinalLT S κ ∧ HasTerminal S) + +instance (S : indexSet J) : HasTerminal S := S.prop.2 + +instance (S : indexSet J) : IsCardinalFiltered S κ := isCardinalFiltered_of_hasTerminal _ _ + +variable {J} in +lemma singleton_mem_indexSet (j : J.obj) : {j} ∈ indexSet J := + ⟨hasCardinalLT_of_finite _ _ (Cardinal.IsRegular.aleph0_le Fact.out), by + let : OrderTop ({j} : Set J.obj) := { top := ⟨j, rfl⟩, le_top := by simp } + exact isTerminalTop.hasTerminal⟩ + +instance : IsCardinalFiltered (indexSet J) κ := + isCardinalFiltered_preorder _ _ (fun K α hK ↦ by + rw [← hasCardinalLT_iff_cardinal_mk_lt] at hK + let t (k : K) : (α k).val := ⊤_ _ + let m := IsCardinalFiltered.max (fun k ↦ (t k).val) hK + let S : Set J.obj := (⋃ (k : K), α k) ∪ {m} + let : OrderTop S := + { top := ⟨m, by simp [S]⟩ + le_top := by + rintro ⟨s, hs⟩ + simp only [Set.union_singleton, Set.mem_insert_iff, Set.mem_iUnion, S] at hs + obtain rfl | ⟨k, hs⟩ := hs + · simp + · simp only [Subtype.mk_le_mk] + exact leOfHom ((by exact terminal.from (C := (α k).val) ⟨_, hs⟩) ≫ + IsCardinalFiltered.toMax _ hK k) } + refine ⟨⟨S, ?_, isTerminalTop.hasTerminal⟩, fun k ↦ ?_⟩ + · have hκ : Cardinal.aleph0 ≤ κ := Cardinal.IsRegular.aleph0_le Fact.out + exact hasCardinalLT_union hκ (hasCardinalLT_iUnion _ hK (fun k ↦ (α k).2.1)) + (hasCardinalLT_of_finite _ _ hκ) + · simp only [← Subtype.coe_le_coe, Set.le_eq_subset] + exact subset_trans (Set.subset_iUnion_of_subset k (subset_refl _)) Set.subset_union_left ) + +instance : IsFiltered (indexSet J) := isFiltered_of_isCardinalFiltered _ κ + +/-- Given `J : CardinalFilteredPoset κ`, this is the functor which sends +a subset `S` of `J.obj` of cardinality `< κ` with a terminal object to `S` +as an object in `CardinalFilteredPoset κ`. -/ +@[simps] +def functor : indexSet J ⥤ CardinalFilteredPoset κ where + obj S := of (PartOrdEmb.of S.val) + map f := ObjectProperty.homMk (PartOrdEmb.ofHom + { toFun x := ⟨x, leOfHom f x.2⟩ + inj' := by rintro ⟨x, _⟩ ⟨y, _⟩ h; simpa using h + map_rel_iff' := by rfl }) + +end cocone + +/-- The (colimit) cocone which expresses `J : CardinalFilteredPoset κ` as a colimit +of its subsets that are of cardinality `< κ` and have a terminal object. -/ +@[simps] +def cocone (J : CardinalFilteredPoset κ) : Cocone (cocone.functor J) where + pt := J + ι.app _ := ObjectProperty.homMk (PartOrdEmb.ofHom (OrderEmbedding.subtype _)) + +open cocone in +/-- Any object `J : CardinalFilteredPoset κ` is a colimit +of its subsets that are of cardinality `< κ` and have a terminal object. -/ +noncomputable def isColimitCocone (J : CardinalFilteredPoset κ) : + IsColimit (cocone J) := + isColimitOfReflects (CardinalFilteredPoset.ι ⋙ forget PartOrdEmb) (by + refine Types.FilteredColimit.isColimitOf' _ _ (fun x ↦ ?_) (fun j ⟨x, _⟩ ⟨y, _⟩ h ↦ ?_) + · exact ⟨⟨_, singleton_mem_indexSet x⟩, ⟨x, rfl⟩, rfl⟩ + · obtain rfl : x = y := by simpa using h + exact ⟨j, 𝟙 _, rfl⟩) + +set_option backward.isDefEq.respectTransparency false in +lemma isCardinalPresentable_of_hasCardinalLT_of_le (J : CardinalFilteredPoset κ) + {κ' : Cardinal.{u}} [Fact κ'.IsRegular] (hJ : HasCardinalLT J.obj κ') (h : κ ≤ κ') : + IsCardinalPresentable J κ' where + preservesColimitOfShape A _ _ := ⟨fun {F} ↦ ⟨fun {c} hc ↦ ⟨by + · have := isFiltered_of_isCardinalFiltered A κ' + have := IsCardinalFiltered.of_le A h + replace hc := isColimitOfPreserves (forget _) hc + refine Types.FilteredColimit.isColimitOf' _ _ (fun f ↦ ?_) (fun j f g h ↦ ?_) + · dsimp at f + choose j g hg using fun (x : J.obj) ↦ Types.jointly_surjective_of_isColimit hc (f x) + let m := IsCardinalFiltered.max j hJ + let φ (x : J.obj) : (F.obj m).obj := F.map (IsCardinalFiltered.toMax j hJ x) (g x) + have hφ (x : J.obj) : f x = c.ι.app _ (φ x) := by + dsimp [φ] + rw [← hg, ← ConcreteCategory.comp_apply, c.w] + rfl + refine ⟨m, + ObjectProperty.homMk (PartOrdEmb.ofHom + { toFun := φ + inj' x y h := Hom.injective f (by simpa [hφ]) + map_rel_iff' {x y} := ?_ }), ?_⟩ + · simp only [Function.Embedding.coeFn_mk, + ← Hom.le_iff_le f, hφ, Hom.le_iff_le (c.ι.app m)] + · dsimp + ext x + exact (hg x).symm.trans + (ConcreteCategory.congr_hom (c.w (IsCardinalFiltered.toMax j hJ x)).symm (g x)) + · choose k a hk using fun (x : J.obj) ↦ + (Types.FilteredColimit.isColimit_eq_iff' hc _ _).1 (ConcreteCategory.congr_hom h x) + dsimp at f g h k a hk ⊢ + obtain ⟨l, b, c, hl⟩ : ∃ (l : A) (c : j ⟶ l) (b : ∀ x, k x ⟶ l), + ∀ x, a x ≫ b x = c := by + let φ (x : J.obj) : j ⟶ IsCardinalFiltered.max k hJ := + a x ≫ IsCardinalFiltered.toMax k hJ x + exact ⟨IsCardinalFiltered.coeq φ hJ, + IsCardinalFiltered.toCoeq φ hJ, + fun x ↦ IsCardinalFiltered.toMax k hJ x ≫ IsCardinalFiltered.coeqHom φ hJ, + fun x ↦ by simpa [φ] using IsCardinalFiltered.coeq_condition φ hJ x⟩ + refine ⟨l, b, ?_⟩ + ext x + simpa only [← hl x, Functor.map_comp, ObjectProperty.FullSubcategory.comp_hom, + PartOrdEmb.hom_comp, RelEmbedding.coe_trans, Function.comp_apply] + using congr_arg _ (hk x)⟩⟩⟩ + +protected lemma isCardinalPresentable_iff (J : CardinalFilteredPoset κ) : + IsCardinalPresentable J κ ↔ HasCardinalLT J.obj κ := by + refine ⟨fun _ ↦ ?_, fun hJ ↦ isCardinalPresentable_of_hasCardinalLT_of_le _ hJ (le_refl _)⟩ + have : IsCardinalPresentable J.cocone.pt κ := by assumption + obtain ⟨X, f, hf⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ (isColimitCocone J) (𝟙 _) + dsimp at f + have : IsSplitMono f := ⟨_, hf⟩ + have : IsSplitMono ((forget _).map f) := by + -- `infer_instance` fails + apply CategoryTheory.instIsSplitMonoMap + exact X.2.1.of_injective f + ((mono_iff_injective ((forget _).map f)).1 inferInstance) + +variable (κ) in +lemma isCardinalFilteredGenerator_hasCardinalLTWithTerminal : + (hasCardinalLTWithTerminal κ).IsCardinalFilteredGenerator κ where + le_isCardinalPresentable := by + rintro J ⟨_, _⟩ + rwa [isCardinalPresentable_iff, J.isCardinalPresentable_iff] + exists_colimitsOfShape J := + ⟨_, inferInstance, inferInstance, ⟨{ + diag := _ + ι := _ + isColimit := isColimitCocone J + prop_diag_obj j := j.2 }⟩⟩ + +instance : IsCardinalAccessibleCategory (CardinalFilteredPoset κ) κ where + exists_generator := + ⟨hasCardinalLTWithTerminal κ, inferInstance, + isCardinalFilteredGenerator_hasCardinalLTWithTerminal κ⟩ + +end CardinalFilteredPoset + +end CategoryTheory diff --git a/Mathlib/Order/Category/PartOrdEmb.lean b/Mathlib/Order/Category/PartOrdEmb.lean index 7441fbffd968a9..bcaefd84f8220b 100644 --- a/Mathlib/Order/Category/PartOrdEmb.lean +++ b/Mathlib/Order/Category/PartOrdEmb.lean @@ -161,6 +161,24 @@ def Iso.mk {α β : PartOrdEmb.{u}} (e : α ≃o β) : α ≅ β where hom := ofHom e inv := ofHom e.symm +/-- The order isomorphism induced by an isomorphism in `PartOrdEmb`. -/ +@[simps] +def orderIsoOfIso {α β : PartOrdEmb.{u}} (e : α ≅ β) : + α ≃o β where + toFun := e.hom + invFun := e.inv + left_inv := ConcreteCategory.congr_hom e.hom_inv_id + right_inv := ConcreteCategory.congr_hom e.inv_hom_id + map_rel_iff' := Hom.le_iff_le _ _ _ + +instance : (forget PartOrdEmb.{u}).ReflectsIsomorphisms where + reflects {α β} f hf := by + rw [CategoryTheory.isIso_iff_bijective] at hf + let e : α ≃o β := + { toEquiv := Equiv.ofBijective _ hf + map_rel_iff' := by simp } + exact (Iso.mk e).isIso_hom + /-- `OrderDual` as a functor. -/ @[simps map] def dual : PartOrdEmb ⥤ PartOrdEmb where @@ -319,6 +337,9 @@ instance : HasColimitsOfShape J PartOrdEmb.{u} where instance : PreservesColimitsOfShape J (forget PartOrdEmb.{u}) where +instance : ReflectsColimitsOfShape J (forget PartOrdEmb.{u}) := + reflectsColimitsOfShape_of_reflectsIsomorphisms + instance : HasFilteredColimitsOfSize.{u, u} PartOrdEmb.{u} where HasColimitsOfShape _ := inferInstance From b72fcff293f3d90f7defbbee75cdf00256e5c34c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Thu, 21 May 2026 13:08:58 +0200 Subject: [PATCH 02/21] whitespace --- .../CategoryTheory/Presentable/CardinalDirectedPoset.lean | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean index 7cd825f760e23e..efab876fbf8b0a 100644 --- a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean +++ b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean @@ -1,5 +1,5 @@ /- -Copyright (c) 2025 Joël Riou. All rights reserved. +Copyright (c) 2026 Joël Riou. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joël Riou -/ @@ -92,8 +92,7 @@ variable {κ} /-- The embedding of the category of `κ`-filtered partially ordered types in the category of partially ordered types. -/ -abbrev CardinalFilteredPoset.ι : - CardinalFilteredPoset κ ⥤ PartOrdEmb := +abbrev CardinalFilteredPoset.ι : CardinalFilteredPoset κ ⥤ PartOrdEmb := ObjectProperty.ι _ namespace CardinalFilteredPoset @@ -272,11 +271,10 @@ protected lemma isCardinalPresentable_iff (J : CardinalFilteredPoset κ) : refine ⟨fun _ ↦ ?_, fun hJ ↦ isCardinalPresentable_of_hasCardinalLT_of_le _ hJ (le_refl _)⟩ have : IsCardinalPresentable J.cocone.pt κ := by assumption obtain ⟨X, f, hf⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ (isColimitCocone J) (𝟙 _) - dsimp at f have : IsSplitMono f := ⟨_, hf⟩ have : IsSplitMono ((forget _).map f) := by -- `infer_instance` fails - apply CategoryTheory.instIsSplitMonoMap + exact instIsSplitMonoMap _ _ exact X.2.1.of_injective f ((mono_iff_injective ((forget _).map f)).1 inferInstance) From db3987d55e266122b8bdbc556f7bcc093516ae53 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Thu, 21 May 2026 19:37:45 +0200 Subject: [PATCH 03/21] characterization of presentable objects --- .../Presentable/CardinalDirectedPoset.lean | 221 +++++++++++++----- 1 file changed, 160 insertions(+), 61 deletions(-) diff --git a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean index efab876fbf8b0a..70e0dda68d2b1d 100644 --- a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean +++ b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean @@ -5,9 +5,9 @@ Authors: Joël Riou -/ module -public import Mathlib.CategoryTheory.Limits.FullSubcategory -public import Mathlib.Order.Category.PartOrdEmb +public import Mathlib.CategoryTheory.Limits.Preorder public import Mathlib.CategoryTheory.Presentable.LocallyPresentable +public import Mathlib.Order.Category.PartOrdEmb /-! # The κ-accessible category of κ-directed posets @@ -17,6 +17,14 @@ category `CardinalFilteredPoset κ` of `κ`-directed partially ordered types (with order embeddings as morphisms), and we show that it is a `κ`-accessible category. +If `κ ≤ κ'` where `κ'` is also a regular cardinal, we characterize +the `κ'`-presentable objects of `CardinalFilteredPoset κ` as +the objects `J` such that the underlying type `J.obj` has +cardinality `< κ'`. + +## References +* [Adámek, J. and Rosický, J., *Locally presentable and accessible categories*][Adamek_Rosicky_1994] + -/ @[expose] public section @@ -111,6 +119,11 @@ lemma Hom.le_iff_le {J₁ J₂ : CardinalFilteredPoset κ} (f : J₁ ⟶ J₂) ( instance (J : CardinalFilteredPoset κ) : IsCardinalFiltered J.obj κ := J.property +instance (J : CardinalFilteredPoset κ) : IsFiltered J.obj := + isFiltered_of_isCardinalFiltered _ κ + +instance (J : CardinalFilteredPoset κ) : Nonempty J.obj := IsFiltered.nonempty + instance : HasCardinalFilteredColimits (CardinalFilteredPoset κ) κ where hasColimitsOfShape J _ _ := by have := isFiltered_of_isCardinalFiltered J κ @@ -136,7 +149,7 @@ instance : ObjectProperty.EssentiallySmall.{u} (hasCardinalLTWithTerminal κ) wh let (a : α) : PartialOrder a.1 := a.2.1 let ι (a : α) : CardinalFilteredPoset κ := { obj := .of a.1 - property := a.2.2.1.1 } + property := a.2.2.down.down } refine ⟨.ofObj ι, inferInstance, fun J ⟨hJ, _⟩ ↦ ?_⟩ obtain ⟨f⟩ : Cardinal.mk J.obj ≤ Cardinal.mk X := by simpa [hX] using ((hasCardinalLT_iff_cardinal_mk_lt _ _).1 hJ).le @@ -147,6 +160,149 @@ instance : ObjectProperty.EssentiallySmall.{u} (hasCardinalLTWithTerminal κ) wh ⟨⟨IsCardinalFiltered.of_equivalence κ e'.symm.equivalence⟩⟩⟩⟩, ⟨CardinalFilteredPoset.ι.preimageIso (PartOrdEmb.Iso.mk (by exact e'.symm))⟩⟩ +set_option backward.isDefEq.respectTransparency false in +lemma isCardinalPresentable_of_hasCardinalLT_of_le (J : CardinalFilteredPoset κ) + {κ' : Cardinal.{u}} [Fact κ'.IsRegular] (hJ : HasCardinalLT J.obj κ') (h : κ ≤ κ') : + IsCardinalPresentable J κ' where + preservesColimitOfShape A _ _ := ⟨fun {F} ↦ ⟨fun {c} hc ↦ ⟨by + · have := isFiltered_of_isCardinalFiltered A κ' + have := IsCardinalFiltered.of_le A h + replace hc := isColimitOfPreserves (forget _) hc + refine Types.FilteredColimit.isColimitOf' _ _ (fun f ↦ ?_) (fun j f g h ↦ ?_) + · dsimp at f + choose j g hg using fun (x : J.obj) ↦ Types.jointly_surjective_of_isColimit hc (f x) + let m := IsCardinalFiltered.max j hJ + let φ (x : J.obj) : (F.obj m).obj := F.map (IsCardinalFiltered.toMax j hJ x) (g x) + have hφ (x : J.obj) : f x = c.ι.app _ (φ x) := by + dsimp [φ] + rw [← hg, ← ConcreteCategory.comp_apply, c.w] + rfl + refine ⟨m, + ObjectProperty.homMk (PartOrdEmb.ofHom + { toFun := φ + inj' x y h := Hom.injective f (by simpa [hφ]) + map_rel_iff' {x y} := ?_ }), ?_⟩ + · simp only [Function.Embedding.coeFn_mk, + ← Hom.le_iff_le f, hφ, Hom.le_iff_le (c.ι.app m)] + · dsimp + ext x + exact (hg x).symm.trans + (ConcreteCategory.congr_hom (c.w (IsCardinalFiltered.toMax j hJ x)).symm (g x)) + · choose k a hk using fun (x : J.obj) ↦ + (Types.FilteredColimit.isColimit_eq_iff' hc _ _).1 (ConcreteCategory.congr_hom h x) + dsimp at f g h k a hk ⊢ + obtain ⟨l, b, c, hl⟩ : ∃ (l : A) (c : j ⟶ l) (b : ∀ x, k x ⟶ l), + ∀ x, a x ≫ b x = c := by + let φ (x : J.obj) : j ⟶ IsCardinalFiltered.max k hJ := + a x ≫ IsCardinalFiltered.toMax k hJ x + exact ⟨IsCardinalFiltered.coeq φ hJ, + IsCardinalFiltered.toCoeq φ hJ, + fun x ↦ IsCardinalFiltered.toMax k hJ x ≫ IsCardinalFiltered.coeqHom φ hJ, + fun x ↦ by simpa [φ] using IsCardinalFiltered.coeq_condition φ hJ x⟩ + refine ⟨l, b, ?_⟩ + ext x + simpa only [← hl x, Functor.map_comp, ObjectProperty.FullSubcategory.comp_hom, + PartOrdEmb.hom_comp, RelEmbedding.coe_trans, Function.comp_apply] + using congr_arg _ (hk x)⟩⟩⟩ + +namespace coconeWithTop + +variable (J : CardinalFilteredPoset κ) + +instance (κ' : Cardinal.{u}) [Fact κ'.IsRegular] : + IsCardinalFiltered (WithTop (J.obj)) κ' := + isCardinalFiltered_of_hasTerminal _ _ + +abbrev withTop : CardinalFilteredPoset κ := .of (.of (WithTop J.obj)) + +@[nolint unusedArguments] +def indexSet {κ' : Cardinal.{u}} [Fact κ'.IsRegular] (_ : κ ≤ κ') : + Set (Set (withTop J).obj) := + setOf (fun S ↦ HasCardinalLT S κ' ∧ ⊤ ∈ S) + +variable {κ' : Cardinal.{u}} [Fact κ'.IsRegular] {h : κ ≤ κ'} + +variable {J} (h) in +lemma pair_mem_indexSet (j : J.obj) : {WithBot.some j, ⊤} ∈ indexSet J h := + ⟨hasCardinalLT_of_finite _ _ (Cardinal.IsRegular.aleph0_le Fact.out), + Set.mem_insert_of_mem _ (by simp)⟩ + +instance (S : indexSet J h) : HasTerminal S := + IsTerminal.hasTerminal (X := ⟨⊤, S.2.2⟩) + (IsTerminal.ofUniqueHom (fun _ ↦ homOfLE (by rw [Subtype.mk_le_mk]; exact le_top)) + (fun _ _ ↦ rfl)) + +instance (S : indexSet J h) : IsCardinalFiltered S κ := isCardinalFiltered_of_hasTerminal _ _ + +instance : IsCardinalFiltered (indexSet J h) κ' := + isCardinalFiltered_preorder _ _ (fun K α hK ↦ by + rw [← hasCardinalLT_iff_cardinal_mk_lt] at hK + have hκ' : Cardinal.aleph0 ≤ κ' := Cardinal.IsRegular.aleph0_le Fact.out + refine ⟨⟨(⋃ (k : K), α k) ∪ {⊤}, + hasCardinalLT_union hκ' (hasCardinalLT_iUnion _ hK (fun k ↦ (α k).property.left)) + (hasCardinalLT_of_finite _ _ hκ'), by simp⟩, fun k ↦ ?_⟩ + rw [Subtype.mk_le_mk] + simp only [Set.le_eq_subset] + exact subset_trans (Set.subset_iUnion (fun i ↦ (α i).1) k) Set.subset_union_left) + +instance : IsFiltered (indexSet J h) := isFiltered_of_isCardinalFiltered _ κ' + +variable (h) +@[simps] +def functor : indexSet J h ⥤ CardinalFilteredPoset κ where + obj S := of (.of S.val) + map f := ObjectProperty.homMk (PartOrdEmb.ofHom + { toFun x := ⟨x, leOfHom f x.2⟩ + inj' := by rintro ⟨x, _⟩ ⟨y, _⟩ h; simpa using h + map_rel_iff' := by rfl }) + +end coconeWithTop + +section + +variable (J : CardinalFilteredPoset κ) {κ' : Cardinal.{u}} [Fact κ'.IsRegular] (h : κ ≤ κ') + +@[simps] +def coconeWithTop : Cocone (coconeWithTop.functor J h) where + pt := .of (.of (WithTop J.obj)) + ι.app _ := ObjectProperty.homMk (PartOrdEmb.ofHom (OrderEmbedding.subtype _)) + +open coconeWithTop in +noncomputable def isColimitCoconeWithTop : + IsColimit (coconeWithTop J h) := + isColimitOfReflects (CardinalFilteredPoset.ι ⋙ forget PartOrdEmb) (by + refine Types.FilteredColimit.isColimitOf' _ _ (fun x ↦ ?_) (fun j ⟨x, _⟩ ⟨y, _⟩ h ↦ ?_) + · induction x with + | some x => + exact ⟨⟨_, pair_mem_indexSet _ x⟩, ⟨x, Set.mem_insert _ _⟩, rfl⟩ + | none => + exact ⟨⟨_, pair_mem_indexSet _ (Classical.arbitrary _)⟩, + ⟨⊤, Set.mem_insert_of_mem _ rfl⟩, rfl⟩ + · obtain rfl : x = y := by simpa using h + exact ⟨j, 𝟙 _, rfl⟩) + +include h in +protected lemma isCardinalPresentable_iff : + IsCardinalPresentable J κ' ↔ HasCardinalLT J.obj κ' := by + refine ⟨fun _ ↦ ?_, fun hJ ↦ isCardinalPresentable_of_hasCardinalLT_of_le _ hJ h⟩ + obtain ⟨X, f, hf⟩ := + IsCardinalPresentable.exists_hom_of_isColimit κ' (isColimitCoconeWithTop J h) + (ObjectProperty.homMk (PartOrdEmb.ofHom WithTop.coeOrderHom)) + replace hf : OrderEmbedding.subtype X.1 ∘ f = WithTop.coeOrderHom := by + ext x + exact ConcreteCategory.congr_hom hf x + refine X.2.1.of_injective f (Function.Injective.of_comp + (f := OrderEmbedding.subtype X.1) ?_) + dsimp at hf ⊢ + rw [hf] + exact WithTop.coe_injective + +end + +protected lemma isCardinalPresentable_iff' (J : CardinalFilteredPoset κ) : + IsCardinalPresentable J κ ↔ HasCardinalLT J.obj κ := + CardinalFilteredPoset.isCardinalPresentable_iff _ (le_refl _) + namespace cocone variable (J : CardinalFilteredPoset κ) @@ -221,69 +377,12 @@ noncomputable def isColimitCocone (J : CardinalFilteredPoset κ) : · obtain rfl : x = y := by simpa using h exact ⟨j, 𝟙 _, rfl⟩) -set_option backward.isDefEq.respectTransparency false in -lemma isCardinalPresentable_of_hasCardinalLT_of_le (J : CardinalFilteredPoset κ) - {κ' : Cardinal.{u}} [Fact κ'.IsRegular] (hJ : HasCardinalLT J.obj κ') (h : κ ≤ κ') : - IsCardinalPresentable J κ' where - preservesColimitOfShape A _ _ := ⟨fun {F} ↦ ⟨fun {c} hc ↦ ⟨by - · have := isFiltered_of_isCardinalFiltered A κ' - have := IsCardinalFiltered.of_le A h - replace hc := isColimitOfPreserves (forget _) hc - refine Types.FilteredColimit.isColimitOf' _ _ (fun f ↦ ?_) (fun j f g h ↦ ?_) - · dsimp at f - choose j g hg using fun (x : J.obj) ↦ Types.jointly_surjective_of_isColimit hc (f x) - let m := IsCardinalFiltered.max j hJ - let φ (x : J.obj) : (F.obj m).obj := F.map (IsCardinalFiltered.toMax j hJ x) (g x) - have hφ (x : J.obj) : f x = c.ι.app _ (φ x) := by - dsimp [φ] - rw [← hg, ← ConcreteCategory.comp_apply, c.w] - rfl - refine ⟨m, - ObjectProperty.homMk (PartOrdEmb.ofHom - { toFun := φ - inj' x y h := Hom.injective f (by simpa [hφ]) - map_rel_iff' {x y} := ?_ }), ?_⟩ - · simp only [Function.Embedding.coeFn_mk, - ← Hom.le_iff_le f, hφ, Hom.le_iff_le (c.ι.app m)] - · dsimp - ext x - exact (hg x).symm.trans - (ConcreteCategory.congr_hom (c.w (IsCardinalFiltered.toMax j hJ x)).symm (g x)) - · choose k a hk using fun (x : J.obj) ↦ - (Types.FilteredColimit.isColimit_eq_iff' hc _ _).1 (ConcreteCategory.congr_hom h x) - dsimp at f g h k a hk ⊢ - obtain ⟨l, b, c, hl⟩ : ∃ (l : A) (c : j ⟶ l) (b : ∀ x, k x ⟶ l), - ∀ x, a x ≫ b x = c := by - let φ (x : J.obj) : j ⟶ IsCardinalFiltered.max k hJ := - a x ≫ IsCardinalFiltered.toMax k hJ x - exact ⟨IsCardinalFiltered.coeq φ hJ, - IsCardinalFiltered.toCoeq φ hJ, - fun x ↦ IsCardinalFiltered.toMax k hJ x ≫ IsCardinalFiltered.coeqHom φ hJ, - fun x ↦ by simpa [φ] using IsCardinalFiltered.coeq_condition φ hJ x⟩ - refine ⟨l, b, ?_⟩ - ext x - simpa only [← hl x, Functor.map_comp, ObjectProperty.FullSubcategory.comp_hom, - PartOrdEmb.hom_comp, RelEmbedding.coe_trans, Function.comp_apply] - using congr_arg _ (hk x)⟩⟩⟩ - -protected lemma isCardinalPresentable_iff (J : CardinalFilteredPoset κ) : - IsCardinalPresentable J κ ↔ HasCardinalLT J.obj κ := by - refine ⟨fun _ ↦ ?_, fun hJ ↦ isCardinalPresentable_of_hasCardinalLT_of_le _ hJ (le_refl _)⟩ - have : IsCardinalPresentable J.cocone.pt κ := by assumption - obtain ⟨X, f, hf⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ (isColimitCocone J) (𝟙 _) - have : IsSplitMono f := ⟨_, hf⟩ - have : IsSplitMono ((forget _).map f) := by - -- `infer_instance` fails - exact instIsSplitMonoMap _ _ - exact X.2.1.of_injective f - ((mono_iff_injective ((forget _).map f)).1 inferInstance) - variable (κ) in lemma isCardinalFilteredGenerator_hasCardinalLTWithTerminal : (hasCardinalLTWithTerminal κ).IsCardinalFilteredGenerator κ where le_isCardinalPresentable := by rintro J ⟨_, _⟩ - rwa [isCardinalPresentable_iff, J.isCardinalPresentable_iff] + rwa [isCardinalPresentable_iff, J.isCardinalPresentable_iff'] exists_colimitsOfShape J := ⟨_, inferInstance, inferInstance, ⟨{ diag := _ From bde3f62a8022812a075026ec2ecb20f371814d41 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Thu, 21 May 2026 21:04:55 +0200 Subject: [PATCH 04/21] wip --- .../Presentable/CardinalDirectedPoset.lean | 50 +++++++++++++------ 1 file changed, 34 insertions(+), 16 deletions(-) diff --git a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean index 70e0dda68d2b1d..0516855d654446 100644 --- a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean +++ b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean @@ -135,6 +135,15 @@ instance (A : Type u) [SmallCategory A] [IsCardinalFiltered A κ] : change PreservesColimitsOfShape A (CardinalFilteredPoset.ι ⋙ forget _) infer_instance +instance (J : CardinalFilteredPoset κ) (κ' : Cardinal.{u}) [Fact κ'.IsRegular] : + IsCardinalFiltered (WithTop (J.obj)) κ' := + isCardinalFiltered_of_hasTerminal _ _ + +/-- The map `CardinalFilteredPoset κ → CardinalFilteredPoset κ` which sends +a partially ordered `κ`-filtered type `J` to `WithTop J`. -/ +abbrev withTop (J : CardinalFilteredPoset κ) : CardinalFilteredPoset κ := + .of (.of (WithTop J.obj)) + variable (κ) in /-- The property of posets in `CardinalFilteredPoset κ` that are of cardinality `< κ` and have terminal object. -/ @@ -209,21 +218,20 @@ namespace coconeWithTop variable (J : CardinalFilteredPoset κ) -instance (κ' : Cardinal.{u}) [Fact κ'.IsRegular] : - IsCardinalFiltered (WithTop (J.obj)) κ' := - isCardinalFiltered_of_hasTerminal _ _ - -abbrev withTop : CardinalFilteredPoset κ := .of (.of (WithTop J.obj)) - +/-- Given two regular cardinals `κ ≤ κ'` and `J : CardinalFilteredPoset κ`, +this is the partially ordered set consisting of subsets `S` of `J.withTop` +that are of cardinality `< κ'` and contain `⊤`. +See `CardinalFilteredPoset.isColimitCoconeWithTop` for the fact that `withTop J` +identifies to the colimit of such `S`. -/ @[nolint unusedArguments] def indexSet {κ' : Cardinal.{u}} [Fact κ'.IsRegular] (_ : κ ≤ κ') : - Set (Set (withTop J).obj) := + Set (Set J.withTop.obj) := setOf (fun S ↦ HasCardinalLT S κ' ∧ ⊤ ∈ S) variable {κ' : Cardinal.{u}} [Fact κ'.IsRegular] {h : κ ≤ κ'} variable {J} (h) in -lemma pair_mem_indexSet (j : J.obj) : {WithBot.some j, ⊤} ∈ indexSet J h := +lemma pair_mem_indexSet (j : J.obj) : {WithTop.some j, ⊤} ∈ indexSet J h := ⟨hasCardinalLT_of_finite _ _ (Cardinal.IsRegular.aleph0_le Fact.out), Set.mem_insert_of_mem _ (by simp)⟩ @@ -247,7 +255,11 @@ instance : IsCardinalFiltered (indexSet J h) κ' := instance : IsFiltered (indexSet J h) := isFiltered_of_isCardinalFiltered _ κ' -variable (h) +variable (h) in +/-- Given `J : CardinalFilteredPoset κ` and an inequality `κ ≤ κ'` +where `κ'` is a regular cardinal, this is the functor which sends +a subset `S` of `J.obj` of cardinality `< κ'` and containing `⊤` to `S` +as an object in `CardinalFilteredPoset κ`. -/ @[simps] def functor : indexSet J h ⥤ CardinalFilteredPoset κ where obj S := of (.of S.val) @@ -262,14 +274,20 @@ section variable (J : CardinalFilteredPoset κ) {κ' : Cardinal.{u}} [Fact κ'.IsRegular] (h : κ ≤ κ') +/-- If `κ ≤ κ'` is an inequality between regular cardinals, and +`J : CardinalFilteredPoset κ`, this is the (colimit) cocone which +expresses `J.withTop` as a colimit of its subsets that are of +cardinality `< κ'` and contain `⊤`. -/ @[simps] def coconeWithTop : Cocone (coconeWithTop.functor J h) where - pt := .of (.of (WithTop J.obj)) + pt := J.withTop ι.app _ := ObjectProperty.homMk (PartOrdEmb.ofHom (OrderEmbedding.subtype _)) open coconeWithTop in -noncomputable def isColimitCoconeWithTop : - IsColimit (coconeWithTop J h) := +/-- If `κ ≤ κ'` is an inequality between regular cardinals, and +`J : CardinalFilteredPoset κ`, then `J.withTop` is the colimit of +its subsets that are of cardinality `< κ'` and contain `⊤`. -/ +noncomputable def isColimitCoconeWithTop : IsColimit (coconeWithTop J h) := isColimitOfReflects (CardinalFilteredPoset.ι ⋙ forget PartOrdEmb) (by refine Types.FilteredColimit.isColimitOf' _ _ (fun x ↦ ?_) (fun j ⟨x, _⟩ ⟨y, _⟩ h ↦ ?_) · induction x with @@ -278,7 +296,7 @@ noncomputable def isColimitCoconeWithTop : | none => exact ⟨⟨_, pair_mem_indexSet _ (Classical.arbitrary _)⟩, ⟨⊤, Set.mem_insert_of_mem _ rfl⟩, rfl⟩ - · obtain rfl : x = y := by simpa using h + · obtain rfl : x = y := h exact ⟨j, 𝟙 _, rfl⟩) include h in @@ -307,7 +325,7 @@ namespace cocone variable (J : CardinalFilteredPoset κ) -/-- Given `J : CardinalFilteredPoset κ`, this is hte partially ordered set consisting +/-- Given `J : CardinalFilteredPoset κ`, this is the partially ordered set consisting of subsets of `J.obj` that are of cardinality `< κ` and have a terminal object. -/ def indexSet : Set (Set J.obj) := setOf (fun S ↦ HasCardinalLT S κ ∧ HasTerminal S) @@ -351,7 +369,7 @@ a subset `S` of `J.obj` of cardinality `< κ` with a terminal object to `S` as an object in `CardinalFilteredPoset κ`. -/ @[simps] def functor : indexSet J ⥤ CardinalFilteredPoset κ where - obj S := of (PartOrdEmb.of S.val) + obj S := of (.of S.val) map f := ObjectProperty.homMk (PartOrdEmb.ofHom { toFun x := ⟨x, leOfHom f x.2⟩ inj' := by rintro ⟨x, _⟩ ⟨y, _⟩ h; simpa using h @@ -388,7 +406,7 @@ lemma isCardinalFilteredGenerator_hasCardinalLTWithTerminal : diag := _ ι := _ isColimit := isColimitCocone J - prop_diag_obj j := j.2 }⟩⟩ + prop_diag_obj j := j.prop }⟩⟩ instance : IsCardinalAccessibleCategory (CardinalFilteredPoset κ) κ where exists_generator := From 882d14b4187acdd15009272ab022180b48bb1cf1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Thu, 21 May 2026 21:21:09 +0200 Subject: [PATCH 05/21] =?UTF-8?q?feat(CategoryTheory):=20the=20category=20?= =?UTF-8?q?of=20=CE=BA-directed=20posets?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib.lean | 1 + .../Presentable/CardinalDirectedPoset.lean | 254 ++++++++++++++++++ Mathlib/Order/Category/PartOrdEmb.lean | 21 ++ 3 files changed, 276 insertions(+) create mode 100644 Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean diff --git a/Mathlib.lean b/Mathlib.lean index 2e6f05fb7e70c2..d789df0c3b3a8a 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3234,6 +3234,7 @@ public import Mathlib.CategoryTheory.Preadditive.Yoneda.Limits public import Mathlib.CategoryTheory.Preadditive.Yoneda.Projective public import Mathlib.CategoryTheory.Presentable.Adjunction public import Mathlib.CategoryTheory.Presentable.Basic +public import Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset public import Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation public import Mathlib.CategoryTheory.Presentable.ColimitPresentation public import Mathlib.CategoryTheory.Presentable.Dense diff --git a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean new file mode 100644 index 00000000000000..e72c887e4e4b9e --- /dev/null +++ b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean @@ -0,0 +1,254 @@ +/- +Copyright (c) 2026 Joël Riou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joël Riou +-/ +module + +public import Mathlib.CategoryTheory.Limits.Preorder +public import Mathlib.CategoryTheory.Presentable.LocallyPresentable +public import Mathlib.Order.Category.PartOrdEmb + +/-! +# The κ-accessible category of κ-directed posets + +Given a regular cardinal `κ : Cardinal.{u}`, we define the +category `CardinalFilteredPoset κ` of `κ`-directed partially ordered +types (with order embeddings as morphisms), and we show that it is +a `κ`-accessible category. + +If `κ ≤ κ'` where `κ'` is also a regular cardinal, we characterize +the `κ'`-presentable objects of `CardinalFilteredPoset κ` as +the objects `J` such that the underlying type `J.obj` has +cardinality `< κ'`. + +## References +* [Adámek, J. and Rosický, J., *Locally presentable and accessible categories*][Adamek_Rosicky_1994] + +-/ + +@[expose] public section + +universe u + +open CategoryTheory Limits + +namespace PartOrdEmb + +variable (κ : Cardinal.{u}) [Fact κ.IsRegular] + +/-- The property of objects in `PartOrdEmb` that are +satisfied by partially ordered types of cardinality `< κ`. -/ +abbrev isCardinalFiltered : ObjectProperty PartOrdEmb.{u} := + fun X ↦ IsCardinalFiltered X κ + +@[simp] +lemma isCardinalFiltered_iff (X : PartOrdEmb.{u}) : + isCardinalFiltered κ X ↔ IsCardinalFiltered X κ := Iff.rfl + +instance : (isCardinalFiltered κ).IsClosedUnderIsomorphisms where + of_iso e _ := .of_equivalence κ (orderIsoOfIso e).equivalence + +namespace Limits.CoconePt + +variable {κ} {J : Type u} [SmallCategory J] [IsCardinalFiltered J κ] + {F : J ⥤ PartOrdEmb.{u}} {c : Cocone (F ⋙ forget _)} (hc : IsColimit c) + +lemma isCardinalFiltered_pt (hF : ∀ j, IsCardinalFiltered (F.obj j) κ) : + letI := isFiltered_of_isCardinalFiltered J κ + IsCardinalFiltered (CoconePt hc) κ := by + letI := isFiltered_of_isCardinalFiltered J κ + refine isCardinalFiltered_preorder _ _ (fun K f hK ↦ ?_) + rw [← hasCardinalLT_iff_cardinal_mk_lt] at hK + choose j₀ x₀ hx₀ using fun k ↦ Types.jointly_surjective_of_isColimit hc (f k) + let j := IsCardinalFiltered.max j₀ hK + let x₁ (k : K) : F.obj j := F.map (IsCardinalFiltered.toMax j₀ hK k) (x₀ k) + have hx₁ (k : K) : c.ι.app j (x₁ k) = c.ι.app (j₀ k) (x₀ k) := + ConcreteCategory.congr_hom (c.w (IsCardinalFiltered.toMax j₀ hK k)) _ + refine ⟨(cocone hc).ι.app j (IsCardinalFiltered.max x₁ hK), + fun k ↦ ?_⟩ + rw [← hx₀, ← hx₁] + exact ((cocone hc).ι.app j).hom.monotone + (leOfHom (IsCardinalFiltered.toMax x₁ hK k)) + +end Limits.CoconePt + +instance (J : Type u) [SmallCategory J] [IsCardinalFiltered J κ] : + (isCardinalFiltered κ).IsClosedUnderColimitsOfShape J where + colimitsOfShape_le := by + have := isFiltered_of_isCardinalFiltered J κ + rintro X ⟨p⟩ + simp only [(isCardinalFiltered κ).prop_iff_of_iso + (p.isColimit.coconePointUniqueUpToIso + (Limits.isColimitCocone (colimit.isColimit (p.diag ⋙ forget PartOrdEmb)))), + isCardinalFiltered_iff, Limits.cocone_pt_coe] + exact Limits.CoconePt.isCardinalFiltered_pt _ p.prop_diag_obj + +end PartOrdEmb + +namespace CategoryTheory + +variable (κ : Cardinal.{u}) [Fact κ.IsRegular] + +/-- The category of `κ`-filtered partially ordered types, +with morphisms given by order embeddings. -/ +abbrev CardinalFilteredPoset := + (PartOrdEmb.isCardinalFiltered κ).FullSubcategory + +variable {κ} + +/-- The embedding of the category of `κ`-filtered +partially ordered types in the category of partially +ordered types. -/ +abbrev CardinalFilteredPoset.ι : CardinalFilteredPoset κ ⥤ PartOrdEmb := + ObjectProperty.ι _ + +namespace CardinalFilteredPoset + +/-- Constructor for objects in `CardinalFilteredPoset κ`. -/ +abbrev of (J : PartOrdEmb.{u}) [IsCardinalFiltered J κ] : CardinalFilteredPoset κ where + obj := J + property := inferInstance + +instance (J : CardinalFilteredPoset κ) : IsCardinalFiltered J.obj κ := J.property + +instance (J : CardinalFilteredPoset κ) : IsFiltered J.obj := + isFiltered_of_isCardinalFiltered _ κ + +instance (J : CardinalFilteredPoset κ) : Nonempty J.obj := IsFiltered.nonempty + +instance : HasCardinalFilteredColimits (CardinalFilteredPoset κ) κ where + hasColimitsOfShape J _ _ := by + have := isFiltered_of_isCardinalFiltered J κ + infer_instance + +instance (A : Type u) [SmallCategory A] [IsCardinalFiltered A κ] : + PreservesColimitsOfShape A (forget (CardinalFilteredPoset κ)) := by + have := isFiltered_of_isCardinalFiltered A κ + change PreservesColimitsOfShape A (CardinalFilteredPoset.ι ⋙ forget _) + infer_instance + +instance (J : CardinalFilteredPoset κ) (κ' : Cardinal.{u}) [Fact κ'.IsRegular] : + IsCardinalFiltered (WithTop (J.obj)) κ' := + isCardinalFiltered_of_hasTerminal _ _ + +/-- The map `CardinalFilteredPoset κ → CardinalFilteredPoset κ` which sends +a partially ordered `κ`-filtered type `J` to `WithTop J`. -/ +abbrev withTop (J : CardinalFilteredPoset κ) : CardinalFilteredPoset κ := + .of (.of (WithTop J.obj)) + +variable (κ) in +/-- The property of posets in `CardinalFilteredPoset κ` that are +of cardinality `< κ` and have terminal object. -/ +def hasCardinalLTWithTerminal : ObjectProperty (CardinalFilteredPoset κ) := + fun J ↦ HasCardinalLT J.obj κ ∧ HasTerminal J.obj + +instance : ObjectProperty.EssentiallySmall.{u} (hasCardinalLTWithTerminal κ) where + exists_small_le' := by + obtain ⟨X, hX⟩ : ∃ (X : Type u), Cardinal.mk X = κ := ⟨κ.ord.ToType, by simp⟩ + let α : Type u := Σ (S : Set X) (_ : PartialOrder S), + ULift.{u} (PLift (IsCardinalFiltered S κ)) + let (a : α) : PartialOrder a.1 := a.2.1 + let ι (a : α) : CardinalFilteredPoset κ := + { obj := .of a.1 + property := a.2.2.down.down } + refine ⟨.ofObj ι, inferInstance, fun J ⟨hJ, _⟩ ↦ ?_⟩ + obtain ⟨f⟩ : Cardinal.mk J.obj ≤ Cardinal.mk X := by + simpa [hX] using ((hasCardinalLT_iff_cardinal_mk_lt _ _).1 hJ).le + let e := Equiv.ofInjective _ f.injective + letI : PartialOrder (Set.range f) := PartialOrder.lift e.symm e.symm.injective + let e' : Set.range f ≃o J.obj := { toEquiv := e.symm, map_rel_iff' := by rfl } + exact ⟨_, ⟨⟨Set.range f, inferInstance, + ⟨⟨IsCardinalFiltered.of_equivalence κ e'.symm.equivalence⟩⟩⟩⟩, + ⟨CardinalFilteredPoset.ι.preimageIso (PartOrdEmb.Iso.mk (by exact e'.symm))⟩⟩ + +namespace coconeWithTop + +variable (J : CardinalFilteredPoset κ) + +/-- Given two regular cardinals `κ ≤ κ'` and `J : CardinalFilteredPoset κ`, +this is the partially ordered set consisting of subsets `S` of `J.withTop` +that are of cardinality `< κ'` and contain `⊤`. +See `CardinalFilteredPoset.isColimitCoconeWithTop` for the fact that `withTop J` +identifies to the colimit of such `S`. -/ +@[nolint unusedArguments] +def indexSet {κ' : Cardinal.{u}} [Fact κ'.IsRegular] (_ : κ ≤ κ') : + Set (Set J.withTop.obj) := + setOf (fun S ↦ HasCardinalLT S κ' ∧ ⊤ ∈ S) + +variable {κ' : Cardinal.{u}} [Fact κ'.IsRegular] {h : κ ≤ κ'} + +variable {J} (h) in +lemma pair_mem_indexSet (j : J.obj) : {WithTop.some j, ⊤} ∈ indexSet J h := + ⟨hasCardinalLT_of_finite _ _ (Cardinal.IsRegular.aleph0_le Fact.out), + Set.mem_insert_of_mem _ (by simp)⟩ + +instance (S : indexSet J h) : HasTerminal S := + IsTerminal.hasTerminal (X := ⟨⊤, S.2.2⟩) + (IsTerminal.ofUniqueHom (fun _ ↦ homOfLE (by rw [Subtype.mk_le_mk]; exact le_top)) + (fun _ _ ↦ rfl)) + +instance (S : indexSet J h) : IsCardinalFiltered S κ := isCardinalFiltered_of_hasTerminal _ _ + +instance : IsCardinalFiltered (indexSet J h) κ' := + isCardinalFiltered_preorder _ _ (fun K α hK ↦ by + rw [← hasCardinalLT_iff_cardinal_mk_lt] at hK + have hκ' : Cardinal.aleph0 ≤ κ' := Cardinal.IsRegular.aleph0_le Fact.out + refine ⟨⟨(⋃ (k : K), α k) ∪ {⊤}, + hasCardinalLT_union hκ' (hasCardinalLT_iUnion _ hK (fun k ↦ (α k).property.left)) + (hasCardinalLT_of_finite _ _ hκ'), by simp⟩, fun k ↦ ?_⟩ + rw [Subtype.mk_le_mk] + simp only [Set.le_eq_subset] + exact subset_trans (Set.subset_iUnion (fun i ↦ (α i).1) k) Set.subset_union_left) + +instance : IsFiltered (indexSet J h) := isFiltered_of_isCardinalFiltered _ κ' + +variable (h) in +/-- Given `J : CardinalFilteredPoset κ` and an inequality `κ ≤ κ'` +where `κ'` is a regular cardinal, this is the functor which sends +a subset `S` of `J.obj` of cardinality `< κ'` and containing `⊤` to `S` +as an object in `CardinalFilteredPoset κ`. -/ +@[simps] +def functor : indexSet J h ⥤ CardinalFilteredPoset κ where + obj S := of (.of S.val) + map f := ObjectProperty.homMk (PartOrdEmb.ofHom + { toFun x := ⟨x, leOfHom f x.2⟩ + inj' := by rintro ⟨x, _⟩ ⟨y, _⟩ h; simpa using h + map_rel_iff' := by rfl }) + +end coconeWithTop + +section + +variable (J : CardinalFilteredPoset κ) {κ' : Cardinal.{u}} [Fact κ'.IsRegular] (h : κ ≤ κ') + +/-- If `κ ≤ κ'` is an inequality between regular cardinals, and +`J : CardinalFilteredPoset κ`, this is the (colimit) cocone which +expresses `J.withTop` as a colimit of its subsets that are of +cardinality `< κ'` and contain `⊤`. -/ +@[simps] +def coconeWithTop : Cocone (coconeWithTop.functor J h) where + pt := J.withTop + ι.app _ := ObjectProperty.homMk (PartOrdEmb.ofHom (OrderEmbedding.subtype _)) + +open coconeWithTop in +/-- If `κ ≤ κ'` is an inequality between regular cardinals, and +`J : CardinalFilteredPoset κ`, then `J.withTop` is the colimit of +its subsets that are of cardinality `< κ'` and contain `⊤`. -/ +noncomputable def isColimitCoconeWithTop : IsColimit (coconeWithTop J h) := + isColimitOfReflects (CardinalFilteredPoset.ι ⋙ forget PartOrdEmb) (by + refine Types.FilteredColimit.isColimitOf' _ _ (fun x ↦ ?_) (fun j ⟨x, _⟩ ⟨y, _⟩ h ↦ ?_) + · induction x with + | some x => + exact ⟨⟨_, pair_mem_indexSet _ x⟩, ⟨x, Set.mem_insert _ _⟩, rfl⟩ + | none => + exact ⟨⟨_, pair_mem_indexSet _ (Classical.arbitrary _)⟩, + ⟨⊤, Set.mem_insert_of_mem _ rfl⟩, rfl⟩ + · obtain rfl : x = y := h + exact ⟨j, 𝟙 _, rfl⟩) + +end + +end CardinalFilteredPoset + +end CategoryTheory diff --git a/Mathlib/Order/Category/PartOrdEmb.lean b/Mathlib/Order/Category/PartOrdEmb.lean index 7441fbffd968a9..c1244941685b10 100644 --- a/Mathlib/Order/Category/PartOrdEmb.lean +++ b/Mathlib/Order/Category/PartOrdEmb.lean @@ -161,6 +161,24 @@ def Iso.mk {α β : PartOrdEmb.{u}} (e : α ≃o β) : α ≅ β where hom := ofHom e inv := ofHom e.symm +/-- The order isomorphism corresponding to an isomorphism in `PartOrdEmb`. -/ +@[simps] +def orderIsoOfIso {α β : PartOrdEmb.{u}} (e : α ≅ β) : + α ≃o β where + toFun := e.hom + invFun := e.inv + left_inv := ConcreteCategory.congr_hom e.hom_inv_id + right_inv := ConcreteCategory.congr_hom e.inv_hom_id + map_rel_iff' := Hom.le_iff_le _ _ _ + +instance : (forget PartOrdEmb.{u}).ReflectsIsomorphisms where + reflects {α β} f hf := by + rw [CategoryTheory.isIso_iff_bijective] at hf + let e : α ≃o β := + { toEquiv := Equiv.ofBijective _ hf + map_rel_iff' := by simp } + exact (Iso.mk e).isIso_hom + /-- `OrderDual` as a functor. -/ @[simps map] def dual : PartOrdEmb ⥤ PartOrdEmb where @@ -319,6 +337,9 @@ instance : HasColimitsOfShape J PartOrdEmb.{u} where instance : PreservesColimitsOfShape J (forget PartOrdEmb.{u}) where +instance : ReflectsColimitsOfShape J (forget PartOrdEmb.{u}) := + reflectsColimitsOfShape_of_reflectsIsomorphisms + instance : HasFilteredColimitsOfSize.{u, u} PartOrdEmb.{u} where HasColimitsOfShape _ := inferInstance From a5a1782292c3c91d50157504dbc9258a48a61c87 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Thu, 21 May 2026 21:22:03 +0200 Subject: [PATCH 06/21] fix --- .../Presentable/CardinalDirectedPoset.lean | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean index e72c887e4e4b9e..414337b977df97 100644 --- a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean +++ b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean @@ -14,13 +14,8 @@ public import Mathlib.Order.Category.PartOrdEmb Given a regular cardinal `κ : Cardinal.{u}`, we define the category `CardinalFilteredPoset κ` of `κ`-directed partially ordered -types (with order embeddings as morphisms), and we show that it is -a `κ`-accessible category. - -If `κ ≤ κ'` where `κ'` is also a regular cardinal, we characterize -the `κ'`-presentable objects of `CardinalFilteredPoset κ` as -the objects `J` such that the underlying type `J.obj` has -cardinality `< κ'`. +types (with order embeddings as morphisms). We shall show that it is +a `κ`-accessible category (TODO @joelriou). ## References * [Adámek, J. and Rosický, J., *Locally presentable and accessible categories*][Adamek_Rosicky_1994] From 96346f663197ceae2d0f5c8ecb9c374057fd2f30 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Thu, 21 May 2026 21:25:19 +0200 Subject: [PATCH 07/21] leaving out some code here --- .../Presentable/CardinalDirectedPoset.lean | 25 ------------------- 1 file changed, 25 deletions(-) diff --git a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean index 414337b977df97..27fd5d94dc811e 100644 --- a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean +++ b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean @@ -132,31 +132,6 @@ a partially ordered `κ`-filtered type `J` to `WithTop J`. -/ abbrev withTop (J : CardinalFilteredPoset κ) : CardinalFilteredPoset κ := .of (.of (WithTop J.obj)) -variable (κ) in -/-- The property of posets in `CardinalFilteredPoset κ` that are -of cardinality `< κ` and have terminal object. -/ -def hasCardinalLTWithTerminal : ObjectProperty (CardinalFilteredPoset κ) := - fun J ↦ HasCardinalLT J.obj κ ∧ HasTerminal J.obj - -instance : ObjectProperty.EssentiallySmall.{u} (hasCardinalLTWithTerminal κ) where - exists_small_le' := by - obtain ⟨X, hX⟩ : ∃ (X : Type u), Cardinal.mk X = κ := ⟨κ.ord.ToType, by simp⟩ - let α : Type u := Σ (S : Set X) (_ : PartialOrder S), - ULift.{u} (PLift (IsCardinalFiltered S κ)) - let (a : α) : PartialOrder a.1 := a.2.1 - let ι (a : α) : CardinalFilteredPoset κ := - { obj := .of a.1 - property := a.2.2.down.down } - refine ⟨.ofObj ι, inferInstance, fun J ⟨hJ, _⟩ ↦ ?_⟩ - obtain ⟨f⟩ : Cardinal.mk J.obj ≤ Cardinal.mk X := by - simpa [hX] using ((hasCardinalLT_iff_cardinal_mk_lt _ _).1 hJ).le - let e := Equiv.ofInjective _ f.injective - letI : PartialOrder (Set.range f) := PartialOrder.lift e.symm e.symm.injective - let e' : Set.range f ≃o J.obj := { toEquiv := e.symm, map_rel_iff' := by rfl } - exact ⟨_, ⟨⟨Set.range f, inferInstance, - ⟨⟨IsCardinalFiltered.of_equivalence κ e'.symm.equivalence⟩⟩⟩⟩, - ⟨CardinalFilteredPoset.ι.preimageIso (PartOrdEmb.Iso.mk (by exact e'.symm))⟩⟩ - namespace coconeWithTop variable (J : CardinalFilteredPoset κ) From 69d6fc5c86494af80dac3797d2a42840469e9097 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <37772949+joelriou@users.noreply.github.com> Date: Thu, 21 May 2026 22:50:23 +0200 Subject: [PATCH 08/21] Update Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean Co-authored-by: Dagur Asgeirsson --- Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean index 27fd5d94dc811e..34ea4ae983b0c0 100644 --- a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean +++ b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean @@ -35,7 +35,7 @@ variable (κ : Cardinal.{u}) [Fact κ.IsRegular] /-- The property of objects in `PartOrdEmb` that are satisfied by partially ordered types of cardinality `< κ`. -/ abbrev isCardinalFiltered : ObjectProperty PartOrdEmb.{u} := - fun X ↦ IsCardinalFiltered X κ + fun X ↦ IsCardinalFiltered X κ @[simp] lemma isCardinalFiltered_iff (X : PartOrdEmb.{u}) : From 7ce5d15f807c92444300b44202bb3b38cc50ca30 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <37772949+joelriou@users.noreply.github.com> Date: Thu, 21 May 2026 22:50:32 +0200 Subject: [PATCH 09/21] Update Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean Co-authored-by: Dagur Asgeirsson --- Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean index 34ea4ae983b0c0..cb0f76df78a710 100644 --- a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean +++ b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean @@ -50,9 +50,9 @@ variable {κ} {J : Type u} [SmallCategory J] [IsCardinalFiltered J κ] {F : J ⥤ PartOrdEmb.{u}} {c : Cocone (F ⋙ forget _)} (hc : IsColimit c) lemma isCardinalFiltered_pt (hF : ∀ j, IsCardinalFiltered (F.obj j) κ) : - letI := isFiltered_of_isCardinalFiltered J κ + haveI := isFiltered_of_isCardinalFiltered J κ IsCardinalFiltered (CoconePt hc) κ := by - letI := isFiltered_of_isCardinalFiltered J κ + haveI := isFiltered_of_isCardinalFiltered J κ refine isCardinalFiltered_preorder _ _ (fun K f hK ↦ ?_) rw [← hasCardinalLT_iff_cardinal_mk_lt] at hK choose j₀ x₀ hx₀ using fun k ↦ Types.jointly_surjective_of_isColimit hc (f k) From 8702bdc64b3cda012baa0428936005d76bd0a981 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <37772949+joelriou@users.noreply.github.com> Date: Thu, 21 May 2026 22:50:41 +0200 Subject: [PATCH 10/21] Update Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean Co-authored-by: Dagur Asgeirsson --- Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean index cb0f76df78a710..6b916063b07cde 100644 --- a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean +++ b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean @@ -214,7 +214,7 @@ noncomputable def isColimitCoconeWithTop : IsColimit (coconeWithTop J h) := | none => exact ⟨⟨_, pair_mem_indexSet _ (Classical.arbitrary _)⟩, ⟨⊤, Set.mem_insert_of_mem _ rfl⟩, rfl⟩ - · obtain rfl : x = y := h + · subst h exact ⟨j, 𝟙 _, rfl⟩) end From 4981f8b8d8eb8071c0e23c7e5995154f8656df5d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Fri, 22 May 2026 09:38:22 +0200 Subject: [PATCH 11/21] suggestions by @dagurtomas --- .../CategoryTheory/Presentable/CardinalDirectedPoset.lean | 3 +++ Mathlib/Order/Category/PartOrdEmb.lean | 7 +++++++ 2 files changed, 10 insertions(+) diff --git a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean index 6b916063b07cde..c8d51f8dfe263f 100644 --- a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean +++ b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean @@ -136,6 +136,9 @@ namespace coconeWithTop variable (J : CardinalFilteredPoset κ) +-- The `@[nolint unusedArguments]` facilitates the definitions below towards +-- `isColimitCoconeWithTop`: in particlar, it allows to setup `IsCardinalFiltered` +-- instances on `indexSet J h` assuming `h : κ ≤ κ'`. /-- Given two regular cardinals `κ ≤ κ'` and `J : CardinalFilteredPoset κ`, this is the partially ordered set consisting of subsets `S` of `J.withTop` that are of cardinality `< κ'` and contain `⊤`. diff --git a/Mathlib/Order/Category/PartOrdEmb.lean b/Mathlib/Order/Category/PartOrdEmb.lean index c1244941685b10..96ebf343cfd545 100644 --- a/Mathlib/Order/Category/PartOrdEmb.lean +++ b/Mathlib/Order/Category/PartOrdEmb.lean @@ -171,6 +171,13 @@ def orderIsoOfIso {α β : PartOrdEmb.{u}} (e : α ≅ β) : right_inv := ConcreteCategory.congr_hom e.inv_hom_id map_rel_iff' := Hom.le_iff_le _ _ _ +/-- Isomorphisms in `PartOrdEmb` correspond to order isomorphisms. -/ +@[simps] +def orderIsoEquivIso {α β : PartOrdEmb.{u}} : + (α ≅ β) ≃ (α ≃o β) where + toFun := orderIsoOfIso + invFun := Iso.mk + instance : (forget PartOrdEmb.{u}).ReflectsIsomorphisms where reflects {α β} f hf := by rw [CategoryTheory.isIso_iff_bijective] at hf From f69a6cc4ec6c1939ad349c4b21a64b4e68f5a18a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Fri, 22 May 2026 11:11:13 +0200 Subject: [PATCH 12/21] wip --- .../Presentable/CardinalDirectedPoset.lean | 198 +++++++++--------- Mathlib/Order/Category/PartOrdEmb.lean | 43 +++- 2 files changed, 138 insertions(+), 103 deletions(-) diff --git a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean index 62faf09c72d7cf..384b452125bdd8 100644 --- a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean +++ b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean @@ -144,6 +144,44 @@ a partially ordered `κ`-filtered type `J` to `WithTop J`. -/ abbrev withTop (J : CardinalFilteredPoset κ) : CardinalFilteredPoset κ := .of (.of (WithTop J.obj)) +section + +variable {J : CardinalFilteredPoset κ} (P : Set J.obj → Prop) + [IsDirectedOrder (Subtype P)] [Nonempty (Subtype P)] + [∀ (S : Subtype P), IsCardinalFiltered S.val κ] + +/-- Given a predicate `P : Set J.obj → Prop` on the underlying type +of `J : CardinalFilteredPoset κ` such that all the subsets satisfying `P` +are `κ`-filtered, this is the functor `Subtype P ⥤ CardinalFilteredPoset κ` +which sends a subset `S` of `J` satisfying `P` to the induced +partially ordered type `J`, as an object in `CardinalFilteredPoset κ`. -/ +@[simps!] +def functorOfPredicateSet : Subtype P ⥤ CardinalFilteredPoset κ := + ObjectProperty.lift _ (PartOrdEmb.functorOfPredicateSet P) + (fun S ↦ inferInstanceAs (IsCardinalFiltered S.val κ)) + +/-- Given a predicate `P : Set J.obj → Prop` on the underlying type +of `J : CardinalFilteredPoset κ` such that all the subsets satisfying `P` +are `κ`-filtered, this is the cocone with point `J` given +by all the inclusions of the substs satisfying `P`. -/ +@[simps] +def coconeOfPredicateSet : Cocone (functorOfPredicateSet P) where + pt := J + ι.app j := ObjectProperty.homMk ((PartOrdEmb.coconeOfPredicateSet P).ι.app j) + +/-- Let `P` be a predicate on `Set J.obj` where `J : CardinalFilteredPoset κ`. +We assume that `Subtype P` is directed and nonempty, and that any `a : J.obj` +belongs to some `S : Set J.obj` satisfying `P`. Then, `J` is the colimit in the +category `CardinalFilteredPoset κ` of these subsets. -/ +noncomputable def isColimitCoconeOfPredicateSet + [IsDirectedOrder (Subtype P)] [Nonempty (Subtype P)] + (hP : ∀ (a : J.obj), ∃ (S : Set J.obj), P S ∧ a ∈ S) : + IsColimit (coconeOfPredicateSet P) := + isColimitOfReflects (CardinalFilteredPoset.ι) + (PartOrdEmb.isColimitOfPredicateSet P hP) + +end + variable (κ) in /-- The property of posets in `CardinalFilteredPoset κ` that are of cardinality `< κ` and have terminal object. -/ @@ -214,38 +252,27 @@ lemma isCardinalPresentable_of_hasCardinalLT_of_le (J : CardinalFilteredPoset κ PartOrdEmb.hom_comp, RelEmbedding.coe_trans, Function.comp_apply] using congr_arg _ (hk x)⟩⟩⟩ -namespace coconeWithTop +section variable (J : CardinalFilteredPoset κ) --- The `@[nolint unusedArguments]` facilitates the definitions below towards --- `isColimitCoconeWithTop`: in particlar, it allows to setup `IsCardinalFiltered` --- instances on `indexSet J h` assuming `h : κ ≤ κ'`. -/-- Given two regular cardinals `κ ≤ κ'` and `J : CardinalFilteredPoset κ`, -this is the partially ordered set consisting of subsets `S` of `J.withTop` -that are of cardinality `< κ'` and contain `⊤`. -See `CardinalFilteredPoset.isColimitCoconeWithTop` for the fact that `withTop J` -identifies to the colimit of such `S`. -/ -@[nolint unusedArguments] -def indexSet {κ' : Cardinal.{u}} [Fact κ'.IsRegular] (_ : κ ≤ κ') : - Set (Set J.withTop.obj) := - setOf (fun S ↦ HasCardinalLT S κ' ∧ ⊤ ∈ S) - -variable {κ' : Cardinal.{u}} [Fact κ'.IsRegular] {h : κ ≤ κ'} - -variable {J} (h) in -lemma pair_mem_indexSet (j : J.obj) : {WithTop.some j, ⊤} ∈ indexSet J h := - ⟨hasCardinalLT_of_finite _ _ (Cardinal.IsRegular.aleph0_le Fact.out), - Set.mem_insert_of_mem _ (by simp)⟩ +-- `@[nolint unusedArguments]` allows to setup some instances which uses +-- the fact that `κ'` is regular. +def PropSetWithTop (κ' : Cardinal.{u}) [Fact κ'.IsRegular] + (S : Set J.withTop.obj) : Prop := + HasCardinalLT S κ' ∧ ⊤ ∈ S + +variable (κ' : Cardinal.{u}) [Fact κ'.IsRegular] -instance (S : indexSet J h) : HasTerminal S := +instance (S : Subtype (J.PropSetWithTop κ')) : HasTerminal S := IsTerminal.hasTerminal (X := ⟨⊤, S.2.2⟩) (IsTerminal.ofUniqueHom (fun _ ↦ homOfLE (by rw [Subtype.mk_le_mk]; exact le_top)) (fun _ _ ↦ rfl)) -instance (S : indexSet J h) : IsCardinalFiltered S κ := isCardinalFiltered_of_hasTerminal _ _ +instance (S : Subtype (J.PropSetWithTop κ')) : IsCardinalFiltered S κ := + isCardinalFiltered_of_hasTerminal _ _ -instance : IsCardinalFiltered (indexSet J h) κ' := +instance : IsCardinalFiltered (Subtype (J.PropSetWithTop κ')) κ' := isCardinalFiltered_preorder _ _ (fun K α hK ↦ by rw [← hasCardinalLT_iff_cardinal_mk_lt] at hK have hκ' : Cardinal.aleph0 ≤ κ' := Cardinal.IsRegular.aleph0_le Fact.out @@ -256,58 +283,43 @@ instance : IsCardinalFiltered (indexSet J h) κ' := simp only [Set.le_eq_subset] exact subset_trans (Set.subset_iUnion (fun i ↦ (α i).1) k) Set.subset_union_left) -instance : IsFiltered (indexSet J h) := isFiltered_of_isCardinalFiltered _ κ' +instance : IsFiltered (Subtype (J.PropSetWithTop κ')) := + isFiltered_of_isCardinalFiltered _ κ' -variable (h) in -/-- Given `J : CardinalFilteredPoset κ` and an inequality `κ ≤ κ'` -where `κ'` is a regular cardinal, this is the functor which sends -a subset `S` of `J.obj` of cardinality `< κ'` and containing `⊤` to `S` -as an object in `CardinalFilteredPoset κ`. -/ -@[simps] -def functor : indexSet J h ⥤ CardinalFilteredPoset κ where - obj S := of (.of S.val) - map f := ObjectProperty.homMk (PartOrdEmb.ofHom - { toFun x := ⟨x, leOfHom f x.2⟩ - inj' := by rintro ⟨x, _⟩ ⟨y, _⟩ h; simpa using h - map_rel_iff' := by rfl }) +instance : IsDirectedOrder (Subtype (J.PropSetWithTop κ')) := + IsFiltered.isDirectedOrder _ -end coconeWithTop +instance : Nonempty (Subtype (J.PropSetWithTop κ')) := + IsFiltered.nonempty -section - -variable (J : CardinalFilteredPoset κ) {κ' : Cardinal.{u}} [Fact κ'.IsRegular] (h : κ ≤ κ') +variable {J} in +lemma propSetWithTop_pair (j : J.obj) : J.PropSetWithTop κ' {WithTop.some j, ⊤} := + ⟨hasCardinalLT_of_finite _ _ (Cardinal.IsRegular.aleph0_le Fact.out), + Set.mem_insert_of_mem _ (by simp)⟩ -/-- If `κ ≤ κ'` is an inequality between regular cardinals, and -`J : CardinalFilteredPoset κ`, this is the (colimit) cocone which -expresses `J.withTop` as a colimit of its subsets that are of -cardinality `< κ'` and contain `⊤`. -/ -@[simps] -def coconeWithTop : Cocone (coconeWithTop.functor J h) where - pt := J.withTop - ι.app _ := ObjectProperty.homMk (PartOrdEmb.ofHom (OrderEmbedding.subtype _)) - -open coconeWithTop in -/-- If `κ ≤ κ'` is an inequality between regular cardinals, and -`J : CardinalFilteredPoset κ`, then `J.withTop` is the colimit of -its subsets that are of cardinality `< κ'` and contain `⊤`. -/ -noncomputable def isColimitCoconeWithTop : IsColimit (coconeWithTop J h) := - isColimitOfReflects (CardinalFilteredPoset.ι ⋙ forget PartOrdEmb) (by - refine Types.FilteredColimit.isColimitOf' _ _ (fun x ↦ ?_) (fun j ⟨x, _⟩ ⟨y, _⟩ h ↦ ?_) - · induction x with - | some x => - exact ⟨⟨_, pair_mem_indexSet _ x⟩, ⟨x, Set.mem_insert _ _⟩, rfl⟩ - | none => - exact ⟨⟨_, pair_mem_indexSet _ (Classical.arbitrary _)⟩, - ⟨⊤, Set.mem_insert_of_mem _ rfl⟩, rfl⟩ - · subst h - exact ⟨j, 𝟙 _, rfl⟩) - -include h in -protected lemma isCardinalPresentable_iff : +lemma exists_mem_propSetWithTop (a : J.withTop.obj) : + ∃ S, J.PropSetWithTop κ' S ∧ a ∈ S := by + induction a with + | some a => exact ⟨_, propSetWithTop_pair _ a, by aesop⟩ + | none => exact ⟨_, propSetWithTop_pair _ (Classical.arbitrary _), by aesop⟩ + +abbrev coconeWithTop : Cocone (functorOfPredicateSet (J.PropSetWithTop κ')) := + coconeOfPredicateSet (PropSetWithTop J κ') + +/-- If `J : CardinalFilteredPoset κ` and `κ'` is any regular cardinal, +then `J.withTop` is the colimit of its subsets that are of cardinality `< κ'` and contain `⊤`. -/ +noncomputable def isColimitCoconeWithTop : IsColimit (coconeWithTop J κ') := + isColimitCoconeOfPredicateSet _ (fun a ↦ by + induction a with + | some a => exact ⟨_, propSetWithTop_pair _ a, by aesop⟩ + | none => exact ⟨_, propSetWithTop_pair _ (Classical.arbitrary _), by aesop⟩) + +variable {κ'} in +protected lemma isCardinalPresentable_iff (h : κ ≤ κ') : IsCardinalPresentable J κ' ↔ HasCardinalLT J.obj κ' := by refine ⟨fun _ ↦ ?_, fun hJ ↦ isCardinalPresentable_of_hasCardinalLT_of_le _ hJ h⟩ obtain ⟨X, f, hf⟩ := - IsCardinalPresentable.exists_hom_of_isColimit κ' (isColimitCoconeWithTop J h) + IsCardinalPresentable.exists_hom_of_isColimit κ' (isColimitCoconeWithTop J κ') (ObjectProperty.homMk (PartOrdEmb.ofHom WithTop.coeOrderHom)) replace hf : OrderEmbedding.subtype X.1 ∘ f = WithTop.coeOrderHom := by ext x @@ -324,25 +336,25 @@ protected lemma isCardinalPresentable_iff' (J : CardinalFilteredPoset κ) : IsCardinalPresentable J κ ↔ HasCardinalLT J.obj κ := CardinalFilteredPoset.isCardinalPresentable_iff _ (le_refl _) -namespace cocone +section variable (J : CardinalFilteredPoset κ) -/-- Given `J : CardinalFilteredPoset κ`, this is the partially ordered set consisting -of subsets of `J.obj` that are of cardinality `< κ` and have a terminal object. -/ -def indexSet : Set (Set J.obj) := setOf (fun S ↦ HasCardinalLT S κ ∧ HasTerminal S) +def PropSet (S : Set J.obj) : Prop := + HasCardinalLT S κ ∧ HasTerminal S -instance (S : indexSet J) : HasTerminal S := S.prop.2 +instance (S : Subtype J.PropSet) : HasTerminal S := S.prop.2 -instance (S : indexSet J) : IsCardinalFiltered S κ := isCardinalFiltered_of_hasTerminal _ _ +instance (S : Subtype J.PropSet) : IsCardinalFiltered S κ := + isCardinalFiltered_of_hasTerminal _ _ variable {J} in -lemma singleton_mem_indexSet (j : J.obj) : {j} ∈ indexSet J := +lemma propSetWithTop_singleton (j : J.obj) : J.PropSet {j} := ⟨hasCardinalLT_of_finite _ _ (Cardinal.IsRegular.aleph0_le Fact.out), by let : OrderTop ({j} : Set J.obj) := { top := ⟨j, rfl⟩, le_top := by simp } exact isTerminalTop.hasTerminal⟩ -instance : IsCardinalFiltered (indexSet J) κ := +instance : IsCardinalFiltered (Subtype J.PropSet) κ := isCardinalFiltered_preorder _ _ (fun K α hK ↦ by rw [← hasCardinalLT_iff_cardinal_mk_lt] at hK let t (k : K) : (α k).val := ⊤_ _ @@ -365,38 +377,24 @@ instance : IsCardinalFiltered (indexSet J) κ := · simp only [← Subtype.coe_le_coe, Set.le_eq_subset] exact subset_trans (Set.subset_iUnion_of_subset k (subset_refl _)) Set.subset_union_left ) -instance : IsFiltered (indexSet J) := isFiltered_of_isCardinalFiltered _ κ +instance : IsFiltered (Subtype J.PropSet) := isFiltered_of_isCardinalFiltered _ κ -/-- Given `J : CardinalFilteredPoset κ`, this is the functor which sends -a subset `S` of `J.obj` of cardinality `< κ` with a terminal object to `S` -as an object in `CardinalFilteredPoset κ`. -/ -@[simps] -def functor : indexSet J ⥤ CardinalFilteredPoset κ where - obj S := of (.of S.val) - map f := ObjectProperty.homMk (PartOrdEmb.ofHom - { toFun x := ⟨x, leOfHom f x.2⟩ - inj' := by rintro ⟨x, _⟩ ⟨y, _⟩ h; simpa using h - map_rel_iff' := by rfl }) +instance : IsDirectedOrder (Subtype J.PropSet) := + IsFiltered.isDirectedOrder _ -end cocone +instance : Nonempty (Subtype J.PropSet) := + IsFiltered.nonempty -/-- The (colimit) cocone which expresses `J : CardinalFilteredPoset κ` as a colimit -of its subsets that are of cardinality `< κ` and have a terminal object. -/ -@[simps] -def cocone (J : CardinalFilteredPoset κ) : Cocone (cocone.functor J) where - pt := J - ι.app _ := ObjectProperty.homMk (PartOrdEmb.ofHom (OrderEmbedding.subtype _)) +abbrev cocone : Cocone (functorOfPredicateSet J.PropSet) := + coconeOfPredicateSet J.PropSet -open cocone in /-- Any object `J : CardinalFilteredPoset κ` is a colimit of its subsets that are of cardinality `< κ` and have a terminal object. -/ noncomputable def isColimitCocone (J : CardinalFilteredPoset κ) : IsColimit (cocone J) := - isColimitOfReflects (CardinalFilteredPoset.ι ⋙ forget PartOrdEmb) (by - refine Types.FilteredColimit.isColimitOf' _ _ (fun x ↦ ?_) (fun j ⟨x, _⟩ ⟨y, _⟩ h ↦ ?_) - · exact ⟨⟨_, singleton_mem_indexSet x⟩, ⟨x, rfl⟩, rfl⟩ - · obtain rfl : x = y := by simpa using h - exact ⟨j, 𝟙 _, rfl⟩) + isColimitCoconeOfPredicateSet _ (fun a ↦ ⟨_, propSetWithTop_singleton a, by simp⟩) + +end variable (κ) in lemma isCardinalFilteredGenerator_hasCardinalLTWithTerminal : diff --git a/Mathlib/Order/Category/PartOrdEmb.lean b/Mathlib/Order/Category/PartOrdEmb.lean index 96ebf343cfd545..7e893f7a0b827d 100644 --- a/Mathlib/Order/Category/PartOrdEmb.lean +++ b/Mathlib/Order/Category/PartOrdEmb.lean @@ -209,11 +209,10 @@ theorem partOrdEmb_dual_comp_forget_to_pardOrd : namespace PartOrdEmb -variable {J : Type u} [SmallCategory J] [IsFiltered J] {F : J ⥤ PartOrdEmb.{u}} - namespace Limits -variable {c : Cocone (F ⋙ forget _)} (hc : IsColimit c) +variable {J : Type u} [SmallCategory J] [IsFiltered J] {F : J ⥤ PartOrdEmb.{u}} + {c : Cocone (F ⋙ forget _)} (hc : IsColimit c) /-- Given a functor `F : J ⥤ PartOrdEmb` and a colimit cocone `c` for `F ⋙ forget _`, this is the type `c.pt` on which we define a partial order @@ -355,4 +354,42 @@ instance : PreservesFilteredColimitsOfSize.{u, u} (forget PartOrdEmb.{u}) where end Limits +variable {α : PartOrdEmb.{u}} (P : Set α → Prop) + +/-- Given a predicate `P : Set α → Prop` on the underlying type of `α : PartOrdEmb.{u}`, +this is the functor `Subtype P ⥤ PartOrdEmb.{u}` which sends a subset `J` of `α` +satisfying `P` to the induced partially ordered type `J`. -/ +@[simps] +def functorOfPredicateSet : Subtype P ⥤ PartOrdEmb.{u} where + obj J := .of J.val + map f := + ofHom { + toFun x := ⟨x, leOfHom f x.prop⟩ + inj' _ _ _ := by aesop + map_rel_iff' := by rfl } + +/-- Given a predicate `P : Set α → Prop` on the underlying type of `α : PartOrdEmb.{u}`, +this is the cocone with point `α` given by all the inclusions of the subsets +satisfying `P`. -/ +@[simps] +def coconeOfPredicateSet : Cocone (functorOfPredicateSet P) where + pt := α + ι.app J := ofHom (OrderEmbedding.subtype _) + +variable [IsDirectedOrder (Subtype P)] [Nonempty (Subtype P)] + +/-- Let `P` be a predicate on `Set α` where `α : PartOrdEmb`. We assume +that `Subtype P` is directed and nonempty, and that any `a : α` belongs +to some `J : Set α` satisfying `P`. Then, `α` is the colimit in the +category `PartOrdEmb` of these subsets. -/ +noncomputable def isColimitOfPredicateSet + [IsDirectedOrder (Subtype P)] [Nonempty (Subtype P)] + (hP : ∀ (a : α), ∃ (J : Set α), P J ∧ a ∈ J) : + IsColimit (coconeOfPredicateSet P) := + isColimitOfReflects (forget PartOrdEmb.{u}) (by + refine Types.FilteredColimit.isColimitOf' _ _ (fun a ↦ ?_) + (fun J x y h ↦ ⟨J, 𝟙 _, Subtype.ext h⟩) + obtain ⟨J, hJ, ha⟩ := hP a + exact ⟨⟨J, hJ⟩, ⟨a, ha⟩, rfl⟩) + end PartOrdEmb From a4c0062efe1b4eea98e2d9ef770a69e920b6207b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Fri, 22 May 2026 11:17:15 +0200 Subject: [PATCH 13/21] fix --- Mathlib/Order/Category/PartOrdEmb.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Mathlib/Order/Category/PartOrdEmb.lean b/Mathlib/Order/Category/PartOrdEmb.lean index 7e893f7a0b827d..72f44fadeddfe6 100644 --- a/Mathlib/Order/Category/PartOrdEmb.lean +++ b/Mathlib/Order/Category/PartOrdEmb.lean @@ -376,8 +376,6 @@ def coconeOfPredicateSet : Cocone (functorOfPredicateSet P) where pt := α ι.app J := ofHom (OrderEmbedding.subtype _) -variable [IsDirectedOrder (Subtype P)] [Nonempty (Subtype P)] - /-- Let `P` be a predicate on `Set α` where `α : PartOrdEmb`. We assume that `Subtype P` is directed and nonempty, and that any `a : α` belongs to some `J : Set α` satisfying `P`. Then, `α` is the colimit in the From 7ef6383c6d4731609329e3bb16419b54bf45438c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Fri, 29 May 2026 15:19:45 +0200 Subject: [PATCH 14/21] fix name --- Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean index ec148e93ef43fa..f0bb440be4ba26 100644 --- a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean +++ b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean @@ -356,7 +356,7 @@ instance (S : Subtype J.PropSet) : IsCardinalFiltered S κ := isCardinalFiltered_of_hasTerminal _ _ variable {J} in -lemma propSetWithTop_singleton (j : J.obj) : J.PropSet {j} := +lemma propSet_singleton (j : J.obj) : J.PropSet {j} := ⟨hasCardinalLT_of_finite _ _ (Cardinal.IsRegular.aleph0_le Fact.out), by let : OrderTop ({j} : Set J.obj) := { top := ⟨j, rfl⟩, le_top := by simp } exact isTerminalTop.hasTerminal⟩ @@ -399,7 +399,7 @@ abbrev cocone : Cocone (functorOfPredicateSet J.PropSet) := of its subsets that are of cardinality `< κ` and have a terminal object. -/ noncomputable def isColimitCocone (J : CardinalFilteredPoset κ) : IsColimit (cocone J) := - isColimitCoconeOfPredicateSet _ (fun a ↦ ⟨_, propSetWithTop_singleton a, by simp⟩) + isColimitCoconeOfPredicateSet _ (fun a ↦ ⟨_, propSet_singleton a, by simp⟩) end From c43390406fa57f38e648c6bc9321872771b43a71 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Fri, 29 May 2026 15:26:46 +0200 Subject: [PATCH 15/21] docstrings --- .../CategoryTheory/Presentable/CardinalDirectedPoset.lean | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean index f0bb440be4ba26..427b606043a9ae 100644 --- a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean +++ b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean @@ -200,7 +200,7 @@ instance : ObjectProperty.EssentiallySmall.{u} (hasCardinalLTWithTerminal κ) wh obtain ⟨f⟩ : Cardinal.mk J.obj ≤ Cardinal.mk X := by simpa [hX] using ((hasCardinalLT_iff_cardinal_mk_lt _ _).1 hJ).le let e := Equiv.ofInjective _ f.injective - letI : PartialOrder (Set.range f) := PartialOrder.lift e.symm e.symm.injective + letI : PartialOrder (Set.range f) := PartialOrder.lift _ e.symm.injective let e' : Set.range f ≃o J.obj := { toEquiv := e.symm, map_rel_iff' := by rfl } exact ⟨_, ⟨⟨Set.range f, inferInstance, ⟨⟨IsCardinalFiltered.of_equivalence κ e'.symm.equivalence⟩⟩⟩⟩, @@ -347,6 +347,9 @@ section variable (J : CardinalFilteredPoset κ) +/-- Given `J : CardinalFilteredPoset κ`, this is the predicate +on `Set J.obj` that is satisfied by subsets that are of +cardinality `< κ` and have a terminal object. -/ def PropSet (S : Set J.obj) : Prop := HasCardinalLT S κ ∧ HasTerminal S @@ -392,6 +395,9 @@ instance : IsDirectedOrder (Subtype J.PropSet) := instance : Nonempty (Subtype J.PropSet) := IsFiltered.nonempty +/-- For any object `J : CardinalFilteredPoset κ`, this is a colimit +cocone exhibiting `J` as the colimit of its subsets +that are of cardinality `< κ` and have a terminal object. -/ abbrev cocone : Cocone (functorOfPredicateSet J.PropSet) := coconeOfPredicateSet J.PropSet From 46a35aae9aeedad8272de695d0bb12d8203f53ed Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <37772949+joelriou@users.noreply.github.com> Date: Wed, 17 Jun 2026 13:41:50 +0200 Subject: [PATCH 16/21] Update Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean Co-authored-by: Dagur Asgeirsson --- Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean index 427b606043a9ae..a3dfe8bc12e39f 100644 --- a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean +++ b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean @@ -228,8 +228,7 @@ lemma isCardinalPresentable_of_hasCardinalLT_of_le (J : CardinalFilteredPoset κ { toFun := φ inj' x y h := Hom.injective f (by simpa [hφ]) map_rel_iff' {x y} := ?_ }), ?_⟩ - · simp only [Function.Embedding.coeFn_mk, - ← Hom.le_iff_le f, hφ, Hom.le_iff_le (c.ι.app m)] + · simp [← Hom.le_iff_le f, hφ] · dsimp ext x exact (hg x).symm.trans From ca9ade20f3ea57fde7d4c358d3efae3a3fff8d88 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <37772949+joelriou@users.noreply.github.com> Date: Wed, 17 Jun 2026 13:44:26 +0200 Subject: [PATCH 17/21] Update Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean Co-authored-by: Dagur Asgeirsson --- Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean index a3dfe8bc12e39f..4eda8f6032e0e4 100644 --- a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean +++ b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean @@ -231,8 +231,8 @@ lemma isCardinalPresentable_of_hasCardinalLT_of_le (J : CardinalFilteredPoset κ · simp [← Hom.le_iff_le f, hφ] · dsimp ext x - exact (hg x).symm.trans - (ConcreteCategory.congr_hom (c.w (IsCardinalFiltered.toMax j hJ x)).symm (g x)) + rw [← hg x] + exact (ConcreteCategory.congr_hom (c.w (IsCardinalFiltered.toMax j hJ x)).symm (g x)) · choose k a hk using fun (x : J.obj) ↦ (Types.FilteredColimit.isColimit_eq_iff' hc _ _).1 (ConcreteCategory.congr_hom h x) dsimp at f g h k a hk ⊢ From 2c6ab4439dece0f09b375380ef562df5ade55a24 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 17 Jun 2026 14:04:54 +0200 Subject: [PATCH 18/21] unif_hint --- Mathlib/CategoryTheory/ConcreteCategory/Basic.lean | 10 ++++++++++ .../Presentable/CardinalDirectedPoset.lean | 3 ++- 2 files changed, 12 insertions(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean b/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean index 0b12ec2dff0fbe..936e3f3e1476ae 100644 --- a/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean +++ b/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean @@ -210,6 +210,16 @@ instance ObjectProperty.FullSubcategory.concreteCategory {C : Type u} [Category. @[deprecated (since := "2026-04-18")] alias FullSubcategory.concreteCategory := ObjectProperty.FullSubcategory.concreteCategory +/-- Unification hint for `ConcreteCategory.hom` on full subcategories. -/ +unif_hint ObjectProperty.FullSubcategory.concreteCategory_hom + {C : Type u} [Category.{v} C] + {FC : C → C → Type*} {CC : C → Type w} + [∀ X Y, FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory.{w} C FC] + (P : ObjectProperty C) (X Y : P.FullSubcategory) (f : X ⟶ Y) where + ⊢ + ConcreteCategory.hom (C := P.FullSubcategory) f ≟ + ConcreteCategory.hom (C := C) f.hom + end ConcreteCategory variable {C : Type u} [Category.{v} C] diff --git a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean index c0ccb409e461f9..2691de136b3a96 100644 --- a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean +++ b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean @@ -207,6 +207,7 @@ instance : ObjectProperty.EssentiallySmall.{u} (hasCardinalLTWithTerminal κ) wh ⟨⟨IsCardinalFiltered.of_equivalence κ e'.symm.equivalence⟩⟩⟩⟩, ⟨CardinalFilteredPoset.ι.preimageIso (PartOrdEmb.Iso.mk (by exact e'.symm))⟩⟩ +set_option backward.defeqAttrib.useBackward true in set_option backward.isDefEq.respectTransparency false in lemma isCardinalPresentable_of_hasCardinalLT_of_le (J : CardinalFilteredPoset κ) {κ' : Cardinal.{u}} [Fact κ'.IsRegular] (hJ : HasCardinalLT J.obj κ') (h : κ ≤ κ') : @@ -249,7 +250,7 @@ lemma isCardinalPresentable_of_hasCardinalLT_of_le (J : CardinalFilteredPoset κ ext x simpa only [← hl x, Functor.map_comp, ObjectProperty.FullSubcategory.comp_hom, PartOrdEmb.hom_comp, RelEmbedding.coe_trans, Function.comp_apply] - using congr_arg _ (hk x)⟩⟩⟩ + using! congr_arg _ (hk x)⟩⟩⟩ section From 8bce3789346798711024e4e72d5d9d0e517f8a27 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 17 Jun 2026 15:00:07 +0200 Subject: [PATCH 19/21] fix --- Mathlib/CategoryTheory/Galois/GaloisObjects.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/CategoryTheory/Galois/GaloisObjects.lean b/Mathlib/CategoryTheory/Galois/GaloisObjects.lean index d6bddab93e3d71..bb36e098ebf18c 100644 --- a/Mathlib/CategoryTheory/Galois/GaloisObjects.lean +++ b/Mathlib/CategoryTheory/Galois/GaloisObjects.lean @@ -54,10 +54,10 @@ instance autMulFiber (F : C ⥤ FintypeCat.{w}) (X : C) : MulAction (Aut X) (F.o smul σ a := F.map σ.hom a one_smul a := by change F.map (𝟙 X) a = a - simp only [map_id, FintypeCat.id_apply] + simp mul_smul g h a := by change F.map (h.hom ≫ g.hom) a = (F.map h.hom ≫ F.map g.hom) a - simp only [map_comp, FintypeCat.comp_apply] + simp variable [GaloisCategory C] (F : C ⥤ FintypeCat.{w}) [FiberFunctor F] From 33a45c4fcaf8ad56cb700bfe3efba27e2b728db9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 17 Jun 2026 16:03:44 +0200 Subject: [PATCH 20/21] removed disrupting unif_hint --- Mathlib/CategoryTheory/ConcreteCategory/Basic.lean | 10 ---------- Mathlib/CategoryTheory/Galois/GaloisObjects.lean | 4 ++-- .../Presentable/CardinalDirectedPoset.lean | 5 +++-- 3 files changed, 5 insertions(+), 14 deletions(-) diff --git a/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean b/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean index 936e3f3e1476ae..0b12ec2dff0fbe 100644 --- a/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean +++ b/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean @@ -210,16 +210,6 @@ instance ObjectProperty.FullSubcategory.concreteCategory {C : Type u} [Category. @[deprecated (since := "2026-04-18")] alias FullSubcategory.concreteCategory := ObjectProperty.FullSubcategory.concreteCategory -/-- Unification hint for `ConcreteCategory.hom` on full subcategories. -/ -unif_hint ObjectProperty.FullSubcategory.concreteCategory_hom - {C : Type u} [Category.{v} C] - {FC : C → C → Type*} {CC : C → Type w} - [∀ X Y, FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory.{w} C FC] - (P : ObjectProperty C) (X Y : P.FullSubcategory) (f : X ⟶ Y) where - ⊢ - ConcreteCategory.hom (C := P.FullSubcategory) f ≟ - ConcreteCategory.hom (C := C) f.hom - end ConcreteCategory variable {C : Type u} [Category.{v} C] diff --git a/Mathlib/CategoryTheory/Galois/GaloisObjects.lean b/Mathlib/CategoryTheory/Galois/GaloisObjects.lean index bb36e098ebf18c..d6bddab93e3d71 100644 --- a/Mathlib/CategoryTheory/Galois/GaloisObjects.lean +++ b/Mathlib/CategoryTheory/Galois/GaloisObjects.lean @@ -54,10 +54,10 @@ instance autMulFiber (F : C ⥤ FintypeCat.{w}) (X : C) : MulAction (Aut X) (F.o smul σ a := F.map σ.hom a one_smul a := by change F.map (𝟙 X) a = a - simp + simp only [map_id, FintypeCat.id_apply] mul_smul g h a := by change F.map (h.hom ≫ g.hom) a = (F.map h.hom ≫ F.map g.hom) a - simp + simp only [map_comp, FintypeCat.comp_apply] variable [GaloisCategory C] (F : C ⥤ FintypeCat.{w}) [FiberFunctor F] diff --git a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean index 2691de136b3a96..53c57ad194d2c6 100644 --- a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean +++ b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean @@ -233,8 +233,9 @@ lemma isCardinalPresentable_of_hasCardinalLT_of_le (J : CardinalFilteredPoset κ · simp [← Hom.le_iff_le f, hφ] · dsimp ext x - rw [← hg x] - exact (ConcreteCategory.congr_hom (c.w (IsCardinalFiltered.toMax j hJ x)).symm (g x)) + trans (c.ι.app (j x)) (g x) + · exact (hg x).symm + · exact (ConcreteCategory.congr_hom (c.w (IsCardinalFiltered.toMax j hJ x)).symm (g x)) · choose k a hk using fun (x : J.obj) ↦ (Types.FilteredColimit.isColimit_eq_iff' hc _ _).1 (ConcreteCategory.congr_hom h x) dsimp at f g h k a hk ⊢ From 38bfba0ea120c880910292d177025f7040d0ddf5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 17 Jun 2026 16:08:31 +0200 Subject: [PATCH 21/21] removed parentheses --- Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean index 53c57ad194d2c6..8217cf1f7859a6 100644 --- a/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean +++ b/Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean @@ -233,7 +233,7 @@ lemma isCardinalPresentable_of_hasCardinalLT_of_le (J : CardinalFilteredPoset κ · simp [← Hom.le_iff_le f, hφ] · dsimp ext x - trans (c.ι.app (j x)) (g x) + trans c.ι.app (j x) (g x) · exact (hg x).symm · exact (ConcreteCategory.congr_hom (c.w (IsCardinalFiltered.toMax j hJ x)).symm (g x)) · choose k a hk using fun (x : J.obj) ↦