The Orthogonal-reflection construction

Given W : MorphismProperty C (which should be small) and assuming the existence of certain colimits in C, we construct a morphism toSucc W Z : Z ⟶ succ W Z for any Z : C. This morphism belongs to W.isLocal.isLocal and is an isomorphism iff Z belongs to W.isLocal (see the lemma isIso_toSucc_iff). The morphism toSucc W Z : Z ⟶ succ W Z is defined as a composition of two morphisms that are roughly described as follows:

• toStep W Z : Z ⟶ step W Z: for any morphism f : X ⟶ Y satisfying W and any morphism X ⟶ Z, we "attach" a morphism Y ⟶ step W Z (using coproducts and a pushout in essentially the same way as it is done in the file Mathlib/CategoryTheory/SmallObject/Construction.lean for the small object argument);
• fromStep W Z : step W Z ⟶ succ W Z: this morphism coequalizes all pairs of morphisms g₁ g₂ : Y ⟶ step W Z such that there is a f : X ⟶ Y satisfying W such that f ≫ g₁ = f ≫ g₂.

The morphism toSucc W Z : Z ⟶ succ W Z is a variant of the (wrong) definition p. 32 in the book by Adámek and Rosický. In this book, a slightly different object than succ W Z is defined directly as a colimit of an intricate diagram, but contrary to what is stated on p. 33, it does not satisfy isIso_toSucc_iff. The author of this file was unable to understand the attempt of the authors to fix this mistake in the errata to this book. This led to the definition in two steps outlined above.

Main results

The morphisms described above toSucc W Z : Z ⟶ succ W Z for all Z : C allow to define succStruct W Z₀ : SuccStruct C for any Z₀ : C. By applying a transfinite iteration to this SuccStruct, we obtain the following results under the assumption that W : MorphismProperty C is a w-small property of morphisms in a locally κ-presentable category C (with κ : Cardinal.{w} a regular cardinal) such that the domains and codomains of the morphisms satisfying W are κ-presentable:

• MorphismProperty.isRightAdjoint_ι_isLocal: existence of the left adjoint of the inclusion W.isLocal ⥤ C;
• MorphismProperty.isLocallyPresentable_isLocal: the full subcategory W.isLocal is locally presentable.

This is essentially the implication (i) → (ii) in Theorem 1.39 (and the corollary 1.40) in the book by Adámek and Rosický (note that according to the errata to this book, the implication (ii) → (i) is wrong when κ = ℵ₀).

References

• [Adámek, J. and Rosický, J., Locally presentable and accessible categories][Adamek_Rosicky_1994]

theorem CategoryTheory.MorphismProperty.isClosedUnderColimitsOfShape_isLocal {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (J : Type u') [Category.{v', u'} J] [EssentiallySmall.{w, v', u'} J] (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalFiltered J κ] (hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ) : W.isLocal.IsClosedUnderColimitsOfShape J

theorem CategoryTheory.MorphismProperty.isCardinalAccessible_ι_isLocal {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [HasCardinalFilteredColimits C κ] (hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ) : W.isLocal.ι.IsCardinalAccessible κ

def CategoryTheory.OrthogonalReflection.D₁ {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) : Type (max u v)

Given W : MorphismProperty C and Z : C, this is the index type parametrising the data of a morphism f : X ⟶ Y satisfying W and a morphism X ⟶ Z.

instance CategoryTheory.OrthogonalReflection.instSmallD₁OfIsSmallOfLocallySmall {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [MorphismProperty.IsSmall.{w, v, u} W] [LocallySmall.{w, v, u} C] : Small.{w, max u v} (D₁ W Z)

theorem CategoryTheory.OrthogonalReflection.D₁.hasCoproductsOfShape {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [MorphismProperty.IsSmall.{w, v, u} W] [LocallySmall.{w, v, u} C] [Limits.HasCoproducts C] : Limits.HasCoproductsOfShape (D₁ W Z) C

def CategoryTheory.OrthogonalReflection.D₁.obj₁ {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {Z : C} (d : D₁ W Z) : C

If d : D₁ W Z corresponds to the data of f : X ⟶ Y satisfying W and of a morphism X ⟶ Z, this is the object X.

def CategoryTheory.OrthogonalReflection.D₁.obj₂ {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {Z : C} (d : D₁ W Z) : C

If d : D₁ W Z corresponds to the data of f : X ⟶ Y satisfying W and of a morphism X ⟶ Z, this is the object Y.

@[reducible, inline]

noncomputable abbrev CategoryTheory.OrthogonalReflection.D₁.l {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasCoproduct obj₁] : ∐ obj₁ ⟶ Z

Considering all diagrams consisting of a morphism f : X ⟶ Y satisfying W and of a morphism d : X ⟶ Z, this is the morphism from the coproduct of all these X objects to Z given by these morphisms d.

@[reducible, inline]

noncomputable abbrev CategoryTheory.OrthogonalReflection.D₁.ιLeft {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {Z : C} [Limits.HasCoproduct obj₁] {X Y : C} (f : X ⟶ Y) (hf : W f) (g : X ⟶ Z) : X ⟶ ∐ obj₁

The inclusion of a summand in ∐ obj₁.

theorem CategoryTheory.OrthogonalReflection.D₁.ιLeft_comp_l {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {Z : C} [Limits.HasCoproduct obj₁] {X Y : C} (f : X ⟶ Y) (hf : W f) (g : X ⟶ Z) : CategoryStruct.comp (ιLeft f hf g) (l W Z) = g

theorem CategoryTheory.OrthogonalReflection.D₁.ιLeft_comp_l_assoc {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {Z : C} [Limits.HasCoproduct obj₁] {X Y : C} (f : X ⟶ Y) (hf : W f) (g : X ⟶ Z) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryStruct.comp (ιLeft f hf g) (CategoryStruct.comp (l W Z) h) = CategoryStruct.comp g h

@[reducible, inline]

noncomputable abbrev CategoryTheory.OrthogonalReflection.D₁.t {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasCoproduct obj₁] [Limits.HasCoproduct obj₂] : ∐ obj₁ ⟶ ∐ obj₂

The coproduct of all the morphisms f indexed by all diagrams consisting of a morphism f : X ⟶ Y satisfying W and of a morphism d : X ⟶ Z.

@[reducible, inline]

noncomputable abbrev CategoryTheory.OrthogonalReflection.D₁.ιRight {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {Z : C} [Limits.HasCoproduct obj₂] {X Y : C} (f : X ⟶ Y) (hf : W f) (g : X ⟶ Z) : Y ⟶ ∐ obj₂

The inclusion of a summand in ∐ obj₂.

theorem CategoryTheory.OrthogonalReflection.D₁.ι_comp_t {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {Z : C} [Limits.HasCoproduct obj₁] [Limits.HasCoproduct obj₂] (d : D₁ W Z) : CategoryStruct.comp (Limits.Sigma.ι obj₁ d) (t W Z) = CategoryStruct.comp (↑d.fst).hom (Limits.Sigma.ι obj₂ d)

theorem CategoryTheory.OrthogonalReflection.D₁.ι_comp_t_assoc {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {Z : C} [Limits.HasCoproduct obj₁] [Limits.HasCoproduct obj₂] (d : D₁ W Z) {Z✝ : C} (h : ∐ obj₂ ⟶ Z✝) : CategoryStruct.comp (Limits.Sigma.ι obj₁ d) (CategoryStruct.comp (t W Z) h) = CategoryStruct.comp (↑d.fst).hom (CategoryStruct.comp (Limits.Sigma.ι obj₂ d) h)

theorem CategoryTheory.OrthogonalReflection.D₁.ιLeft_comp_t {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {Z : C} [Limits.HasCoproduct obj₁] [Limits.HasCoproduct obj₂] {X Y : C} (f : X ⟶ Y) (hf : W f) (g : X ⟶ Z) : CategoryStruct.comp (ιLeft f hf g) (t W Z) = CategoryStruct.comp f (ιRight f hf g)

theorem CategoryTheory.OrthogonalReflection.D₁.ιLeft_comp_t_assoc {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {Z : C} [Limits.HasCoproduct obj₁] [Limits.HasCoproduct obj₂] {X Y : C} (f : X ⟶ Y) (hf : W f) (g : X ⟶ Z) {Z✝ : C} (h : ∐ obj₂ ⟶ Z✝) : CategoryStruct.comp (ιLeft f hf g) (CategoryStruct.comp (t W Z) h) = CategoryStruct.comp f (CategoryStruct.comp (ιRight f hf g) h)

@[reducible, inline]

noncomputable abbrev CategoryTheory.OrthogonalReflection.step {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasCoproduct D₁.obj₁] [Limits.HasCoproduct D₁.obj₂] [Limits.HasPushouts C] : C

The intermediate object in the definition of the morphism toSucc W Z : Z ⟶ succ W Z. It is the pushout of the following square:

∐ D₁.obj₁ ⟶ ∐ D₁.obj₂
   |           |
   v           v
   Z      ⟶   step W Z

where the coproduct is taken over all the diagram consisting of a morphism f : X ⟶ Y satisfying W and a morphism X ⟶ Z. The top map is the coproduct of all of these f.

@[reducible, inline]

noncomputable abbrev CategoryTheory.OrthogonalReflection.toStep {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasCoproduct D₁.obj₁] [Limits.HasCoproduct D₁.obj₂] [Limits.HasPushouts C] : Z ⟶ step W Z

The canonical map from Z to the pushout of D₁.t W Z and D₁.l W Z.

def CategoryTheory.OrthogonalReflection.D₂ {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasCoproduct D₁.obj₁] [Limits.HasCoproduct D₁.obj₂] [Limits.HasPushouts C] : Type (max u v)

The index type parametrising the data of two morphisms g₁ g₂ : Y ⟶ step W Z, and a map f : X ⟶ Y satisfying W such that f ≫ g₁ = f ≫ g₂.

def CategoryTheory.OrthogonalReflection.D₂.multispanShape {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasCoproduct D₁.obj₁] [Limits.HasCoproduct D₁.obj₂] [Limits.HasPushouts C] : Limits.MultispanShape

The shape of the multicoequalizer of all pairs of morphisms g₁ g₂ : Y ⟶ step W Z with a f : X ⟶ Y satisfying W such that f ≫ g₁ = f ≫ g₂.

@[simp]

theorem CategoryTheory.OrthogonalReflection.D₂.multispanShape_snd {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasCoproduct D₁.obj₁] [Limits.HasCoproduct D₁.obj₂] [Limits.HasPushouts C] (x✝ : D₂ W Z) : (multispanShape W Z).snd x✝ = ()

@[simp]

theorem CategoryTheory.OrthogonalReflection.D₂.multispanShape_fst {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasCoproduct D₁.obj₁] [Limits.HasCoproduct D₁.obj₂] [Limits.HasPushouts C] (x✝ : D₂ W Z) : (multispanShape W Z).fst x✝ = ()

@[simp]

theorem CategoryTheory.OrthogonalReflection.D₂.multispanShape_L {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasCoproduct D₁.obj₁] [Limits.HasCoproduct D₁.obj₂] [Limits.HasPushouts C] : (multispanShape W Z).L = D₂ W Z

@[simp]

theorem CategoryTheory.OrthogonalReflection.D₂.multispanShape_R {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasCoproduct D₁.obj₁] [Limits.HasCoproduct D₁.obj₂] [Limits.HasPushouts C] : (multispanShape W Z).R = Unit

instance CategoryTheory.OrthogonalReflection.instSmallD₂ {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasCoproduct D₁.obj₁] [Limits.HasCoproduct D₁.obj₂] [Limits.HasPushouts C] [MorphismProperty.IsSmall.{w, v, u} W] [LocallySmall.{w, v, u} C] : Small.{w, max u v} (D₂ W Z)

instance CategoryTheory.OrthogonalReflection.instSmallLMultispanShape {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasCoproduct D₁.obj₁] [Limits.HasCoproduct D₁.obj₂] [Limits.HasPushouts C] [MorphismProperty.IsSmall.{w, v, u} W] [LocallySmall.{w, v, u} C] : Small.{w, max u v} (D₂.multispanShape W Z).L

theorem CategoryTheory.OrthogonalReflection.D₂.hasColimitsOfShape {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasCoproduct D₁.obj₁] [Limits.HasCoproduct D₁.obj₂] [Limits.HasPushouts C] [MorphismProperty.IsSmall.{w, v, u} W] [LocallySmall.{w, v, u} C] [Limits.HasColimitsOfSize.{w, w, v, u} C] : Limits.HasColimitsOfShape (Limits.WalkingMultispan (multispanShape W Z)) C

noncomputable def CategoryTheory.OrthogonalReflection.D₂.multispanIndex {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasCoproduct D₁.obj₁] [Limits.HasCoproduct D₁.obj₂] [Limits.HasPushouts C] : Limits.MultispanIndex (multispanShape W Z) C

The diagram of the multicoequalizer of all pair of morphisms g₁ g₂ : Y ⟶ step W Z with a f : X ⟶ Y satisfying W such that f ≫ g₁ = f ≫ g₂.

@[simp]

theorem CategoryTheory.OrthogonalReflection.D₂.multispanIndex_left {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasCoproduct D₁.obj₁] [Limits.HasCoproduct D₁.obj₂] [Limits.HasPushouts C] (d : (multispanShape W Z).L) : (multispanIndex W Z).left d = (↑d.fst).right

@[simp]

theorem CategoryTheory.OrthogonalReflection.D₂.multispanIndex_fst {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasCoproduct D₁.obj₁] [Limits.HasCoproduct D₁.obj₂] [Limits.HasPushouts C] (d : (multispanShape W Z).L) : (multispanIndex W Z).fst d = (↑d.snd).1

@[simp]

theorem CategoryTheory.OrthogonalReflection.D₂.multispanIndex_snd {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasCoproduct D₁.obj₁] [Limits.HasCoproduct D₁.obj₂] [Limits.HasPushouts C] (d : (multispanShape W Z).L) : (multispanIndex W Z).snd d = (↑d.snd).2

@[simp]

theorem CategoryTheory.OrthogonalReflection.D₂.multispanIndex_right {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasCoproduct D₁.obj₁] [Limits.HasCoproduct D₁.obj₂] [Limits.HasPushouts C] (x✝ : (multispanShape W Z).R) : (multispanIndex W Z).right x✝ = step W Z

@[reducible, inline]

noncomputable abbrev CategoryTheory.OrthogonalReflection.succ {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasCoproduct D₁.obj₁] [Limits.HasCoproduct D₁.obj₂] [Limits.HasPushouts C] [Limits.HasMulticoequalizer (D₂.multispanIndex W Z)] : C

The object succ W Z is the multicoequalizer of all pairs of morphisms g₁ g₂ : Y ⟶ step W Z with a f : X ⟶ Y satisfying W such that f ≫ g₁ = f ≫ g₂.

@[reducible, inline]

noncomputable abbrev CategoryTheory.OrthogonalReflection.fromStep {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasCoproduct D₁.obj₁] [Limits.HasCoproduct D₁.obj₂] [Limits.HasPushouts C] [Limits.HasMulticoequalizer (D₂.multispanIndex W Z)] : step W Z ⟶ succ W Z

The projection from Z to the multicoequalizer of all morphisms g₁ g₂ : Y ⟶ step W Z with a f : X ⟶ Y satisfying W such that f ≫ g₁ = f ≫ g₂.

theorem CategoryTheory.OrthogonalReflection.D₂.condition {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {Z : C} [Limits.HasCoproduct D₁.obj₁] [Limits.HasCoproduct D₁.obj₂] [Limits.HasPushouts C] [Limits.HasMulticoequalizer (multispanIndex W Z)] {X Y : C} (f : X ⟶ Y) (hf : W f) {g₁ g₂ : Y ⟶ step W Z} (h : CategoryStruct.comp f g₁ = CategoryStruct.comp f g₂) : CategoryStruct.comp g₁ (fromStep W Z) = CategoryStruct.comp g₂ (fromStep W Z)

theorem CategoryTheory.OrthogonalReflection.D₂.condition_assoc {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {Z : C} [Limits.HasCoproduct D₁.obj₁] [Limits.HasCoproduct D₁.obj₂] [Limits.HasPushouts C] [Limits.HasMulticoequalizer (multispanIndex W Z)] {X Y : C} (f : X ⟶ Y) (hf : W f) {g₁ g₂ : Y ⟶ step W Z} (h : CategoryStruct.comp f g₁ = CategoryStruct.comp f g₂) {Z✝ : C} (h✝ : succ W Z ⟶ Z✝) : CategoryStruct.comp g₁ (CategoryStruct.comp (fromStep W Z) h✝) = CategoryStruct.comp g₂ (CategoryStruct.comp (fromStep W Z) h✝)

@[reducible, inline]

noncomputable abbrev CategoryTheory.OrthogonalReflection.toSucc {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasCoproduct D₁.obj₁] [Limits.HasCoproduct D₁.obj₂] [Limits.HasPushouts C] [Limits.HasMulticoequalizer (D₂.multispanIndex W Z)] : Z ⟶ succ W Z

The morphism Z ⟶ succ W Z.

theorem CategoryTheory.OrthogonalReflection.toSucc_injectivity {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {Z : C} [Limits.HasCoproduct D₁.obj₁] [Limits.HasCoproduct D₁.obj₂] [Limits.HasPushouts C] [Limits.HasMulticoequalizer (D₂.multispanIndex W Z)] {X Y : C} (f : X ⟶ Y) (hf : W f) (g₁ g₂ : Y ⟶ Z) (hg : CategoryStruct.comp f g₁ = CategoryStruct.comp f g₂) : CategoryStruct.comp g₁ (toSucc W Z) = CategoryStruct.comp g₂ (toSucc W Z)

theorem CategoryTheory.OrthogonalReflection.toSucc_surjectivity {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {Z : C} [Limits.HasCoproduct D₁.obj₁] [Limits.HasCoproduct D₁.obj₂] [Limits.HasPushouts C] [Limits.HasMulticoequalizer (D₂.multispanIndex W Z)] {X Y : C} (f : X ⟶ Y) (hf : W f) (g : X ⟶ Z) : ∃ (g' : Y ⟶ succ W Z), CategoryStruct.comp f g' = CategoryStruct.comp g (toSucc W Z)

theorem CategoryTheory.OrthogonalReflection.isLocal_isLocal_toSucc {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasCoproduct D₁.obj₁] [Limits.HasCoproduct D₁.obj₂] [Limits.HasPushouts C] [Limits.HasMulticoequalizer (D₂.multispanIndex W Z)] : W.isLocal.isLocal (toSucc W Z)

@[deprecated CategoryTheory.OrthogonalReflection.isLocal_isLocal_toSucc (since := "2025-11-20")]

theorem CategoryTheory.OrthogonalReflection.leftBousfieldW_isLocal_toSucc {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasCoproduct D₁.obj₁] [Limits.HasCoproduct D₁.obj₂] [Limits.HasPushouts C] [Limits.HasMulticoequalizer (D₂.multispanIndex W Z)] : W.isLocal.isLocal (toSucc W Z)

Alias of CategoryTheory.OrthogonalReflection.isLocal_isLocal_toSucc.

theorem CategoryTheory.OrthogonalReflection.isIso_toSucc_iff {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasCoproduct D₁.obj₁] [Limits.HasCoproduct D₁.obj₂] [Limits.HasPushouts C] [Limits.HasMulticoequalizer (D₂.multispanIndex W Z)] : IsIso (toSucc W Z) ↔ W.isLocal Z

noncomputable def CategoryTheory.OrthogonalReflection.succStruct {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) [Limits.HasPushouts C] [∀ (Z : C), Limits.HasCoproduct D₁.obj₁] [∀ (Z : C), Limits.HasCoproduct D₁.obj₂] [∀ (Z : C), Limits.HasMulticoequalizer (D₂.multispanIndex W Z)] (Z₀ : C) : SmallObject.SuccStruct C

The successor structure of the orthogonal-reflection construction.

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

The transfinite iteration of succStruct W Z to the power κ.ord.ToType.

noncomputable def CategoryTheory.OrthogonalReflection.reflection {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasPushouts C] [∀ (Z : C), Limits.HasCoproduct D₁.obj₁] [∀ (Z : C), Limits.HasCoproduct D₁.obj₂] [∀ (Z : C), Limits.HasMulticoequalizer (D₂.multispanIndex W Z)] (κ : Cardinal.{w}) [OrderBot κ.ord.ToType] [Limits.HasIterationOfShape κ.ord.ToType C] : Z ⟶ reflectionObj W Z κ

The map which shall exhibit reflectionObj W Z κ as the image of Z by the left adjoint of the inclusion of W.isLocal, see corepresentableBy.

noncomputable def CategoryTheory.OrthogonalReflection.transfiniteCompositionOfShapeReflection {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasPushouts C] [∀ (Z : C), Limits.HasCoproduct D₁.obj₁] [∀ (Z : C), Limits.HasCoproduct D₁.obj₂] [∀ (Z : C), Limits.HasMulticoequalizer (D₂.multispanIndex W Z)] (κ : Cardinal.{w}) [OrderBot κ.ord.ToType] [Limits.HasIterationOfShape κ.ord.ToType C] : W.isLocal.isLocal.TransfiniteCompositionOfShape κ.ord.ToType (reflection W Z κ)

The morphism reflection W Z κ : Z ⟶ reflectionObj W Z κ is a transfinite compositions of morphisms in LeftBousfield.W W.isLocal.

@[reducible, inline]

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

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

noncomputable def CategoryTheory.OrthogonalReflection.iterationObjSuccIso {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasPushouts C] [∀ (Z : C), Limits.HasCoproduct D₁.obj₁] [∀ (Z : C), Limits.HasCoproduct D₁.obj₂] [∀ (Z : C), Limits.HasMulticoequalizer (D₂.multispanIndex W Z)] (κ : Cardinal.{w}) [OrderBot κ.ord.ToType] [Limits.HasIterationOfShape κ.ord.ToType C] [Fact κ.IsRegular] (j : κ.ord.ToType) : (iteration W Z κ).obj (Order.succ j) ≅ succ W ((iteration W Z κ).obj j)

(iteration W Z κ).obj (Order.succ j) identifies to the image of (iteration W Z κ).obj j by succ.

theorem CategoryTheory.OrthogonalReflection.iteration_map_succ {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasPushouts C] [∀ (Z : C), Limits.HasCoproduct D₁.obj₁] [∀ (Z : C), Limits.HasCoproduct D₁.obj₂] [∀ (Z : C), Limits.HasMulticoequalizer (D₂.multispanIndex W Z)] (κ : Cardinal.{w}) [OrderBot κ.ord.ToType] [Limits.HasIterationOfShape κ.ord.ToType C] [Fact κ.IsRegular] (j : κ.ord.ToType) : (iteration W Z κ).map (homOfLE ⋯) = CategoryStruct.comp (toSucc W ((iteration W Z κ).obj j)) (iterationObjSuccIso W Z κ j).inv

theorem CategoryTheory.OrthogonalReflection.iteration_map_succ_assoc {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasPushouts C] [∀ (Z : C), Limits.HasCoproduct D₁.obj₁] [∀ (Z : C), Limits.HasCoproduct D₁.obj₂] [∀ (Z : C), Limits.HasMulticoequalizer (D₂.multispanIndex W Z)] (κ : Cardinal.{w}) [OrderBot κ.ord.ToType] [Limits.HasIterationOfShape κ.ord.ToType C] [Fact κ.IsRegular] (j : κ.ord.ToType) {Z✝ : C} (h : (iteration W Z κ).obj (Order.succ j) ⟶ Z✝) : CategoryStruct.comp ((iteration W Z κ).map (homOfLE ⋯)) h = CategoryStruct.comp (toStep W ((iteration W Z κ).obj j)) (CategoryStruct.comp (fromStep W ((iteration W Z κ).obj j)) (CategoryStruct.comp (iterationObjSuccIso W Z κ j).inv h))

theorem CategoryTheory.OrthogonalReflection.iteration_map_succ_injectivity {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {Z : C} [Limits.HasPushouts C] [∀ (Z : C), Limits.HasCoproduct D₁.obj₁] [∀ (Z : C), Limits.HasCoproduct D₁.obj₂] [∀ (Z : C), Limits.HasMulticoequalizer (D₂.multispanIndex W Z)] {κ : Cardinal.{w}} [OrderBot κ.ord.ToType] [Limits.HasIterationOfShape κ.ord.ToType C] [Fact κ.IsRegular] {X Y : C} (f : X ⟶ Y) (hf : W f) {j : κ.ord.ToType} (g₁ g₂ : Y ⟶ (iteration W Z κ).obj j) (hg : CategoryStruct.comp f g₁ = CategoryStruct.comp f g₂) : CategoryStruct.comp g₁ ((iteration W Z κ).map (homOfLE ⋯)) = CategoryStruct.comp g₂ ((iteration W Z κ).map (homOfLE ⋯))

theorem CategoryTheory.OrthogonalReflection.iteration_map_succ_surjectivity {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {Z : C} [Limits.HasPushouts C] [∀ (Z : C), Limits.HasCoproduct D₁.obj₁] [∀ (Z : C), Limits.HasCoproduct D₁.obj₂] [∀ (Z : C), Limits.HasMulticoequalizer (D₂.multispanIndex W Z)] {κ : Cardinal.{w}} [OrderBot κ.ord.ToType] [Limits.HasIterationOfShape κ.ord.ToType C] [Fact κ.IsRegular] {X Y : C} (f : X ⟶ Y) (hf : W f) {j : κ.ord.ToType} (g : X ⟶ (iteration W Z κ).obj j) : ∃ (g' : Y ⟶ (iteration W Z κ).obj (Order.succ j)), CategoryStruct.comp f g' = CategoryStruct.comp g ((iteration W Z κ).map (homOfLE ⋯))

theorem CategoryTheory.OrthogonalReflection.isLocal_isLocal_reflection {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) [Limits.HasPushouts C] [∀ (Z : C), Limits.HasCoproduct D₁.obj₁] [∀ (Z : C), Limits.HasCoproduct D₁.obj₂] [∀ (Z : C), Limits.HasMulticoequalizer (D₂.multispanIndex W Z)] (κ : Cardinal.{w}) [OrderBot κ.ord.ToType] [Limits.HasIterationOfShape κ.ord.ToType C] : W.isLocal.isLocal (reflection W Z κ)

theorem CategoryTheory.OrthogonalReflection.isLocal_reflectionObj {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} (Z : C) [Limits.HasPushouts C] [∀ (Z : C), Limits.HasCoproduct D₁.obj₁] [∀ (Z : C), Limits.HasCoproduct D₁.obj₂] [∀ (Z : C), Limits.HasMulticoequalizer (D₂.multispanIndex W Z)] {κ : Cardinal.{w}} [OrderBot κ.ord.ToType] [Limits.HasIterationOfShape κ.ord.ToType C] [Fact κ.IsRegular] (hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ) : W.isLocal (reflectionObj W Z κ)

noncomputable def CategoryTheory.OrthogonalReflection.corepresentableBy {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} (Z : C) [Limits.HasPushouts C] [∀ (Z : C), Limits.HasCoproduct D₁.obj₁] [∀ (Z : C), Limits.HasCoproduct D₁.obj₂] [∀ (Z : C), Limits.HasMulticoequalizer (D₂.multispanIndex W Z)] {κ : Cardinal.{w}} [OrderBot κ.ord.ToType] [Limits.HasIterationOfShape κ.ord.ToType C] [Fact κ.IsRegular] (hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ) : (W.isLocal.ι.comp (coyoneda.obj (Opposite.op Z))).CorepresentableBy { obj := 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.ι.

theorem CategoryTheory.OrthogonalReflection.isRightAdjoint_ι {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) [Limits.HasPushouts C] [∀ (Z : C), Limits.HasCoproduct D₁.obj₁] [∀ (Z : C), Limits.HasCoproduct D₁.obj₂] [∀ (Z : C), Limits.HasMulticoequalizer (D₂.multispanIndex W Z)] (κ : Cardinal.{w}) [OrderBot κ.ord.ToType] [Limits.HasIterationOfShape κ.ord.ToType C] [Fact κ.IsRegular] (hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ) : W.isLocal.ι.IsRightAdjoint

theorem CategoryTheory.MorphismProperty.isRightAdjoint_ι_isLocal {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsSmall.{w, v, u} W] [LocallySmall.{w, v, u} C] (hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ) [Limits.HasColimitsOfSize.{w, w, v, u} C] : W.isLocal.ι.IsRightAdjoint

theorem CategoryTheory.MorphismProperty.isLocallyPresentable_isLocal {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (κ : Cardinal.{w}) [Fact κ.IsRegular] [IsCardinalLocallyPresentable C κ] [IsSmall.{w, v, u} W] (hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable X κ ∧ IsCardinalPresentable Y κ) : IsCardinalLocallyPresentable W.isLocal.FullSubcategory κ