Commit 2025-11-08 14:58 cff918fa
View on Github →feat(CategoryTheory): the orthogonal-reflection construction (#30492)
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 LeftBousfield.W W.isLocal and is an isomorphism iff Z belongs to W.isLocal. The main definition is a fix to the (wrong) construction in the book Locally presentable and accessible categories by Adámek and Rosický.
In a future PR, we shall consider a transfinite iteration of this construction.