Objects that are local with respect to a property of morphisms

Given W : MorphismProperty C, we define W.isLocal : ObjectProperty C which is the property of objects Z such that for any f : X ⟶ Y satisfying W, the precomposition with f gives a bijection (Y ⟶ Z) ≃ (X ⟶ Z). (In the file CategoryTheory.Localization.Bousfield, it is shown that this is part of a Galois connection, with "dual" construction Localization.LeftBousfield.W : ObjectProperty C → MorphismProperty C.)

def CategoryTheory.MorphismProperty.isLocal {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) : ObjectProperty C

Given W : MorphismProperty C, this is the property of W-local objects, i.e. the objects Z such that for any f : X ⟶ Y such that W f holds, the precomposition with f gives a bijection (Y ⟶ Z) ≃ (X ⟶ Z). (See the file CategoryTheory.Localization.Bousfield for the "dual" construction Localization.LeftBousfield.W : ObjectProperty C → MorphismProperty C.)

Equations

• W.isLocal Z = ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → Function.Bijective fun (g : Y ⟶ Z) => CategoryTheory.CategoryStruct.comp f g

theorem CategoryTheory.MorphismProperty.isLocal_iff {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (Z : C) : W.isLocal Z ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → Function.Bijective fun (g : Y ⟶ Z) => CategoryStruct.comp f g

instance CategoryTheory.MorphismProperty.instIsClosedUnderIsomorphismsIsLocal {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) : W.isLocal.IsClosedUnderIsomorphisms