Lemmas about sharply smaller regular cardinals

We obtain two lemmas Cardinal.SharplyLT.of_pow_lt and Cardinal.SharplyLT.of_le which allow to show that certain regular cardinals are sharply smaller than others. We also obtain Cardinal.SharplyLT.exists_of_small (and variants exists_of_pair and exists_of_triple) which shows that for any small family of regular cardinals, there exists a regular cardinal that is sharply greater than all the cardinals in the family.

References

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

def CategoryTheory.CardinalDirectedPoset.SetCardinalLT.fromSigma (κ : Cardinal.{u}) (X : Type u) (x : (κ' : ↑(Set.Iio κ)) × ((↑κ').ord.ToType → X)) : SetCardinalLT κ X

The surjectivity of this map (see lemma fromSigma_surjective) says that if X is a type, then any subset of X that is of cardinality < κ can be obtained as the range of a map κ'.ord.ToType → X for some κ' < κ.

Equations

• CategoryTheory.CardinalDirectedPoset.SetCardinalLT.fromSigma κ X x = ⟨Set.range x.snd, ⋯⟩

theorem CategoryTheory.CardinalDirectedPoset.SetCardinalLT.fromSigma_surjective (κ : Cardinal.{u}) (X : Type u) : Function.Surjective (fromSigma κ X)

If X is a type, then any subset of X that is of cardinality < κ can be obtained as the range of a map κ'.ord.ToType → X for some κ' < κ.

theorem Cardinal.SharplyLT.of_pow_lt {κ₁ κ₂ : Cardinal.{u}} [Fact κ₁.IsRegular] [Fact κ₂.IsRegular] (h₀ : κ₁ < κ₂) (h : ∀ (α β : Cardinal.{u}), α < κ₁ → β < κ₂ → β ^ α < κ₂) : κ₁.SharplyLT κ₂

theorem Cardinal.SharplyLT.succ_two_pow_of_le {κ₁ κ₂ : Cardinal.{u}} [Fact κ₁.IsRegular] (h₀ : κ₁ ≤ κ₂) (hκ₂ : aleph0 ≤ κ₂) : κ₁.SharplyLT (Order.succ (2 ^ κ₂))

theorem Cardinal.SharplyLT.exists_of_small {ι : Type u_1} [Small.{u, u_1} ι] (κ : ι → Cardinal.{u}) [∀ (i : ι), Fact (κ i).IsRegular] : ∃ (κ' : Cardinal.{u}) (x : Fact κ'.IsRegular), ∀ (i : ι), (κ i).SharplyLT κ'

theorem Cardinal.SharplyLT.exists_of_pair (κ₁ κ₂ : Cardinal.{u}) [Fact κ₁.IsRegular] [Fact κ₂.IsRegular] : ∃ (κ' : Cardinal.{u}) (x : Fact κ'.IsRegular), κ₁.SharplyLT κ' ∧ κ₂.SharplyLT κ'

theorem Cardinal.SharplyLT.exists_of_triple (κ₁ κ₂ κ₃ : Cardinal.{u}) [Fact κ₁.IsRegular] [Fact κ₂.IsRegular] [Fact κ₃.IsRegular] : ∃ (κ' : Cardinal.{u}) (x : Fact κ'.IsRegular), κ₁.SharplyLT κ' ∧ κ₂.SharplyLT κ' ∧ κ₃.SharplyLT κ'