Theorems · Definition · category theory

CategoryTheory.ObjectProperty.IsCodetecting

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

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

Defined in

Mathlib.CategoryTheory.Generator.Basic

Cited by

13 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

CategoryTheory.Category