feat(CategoryTheory): HasCardinalLT for MorphismProperty and ObjectProperty (#31421)

This PR introduces abbreviations to say that the type of objects or morphisms satisfying a certain property is of cardinality `< κ`.

Author: joelriou

Mathlib.lean

@@ -2775,6 +2775,7 @@ public import Mathlib.CategoryTheory.MorphismProperty.Concrete
 public import Mathlib.CategoryTheory.MorphismProperty.Descent
 public import Mathlib.CategoryTheory.MorphismProperty.Factorization
 public import Mathlib.CategoryTheory.MorphismProperty.FunctorCategory
+public import Mathlib.CategoryTheory.MorphismProperty.HasCardinalLT
 public import Mathlib.CategoryTheory.MorphismProperty.Ind
 public import Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
 public import Mathlib.CategoryTheory.MorphismProperty.IsSmall
@@ -2801,6 +2802,7 @@ public import Mathlib.CategoryTheory.ObjectProperty.EpiMono
 public import Mathlib.CategoryTheory.ObjectProperty.Extensions
 public import Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
 public import Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
+public import Mathlib.CategoryTheory.ObjectProperty.HasCardinalLT
 public import Mathlib.CategoryTheory.ObjectProperty.Ind
 public import Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
 public import Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape

Mathlib/CategoryTheory/MorphismProperty/Basic.lean

@@ -147,6 +147,16 @@ variable (P : MorphismProperty C)
 /-- The set in `Set (Arrow C)` which corresponds to `P : MorphismProperty C`. -/
 def toSet : Set (Arrow C) := setOf (fun f ↦ P f.hom)
 
+lemma mem_toSet_iff (f : Arrow C) : f ∈ P.toSet ↔ P f.hom := Iff.rfl
+
+lemma toSet_iSup {ι : Type*} (W : ι → MorphismProperty C) :
+    (⨆ i , W i).toSet = ⋃ i, (W i).toSet := by
+  ext
+  simp [mem_toSet_iff]
+
+lemma toSet_max (W₁ W₂ : MorphismProperty C) :
+    (W₁ ⊔ W₂).toSet = W₁.toSet ∪ W₂.toSet := rfl
+
 /-- The family of morphisms indexed by `P.toSet` which corresponds
 to `P : MorphismProperty C`, see `MorphismProperty.ofHoms_homFamily`. -/
 def homFamily (f : P.toSet) : f.1.left ⟶ f.1.right := f.1.hom

Mathlib/CategoryTheory/MorphismProperty/HasCardinalLT.lean

@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2025 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+module
+
+public import Mathlib.SetTheory.Cardinal.HasCardinalLT
+public import Mathlib.CategoryTheory.MorphismProperty.Basic
+
+/-!
+# 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 `< κ`.
+
+-/
+
+@[expose] public section
+
+universe w v u
+
+namespace CategoryTheory
+
+variable {C : Type u} [Category.{v} C]
+
+namespace MorphismProperty
+
+/-- The property that the subtype of arrows satisfying a property `P : MorphismProperty C`
+is of cardinality `< κ`. -/
+protected abbrev HasCardinalLT (P : MorphismProperty C) (κ : Cardinal.{w}) :=
+    _root_.HasCardinalLT P.toSet κ
+
+lemma hasCardinalLT_ofHoms {C : Type*} [Category C]
+    {ι : Type*} {X Y : ι → C} (f : ∀ i, X i ⟶ Y i) {κ : Cardinal}
+    (h : HasCardinalLT ι κ) : (MorphismProperty.ofHoms f).HasCardinalLT κ :=
+  h.of_surjective (fun i ↦ ⟨Arrow.mk (f i), ⟨i⟩⟩) (by
+    rintro ⟨f, hf⟩
+    rw [MorphismProperty.mem_toSet_iff, MorphismProperty.ofHoms_iff] at hf
+    obtain ⟨i, hf⟩ := hf
+    obtain rfl : f = _ := hf
+    exact ⟨i, rfl⟩)
+
+lemma HasCardinalLT.iSup
+    {ι : Type*} {P : ι → MorphismProperty C} {κ : Cardinal.{w}} [Fact κ.IsRegular]
+    (hP : ∀ i, (P i).HasCardinalLT κ) (hι : HasCardinalLT ι κ) :
+    (⨆ i, P i).HasCardinalLT κ := by
+  dsimp only [MorphismProperty.HasCardinalLT]
+  rw [toSet_iSup]
+  exact hasCardinalLT_iUnion _ hι hP
+
+lemma HasCardinalLT.sup
+    {P₁ P₂ : MorphismProperty C} {κ : Cardinal.{w}}
+    (h₁ : P₁.HasCardinalLT κ) (h₂ : P₂.HasCardinalLT κ)
+    (hκ : Cardinal.aleph0 ≤ κ) :
+    (P₁ ⊔ P₂).HasCardinalLT κ := by
+  dsimp only [MorphismProperty.HasCardinalLT]
+  rw [MorphismProperty.toSet_max]
+  exact hasCardinalLT_union hκ h₁ h₂
+
+end MorphismProperty
+
+end CategoryTheory

Mathlib/CategoryTheory/ObjectProperty/HasCardinalLT.lean

@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2025 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+module
+
+public import Mathlib.SetTheory.Cardinal.HasCardinalLT
+public import Mathlib.CategoryTheory.ObjectProperty.Basic
+
+/-!
+# Properties of objects that are bounded by a cardinal
+
+Given `P : ObjectProperty C` and `κ : Cardinal`, we introduce a predicate
+`P.HasCardinalLT κ` saying that the cardinality of `Subtype P` is `< κ`.
+
+-/
+
+@[expose] public section
+
+universe w v u
+
+namespace CategoryTheory
+
+variable {C : Type u} [Category.{v} C]
+
+namespace ObjectProperty
+
+/-- The property that the subtype of objects satisfying a property `P : ObjectProperty C`
+is of cardinality `< κ`. -/
+protected abbrev HasCardinalLT (P : ObjectProperty C) (κ : Cardinal.{w}) :=
+    _root_.HasCardinalLT (Subtype P) κ
+
+lemma hasCardinalLT_subtype_ofObj
+    {ι : Type*} (X : ι → C) {κ : Cardinal.{w}}
+    (h : HasCardinalLT ι κ) : (ObjectProperty.ofObj X).HasCardinalLT κ :=
+  h.of_surjective (fun i ↦ ⟨X i, by simp⟩) (by rintro ⟨_, ⟨i⟩⟩; exact ⟨i, rfl⟩)
+
+lemma HasCardinalLT.iSup
+    {ι : Type*} {P : ι → ObjectProperty C} {κ : Cardinal.{w}} [Fact κ.IsRegular]
+    (hP : ∀ i, (P i).HasCardinalLT κ) (hι : HasCardinalLT ι κ) :
+    (⨆ i, P i).HasCardinalLT κ :=
+  hasCardinalLT_subtype_iSup _ hι hP
+
+lemma HasCardinalLT.sup
+    {P₁ P₂ : ObjectProperty C} {κ : Cardinal.{w}}
+    (h₁ : P₁.HasCardinalLT κ) (h₂ : P₂.HasCardinalLT κ)
+    (hκ : Cardinal.aleph0 ≤ κ) :
+    (P₁ ⊔ P₂).HasCardinalLT κ :=
+  hasCardinalLT_union hκ h₁ h₂
+
+end ObjectProperty
+
+end CategoryTheory