Theorems · Definition · category theory

CategoryTheory.ObjectProperty.IsSeparating

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

We say that P : ObjectProperty C is separating if the functors C(G, -) for G : C such that P G are collectively faithful, i.e., if h ≫ f = h ≫ g for all h with domain in 𝒢 implies f = g.

Defined in

Mathlib.CategoryTheory.Generator.Basic

Cited by

41 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

CategoryTheory.Category