Documentation

Mathlib.CategoryTheory.Presentable.Finite

Finitely Presentable Objects #

We define finitely presentable objects as a synonym for ℵ₀-presentable objects, and link this definition with the preservation of filtered colimits.

@[reducible, inline]

A functor F : C ⥤ D is finitely accessible if it is ℵ₀-accessible. Equivalently, it preserves all filtered colimits. See CategoryTheory.Functor.IsFinitelyAccessible_iff_preservesFilteredColimits.

Equations
Instances For
    @[reducible, inline]

    An object X is finitely presentable if Hom(X, -) preserves all filtered colimits.

    Equations
    Instances For