Skip to content

Commit 0265743

Browse files
ScriptRaccoonScriptRaccoon
committed
generate yaml files for all implications by topic
1 parent 013ee40 commit 0265743

31 files changed

Lines changed: 2340 additions & 23 deletions

‎.vscode/settings.json‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -229,6 +229,7 @@
229229
"surjectivity",
230230
"Tarski",
231231
"tensoring",
232+
"topoi",
232233
"Turso",
233234
"unital",
234235
"unitalization",

‎databases/catdat/data_yaml/category-implications/Malcev.yaml‎

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
# results on Malcev and unital categories
2+
3+
- id: malcev_condition
4+
assumptions:
5+
- Malcev
6+
conclusions:
7+
- finitely complete
8+
reason: This holds by definition.
9+
is_equivalence: false
10+
11+
- id: malcev_thin_condition
12+
assumptions:
13+
- finitely complete
14+
- thin
15+
conclusions:
16+
- Malcev
17+
reason: In a thin category, every subobject of $X^2 = X$ containing $X$ is already $X$.
18+
is_equivalence: false
19+
20+
- id: malcev_additive_criterion
21+
assumptions:
22+
- additive
23+
- finitely complete
24+
conclusions:
25+
- Malcev
26+
reason: See Prop. 2.2.13. in <a href="https://ncatlab.org/nlab/show/Malcev,+protomodular,+homological+and+semi-abelian+categories" target="_blank">Malcev, protomodular, homological and semi-abelian categories</a>.
27+
is_equivalence: false
28+
29+
- id: malcev_implies_unital
30+
assumptions:
31+
- Malcev
32+
- pointed
33+
conclusions:
34+
- unital
35+
reason: This follows from Corollary 2.2.10 in <a href="https://ncatlab.org/nlab/show/Malcev,+protomodular,+homological+and+semi-abelian+categories" target="_blank">Malcev, protomodular, homological and semi-abelian categories</a>. The proof is also written down in <a href="https://math.stackexchange.com/a/5034834/1650" target="_blank">MSE/5033161</a>.
36+
is_equivalence: false
37+
38+
- id: biproducts_unital
39+
assumptions:
40+
- biproducts
41+
- finitely complete
42+
conclusions:
43+
- unital
44+
reason: For all objects $X,Y$ the morphism $X \sqcup Y \to X \times Y$ is an isomorphism, hence a strong epimorphism.
45+
is_equivalence: false
46+
47+
- id: unital_assumptions
48+
assumptions:
49+
- unital
50+
conclusions:
51+
- finitely complete
52+
- pointed
53+
reason: This holds by definition.
54+
is_equivalence: false

‎databases/catdat/data_yaml/category-implications/NNO.yaml‎

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
# results on natural numbers objects
2+
3+
- id: nno_assumption
4+
assumptions:
5+
- natural numbers object
6+
conclusions:
7+
- finite products
8+
reason: This holds by definition.
9+
is_equivalence: false
10+
11+
- id: nno_criterion
12+
assumptions:
13+
- countably distributive
14+
conclusions:
15+
- natural numbers object
16+
reason: "Consider the copower $N := \\coprod_{n \\in \\IN} 1$ with inclusions $i_n : 1 \\to N$ for $n \\in \\IN$. We define $z := i_1 : 1 \\to N$ and $s : N \\to N$ by $s \\circ i_n = i_{n+1}$. Since the category is countably distributive, we have $A \\times N \\cong \\coprod_{n \\in \\IN} A$ for every object $A$. Given morphisms $f : A \\to X$, $g : X \\to X$, a morphism $\\Phi : A \\times N \\to X$ therefore corresponds to a family of morphisms $\\phi_n : A \\to X$ for $n \\in \\IN$. The condition $\\Phi(a,z)=f(a)$ becomes $\\phi_0 = f$. The condition $\\Phi(a,s(n)) = g(\\Phi(a,n))$ becomes $\\phi_{n+1} = g \\circ \\phi_n$. This recursively defines the morphisms $\\phi_n$. (We are basically using that $\\IN$ is a natural numbers object in $\\Set$.) Concretely, $\\phi_n = g^n \\circ f$."
17+
is_equivalence: false
18+
19+
- id: nno_pointed_case
20+
assumptions:
21+
- natural numbers object
22+
- pointed
23+
conclusions:
24+
- trivial
25+
reason: "Let $(N,z,s)$ be a natural numbers object in a category with a zero object, denoted $0$. The morphism $z : 0 \\to N$ must be zero. The universal property applied to $A=1$ implies that $s : N \\to N$ is an initial object in the category of endomorphisms. This exists, it is given by the identity $0 \\to 0$. Therefore, $N = 0$. The general universal property now becomes: For all $f : A \\to X$, $g : X \\to X$ there is a unique $\\Phi : A \\to X$ such that $\\Phi(a) = f(a)$ and $\\Phi(a)=g(\\Phi(a))$. Apply this to $g = 0$ to conclude $f = 0$."
26+
is_equivalence: false
27+
28+
- id: nno_terminal
29+
assumptions:
30+
- natural numbers object
31+
- strict terminal object
32+
conclusions:
33+
- one-way
34+
reason: "By assumption, $z : 1 \\to N$ is an isomorphism. Therefore, the terminal object $1$ is a NNO with $z = \\id_1$ and $s = \\id_1$. This precisely means that for all $f : A \\to X$ and $g : X \\to X$ there is a unique $\\Phi : A \\to X$ with $\\Phi = f$ and $\\Phi = g \\circ \\Phi$. In other words, we have $f = g \\circ f$, and therefore $g = \\id_X$ (take $f = \\id_X$), which proves the claim. (From here one can further deduce that the category is thin.)"
35+
is_equivalence: false
36+
37+
- id: nno_thin
38+
assumptions:
39+
- finite products
40+
- thin
41+
conclusions:
42+
- natural numbers object
43+
reason: The triple $(1, \id_1, \id_1)$ is clearly a NNO.
44+
is_equivalence: false

‎databases/catdat/data_yaml/category-implications/accessible.yaml‎

Lines changed: 241 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,241 @@
1+
# results on locally presentable categories, accessible categories,
2+
# and related notions such as locally strongly finitely presentable, etc.
3+
4+
- id: locally_presentable_definition_finite
5+
assumptions:
6+
- locally finitely presentable
7+
conclusions:
8+
- cocomplete
9+
- finitely accessible
10+
reason: This follows from one of equivalent formulations of locally finitely presentable categories.
11+
is_equivalence: true
12+
13+
- id: locally_presentable_definition_countable
14+
assumptions:
15+
- locally ℵ₁-presentable
16+
conclusions:
17+
- cocomplete
18+
- ℵ₁-accessible
19+
reason: This follows from one of equivalent formulations of locally ℵ₁-presentable categories.
20+
is_equivalence: true
21+
22+
- id: locally_presentable_definition
23+
assumptions:
24+
- locally presentable
25+
conclusions:
26+
- accessible
27+
- cocomplete
28+
reason: This follows from one of equivalent formulations of locally presentable categories.
29+
is_equivalence: true
30+
31+
- id: locally_finitely_presentable_consequence
32+
assumptions:
33+
- locally finitely presentable
34+
conclusions:
35+
- exact filtered colimits
36+
reason: Special case of <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>, Prop. 1.59 with $\lambda = \aleph_0$.
37+
is_equivalence: false
38+
39+
- id: locally_finitely_presentable_raise
40+
assumptions:
41+
- locally finitely presentable
42+
conclusions:
43+
- locally ℵ₁-presentable
44+
reason: This is trivial.
45+
is_equivalence: false
46+
47+
- id: locally_countably_presentable_raise
48+
assumptions:
49+
- locally ℵ₁-presentable
50+
conclusions:
51+
- locally presentable
52+
reason: This is trivial.
53+
is_equivalence: false
54+
55+
- id: accessible_trivial_consequence
56+
assumptions:
57+
- accessible
58+
conclusions:
59+
- generating set
60+
reason: For a $\kappa$-accessible category, the set $G$ appearing in the definition gives a small dense full subcategory, which is in particular a generating set.
61+
is_equivalence: false
62+
63+
- id: accessible_well-powered
64+
assumptions:
65+
- accessible
66+
conclusions:
67+
- well-powered
68+
reason: See <a href="https://ncatlab.org/nlab/show/accessible+category#wellpoweredness_and_wellcopoweredness" target="_blank">nLab</a>.
69+
is_equivalence: false
70+
71+
- id: accessible_locally_small
72+
assumptions:
73+
- accessible
74+
conclusions:
75+
- locally essentially small
76+
reason: See the proof of Prop. 2.1.5 in <a href="https://bookstore.ams.org/conm-104" target="_blank">Makkai-Pare</a>.
77+
is_equivalence: false
78+
79+
- id: accessible_well-copowered
80+
assumptions:
81+
- accessible
82+
- pushouts
83+
conclusions:
84+
- well-copowered
85+
reason: See Thm. 2.49 in <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a> or Prop. 6.1.3 in <a href="https://bookstore.ams.org/conm-104" target="_blank">Makkai-Pare</a>.
86+
is_equivalence: false
87+
88+
- id: finite_accessible
89+
assumptions:
90+
- Cauchy complete
91+
- essentially finite
92+
conclusions:
93+
- finitely accessible
94+
reason: See <a href="https://mathoverflow.net/questions/509853" target="_blank">MO/509853</a>, where it is in fact shown that the ind-completion of any finite Cauchy-complete category becomes itself.
95+
is_equivalence: false
96+
97+
- id: locally_presentable_essentially_small
98+
assumptions:
99+
- locally copresentable
100+
- locally presentable
101+
conclusions:
102+
- essentially small
103+
reason: This follows from <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>, Thm. 1.64.
104+
is_equivalence: false
105+
106+
- id: grothendieck_abelian_presentable
107+
assumptions:
108+
- Grothendieck abelian
109+
conclusions:
110+
- locally presentable
111+
reason: See <a href="https://arxiv.org/abs/1409.7051" target="_blank">Deriving Auslander's formula</a>, Cor. 5.2, or <a href="https://arxiv.org/abs/math/0102087" target="_blank">Sheafifiable homotopy model categories</a>, Prop. 3.10.
112+
is_equivalence: false
113+
114+
- id: locally_strongly_finitely_presentable_raise
115+
assumptions:
116+
- locally strongly finitely presentable
117+
conclusions:
118+
- locally finitely presentable
119+
reason: See <a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>, Cor. 3.7.
120+
is_equivalence: false
121+
122+
- id: finitely_accessible_raise
123+
assumptions:
124+
- finitely accessible
125+
conclusions:
126+
- ℵ₁-accessible
127+
reason: This is because any regular cardinal is strictly smaller than its successor cardinal. See <a href="https://ncatlab.org/nlab/show/sharply+smaller+cardinal" target="_blank">nLab</a>.
128+
is_equivalence: false
129+
130+
- id: countably_accessible_special_case
131+
assumptions:
132+
- ℵ₁-accessible
133+
conclusions:
134+
- accessible
135+
reason: This is trivial.
136+
is_equivalence: false
137+
138+
- id: accessible_require_filtered_colimit
139+
assumptions:
140+
- finitely accessible
141+
conclusions:
142+
- filtered colimits
143+
reason: This holds by definition.
144+
is_equivalence: false
145+
146+
- id: accessible_require_Cauchy_complete
147+
assumptions:
148+
- accessible
149+
conclusions:
150+
- Cauchy complete
151+
reason: This is because the walking idempotent is $\kappa$-filtered for any regular cardinal $\kappa$.
152+
is_equivalence: false
153+
154+
- id: small_accessible_characterization
155+
assumptions:
156+
- Cauchy complete
157+
- essentially small
158+
conclusions:
159+
- accessible
160+
reason: See <a href="https://bookstore.ams.org/conm-104" target="_blank">Makkai-Pare</a>, Thm. 2.2.2.
161+
is_equivalence: false
162+
163+
- id: countably_accessible_thin
164+
assumptions:
165+
- essentially countable
166+
- thin
167+
conclusions:
168+
- ℵ₁-accessible
169+
reason: In general, every $\kappa$-filtered diagram in a poset whose elements are less than $\kappa$ admits the greatest element. Therefore, all the elements are $\kappa$-presentable, and the poset is $\kappa$-accessible.
170+
is_equivalence: false
171+
172+
- id: locally_presentable_another_definition
173+
assumptions:
174+
- accessible
175+
- complete
176+
conclusions:
177+
- locally presentable
178+
reason: This follows from one of equivalent formulations of locally presentable categories.
179+
is_equivalence: false
180+
181+
- id: locally_strongly_finitely_presentable_definition
182+
assumptions:
183+
- locally strongly finitely presentable
184+
conclusions:
185+
- cocomplete
186+
- generalized variety
187+
reason: This is trivial.
188+
is_equivalence: true
189+
190+
- id: locally_multi-presentable_definition
191+
assumptions:
192+
- locally multi-presentable
193+
conclusions:
194+
- accessible
195+
- connected limits
196+
reason: This follows from one of equivalent formulations of locally multi-presentable categories.
197+
is_equivalence: true
198+
199+
- id: locally_multi-presentable_another_definition
200+
assumptions:
201+
- locally multi-presentable
202+
conclusions:
203+
- accessible
204+
- multi-cocomplete
205+
reason: This follows from one of equivalent formulations of locally multi-presentable categories.
206+
is_equivalence: true
207+
208+
- id: locally_finitely_multi-presentable_definition
209+
assumptions:
210+
- locally finitely multi-presentable
211+
conclusions:
212+
- connected limits
213+
- finitely accessible
214+
reason: This follows from one of equivalent formulations of locally finitely multi-presentable categories.
215+
is_equivalence: true
216+
217+
- id: locally_finitely_multi-presentable_another_definition
218+
assumptions:
219+
- locally finitely multi-presentable
220+
conclusions:
221+
- finitely accessible
222+
- multi-cocomplete
223+
reason: This follows from one of equivalent formulations of locally finitely multi-presentable categories.
224+
is_equivalence: true
225+
226+
- id: locally_poly-presentable_definition
227+
assumptions:
228+
- locally poly-presentable
229+
conclusions:
230+
- accessible
231+
- wide pullbacks
232+
reason: This holds by definition.
233+
is_equivalence: true
234+
235+
- id: locally-finitely-multi-presentable_stable-monos
236+
assumptions:
237+
- locally finitely multi-presentable
238+
conclusions:
239+
- filtered-colimit-stable monomorphisms
240+
reason: Every locally finitely multi-presentable category is a multi-reflective full subcategory of a presheaf category closed under filtered colimits (<a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>, 4.30). Since multi-reflective full subcategories are in general closed under connected limits (<a href="https://ncatlab.org/nlab/show/Locally+Presentable+and+Accessible+Categories" target="_blank">Adamek-Rosicky</a>, Thm. 4.26), in particular, we can calculate not only filtered colimits but also kernel pairs as well as in a presheaf category.
241+
is_equivalence: false

0 commit comments

Comments
 (0)