Theorems · Inductive type · category theory

CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.MorphismProperty C → (κ : Cardinal.{w}) → [Fact κ.IsRegular] → [OrderBot κ.ord.ToType] → Prop

Given I : MorphismProperty C and a regular cardinal κ : Cardinal.{w}, this property asserts the technical conditions which allow to proceed to the small object argument by doing a construction by transfinite induction indexed by the well-ordered type κ.ord.ToType.

Defined in

Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Cited by

49 results in Mathlib

Foundations

Depth 42 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryFactOrderBot