Theorems · Definition · category theory

CategoryTheory.ObjectProperty.isLocal

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.ObjectProperty C → CategoryTheory.MorphismProperty C

Given P : ObjectProperty C, this is the class of morphisms f : X ⟶ Y such that for all Z : C such that P Z, the precomposition with f induces a bijection (Y ⟶ Z) ≃ (X ⟶ Z). (One of the applications of this notion is the left Bousfield localization of model categories.)

Defined in

Mathlib.CategoryTheory.Localization.Bousfield

Cited by

20 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

CategoryTheory.Category