Theorems · Definition · category theory

CategoryTheory.OrthogonalReflection.iteration

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (W : CategoryTheory.MorphismProperty C) →
      C →
        [inst_1 : CategoryTheory.Limits.HasPushouts C] →
          [inst_2 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] →
            [inst_3 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] →
              [∀ (Z : C),
                    CategoryTheory.Limits.HasMulticoequalizer
                      (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] →
                (κ : Cardinal.{w}) →
                  [OrderBot κ.ord.ToType] →
                    [CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C] → CategoryTheory.Functor κ.ord.ToType C

The functor κ.ord.ToType ⥤ C that is the diagram of the transfinite composition transfiniteCompositionOfShapeReflection.

Defined in

Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Cited by

6 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasPushoutsCategoryTheory.Limits.HasCoproductCategoryTheory.Limits.HasCoproductCategoryTheory.Limits.HasMulticoequalizerOrderBotCategoryTheory.Limits.HasIterationOfShape