Theorems · Inductive type · category theory

CategoryTheory.HasCoseparator

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

For a category C and an object G : C, G is a coseparator of C if the functor C(-, G) is faithful. While IsCoseparator G : Prop is the proposition that G is a coseparator of C, an HasCoseparator C : Prop is the proposition that such a coseparator exists. Note that HasCoseparator C is a proposition. It does not designate a favored coseparator and merely asserts the existence of one.

Defined in

Mathlib.CategoryTheory.Generator.Basic

Cited by

11 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

CategoryTheory.Category