Theorems · Theorem · category theory

CategoryTheory.OrthogonalReflection.iteration_map_succ_surjectivity

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {Z : 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₂]
  [inst_4 :
    ∀ (Z : C), CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)]
  {κ : Cardinal.{w}} [inst_5 : OrderBot κ.ord.ToType]
  [inst_6 : CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C] [Fact κ.IsRegular] {X Y : C} (f : X ⟶ Y),
  W f →
    ∀ {j : κ.ord.ToType} (g : X ⟶ (CategoryTheory.OrthogonalReflection.iteration W Z κ).obj j),
      ∃ g',
        CategoryTheory.CategoryStruct.comp f g' =
          CategoryTheory.CategoryStruct.comp g
            ((CategoryTheory.OrthogonalReflection.iteration W Z κ).map (CategoryTheory.homOfLE ⋯))

Defined in

Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasPushoutsCategoryTheory.Limits.HasCoproductCategoryTheory.Limits.HasCoproductCategoryTheory.Limits.HasMulticoequalizerOrderBotCategoryTheory.Limits.HasIterationOfShapeFact