Skip to content

Commit 6099442

Browse files
joelrioujoelriou
committed
feat(CategoryTheory/ObjectProperty): closure of a property under certain limits (#29854)
In this PR, given a property `P` of objects in a category `C` and family of categories `J : α → Type _`, we introduce the closure `P.limitsClosure J` of `P` under limits of shapes `J a` for all `a : α`, and under certain smallness circumstances, we show that its essentially small. - [x] depends on: #29851 - [x] depends on: #29881 - [x] depends on: #29903 - [x] depends on: #29849 - [x] depends on: #29843
1 parent 2fe1cd3 commit 6099442

File tree

6 files changed

+395
-0
lines changed

6 files changed

+395
-0
lines changed

‎Mathlib.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2717,11 +2717,13 @@ import Mathlib.CategoryTheory.Noetherian
27172717
import Mathlib.CategoryTheory.ObjectProperty.Basic
27182718
import Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
27192719
import Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
2720+
import Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
27202721
import Mathlib.CategoryTheory.ObjectProperty.ContainsZero
27212722
import Mathlib.CategoryTheory.ObjectProperty.EpiMono
27222723
import Mathlib.CategoryTheory.ObjectProperty.Extensions
27232724
import Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
27242725
import Mathlib.CategoryTheory.ObjectProperty.Ind
2726+
import Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
27252727
import Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
27262728
import Mathlib.CategoryTheory.ObjectProperty.Local
27272729
import Mathlib.CategoryTheory.ObjectProperty.Opposite

‎Mathlib/CategoryTheory/ObjectProperty/ClosedUnderIsomorphisms.lean‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -74,6 +74,10 @@ instance : IsClosedUnderIsomorphisms (isoClosure P) where
7474
rintro X Y e ⟨Z, hZ, ⟨f⟩⟩
7575
exact ⟨Z, hZ, ⟨e.symm.trans f⟩⟩
7676

77+
lemma isClosedUnderIsomorphisms_iff_isoClosure_eq_self :
78+
IsClosedUnderIsomorphisms P ↔ isoClosure P = P :=
79+
⟨fun _ ↦ isoClosure_eq_self _, fun h ↦ by rw [← h]; infer_instance⟩
80+
7781
instance (F : C ⥤ D) : IsClosedUnderIsomorphisms (P.map F) where
7882
of_iso := by
7983
rintro _ _ e ⟨X, hX, ⟨e'⟩⟩

‎Mathlib/CategoryTheory/ObjectProperty/CompleteLattice.lean‎

Lines changed: 75 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,75 @@
1+
/-
2+
Copyright (c) 2025 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+
import Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
7+
import Mathlib.Order.CompleteLattice.Basic
8+
9+
/-!
10+
# ObjectProperty is a complete lattice
11+
12+
-/
13+
14+
universe v u
15+
16+
namespace CategoryTheory.ObjectProperty
17+
18+
variable {C : Type u} [Category.{v} C]
19+
20+
example : CompleteLattice (ObjectProperty C) := inferInstance
21+
22+
section
23+
24+
variable (P Q : ObjectProperty C) (X : C)
25+
26+
@[simp high] lemma prop_inf_iff : (P ⊓ Q) X ↔ P X ∧ Q X := Iff.rfl
27+
28+
@[simp high] lemma prop_sup_iff : (P ⊔ Q) X ↔ P X ∨ Q X := Iff.rfl
29+
30+
lemma isoClosure_sup : (P ⊔ Q).isoClosure = P.isoClosure ⊔ Q.isoClosure := by
31+
ext X
32+
simp only [prop_sup_iff]
33+
constructor
34+
· rintro ⟨Y, hY, ⟨e⟩⟩
35+
simp only [prop_sup_iff] at hY
36+
obtain hY | hY := hY
37+
· exact Or.inl ⟨Y, hY, ⟨e⟩⟩
38+
· exact Or.inr ⟨Y, hY, ⟨e⟩⟩
39+
· rintro (hY | hY)
40+
· exact monotone_isoClosure le_sup_left _ hY
41+
· exact monotone_isoClosure le_sup_right _ hY
42+
43+
instance [P.IsClosedUnderIsomorphisms] [Q.IsClosedUnderIsomorphisms] :
44+
(P ⊔ Q).IsClosedUnderIsomorphisms := by
45+
simp only [isClosedUnderIsomorphisms_iff_isoClosure_eq_self, isoClosure_sup, isoClosure_eq_self]
46+
47+
end
48+
49+
section
50+
51+
variable {α : Sort*} (P : α → ObjectProperty C) (X : C)
52+
53+
@[simp high] lemma prop_iSup_iff :
54+
(⨆ (a : α), P a) X ↔ ∃ (a : α), P a X := by simp
55+
56+
lemma isoClosure_iSup :
57+
((⨆ (a : α), P a)).isoClosure = ⨆ (a : α), (P a).isoClosure := by
58+
refine le_antisymm ?_ ?_
59+
· rintro X ⟨Y, hY, ⟨e⟩⟩
60+
simp only [prop_iSup_iff] at hY ⊢
61+
obtain ⟨a, hY⟩ := hY
62+
exact ⟨a, _, hY, ⟨e⟩⟩
63+
· simp only [iSup_le_iff]
64+
intro a
65+
rw [isoClosure_le_iff]
66+
exact (le_iSup P a).trans (le_isoClosure _)
67+
68+
instance [∀ a, (P a).IsClosedUnderIsomorphisms] :
69+
((⨆ (a : α), P a)).IsClosedUnderIsomorphisms := by
70+
simp only [isClosedUnderIsomorphisms_iff_isoClosure_eq_self,
71+
isoClosure_iSup, isoClosure_eq_self]
72+
73+
end
74+
75+
end CategoryTheory.ObjectProperty

‎Mathlib/CategoryTheory/ObjectProperty/LimitsClosure.lean‎

Lines changed: 215 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,215 @@
1+
/-
2+
Copyright (c) 2025 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+
import Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
7+
import Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
8+
import Mathlib.Order.TransfiniteIteration
9+
import Mathlib.SetTheory.Cardinal.HasCardinalLT
10+
11+
/-!
12+
# Closure of a property of objects under limits of certain shapes
13+
14+
In this file, given a property `P` of objects in a category `C` and
15+
family of categories `J : α → Type _`, we introduce the closure
16+
`P.limitsClosure J` of `P` under limits of shapes `J a` for all `a : α`,
17+
and under certain smallness assumptions, we show that its essentially small.
18+
19+
-/
20+
universe w w' t v' u' v u
21+
22+
namespace CategoryTheory.ObjectProperty
23+
24+
open Limits
25+
26+
variable {C : Type u} [Category.{v} C] (P : ObjectProperty C)
27+
{α : Type t} (J : α → Type u') [∀ a, Category.{v'} (J a)]
28+
29+
/-- The closure of property of objects of a category under limits of
30+
shape `J a` for a family of categories `J`. -/
31+
inductive limitsClosure : ObjectProperty C
32+
| of_mem (X : C) (hX : P X) : limitsClosure X
33+
| of_isoClosure {X Y : C} (e : X ≅ Y) (hX : limitsClosure X) : limitsClosure Y
34+
| of_limitPresentation {X : C} {a : α} (pres : LimitPresentation (J a) X)
35+
(h : ∀ j, limitsClosure (pres.diag.obj j)) : limitsClosure X
36+
37+
@[simp]
38+
lemma le_limitsClosure : P ≤ P.limitsClosure J :=
39+
fun X hX ↦ .of_mem X hX
40+
41+
instance : (P.limitsClosure J).IsClosedUnderIsomorphisms where
42+
of_iso e hX := .of_isoClosure e hX
43+
44+
instance (a : α) : (P.limitsClosure J).IsClosedUnderLimitsOfShape (J a) where
45+
limitsOfShape_le := by
46+
rintro X ⟨hX⟩
47+
exact .of_limitPresentation hX.toLimitPresentation hX.prop_diag_obj
48+
49+
variable {P J} in
50+
lemma limitsClosure_le {Q : ObjectProperty C} [Q.IsClosedUnderIsomorphisms]
51+
[∀ (a : α), Q.IsClosedUnderLimitsOfShape (J a)] (h : P ≤ Q) :
52+
P.limitsClosure J ≤ Q := by
53+
intro X hX
54+
induction hX with
55+
| of_mem X hX => exact h _ hX
56+
| of_isoClosure e hX hX' => exact Q.prop_of_iso e hX'
57+
| of_limitPresentation pres h h' => exact Q.prop_of_isLimit pres.isLimit h'
58+
59+
variable {P} in
60+
lemma limitsClosure_monotone {Q : ObjectProperty C} (h : P ≤ Q) :
61+
P.limitsClosure J ≤ Q.limitsClosure J :=
62+
limitsClosure_le (h.trans (Q.le_limitsClosure J))
63+
64+
lemma limitsClosure_isoClosure :
65+
P.isoClosure.limitsClosure J = P.limitsClosure J := by
66+
refine le_antisymm (limitsClosure_le ?_)
67+
(limitsClosure_monotone _ P.le_isoClosure)
68+
rw [isoClosure_le_iff]
69+
exact le_limitsClosure P J
70+
71+
/-- Given `P : ObjectProperty C` and a family of categories `J : α → Type _`,
72+
this property objects contains `P` and all objects that are equal to `lim F`
73+
for some functor `F : J a ⥤ C` such that `F.obj j` satisfies `P` for any `j`. -/
74+
def strictLimitsClosureStep : ObjectProperty C :=
75+
P ⊔ (⨆ (a : α), P.strictLimitsOfShape (J a))
76+
77+
@[simp]
78+
lemma le_strictLimitsClosureStep : P ≤ P.strictLimitsClosureStep J := le_sup_left
79+
80+
variable {P} in
81+
lemma strictLimitsClosureStep_monotone {Q : ObjectProperty C} (h : P ≤ Q) :
82+
P.strictLimitsClosureStep J ≤ Q.strictLimitsClosureStep J := by
83+
dsimp [strictLimitsClosureStep]
84+
simp only [sup_le_iff, iSup_le_iff]
85+
exact ⟨h.trans le_sup_left, fun a ↦ (strictLimitsOfShape_monotone (J a) h).trans
86+
(le_trans (by rfl) ((le_iSup _ a).trans le_sup_right))⟩
87+
88+
section
89+
90+
variable {β : Type w'} [LinearOrder β] [OrderBot β] [SuccOrder β] [WellFoundedLT β]
91+
92+
/-- Given `P : ObjectProperty C`, a family of categories `J a`, this
93+
is the transfinite iteration of `Q ↦ Q.strictLimitsClosureStep J`. -/
94+
abbrev strictLimitsClosureIter (b : β) : ObjectProperty C :=
95+
transfiniteIterate (φ := fun Q ↦ Q.strictLimitsClosureStep J) b P
96+
97+
lemma le_strictLimitsClosureIter (b : β) :
98+
P ≤ P.strictLimitsClosureIter J b :=
99+
le_of_eq_of_le (transfiniteIterate_bot _ _).symm
100+
(monotone_transfiniteIterate _ _ (fun _ ↦ le_strictLimitsClosureStep _ _) bot_le)
101+
102+
lemma strictLimitsClosureIter_le_limitsClosure (b : β) :
103+
P.strictLimitsClosureIter J b ≤ P.limitsClosure J := by
104+
induction b using SuccOrder.limitRecOn with
105+
| isMin b hb =>
106+
obtain rfl := hb.eq_bot
107+
simp
108+
| succ b hb hb' =>
109+
rw [strictLimitsClosureIter, transfiniteIterate_succ _ _ _ hb,
110+
strictLimitsClosureStep, sup_le_iff, iSup_le_iff]
111+
exact ⟨hb', fun a ↦ ((strictLimitsOfShape_le_limitsOfShape _ _).trans
112+
(limitsOfShape_monotone _ hb')).trans (limitsOfShape_le _ _)⟩
113+
| isSuccLimit b hb hb' =>
114+
simp only [transfiniteIterate_limit _ _ _ hb,
115+
iSup_le_iff, Subtype.forall, Set.mem_Iio]
116+
intro c hc
117+
exact hb' _ hc
118+
119+
instance [ObjectProperty.Small.{w} P] [LocallySmall.{w} C] [Small.{w} α]
120+
[∀ a, Small.{w} (J a)] [∀ a, LocallySmall.{w} (J a)] (b : β)
121+
[hb₀ : Small.{w} (Set.Iio b)] :
122+
ObjectProperty.Small.{w} (P.strictLimitsClosureIter J b) := by
123+
have H {b c : β} (hbc : b ≤ c) [Small.{w} (Set.Iio c)] : Small.{w} (Set.Iio b) :=
124+
small_of_injective (f := fun x ↦ (⟨x.1, lt_of_lt_of_le x.2 hbc⟩ : Set.Iio c))
125+
(fun _ _ _ ↦ by aesop)
126+
induction b using SuccOrder.limitRecOn generalizing hb₀ with
127+
| isMin b hb =>
128+
obtain rfl := hb.eq_bot
129+
simp only [transfiniteIterate_bot]
130+
infer_instance
131+
| succ b hb hb' =>
132+
have := H (Order.le_succ b)
133+
rw [strictLimitsClosureIter, transfiniteIterate_succ _ _ _ hb,
134+
strictLimitsClosureStep]
135+
infer_instance
136+
| isSuccLimit b hb hb' =>
137+
simp only [transfiniteIterate_limit _ _ _ hb]
138+
have (c : Set.Iio b) : ObjectProperty.Small.{w}
139+
(transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) c.1 P) := by
140+
have := H c.2.le
141+
exact hb' c.1 c.2
142+
infer_instance
143+
144+
end
145+
146+
section
147+
148+
variable (κ : Cardinal.{w}) [Fact κ.IsRegular] (h : ∀ (a : α), HasCardinalLT (J a) κ)
149+
150+
include h
151+
152+
lemma strictLimitsClosureStep_strictLimitsClosureIter_eq_self :
153+
(P.strictLimitsClosureIter J κ.ord).strictLimitsClosureStep J =
154+
(P.strictLimitsClosureIter J κ.ord) := by
155+
have hκ : κ.IsRegular := Fact.out
156+
have (a : α) := (h a).small
157+
refine le_antisymm (fun X hX ↦ ?_) (le_strictLimitsClosureStep _ _)
158+
simp only [strictLimitsClosureStep, prop_sup_iff, prop_iSup_iff] at hX
159+
obtain (hX | ⟨a, F, hF⟩) := hX
160+
· exact hX
161+
· simp only [strictLimitsClosureIter, transfiniteIterate_limit _ _ _
162+
(Cardinal.isSuccLimit_ord hκ.aleph0_le), prop_iSup_iff,
163+
Subtype.exists, Set.mem_Iio, exists_prop] at hF
164+
choose o ho ho' using hF
165+
obtain ⟨m, hm, hm'⟩ : ∃ (m : Ordinal.{w}) (hm : m < κ.ord), ∀ (j : J a), o j ≤ m := by
166+
refine ⟨⨆ j, o ((equivShrink.{w} (J a)).symm j),
167+
Ordinal.iSup_lt_ord ?_ (fun _ ↦ ho _), fun j ↦ ?_⟩
168+
· rw [hκ.cof_eq, ← hasCardinalLT_iff_cardinal_mk_lt _ κ,
169+
← hasCardinalLT_iff_of_equiv (equivShrink.{w} (J a))]
170+
exact h a
171+
· obtain ⟨j, rfl⟩ := (equivShrink.{w} (J a)).symm.surjective j
172+
exact le_ciSup (Ordinal.bddAbove_range _) _
173+
refine monotone_transfiniteIterate _ _
174+
(fun (Q : ObjectProperty C) ↦ Q.le_strictLimitsClosureStep J) (Order.succ_le_iff.2 hm) _ ?_
175+
dsimp
176+
rw [transfiniteIterate_succ _ _ _ (by simp)]
177+
simp only [strictLimitsClosureStep, prop_sup_iff, prop_iSup_iff]
178+
exact Or.inr ⟨a, ⟨_, fun j ↦ monotone_transfiniteIterate _ _
179+
(fun (Q : ObjectProperty C) ↦ Q.le_strictLimitsClosureStep J) (hm' j) _ (ho' j)⟩⟩
180+
181+
lemma isoClosure_strictLimitsClosureIter_eq_limitsClosure :
182+
(P.strictLimitsClosureIter J κ.ord).isoClosure = P.limitsClosure J := by
183+
refine le_antisymm ?_ ?_
184+
· rw [isoClosure_le_iff]
185+
exact P.strictLimitsClosureIter_le_limitsClosure J κ.ord
186+
· have (a : α) :
187+
(P.strictLimitsClosureIter J κ.ord).isoClosure.IsClosedUnderLimitsOfShape (J a) := ⟨by
188+
conv_rhs => rw [← P.strictLimitsClosureStep_strictLimitsClosureIter_eq_self J κ h]
189+
rw [limitsOfShape_isoClosure, ← isoClosure_strictLimitsOfShape,
190+
strictLimitsClosureStep]
191+
exact monotone_isoClosure ((le_trans (by rfl) (le_iSup _ a)).trans le_sup_right)⟩
192+
refine limitsClosure_le
193+
((P.le_strictLimitsClosureIter J κ.ord).trans (le_isoClosure _))
194+
195+
lemma isEssentiallySmall_limitsClosure
196+
[ObjectProperty.EssentiallySmall.{w} P] [LocallySmall.{w} C] [Small.{w} α]
197+
[∀ a, Small.{w} (J a)] [∀ a, LocallySmall.{w} (J a)] :
198+
ObjectProperty.EssentiallySmall.{w} (P.limitsClosure J) := by
199+
obtain ⟨Q, hQ, hQ₁, hQ₂⟩ := EssentiallySmall.exists_small_le.{w} P
200+
have : ObjectProperty.EssentiallySmall.{w} (Q.isoClosure.limitsClosure J) := by
201+
rw [limitsClosure_isoClosure,
202+
← Q.isoClosure_strictLimitsClosureIter_eq_limitsClosure J κ h]
203+
infer_instance
204+
exact .of_le (limitsClosure_monotone J hQ₂)
205+
206+
end
207+
208+
instance [ObjectProperty.EssentiallySmall.{w} P] [LocallySmall.{w} C] [Small.{w} α]
209+
[∀ a, Small.{w} (J a)] [∀ a, LocallySmall.{w} (J a)] :
210+
ObjectProperty.EssentiallySmall.{w} (P.limitsClosure J) := by
211+
obtain ⟨κ, h₁, h₂⟩ := HasCardinalLT.exists_regular_cardinal_forall J
212+
have : Fact κ.IsRegular := ⟨h₁⟩
213+
exact isEssentiallySmall_limitsClosure P J κ h₂
214+
215+
end CategoryTheory.ObjectProperty

‎Mathlib/CategoryTheory/ObjectProperty/LimitsOfShape.lean‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -144,6 +144,11 @@ instance [ObjectProperty.Small.{w} P] [LocallySmall.{w} C] [Small.{w} J] [Locall
144144
rintro ⟨_, ⟨F, hF⟩⟩
145145
exact ⟨⟨P.lift F hF, by assumption⟩, rfl⟩
146146

147+
instance [ObjectProperty.Small.{w} P] [LocallySmall.{w} C] [Small.{w} J] [LocallySmall.{w} J] :
148+
ObjectProperty.EssentiallySmall.{w} (P.limitsOfShape J) := by
149+
rw [← isoClosure_strictLimitsOfShape]
150+
infer_instance
151+
147152
/-- A property of objects satisfies `P.IsClosedUnderLimitsOfShape J` if it
148153
is stable by limits of shape `J`. -/
149154
@[mk_iff]

0 commit comments

Comments
 (0)