Theorems · Theorem · category theory

CategoryTheory.wellPowered_of_isDetecting

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C]
  {𝒢 : CategoryTheory.ObjectProperty C} [CategoryTheory.ObjectProperty.Small.{w, v₁, u₁} 𝒢]
  [inst_3 : CategoryTheory.LocallySmall.{w, v₁, u₁} C], 𝒢.IsDetecting → CategoryTheory.WellPowered.{w, v₁, u₁} C

A category with pullbacks and a small detecting set is well-powered.

Defined in

Mathlib.CategoryTheory.Generator.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasPullbacksCategoryTheory.ObjectProperty.SmallCategoryTheory.LocallySmall