Theorems · Definition · category theory

CategoryTheory.Limits.IsCofiltered.sequentialFunctor

(J : Type u_2) → [Countable J] → [inst : Preorder J] → [CategoryTheory.IsCofiltered J] → CategoryTheory.Functor ℕᵒᵖ J

The initial functor ℕᵒᵖ ⥤ J, which allows us to turn cofiltered limits over countable preorders into sequential limits. TODO: redefine this as (IsFiltered.sequentialFunctor Jᵒᵖ).leftOp. This would need API for initial/ final functors of the form leftOp/rightOp.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Countable

Cited by

2 results in Mathlib

Foundations

Depth 28 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CountablePreorderCategoryTheory.IsCofiltered