Theorems · Definition · category theory

CategoryTheory.OrthogonalReflection.corepresentableBy

{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] →
                      [inst_7 : Fact κ.IsRegular] →
                        (hW :
                            ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
                              W f →
                                CategoryTheory.IsCardinalPresentable X κ ∧ CategoryTheory.IsCardinalPresentable Y κ) →
                          (W.isLocal.ι.comp (CategoryTheory.coyoneda.obj (Opposite.op Z))).CorepresentableBy
                            { obj := CategoryTheory.OrthogonalReflection.reflectionObj W Z κ, property := ⋯ }

The morphism reflection W Z κ : Z ⟶ reflectionObj W Z κ exhibits reflectionObj W Z κ as the image of Z by the left adjoint of the inclusion W.isLocal.ι.

Defined in

Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Cited by

1 results in Mathlib

Foundations

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

Assumes

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