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.
This notion is used in the file Mathlib/CategoryTheory/Presentable/Uniformization.lean
in the proof of the uniformization theorem for accessible categories.
References #
- [Adámek, J. and Rosický, J., Locally presentable and accessible categories][Adamek_Rosicky_1994]
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
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.
@[implicit_reducible]
def
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT
(κ₁ κ₂ : Cardinal.{w})
[Fact κ₁.IsRegular]
(J : Type w)
[PartialOrder J]
(A : Set J)
:
Given a partially ordered type J, this is the property
of subsets of J that are κ₁-directed and of cardinality < κ₂.
Equations
- Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J A = (CategoryTheory.IsCardinalFiltered (↑A) κ₁ ∧ HasCardinalLT (↑A) κ₂)
Instances For
instance
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT.instHasColimitElemValSetCompFunctorDiag
(κ₁ κ₂ : Cardinal.{w})
[Fact κ₁.IsRegular]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{J : Type w}
[PartialOrder J]
(p : (CategoryTheory.isCardinalPresentable C κ₁).ColimitOfShape J X)
[CategoryTheory.IsCardinalAccessibleCategory C κ₁]
(A : Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J))
:
@[reducible, inline]
noncomputable abbrev
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT.colimit
(κ₁ κ₂ : Cardinal.{w})
[Fact κ₁.IsRegular]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{J : Type w}
[PartialOrder J]
(p : (CategoryTheory.isCardinalPresentable C κ₁).ColimitOfShape J X)
[CategoryTheory.IsCardinalAccessibleCategory C κ₁]
(A : Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J))
:
C
Given a presentation p of X : C as a colimit indexed by a partially
ordered type J of κ₁-presentable objects and A a subset of J
that is κ₁-directed and of cardinality < κ₂, this is
the colimit of the restriction of the diagram p.diag to A.
Equations
Instances For
@[reducible, inline]
noncomputable abbrev
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT.colimit.ι
(κ₁ κ₂ : Cardinal.{w})
[Fact κ₁.IsRegular]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{J : Type w}
[PartialOrder J]
(p : (CategoryTheory.isCardinalPresentable C κ₁).ColimitOfShape J X)
[CategoryTheory.IsCardinalAccessibleCategory C κ₁]
(A : Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J))
(a : J)
(ha : a ∈ ↑A)
:
The inclusions in colimit.
Equations
- Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT.colimit.ι κ₁ κ₂ p A a ha = CategoryTheory.Limits.colimit.ι (⋯.functor.comp p.diag) ⟨a, ha⟩
Instances For
noncomputable def
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT.colimit.map
(κ₁ κ₂ : Cardinal.{w})
[Fact κ₁.IsRegular]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{J : Type w}
[PartialOrder J]
(p : (CategoryTheory.isCardinalPresentable C κ₁).ColimitOfShape J X)
[CategoryTheory.IsCardinalAccessibleCategory C κ₁]
{A₁ A₂ : Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J)}
(hA : A₁ ≤ A₂)
:
The functoriality of colimit with respect to the subset A.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT.colimit.ι_map
(κ₁ κ₂ : Cardinal.{w})
[Fact κ₁.IsRegular]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{J : Type w}
[PartialOrder J]
(p : (CategoryTheory.isCardinalPresentable C κ₁).ColimitOfShape J X)
[CategoryTheory.IsCardinalAccessibleCategory C κ₁]
{A₁ A₂ : Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J)}
(hA : A₁ ≤ A₂)
(j : J)
(hj : j ∈ ↑A₁)
:
@[simp]
theorem
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT.colimit.ι_map_assoc
(κ₁ κ₂ : Cardinal.{w})
[Fact κ₁.IsRegular]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{J : Type w}
[PartialOrder J]
(p : (CategoryTheory.isCardinalPresentable C κ₁).ColimitOfShape J X)
[CategoryTheory.IsCardinalAccessibleCategory C κ₁]
{A₁ A₂ : Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J)}
(hA : A₁ ≤ A₂)
(j : J)
(hj : j ∈ ↑A₁)
{Z : C}
(h : colimit κ₁ κ₂ p A₂ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (ι κ₁ κ₂ p A₁ j hj) (CategoryTheory.CategoryStruct.comp (map κ₁ κ₂ p hA) h) = CategoryTheory.CategoryStruct.comp (ι κ₁ κ₂ p A₂ j ⋯) h
theorem
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT.colimit.hom_ext
(κ₁ κ₂ : Cardinal.{w})
[Fact κ₁.IsRegular]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{J : Type w}
[PartialOrder J]
(p : (CategoryTheory.isCardinalPresentable C κ₁).ColimitOfShape J X)
[CategoryTheory.IsCardinalAccessibleCategory C κ₁]
{A : Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J)}
{T : C}
{φ₁ φ₂ : colimit κ₁ κ₂ p A ⟶ T}
(h :
∀ (j : J) (hj : j ∈ ↑A),
CategoryTheory.CategoryStruct.comp (ι κ₁ κ₂ p A j hj) φ₁ = CategoryTheory.CategoryStruct.comp (ι κ₁ κ₂ p A j hj) φ₂)
:
theorem
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT.colimit.hom_ext_iff
{κ₁ κ₂ : Cardinal.{w}}
[Fact κ₁.IsRegular]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{J : Type w}
[PartialOrder J]
{p : (CategoryTheory.isCardinalPresentable C κ₁).ColimitOfShape J X}
[CategoryTheory.IsCardinalAccessibleCategory C κ₁]
{A : Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J)}
{T : C}
{φ₁ φ₂ : colimit κ₁ κ₂ p A ⟶ T}
:
φ₁ = φ₂ ↔ ∀ (j : J) (hj : j ∈ ↑A),
CategoryTheory.CategoryStruct.comp (ι κ₁ κ₂ p A j hj) φ₁ = CategoryTheory.CategoryStruct.comp (ι κ₁ κ₂ p A j hj) φ₂
noncomputable def
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT.colimit.π
(κ₁ κ₂ : Cardinal.{w})
[Fact κ₁.IsRegular]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{J : Type w}
[PartialOrder J]
(p : (CategoryTheory.isCardinalPresentable C κ₁).ColimitOfShape J X)
[CategoryTheory.IsCardinalAccessibleCategory C κ₁]
(A : Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J))
:
As X is the colimit of a diagram p.diag, this is the induced morphism
colimit κ₁ κ₂ p A ⟶ X from the colimit of the restriction of this diagram to A.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT.colimit.ι_π
(κ₁ κ₂ : Cardinal.{w})
[Fact κ₁.IsRegular]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{J : Type w}
[PartialOrder J]
(p : (CategoryTheory.isCardinalPresentable C κ₁).ColimitOfShape J X)
[CategoryTheory.IsCardinalAccessibleCategory C κ₁]
(A : Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J))
(a : J)
(ha : a ∈ ↑A)
:
@[simp]
theorem
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT.colimit.ι_π_assoc
(κ₁ κ₂ : Cardinal.{w})
[Fact κ₁.IsRegular]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{J : Type w}
[PartialOrder J]
(p : (CategoryTheory.isCardinalPresentable C κ₁).ColimitOfShape J X)
[CategoryTheory.IsCardinalAccessibleCategory C κ₁]
(A : Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J))
(a : J)
(ha : a ∈ ↑A)
{Z : C}
(h : X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (ι κ₁ κ₂ p A a ha) (CategoryTheory.CategoryStruct.comp (π κ₁ κ₂ p A) h) = CategoryTheory.CategoryStruct.comp (p.ι.app a) h
@[simp]
theorem
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT.colimit.map_π
(κ₁ κ₂ : Cardinal.{w})
[Fact κ₁.IsRegular]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{J : Type w}
[PartialOrder J]
(p : (CategoryTheory.isCardinalPresentable C κ₁).ColimitOfShape J X)
[CategoryTheory.IsCardinalAccessibleCategory C κ₁]
{A₁ A₂ : Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J)}
(hA : A₁ ≤ A₂)
:
@[simp]
theorem
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT.colimit.map_π_assoc
(κ₁ κ₂ : Cardinal.{w})
[Fact κ₁.IsRegular]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{J : Type w}
[PartialOrder J]
(p : (CategoryTheory.isCardinalPresentable C κ₁).ColimitOfShape J X)
[CategoryTheory.IsCardinalAccessibleCategory C κ₁]
{A₁ A₂ : Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J)}
(hA : A₁ ≤ A₂)
{Z : C}
(h : X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (map κ₁ κ₂ p hA) (CategoryTheory.CategoryStruct.comp (π κ₁ κ₂ p A₂) h) = CategoryTheory.CategoryStruct.comp (π κ₁ κ₂ p A₁) h
noncomputable def
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT.functor
(κ₁ κ₂ : Cardinal.{w})
[Fact κ₁.IsRegular]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{J : Type w}
[PartialOrder J]
(p : (CategoryTheory.isCardinalPresentable C κ₁).ColimitOfShape J X)
[CategoryTheory.IsCardinalAccessibleCategory C κ₁]
:
CategoryTheory.Functor (Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J)) C
Given a presentation p of X : C as a colimit indexed by a partially
ordered type J of κ₁-presentable objects, this is the functor which sends
a subset A of J that is κ₁-directed and of cardinality < κ₂ to the
colimit of the restriction to A of the diagram p.diag.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT.functor_obj
(κ₁ κ₂ : Cardinal.{w})
[Fact κ₁.IsRegular]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{J : Type w}
[PartialOrder J]
(p : (CategoryTheory.isCardinalPresentable C κ₁).ColimitOfShape J X)
[CategoryTheory.IsCardinalAccessibleCategory C κ₁]
(A : Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J))
:
@[simp]
theorem
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT.functor_map
(κ₁ κ₂ : Cardinal.{w})
[Fact κ₁.IsRegular]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{J : Type w}
[PartialOrder J]
(p : (CategoryTheory.isCardinalPresentable C κ₁).ColimitOfShape J X)
[CategoryTheory.IsCardinalAccessibleCategory C κ₁]
{X✝ Y✝ : Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J)}
(f : X✝ ⟶ Y✝)
:
noncomputable def
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT.cocone
(κ₁ κ₂ : Cardinal.{w})
[Fact κ₁.IsRegular]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{J : Type w}
[PartialOrder J]
(p : (CategoryTheory.isCardinalPresentable C κ₁).ColimitOfShape J X)
[CategoryTheory.IsCardinalAccessibleCategory C κ₁]
:
CategoryTheory.Limits.Cocone (functor κ₁ κ₂ p)
The cocone for functor κ₁ κ₂ p with point X.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT.cocone_pt
(κ₁ κ₂ : Cardinal.{w})
[Fact κ₁.IsRegular]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{J : Type w}
[PartialOrder J]
(p : (CategoryTheory.isCardinalPresentable C κ₁).ColimitOfShape J X)
[CategoryTheory.IsCardinalAccessibleCategory C κ₁]
:
@[simp]
theorem
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT.cocone_ι_app
(κ₁ κ₂ : Cardinal.{w})
[Fact κ₁.IsRegular]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{J : Type w}
[PartialOrder J]
(p : (CategoryTheory.isCardinalPresentable C κ₁).ColimitOfShape J X)
[CategoryTheory.IsCardinalAccessibleCategory C κ₁]
(j : Subtype (IsCardinalFilteredAndHasCardinalLT κ₁ κ₂ J))
:
noncomputable def
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT.isColimit
(κ₁ κ₂ : Cardinal.{w})
[Fact κ₁.IsRegular]
[Fact κ₂.IsRegular]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{J : Type w}
[PartialOrder J]
(p : (CategoryTheory.isCardinalPresentable C κ₁).ColimitOfShape J X)
[CategoryTheory.IsCardinalAccessibleCategory C κ₁]
:
CategoryTheory.Limits.IsColimit (cocone κ₁ κ₂ p)
Given a presentation p of X : C as a colimit indexed by a partially
ordered type J of κ₁-presentable objects, X is also the colimit
of all the colimits of the restrictions of the diagram p.diag
to the subsets A of J that are κ₁-directed and of cardinality < κ₂.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Cardinal.SharplyLT.IsCardinalFilteredAndHasCardinalLT.isCardinalFiltered_subtype
{κ₁ κ₂ : Cardinal.{w}}
[Fact κ₁.IsRegular]
[Fact κ₂.IsRegular]
(hκ' :
∀ {X : Type w} [inst : PartialOrder X] [CategoryTheory.IsCardinalFiltered X κ₁] (A : Set X),
HasCardinalLT (↑A) κ₂ → ∃ (B : Set X), A ⊆ B ∧ CategoryTheory.IsCardinalFiltered (↑B) κ₁ ∧ HasCardinalLT (↑B) κ₂)
{J : Type w}
[PartialOrder J]
[CategoryTheory.IsCardinalFiltered J κ₁]
:
@[reducible, inline]
abbrev
Cardinal.SharplyLT.generator
(κ₁ κ₂ : Cardinal.{w})
[Fact κ₁.IsRegular]
(C : Type u)
[CategoryTheory.Category.{v, u} C]
:
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.
Equations
Instances For
theorem
Cardinal.SharplyLT.tfae
{κ₁ κ₂ : Cardinal.{w}}
[Fact κ₁.IsRegular]
[Fact κ₂.IsRegular]
(h : κ₁ < κ₂)
:
[κ₁.SharplyLT κ₂, CategoryTheory.IsCardinalAccessibleCategory (CategoryTheory.CardinalDirectedPoset κ₁) κ₂, ∀ (C : Type (w + 1)) [inst : CategoryTheory.Category.{w, w + 1} C]
[CategoryTheory.IsCardinalAccessibleCategory C κ₁], CategoryTheory.IsCardinalAccessibleCategory C κ₂, ∀ (X : Type w),
HasCardinalLT X κ₂ →
∃ (A : Set (CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ₁ X)), HasCardinalLT (↑A) κ₂ ∧ IsCofinal A, ∀ ⦃X : Type w⦄ [inst : PartialOrder X] [CategoryTheory.IsCardinalFiltered X κ₁] (A : Set X),
HasCardinalLT (↑A) κ₂ →
∃ (B : Set X), A ⊆ B ∧ CategoryTheory.IsCardinalFiltered (↑B) κ₁ ∧ HasCardinalLT (↑B) κ₂].TFAE
theorem
Cardinal.SharplyLT.exists_cofinal
{κ₁ κ₂ : Cardinal.{w}}
[Fact κ₁.IsRegular]
[Fact κ₂.IsRegular]
(h : κ₁.SharplyLT κ₂)
{X : Type w}
(hX : HasCardinalLT X κ₂)
:
∃ (A : Set (CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ₁ X)), HasCardinalLT (↑A) κ₂ ∧ IsCofinal A
theorem
Cardinal.SharplyLT.of_exists_cofinal
{κ₁ κ₂ : Cardinal.{w}}
[Fact κ₁.IsRegular]
[Fact κ₂.IsRegular]
(h₀ : κ₁ < κ₂)
(h :
∀ (X : Type w),
HasCardinalLT X κ₂ →
∃ (A : Set (CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ₁ X)), HasCardinalLT (↑A) κ₂ ∧ IsCofinal A)
:
κ₁.SharplyLT κ₂
theorem
Cardinal.SharplyLT.exists_isCardinalFiltered_set
{κ₁ κ₂ : Cardinal.{w}}
[Fact κ₁.IsRegular]
[Fact κ₂.IsRegular]
(h : κ₁.SharplyLT κ₂)
{X : Type w}
[PartialOrder X]
[CategoryTheory.IsCardinalFiltered X κ₁]
(A : Set X)
(hA : HasCardinalLT (↑A) κ₂)
:
∃ (B : Set X), A ⊆ B ∧ CategoryTheory.IsCardinalFiltered (↑B) κ₁ ∧ HasCardinalLT (↑B) κ₂
theorem
Cardinal.SharplyLT.isCardinalFilteredGenerator
{κ₁ κ₂ : Cardinal.{w}}
[Fact κ₁.IsRegular]
[Fact κ₂.IsRegular]
(h : κ₁.SharplyLT κ₂)
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.IsCardinalAccessibleCategory C κ₁]
:
(generator κ₁ κ₂ C).IsCardinalFilteredGenerator κ₂
theorem
Cardinal.SharplyLT.isCardinalAccessibleCategory
{κ₁ κ₂ : Cardinal.{w}}
[Fact κ₁.IsRegular]
[Fact κ₂.IsRegular]
(h : κ₁.SharplyLT κ₂)
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.IsCardinalAccessibleCategory C κ₁]
:
theorem
Cardinal.SharplyLT.trans
{κ₁ κ₂ : Cardinal.{w}}
[Fact κ₁.IsRegular]
[Fact κ₂.IsRegular]
(h₁₂ : κ₁.SharplyLT κ₂)
{κ₃ : Cardinal.{w}}
[Fact κ₃.IsRegular]
(h₂₃ : κ₂.SharplyLT κ₃)
:
κ₁.SharplyLT κ₃