Skip to content

Commit b5d7e8e

Browse files
joelrioub-mehta
joelriou
authored and
b-mehta
committed
feat(CategoryTheory): the category of κ-directed posets (leanprover-community#39669)
Given a regular cardinal `κ : Cardinal.{u}`, we define the category `CardinalFilteredPoset κ` of `κ`-directed partially ordered types (with order embeddings as morphisms). In a future PR leanprover-community#39655, we shall show that it is a `κ`-accessible category. In this PR, we also show that if `J : CardinalFilteredPoset κ`, the object `J.withTop` obtained by adding a top element is a `κ'`-filtered colimit of objects of cardinality `< κ'` (when `κ'` is a regular cardinal such that `κ ≤ κ'`). This shall be used in leanprover-community#39655 in order to characterize `κ'`-presentable objects in `CardinalFilteredPoset κ` as the objects that are of cardinality `< κ'`.
1 parent 0306da0 commit b5d7e8e

3 files changed

Lines changed: 313 additions & 3 deletions

File tree

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3243,6 +3243,7 @@ public import Mathlib.CategoryTheory.Preadditive.Yoneda.Limits
32433243
public import Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
32443244
public import Mathlib.CategoryTheory.Presentable.Adjunction
32453245
public import Mathlib.CategoryTheory.Presentable.Basic
3246+
public import Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
32463247
public import Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
32473248
public import Mathlib.CategoryTheory.Presentable.ColimitPresentation
32483249
public import Mathlib.CategoryTheory.Presentable.Dense

‎Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean‎

Lines changed: 246 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,246 @@
1+
/-
2+
Copyright (c) 2026 Joël Riou. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Joël Riou
5+
-/
6+
module
7+
8+
public import Mathlib.CategoryTheory.Limits.Preorder
9+
public import Mathlib.CategoryTheory.Presentable.LocallyPresentable
10+
public import Mathlib.Order.Category.PartOrdEmb
11+
12+
/-!
13+
# The κ-accessible category of κ-directed posets
14+
15+
Given a regular cardinal `κ : Cardinal.{u}`, we define the
16+
category `CardinalFilteredPoset κ` of `κ`-directed partially ordered
17+
types (with order embeddings as morphisms). We shall show that it is
18+
a `κ`-accessible category (TODO @joelriou).
19+
20+
## References
21+
* [Adámek, J. and Rosický, J., *Locally presentable and accessible categories*][Adamek_Rosicky_1994]
22+
23+
-/
24+
25+
@[expose] public section
26+
27+
universe u
28+
29+
open CategoryTheory Limits
30+
31+
namespace PartOrdEmb
32+
33+
variable (κ : Cardinal.{u}) [Fact κ.IsRegular]
34+
35+
/-- The property of objects in `PartOrdEmb` that are
36+
satisfied by partially ordered types of cardinality `< κ`. -/
37+
abbrev isCardinalFiltered : ObjectProperty PartOrdEmb.{u} :=
38+
fun X ↦ IsCardinalFiltered X κ
39+
40+
@[simp]
41+
lemma isCardinalFiltered_iff (X : PartOrdEmb.{u}) :
42+
isCardinalFiltered κ X ↔ IsCardinalFiltered X κ := Iff.rfl
43+
44+
instance : (isCardinalFiltered κ).IsClosedUnderIsomorphisms where
45+
of_iso e _ := .of_equivalence κ (orderIsoOfIso e).equivalence
46+
47+
namespace Limits.CoconePt
48+
49+
variable {κ} {J : Type u} [SmallCategory J] [IsCardinalFiltered J κ]
50+
{F : J ⥤ PartOrdEmb.{u}} {c : Cocone (F ⋙ forget _)} (hc : IsColimit c)
51+
52+
lemma isCardinalFiltered_pt (hF : ∀ j, IsCardinalFiltered (F.obj j) κ) :
53+
haveI := isFiltered_of_isCardinalFiltered J κ
54+
IsCardinalFiltered (CoconePt hc) κ := by
55+
haveI := isFiltered_of_isCardinalFiltered J κ
56+
refine isCardinalFiltered_preorder _ _ (fun K f hK ↦ ?_)
57+
rw [← hasCardinalLT_iff_cardinal_mk_lt] at hK
58+
choose j₀ x₀ hx₀ using fun k ↦ Types.jointly_surjective_of_isColimit hc (f k)
59+
let j := IsCardinalFiltered.max j₀ hK
60+
let x₁ (k : K) : F.obj j := F.map (IsCardinalFiltered.toMax j₀ hK k) (x₀ k)
61+
have hx₁ (k : K) : c.ι.app j (x₁ k) = c.ι.app (j₀ k) (x₀ k) :=
62+
ConcreteCategory.congr_hom (c.w (IsCardinalFiltered.toMax j₀ hK k)) _
63+
refine ⟨(cocone hc).ι.app j (IsCardinalFiltered.max x₁ hK),
64+
fun k ↦ ?_⟩
65+
rw [← hx₀, ← hx₁]
66+
exact ((cocone hc).ι.app j).hom.monotone
67+
(leOfHom (IsCardinalFiltered.toMax x₁ hK k))
68+
69+
end Limits.CoconePt
70+
71+
instance (J : Type u) [SmallCategory J] [IsCardinalFiltered J κ] :
72+
(isCardinalFiltered κ).IsClosedUnderColimitsOfShape J where
73+
colimitsOfShape_le := by
74+
have := isFiltered_of_isCardinalFiltered J κ
75+
rintro X ⟨p⟩
76+
simp only [(isCardinalFiltered κ).prop_iff_of_iso
77+
(p.isColimit.coconePointUniqueUpToIso
78+
(Limits.isColimitCocone (colimit.isColimit (p.diag ⋙ forget PartOrdEmb)))),
79+
isCardinalFiltered_iff, Limits.cocone_pt_coe]
80+
exact Limits.CoconePt.isCardinalFiltered_pt _ p.prop_diag_obj
81+
82+
end PartOrdEmb
83+
84+
namespace CategoryTheory
85+
86+
variable (κ : Cardinal.{u}) [Fact κ.IsRegular]
87+
88+
/-- The category of `κ`-filtered partially ordered types,
89+
with morphisms given by order embeddings. -/
90+
abbrev CardinalFilteredPoset :=
91+
(PartOrdEmb.isCardinalFiltered κ).FullSubcategory
92+
93+
variable {κ}
94+
95+
/-- The embedding of the category of `κ`-filtered
96+
partially ordered types in the category of partially
97+
ordered types. -/
98+
abbrev CardinalFilteredPoset.ι : CardinalFilteredPoset κ ⥤ PartOrdEmb :=
99+
ObjectProperty.ι _
100+
101+
namespace CardinalFilteredPoset
102+
103+
/-- Constructor for objects in `CardinalFilteredPoset κ`. -/
104+
abbrev of (J : PartOrdEmb.{u}) [IsCardinalFiltered J κ] : CardinalFilteredPoset κ where
105+
obj := J
106+
property := inferInstance
107+
108+
instance (J : CardinalFilteredPoset κ) : IsCardinalFiltered J.obj κ := J.property
109+
110+
instance (J : CardinalFilteredPoset κ) : IsFiltered J.obj :=
111+
isFiltered_of_isCardinalFiltered _ κ
112+
113+
instance (J : CardinalFilteredPoset κ) : Nonempty J.obj := IsFiltered.nonempty
114+
115+
instance : HasCardinalFilteredColimits (CardinalFilteredPoset κ) κ where
116+
hasColimitsOfShape J _ _ := by
117+
have := isFiltered_of_isCardinalFiltered J κ
118+
infer_instance
119+
120+
instance (A : Type u) [SmallCategory A] [IsCardinalFiltered A κ] :
121+
PreservesColimitsOfShape A (forget (CardinalFilteredPoset κ)) := by
122+
have := isFiltered_of_isCardinalFiltered A κ
123+
change PreservesColimitsOfShape A (CardinalFilteredPoset.ι ⋙ forget _)
124+
infer_instance
125+
126+
instance (J : CardinalFilteredPoset κ) (κ' : Cardinal.{u}) [Fact κ'.IsRegular] :
127+
IsCardinalFiltered (WithTop (J.obj)) κ' :=
128+
isCardinalFiltered_of_hasTerminal _ _
129+
130+
/-- The map `CardinalFilteredPoset κ → CardinalFilteredPoset κ` which sends
131+
a partially ordered `κ`-filtered type `J` to `WithTop J`. -/
132+
abbrev withTop (J : CardinalFilteredPoset κ) : CardinalFilteredPoset κ :=
133+
.of (.of (WithTop J.obj))
134+
135+
section
136+
137+
variable {J : CardinalFilteredPoset κ} (P : Set J.obj → Prop)
138+
[IsDirectedOrder (Subtype P)] [Nonempty (Subtype P)]
139+
[∀ (S : Subtype P), IsCardinalFiltered S.val κ]
140+
141+
/-- Given a predicate `P : Set J.obj → Prop` on the underlying type
142+
of `J : CardinalFilteredPoset κ` such that all the subsets satisfying `P`
143+
are `κ`-filtered, this is the functor `Subtype P ⥤ CardinalFilteredPoset κ`
144+
which sends a subset `S` of `J` satisfying `P` to the induced
145+
partially ordered type `J`, as an object in `CardinalFilteredPoset κ`. -/
146+
@[simps!]
147+
def functorOfPredicateSet : Subtype P ⥤ CardinalFilteredPoset κ :=
148+
ObjectProperty.lift _ (PartOrdEmb.functorOfPredicateSet P)
149+
(fun S ↦ by dsimp; infer_instance)
150+
151+
/-- Given a predicate `P : Set J.obj → Prop` on the underlying type
152+
of `J : CardinalFilteredPoset κ` such that all the subsets satisfying `P`
153+
are `κ`-filtered, this is the cocone with point `J` given
154+
by all the inclusions of the subsets satisfying `P`. -/
155+
@[simps]
156+
def coconeOfPredicateSet : Cocone (functorOfPredicateSet P) where
157+
pt := J
158+
ι.app j := ObjectProperty.homMk ((PartOrdEmb.coconeOfPredicateSet P).ι.app j)
159+
160+
/-- Let `P` be a predicate on `Set J.obj` where `J : CardinalFilteredPoset κ`.
161+
We assume that `Subtype P` is directed and nonempty, and that any `a : J.obj`
162+
belongs to some `S : Set J.obj` satisfying `P`. Then, `J` is the colimit in the
163+
category `CardinalFilteredPoset κ` of these subsets. -/
164+
noncomputable def isColimitCoconeOfPredicateSet
165+
(hP : ∀ (a : J.obj), ∃ (S : Set J.obj), P S ∧ a ∈ S) :
166+
IsColimit (coconeOfPredicateSet P) :=
167+
isColimitOfReflects CardinalFilteredPoset.ι
168+
(PartOrdEmb.isColimitOfPredicateSet P hP)
169+
170+
end
171+
172+
section
173+
174+
variable (J : CardinalFilteredPoset κ)
175+
176+
-- `@[nolint unusedArguments]` allows to setup some instances which uses
177+
-- the fact that `κ'` is regular.
178+
/-- Given `J : CardinalFilteredPoset κ` and a regular cardinal `κ'`,
179+
this is the predicate on `Set J.withTop.obj` that is satisfied by
180+
subsets that are of cardinality `< κ'` and contain `⊤`. -/
181+
@[nolint unusedArguments]
182+
def PropSetWithTop (κ' : Cardinal.{u}) [Fact κ'.IsRegular]
183+
(S : Set J.withTop.obj) : Prop :=
184+
HasCardinalLT S κ' ∧ ⊤ ∈ S
185+
186+
variable (κ' : Cardinal.{u}) [Fact κ'.IsRegular]
187+
188+
instance (S : Subtype (J.PropSetWithTop κ')) : HasTerminal S :=
189+
IsTerminal.hasTerminal (X := ⟨⊤, S.2.2⟩)
190+
(IsTerminal.ofUniqueHom (fun _ ↦ homOfLE (by rw [Subtype.mk_le_mk]; exact le_top))
191+
(fun _ _ ↦ rfl))
192+
193+
instance (S : Subtype (J.PropSetWithTop κ')) : IsCardinalFiltered S κ :=
194+
isCardinalFiltered_of_hasTerminal _ _
195+
196+
instance : IsCardinalFiltered (Subtype (J.PropSetWithTop κ')) κ' :=
197+
isCardinalFiltered_preorder _ _ (fun K α hK ↦ by
198+
rw [← hasCardinalLT_iff_cardinal_mk_lt] at hK
199+
have hκ' : Cardinal.aleph0 ≤ κ' := Cardinal.IsRegular.aleph0_le Fact.out
200+
refine ⟨⟨(⋃ (k : K), α k) ∪ {⊤},
201+
hasCardinalLT_union hκ' (hasCardinalLT_iUnion _ hK (fun k ↦ (α k).property.left))
202+
(hasCardinalLT_of_finite _ _ hκ'), by simp⟩, fun k ↦ ?_⟩
203+
rw [Subtype.mk_le_mk]
204+
simp only [Set.le_eq_subset]
205+
exact subset_trans (Set.subset_iUnion (fun i ↦ (α i).1) k) Set.subset_union_left)
206+
207+
instance : IsFiltered (Subtype (J.PropSetWithTop κ')) :=
208+
isFiltered_of_isCardinalFiltered _ κ'
209+
210+
instance : IsDirectedOrder (Subtype (J.PropSetWithTop κ')) :=
211+
IsFiltered.isDirectedOrder _
212+
213+
instance : Nonempty (Subtype (J.PropSetWithTop κ')) :=
214+
IsFiltered.nonempty
215+
216+
variable {J} in
217+
lemma propSetWithTop_pair (j : J.obj) : J.PropSetWithTop κ' {WithTop.some j, ⊤} :=
218+
⟨hasCardinalLT_of_finite _ _ (Cardinal.IsRegular.aleph0_le Fact.out),
219+
Set.mem_insert_of_mem _ (by simp)⟩
220+
221+
lemma exists_mem_propSetWithTop (a : J.withTop.obj) :
222+
∃ S, J.PropSetWithTop κ' S ∧ a ∈ S := by
223+
induction a with
224+
| some a => exact ⟨_, propSetWithTop_pair _ a, by aesop⟩
225+
| none => exact ⟨_, propSetWithTop_pair _ (Classical.arbitrary _), by aesop⟩
226+
227+
/-- If `J : CardinalFilteredPoset κ` and `κ'` is any regular cardinal,
228+
this is a colimit cocone which exhibits `J.withTop` as the `κ'`-filtered
229+
colimit of its subsets that are of cardinality `< κ'` and contain `⊤`. -/
230+
abbrev coconeWithTop : Cocone (functorOfPredicateSet (J.PropSetWithTop κ')) :=
231+
coconeOfPredicateSet (PropSetWithTop J κ')
232+
233+
/-- If `J : CardinalFilteredPoset κ` and `κ'` is any regular cardinal,
234+
then `J.withTop` is the `κ'`-filtered colimit of its subsets that are of
235+
cardinality `< κ'` and contain `⊤`. -/
236+
noncomputable def isColimitCoconeWithTop : IsColimit (coconeWithTop J κ') :=
237+
isColimitCoconeOfPredicateSet _ (fun a ↦ by
238+
induction a with
239+
| some a => exact ⟨_, propSetWithTop_pair _ a, by aesop⟩
240+
| none => exact ⟨_, propSetWithTop_pair _ (Classical.arbitrary _), by aesop⟩)
241+
242+
end
243+
244+
end CardinalFilteredPoset
245+
246+
end CategoryTheory

‎Mathlib/Order/Category/PartOrdEmb.lean‎

Lines changed: 66 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -161,6 +161,31 @@ def Iso.mk {α β : PartOrdEmb.{u}} (e : α ≃o β) : α ≅ β where
161161
hom := ofHom e
162162
inv := ofHom e.symm
163163

164+
/-- The order isomorphism corresponding to an isomorphism in `PartOrdEmb`. -/
165+
@[simps]
166+
def orderIsoOfIso {α β : PartOrdEmb.{u}} (e : α ≅ β) :
167+
α ≃o β where
168+
toFun := e.hom
169+
invFun := e.inv
170+
left_inv := ConcreteCategory.congr_hom e.hom_inv_id
171+
right_inv := ConcreteCategory.congr_hom e.inv_hom_id
172+
map_rel_iff' := Hom.le_iff_le _ _ _
173+
174+
/-- Isomorphisms in `PartOrdEmb` correspond to order isomorphisms. -/
175+
@[simps]
176+
def orderIsoEquivIso {α β : PartOrdEmb.{u}} :
177+
(α ≅ β) ≃ (α ≃o β) where
178+
toFun := orderIsoOfIso
179+
invFun := Iso.mk
180+
181+
instance : (forget PartOrdEmb.{u}).ReflectsIsomorphisms where
182+
reflects {α β} f hf := by
183+
rw [CategoryTheory.isIso_iff_bijective] at hf
184+
let e : α ≃o β :=
185+
{ toEquiv := Equiv.ofBijective _ hf
186+
map_rel_iff' := by simp }
187+
exact (Iso.mk e).isIso_hom
188+
164189
/-- `OrderDual` as a functor. -/
165190
@[simps map]
166191
def dual : PartOrdEmb ⥤ PartOrdEmb where
@@ -184,11 +209,10 @@ theorem partOrdEmb_dual_comp_forget_to_pardOrd :
184209

185210
namespace PartOrdEmb
186211

187-
variable {J : Type u} [SmallCategory J] [IsFiltered J] {F : J ⥤ PartOrdEmb.{u}}
188-
189212
namespace Limits
190213

191-
variable {c : Cocone (F ⋙ forget _)} (hc : IsColimit c)
214+
variable {J : Type u} [SmallCategory J] [IsFiltered J] {F : J ⥤ PartOrdEmb.{u}}
215+
{c : Cocone (F ⋙ forget _)} (hc : IsColimit c)
192216

193217
/-- Given a functor `F : J ⥤ PartOrdEmb` and a colimit cocone `c` for
194218
`F ⋙ forget _`, this is the type `c.pt` on which we define a partial order
@@ -319,6 +343,9 @@ instance : HasColimitsOfShape J PartOrdEmb.{u} where
319343

320344
instance : PreservesColimitsOfShape J (forget PartOrdEmb.{u}) where
321345

346+
instance : ReflectsColimitsOfShape J (forget PartOrdEmb.{u}) :=
347+
reflectsColimitsOfShape_of_reflectsIsomorphisms
348+
322349
instance : HasFilteredColimitsOfSize.{u, u} PartOrdEmb.{u} where
323350
HasColimitsOfShape _ := inferInstance
324351

@@ -327,4 +354,40 @@ instance : PreservesFilteredColimitsOfSize.{u, u} (forget PartOrdEmb.{u}) where
327354

328355
end Limits
329356

357+
variable {α : PartOrdEmb.{u}} (P : Set α → Prop)
358+
359+
/-- Given a predicate `P : Set α → Prop` on the underlying type of `α : PartOrdEmb.{u}`,
360+
this is the functor `Subtype P ⥤ PartOrdEmb.{u}` which sends a subset `J` of `α`
361+
satisfying `P` to the induced partially ordered type `J`. -/
362+
@[simps obj map]
363+
def functorOfPredicateSet : Subtype P ⥤ PartOrdEmb.{u} where
364+
obj J := .of J.val
365+
map f :=
366+
ofHom {
367+
toFun x := ⟨x, leOfHom f x.prop⟩
368+
inj' _ _ _ := by aesop
369+
map_rel_iff' := by rfl }
370+
371+
/-- Given a predicate `P : Set α → Prop` on the underlying type of `α : PartOrdEmb.{u}`,
372+
this is the cocone with point `α` given by all the inclusions of the subsets
373+
satisfying `P`. -/
374+
@[simps]
375+
def coconeOfPredicateSet : Cocone (functorOfPredicateSet P) where
376+
pt := α
377+
ι.app J := ofHom (OrderEmbedding.subtype _)
378+
379+
/-- Let `P` be a predicate on `Set α` where `α : PartOrdEmb`. We assume
380+
that `Subtype P` is directed and nonempty, and that any `a : α` belongs
381+
to some `J : Set α` satisfying `P`. Then, `α` is the colimit in the
382+
category `PartOrdEmb` of these subsets. -/
383+
noncomputable def isColimitOfPredicateSet
384+
[IsDirectedOrder (Subtype P)] [Nonempty (Subtype P)]
385+
(hP : ∀ (a : α), ∃ (J : Set α), P J ∧ a ∈ J) :
386+
IsColimit (coconeOfPredicateSet P) :=
387+
isColimitOfReflects (forget PartOrdEmb.{u}) (by
388+
refine Types.FilteredColimit.isColimitOf' _ _ (fun a ↦ ?_)
389+
(fun J x y h ↦ ⟨J, 𝟙 _, Subtype.ext h⟩)
390+
obtain ⟨J, hJ, ha⟩ := hP a
391+
exact ⟨⟨J, hJ⟩, ⟨a, ha⟩, rfl⟩)
392+
330393
end PartOrdEmb

0 commit comments

Comments
 (0)