Continuity of functors from well ordered types

Let F : J ⥤ C be functor from a well ordered type J. We introduce the typeclass F.IsWellOrderContinuous to say that if m is a limit element, then F.obj m is the colimit of the F.obj j for j < m.

class CategoryTheory.Functor.IsWellOrderContinuous {C : Type u} [Category.{v, u} C] {J : Type w} [PartialOrder J] (F : Functor J C) : Prop

A functor F : J ⥤ C is well-order-continuous if for any limit element m : J, F.obj m identifies to the colimit of the F.obj j for j < m.

• nonempty_isColimit (m : J) (hm : Order.IsSuccLimit m) : Nonempty (Limits.IsColimit ((Set.principalSegIio m).cocone F))

noncomputable def CategoryTheory.Functor.isColimitOfIsWellOrderContinuous {C : Type u} [Category.{v, u} C] {J : Type w} [PartialOrder J] (F : Functor J C) [F.IsWellOrderContinuous] (m : J) (hm : Order.IsSuccLimit m) : Limits.IsColimit ((Set.principalSegIio m).cocone F)

If F : J ⥤ C is well-order-continuous and m : J is a limit element, then F.obj m identifies to the colimit of the F.obj j for j < m.

Equations

• F.isColimitOfIsWellOrderContinuous m hm = ⋯.some

noncomputable def CategoryTheory.Functor.isColimitOfIsWellOrderContinuous' {C : Type u} [Category.{v, u} C] {J : Type w} [PartialOrder J] (F : Functor J C) [F.IsWellOrderContinuous] {α : Type u_1} [PartialOrder α] (f : (fun (x1 x2 : α) => x1 < x2) ≺i fun (x1 x2 : J) => x1 < x2) (hα : Order.IsSuccLimit f.top) : Limits.IsColimit (f.cocone F)

If F : J ⥤ C is well-order-continuous and h : α <i J is a principal segment such that h.top is a limit element, then F.obj h.top identifies to the colimit of the F.obj j for j : α.

Equations

• F.isColimitOfIsWellOrderContinuous' f hα = (F.isColimitOfIsWellOrderContinuous f.top hα).whiskerEquivalence f.orderIsoIio.equivalence

instance CategoryTheory.Functor.instIsWellOrderContinuousNat {C : Type u} [Category.{v, u} C] (F : Functor ℕ C) : F.IsWellOrderContinuous

instance CategoryTheory.Functor.instIsWellOrderContinuousFin {C : Type u} [Category.{v, u} C] {n : ℕ} (F : Functor (Fin n) C) : F.IsWellOrderContinuous

theorem CategoryTheory.Functor.isWellOrderContinuous_of_iso {C : Type u} [Category.{v, u} C] {J : Type w} [PartialOrder J] {F G : Functor J C} (e : F ≅ G) [F.IsWellOrderContinuous] : G.IsWellOrderContinuous

instance CategoryTheory.Functor.instIsWellOrderContinuousCompFunctor {C : Type u} [Category.{v, u} C] {J : Type w} [PartialOrder J] (F : Functor J C) {J' : Type w'} [PartialOrder J'] (f : (fun (x1 x2 : J') => x1 < x2) ≼i fun (x1 x2 : J) => x1 < x2) [F.IsWellOrderContinuous] : (⋯.functor.comp F).IsWellOrderContinuous

instance CategoryTheory.Functor.instIsWellOrderContinuousCompFunctorEquivalence {C : Type u} [Category.{v, u} C] {J : Type w} [PartialOrder J] (F : Functor J C) {J' : Type w'} [PartialOrder J'] (e : J' ≃o J) [F.IsWellOrderContinuous] : (e.equivalence.functor.comp F).IsWellOrderContinuous

instance CategoryTheory.Functor.IsWellOrderContinuous.restriction_setIci {C : Type u} [Category.{v, u} C] {J : Type w} [LinearOrder J] {F : Functor J C} [F.IsWellOrderContinuous] (j : J) : (⋯.functor.comp F).IsWellOrderContinuous