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 Mathlib/CategoryTheory/Localization/Bousfield.lean, it is shown that this is part of a Galois connection, with "dual" construction ObjectProperty.isLocal : ObjectProperty C → MorphismProperty C.)

We also introduce the dual notion W.isColocal : ObjectProperty 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 Mathlib/CategoryTheory/Localization/Bousfield.lean for the "dual" construction ObjectProperty.isLocal : 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

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

Given W : MorphismProperty C, this is the property of W-colocal objects, i.e. the objects X such that for any g : Y ⟶ Z such that W g holds, the postcomposition with g gives a bijection (X ⟶ Y) ≃ (X ⟶ Z). (See the file Mathlib/CategoryTheory/Localization/Bousfield.lean for the "dual" construction ObjectProperty.isColocal : ObjectProperty C → MorphismProperty C.)

Equations

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

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

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

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

instance CategoryTheory.MorphismProperty.instIsClosedUnderLimitsOfShapeIsLocal {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (J : Type u') [Category.{v', u'} J] : W.isLocal.IsClosedUnderLimitsOfShape J

instance CategoryTheory.MorphismProperty.instIsClosedUnderColimitsOfShapeIsColocal {C : Type u} [Category.{v, u} C] (W : MorphismProperty C) (J : Type u') [Category.{v', u'} J] : W.isColocal.IsClosedUnderColimitsOfShape J