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 morphismf : X ⟶ YsatisfyingWand any morphismX ⟶ Z, we "attach" a morphismY ⟶ step W Z(using coproducts and a pushout in essentially the same way as it is done in the fileMathlib/CategoryTheory/SmallObject/Construction.leanfor the small object argument);fromStep W Z : step W Z ⟶ succ W Z: this morphism coequalizes all pairs of morphismsg₁ g₂ : Y ⟶ step W Zsuch that there is af : X ⟶ YsatisfyingWsuch thatf ≫ 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 inclusionW.isLocal ⥤ C;MorphismProperty.isLocallyPresentable_isLocal: the full subcategoryW.isLocalis 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 κ)
:
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 κ)
:
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.
Instances For
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.
Instances For
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.
Instances For
@[reducible, inline]
noncomputable abbrev
CategoryTheory.OrthogonalReflection.D₁.l
{C : Type u}
[Category.{v, u} C]
(W : MorphismProperty C)
(Z : C)
[Limits.HasCoproduct obj₁]
:
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.
Instances For
@[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)
:
The inclusion of a summand in ∐ obj₁.
Instances For
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₂]
:
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.
Instances For
@[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)
:
The inclusion of a summand in ∐ obj₂.
Instances For
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.
Instances For
@[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]
:
The canonical map from Z to the pushout of D₁.t W Z and D₁.l W Z.
Instances For
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₂.
Instances For
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]
:
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₂.
Instances For
@[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]
:
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]
:
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₂.
Instances For
@[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₂.
Instances For
@[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)]
:
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₂.
Instances For
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)]
:
The morphism Z ⟶ succ W Z.
Instances For
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)]
:
@[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)]
:
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)]
:
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)
:
The successor structure of the orthogonal-reflection construction.
Instances For
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.
Instances For
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]
:
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.
Instances For
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.
Instances For
@[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]
:
The functor κ.ord.ToType ⥤ C that is the diagram of the
transfinite composition transfiniteCompositionOfShapeReflection.
Instances For
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) identifies to the image of
(iteration W Z κ).obj j by succ.
Instances For
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.ι.
Instances For
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 κ)
:
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]
:
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 κ)
: