Properties of morphisms that are bounded by a cardinal #
Given P : MorphismProperty C and κ : Cardinal, we introduce a predicate
P.HasCardinalLT κ saying that the cardinality of P.toSet is < κ.
@[reducible, inline]
abbrev
CategoryTheory.MorphismProperty.HasCardinalLT
{C : Type u}
[Category.{v, u} C]
(P : MorphismProperty C)
(κ : Cardinal.{w})
:
The property that the subtype of arrows satisfying a property P : MorphismProperty C
is of cardinality < κ.
Equations
- P.HasCardinalLT κ = HasCardinalLT (↑P.toSet) κ
Instances For
theorem
CategoryTheory.MorphismProperty.hasCardinalLT_ofHoms
{C : Type u_1}
[Category.{v_1, u_1} C]
{ι : Type u_2}
{X Y : ι → C}
(f : (i : ι) → X i ⟶ Y i)
{κ : Cardinal.{u_3}}
(h : HasCardinalLT ι κ)
:
(ofHoms f).HasCardinalLT κ
theorem
CategoryTheory.MorphismProperty.HasCardinalLT.iSup
{C : Type u}
[Category.{v, u} C]
{ι : Type u_1}
{P : ι → MorphismProperty C}
{κ : Cardinal.{w}}
[Fact κ.IsRegular]
(hP : ∀ (i : ι), (P i).HasCardinalLT κ)
(hι : HasCardinalLT ι κ)
:
(⨆ (i : ι), P i).HasCardinalLT κ
theorem
CategoryTheory.MorphismProperty.HasCardinalLT.sup
{C : Type u}
[Category.{v, u} C]
{P₁ P₂ : MorphismProperty C}
{κ : Cardinal.{w}}
(h₁ : P₁.HasCardinalLT κ)
(h₂ : P₂.HasCardinalLT κ)
(hκ : Cardinal.aleph0 ≤ κ)
:
(P₁ ⊔ P₂).HasCardinalLT κ