Theorems · Definition · category theory

CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (W : CategoryTheory.MorphismProperty C) →
      {n : ℕ} →
        (F : CategoryTheory.ComposableArrows C n) →
          (∀ (i : Fin n), W (F.map (CategoryTheory.homOfLE ⋯))) → W.TransfiniteCompositionOfShape (Fin (n + 1)) F.hom

If F : ComposableArrows C n and all maps F.obj i.castSucc ⟶ F.obj i.succ are in W, then F.hom : F.left ⟶ F.right is a transfinite composition of shape Fin (n + 1) of morphisms in W.

Defined in

Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category