Sharply smaller regular cardinals #
In this file, we introduce the predicate Cardinal.SharplyLT. Given two regular
cardinals κ₁ < κ₂, this condition can be described in different ways:
(i) the category CardinalDirectedPoset κ₁ (of κ₁-directed partially ordered
types, with order embeddings as morphisms), is κ₂-accessible;
(ii) any κ₁-accessible category is κ₂-accessible.
(iii) for any type X of cardinality < κ₂, there exists a cofinal set of
cardinality < κ₂ in the subtype of subsets of X of cardinality < κ₁;
(iv) for any κ₁-directed partially ordered type X and any subset A of X
of cardinality < κ₂, there exists a κ₁-directed subset B of X containing A
that is of cardinality < κ₂.
The equivalence of these conditions (i)-(iv) is Theorem 2.11 in the book by Adámek and Rosický.
Here, we take (i) as the definition, and the equivalence between the various definitions
is obtained in the lemma Cardinal.SharplyLT.tfae. In particular, using (ii),
we show that Cardinal.SharplyLT is transitive.
References #
If κ₁ < κ₂ are two regular cardinals, we say that κ₁ is sharply
smaller than κ₂ if the category CardinalDirectedPoset κ₁
is κ₂-accessible. There are other characterizations (TODO @joelriou),
including the property that any κ₁-accessible category is
also κ₂-accessible.
- isCardinalAccessible_cardinalDirectedPoset : CategoryTheory.IsCardinalAccessibleCategory (CategoryTheory.CardinalDirectedPoset κ₁) κ₂
Instances For
This is the implication (i) → (iii) in the characterizations
of SharplyLT κ₁ κ₂ in the docstring of this file.
The definitions in this section are part of the proof of the
lemma exists_isCardinalFiltered_set_of_exists_cofinal below,
which is the implication (iii) → (iv) in the characterizations
of SharplyLT κ₁ κ₂ which appear in the docstring of this file.
This is the implication (iii) → (iv) in the characterizations
of SharplyLT κ₁ κ₂ in the docstring of this file.
This is the closure of κ₁-presentable objects in the category C with respect
to colimits indexed by categories J such that Arrow J is of cardinality < κ₂.
When C is κ₁-accessible and κ₁ is sharply smaller than κ₂, then any
object of C is a κ₂-filtered colimit of objects in this closure,
see Cardinal.SharplyLT.isCardinalFilteredGenerator below.