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ý ((i) → (iii) is exists_cofinal_of_isCardinalAccessibleCategory_cardinalDirectedPoset, (iii) → (iv) is exists_isCardinalFiltered_set_of_exists_cofinal, (ii) → (i) is obvious; the rest is TODO @joelriou). Here, we take (i) as the definition.

References

• Adámek, J. and Rosický, J., Locally presentable and accessible categories

structure Cardinal.SharplyLT (κ₁ κ₂ : Cardinal.{w}) [Fact κ₁.IsRegular] [Fact κ₂.IsRegular] : Prop

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.

• lt : κ₁ < κ₂
• isCardinalAccessible_cardinalDirectedPoset : CategoryTheory.IsCardinalAccessibleCategory (CategoryTheory.CardinalDirectedPoset κ₁) κ₂

theorem Cardinal.SharplyLT.le {κ₁ κ₂ : Cardinal.{w}} [Fact κ₁.IsRegular] [Fact κ₂.IsRegular] (h : κ₁.SharplyLT κ₂) : κ₁ ≤ κ₂

theorem Cardinal.SharplyLT.exists_cofinal_of_isCardinalAccessibleCategory_cardinalDirectedPoset {κ₁ κ₂ : Cardinal.{w}} [Fact κ₁.IsRegular] [Fact κ₂.IsRegular] (h : κ₁ ≤ κ₂) [CategoryTheory.IsCardinalAccessibleCategory (CategoryTheory.CardinalDirectedPoset κ₁) κ₂] {X : Type w} (hX : HasCardinalLT X κ₂) : ∃ (Y : Set (CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ₁ X)), HasCardinalLT (↑Y) κ₂ ∧ IsCofinal Y

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.

theorem Cardinal.SharplyLT.exists_isCardinalFiltered_set_of_exists_cofinal {κ₁ κ₂ : Cardinal.{w}} [Fact κ₁.IsRegular] [Fact κ₂.IsRegular] (h₀ : κ₁ < κ₂) (h : ∀ (X : Type w), HasCardinalLT X κ₂ → ∃ (Y : Set (CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ₁ X)), HasCardinalLT (↑Y) κ₂ ∧ IsCofinal Y) {X : Type w} [PartialOrder X] [CategoryTheory.IsCardinalFiltered X κ₁] (A : Set X) (hA : HasCardinalLT (↑A) κ₂) : ∃ (B : Set X), A ⊆ B ∧ CategoryTheory.IsCardinalFiltered (↑B) κ₁ ∧ HasCardinalLT (↑B) κ₂

This is the implication (iii) → (iv) in the characterizations of SharplyLT κ₁ κ₂ in the docstring of this file.