Theorems · Definition · category theory

CategoryTheory.ObjectProperty.IsDetecting

{C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.ObjectProperty C → Prop

We say that P : ObjectProperty C is detecting if the functors C(G, -) for G : C such that P G collectively reflect isomorphisms, i.e., if any h with domain G that P G uniquely factors through f, then f is an isomorphism.

Defined in

Mathlib.CategoryTheory.Generator.Basic

Cited by

20 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

CategoryTheory.Category