Theorems · Inductive type · category theory

CategoryTheory.MorphismProperty.IsStableUnderTransfiniteCompositionOfShape

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.MorphismProperty C →
      (J : Type w) → [inst : LinearOrder J] → [SuccOrder J] → [OrderBot J] → [WellFoundedLT J] → Prop

A class of morphisms W : MorphismProperty C is stable under transfinite compositions of shape J if for any well-order-continuous functor F : J ⥤ C such that F.obj j ⟶ F.obj (Order.succ j) is in W, then F.obj ⊥ ⟶ c.pt is in W for any colimit cocone c : Cocone F.

Defined in

Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Cited by

7 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext

Assumes

CategoryTheory.CategoryLinearOrderSuccOrderOrderBotWellFoundedLT