Construction of the localized category

This file constructs the localized category, obtained by formally inverting a class of maps W : MorphismProperty C in a category C.

We first construct a quiver LocQuiver W whose objects are the same as those of C and whose maps are the maps in C and placeholders for the formal inverses of the maps in W.

The localized category W.Localization is obtained by taking the quotient of the path category of LocQuiver W by the congruence generated by four types of relations.

The obvious functor Q W : C ⥤ W.Localization satisfies the universal property of the localization. Indeed, if G : C ⥤ D sends morphisms in W to isomorphisms in D (i.e. we have hG : W.IsInvertedBy G), then there exists a unique functor G' : W.Localization ⥤ D such that Q W ≫ G' = G. This G' is lift G hG. The expected property of lift G hG if expressed by the lemma fac and the uniqueness is expressed by uniq.

References

• P. Gabriel, M. Zisman, Calculus of fractions and homotopy theory

structure CategoryTheory.Localization.Construction.LocQuiver {C : Type uC} [Category.{uC', uC} C] (W : MorphismProperty C) : Type uC

If W : MorphismProperty C, LocQuiver W is a quiver with the same objects as C, and whose morphisms are those in C and placeholders for formal inverses of the morphisms in W.

• obj : C

  underlying object

instance CategoryTheory.Localization.Construction.instQuiverLocQuiver {C : Type uC} [Category.{uC', uC} C] (W : MorphismProperty C) : Quiver (LocQuiver W)

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Localization.Construction.ιPaths {C : Type uC} [Category.{uC', uC} C] (W : MorphismProperty C) (X : C) : Paths (LocQuiver W)

The object in the path category of LocQuiver W attached to an object in the category C

Equations

• CategoryTheory.Localization.Construction.ιPaths W X = { obj := X }

def CategoryTheory.Localization.Construction.ψ₁ {C : Type uC} [Category.{uC', uC} C] (W : MorphismProperty C) {X Y : C} (f : X ⟶ Y) : ιPaths W X ⟶ ιPaths W Y

The morphism in the path category associated to a morphism in the original category.

Equations

• CategoryTheory.Localization.Construction.ψ₁ W f = (CategoryTheory.Paths.of (CategoryTheory.Localization.Construction.LocQuiver W)).map (Sum.inl f)

def CategoryTheory.Localization.Construction.ψ₂ {C : Type uC} [Category.{uC', uC} C] (W : MorphismProperty C) {X Y : C} (w : X ⟶ Y) (hw : W w) : ιPaths W Y ⟶ ιPaths W X

The morphism in the path category corresponding to a formal inverse.

Equations

• CategoryTheory.Localization.Construction.ψ₂ W w hw = (CategoryTheory.Paths.of (CategoryTheory.Localization.Construction.LocQuiver W)).map (Sum.inr ⟨w, hw⟩)

inductive CategoryTheory.Localization.Construction.relations {C : Type uC} [Category.{uC', uC} C] (W : MorphismProperty C) : HomRel (Paths (LocQuiver W))

The relations by which we take the quotient in order to get the localized category.

• id {C : Type uC} [Category.{uC', uC} C] {W : MorphismProperty C} (X : C) : relations W (ψ₁ W (CategoryStruct.id X)) (CategoryStruct.id (ιPaths W X))
• comp {C : Type uC} [Category.{uC', uC} C] {W : MorphismProperty C} {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : relations W (ψ₁ W (CategoryStruct.comp f g)) (CategoryStruct.comp (ψ₁ W f) (ψ₁ W g))
• Winv₁ {C : Type uC} [Category.{uC', uC} C] {W : MorphismProperty C} {X Y : C} (w : X ⟶ Y) (hw : W w) : relations W (CategoryStruct.comp (ψ₁ W w) (ψ₂ W w hw)) (CategoryStruct.id (ιPaths W X))
• Winv₂ {C : Type uC} [Category.{uC', uC} C] {W : MorphismProperty C} {X Y : C} (w : X ⟶ Y) (hw : W w) : relations W (CategoryStruct.comp (ψ₂ W w hw) (ψ₁ W w)) (CategoryStruct.id (ιPaths W Y))

def CategoryTheory.MorphismProperty.Localization {C : Type uC} [Category.{uC', uC} C] (W : MorphismProperty C) : Type uC

The localized category obtained by formally inverting the morphisms in W : MorphismProperty C

Equations

• W.Localization = CategoryTheory.Quotient (CategoryTheory.Localization.Construction.relations W)

instance CategoryTheory.MorphismProperty.instCategoryLocalization {C : Type uC} [Category.{uC', uC} C] (W : MorphismProperty C) : Category.{max uC uC', uC} W.Localization

Equations

• W.instCategoryLocalization = id inferInstance

def CategoryTheory.MorphismProperty.Q {C : Type uC} [Category.{uC', uC} C] (W : MorphismProperty C) : Functor C W.Localization

The obvious functor C ⥤ W.Localization

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Localization.Construction.wIso {C : Type uC} [Category.{uC', uC} C] {W : MorphismProperty C} {X Y : C} (w : X ⟶ Y) (hw : W w) : W.Q.obj X ≅ W.Q.obj Y

The isomorphism in W.Localization associated to a morphism w in W

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev CategoryTheory.Localization.Construction.wInv {C : Type uC} [Category.{uC', uC} C] {W : MorphismProperty C} {X Y : C} (w : X ⟶ Y) (hw : W w) : W.Q.obj Y ⟶ W.Q.obj X

The formal inverse in W.Localization of a morphism w in W.

Equations

• CategoryTheory.Localization.Construction.wInv w hw = (CategoryTheory.Localization.Construction.wIso w hw).inv

theorem CategoryTheory.MorphismProperty.Q_inverts {C : Type uC} [Category.{uC', uC} C] (W : MorphismProperty C) : W.IsInvertedBy W.Q

def CategoryTheory.Localization.Construction.liftToPathCategory {C : Type uC} [Category.{uC', uC} C] {W : MorphismProperty C} {D : Type uD} [Category.{uD', uD} D] (G : Functor C D) (hG : W.IsInvertedBy G) : Functor (Paths (LocQuiver W)) D

The lifting of a functor to the path category of LocQuiver W

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Localization.Construction.liftToPathCategory_obj {C : Type uC} [Category.{uC', uC} C] {W : MorphismProperty C} {D : Type uD} [Category.{uD', uD} D] (G : Functor C D) (hG : W.IsInvertedBy G) (X : Paths (LocQuiver W)) : (liftToPathCategory G hG).obj X = G.obj X.obj

@[simp]

theorem CategoryTheory.Localization.Construction.liftToPathCategory_map {C : Type uC} [Category.{uC', uC} C] {W : MorphismProperty C} {D : Type uD} [Category.{uD', uD} D] (G : Functor C D) (hG : W.IsInvertedBy G) {X✝ Y✝ : Paths (LocQuiver W)} (f : X✝ ⟶ Y✝) : (liftToPathCategory G hG).map f = composePath ({ obj := fun (X : LocQuiver W) => G.obj X.obj, map := fun {X Y : LocQuiver W} (a : X ⟶ Y) => Sum.rec (fun (val : X.obj ⟶ Y.obj) => G.map val) (fun (val : { f : Y.obj ⟶ X.obj // W f }) => inv (G.map ↑val)) a }.mapPath f)

def CategoryTheory.Localization.Construction.lift {C : Type uC} [Category.{uC', uC} C] {W : MorphismProperty C} {D : Type uD} [Category.{uD', uD} D] (G : Functor C D) (hG : W.IsInvertedBy G) : Functor W.Localization D

The lifting of a functor C ⥤ D inverting W as a functor W.Localization ⥤ D

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Localization.Construction.lift_map {C : Type uC} [Category.{uC', uC} C] {W : MorphismProperty C} {D : Type uD} [Category.{uD', uD} D] (G : Functor C D) (hG : W.IsInvertedBy G) (a b : Quotient (relations W)) (hf : a ⟶ b) : (lift G hG).map hf = Quot.liftOn hf (fun (f : a.as ⟶ b.as) => composePath ({ obj := fun (X : LocQuiver W) => G.obj X.obj, map := fun {X Y : LocQuiver W} (a : X ⟶ Y) => Sum.rec (fun (val : X.obj ⟶ Y.obj) => G.map val) (fun (val : { f : Y.obj ⟶ X.obj // W f }) => inv (G.map ↑val)) a }.mapPath f)) ⋯

@[simp]

theorem CategoryTheory.Localization.Construction.lift_obj {C : Type uC} [Category.{uC', uC} C] {W : MorphismProperty C} {D : Type uD} [Category.{uD', uD} D] (G : Functor C D) (hG : W.IsInvertedBy G) (a : Quotient (relations W)) : (lift G hG).obj a = G.obj a.as.obj

@[simp]

theorem CategoryTheory.Localization.Construction.fac {C : Type uC} [Category.{uC', uC} C] {W : MorphismProperty C} {D : Type uD} [Category.{uD', uD} D] (G : Functor C D) (hG : W.IsInvertedBy G) : W.Q.comp (lift G hG) = G

theorem CategoryTheory.Localization.Construction.uniq {C : Type uC} [Category.{uC', uC} C] {W : MorphismProperty C} {D : Type uD} [Category.{uD', uD} D] (G₁ G₂ : Functor W.Localization D) (h : W.Q.comp G₁ = W.Q.comp G₂) : G₁ = G₂

def CategoryTheory.Localization.Construction.objEquiv {C : Type uC} [Category.{uC', uC} C] (W : MorphismProperty C) : C ≃ W.Localization

The canonical bijection between objects in a category and its localization with respect to a morphism_property W

Equations

• CategoryTheory.Localization.Construction.objEquiv W = { toFun := W.Q.obj, invFun := fun (X : W.Localization) => X.as.obj, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem CategoryTheory.Localization.Construction.objEquiv_symm_apply {C : Type uC} [Category.{uC', uC} C] (W : MorphismProperty C) (X : W.Localization) : (objEquiv W).symm X = X.as.obj

@[simp]

theorem CategoryTheory.Localization.Construction.objEquiv_apply {C : Type uC} [Category.{uC', uC} C] (W : MorphismProperty C) (a✝ : C) : (objEquiv W) a✝ = W.Q.obj a✝

theorem CategoryTheory.Localization.Construction.morphismProperty_is_top {C : Type uC} [Category.{uC', uC} C] {W : MorphismProperty C} (P : MorphismProperty W.Localization) [P.IsStableUnderComposition] (hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)) (hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv w hw)) : P = ⊤

A MorphismProperty in W.Localization is satisfied by all morphisms in the localized category if it contains the image of the morphisms in the original category, the inverses of the morphisms in W and if it is stable under composition

theorem CategoryTheory.Localization.Construction.morphismProperty_is_top' {C : Type uC} [Category.{uC', uC} C] {W : MorphismProperty C} (P : MorphismProperty W.Localization) [P.IsStableUnderComposition] (hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)) (hP₂ : ∀ ⦃X Y : W.Localization⦄ (e : X ≅ Y), P e.hom → P e.inv) : P = ⊤

A MorphismProperty in W.Localization is satisfied by all morphisms in the localized category if it contains the image of the morphisms in the original category, if is stable under composition and if the property is stable by passing to inverses.

def CategoryTheory.Localization.Construction.NatTransExtension.app {C : Type uC} [Category.{uC', uC} C] {W : MorphismProperty C} {D : Type uD} [Category.{uD', uD} D] {F₁ F₂ : Functor W.Localization D} (τ : W.Q.comp F₁ ⟶ W.Q.comp F₂) (X : W.Localization) : F₁.obj X ⟶ F₂.obj X

If F₁ and F₂ are functors W.Localization ⥤ D and if we have τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂, we shall define a natural transformation F₁ ⟶ F₂. This is the app field of this natural transformation.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Localization.Construction.NatTransExtension.app_eq {C : Type uC} [Category.{uC', uC} C] {W : MorphismProperty C} {D : Type uD} [Category.{uD', uD} D] {F₁ F₂ : Functor W.Localization D} (τ : W.Q.comp F₁ ⟶ W.Q.comp F₂) (X : C) : app τ (W.Q.obj X) = τ.app X

def CategoryTheory.Localization.Construction.natTransExtension {C : Type uC} [Category.{uC', uC} C] {W : MorphismProperty C} {D : Type uD} [Category.{uD', uD} D] {F₁ F₂ : Functor W.Localization D} (τ : W.Q.comp F₁ ⟶ W.Q.comp F₂) : F₁ ⟶ F₂

If F₁ and F₂ are functors W.Localization ⥤ D, a natural transformation F₁ ⟶ F₂ can be obtained from a natural transformation W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂.

Equations

• CategoryTheory.Localization.Construction.natTransExtension τ = { app := CategoryTheory.Localization.Construction.NatTransExtension.app τ, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Localization.Construction.natTransExtension_app {C : Type uC} [Category.{uC', uC} C] {W : MorphismProperty C} {D : Type uD} [Category.{uD', uD} D] {F₁ F₂ : Functor W.Localization D} (τ : W.Q.comp F₁ ⟶ W.Q.comp F₂) (X : W.Localization) : (natTransExtension τ).app X = NatTransExtension.app τ X

@[simp]

theorem CategoryTheory.Localization.Construction.whiskerLeft_natTransExtension {C : Type uC} [Category.{uC', uC} C] {W : MorphismProperty C} {D : Type uD} [Category.{uD', uD} D] {F G : Functor W.Localization D} (τ : W.Q.comp F ⟶ W.Q.comp G) : whiskerLeft W.Q (natTransExtension τ) = τ

theorem CategoryTheory.Localization.Construction.natTransExtension_hcomp {C : Type uC} [Category.{uC', uC} C] {W : MorphismProperty C} {D : Type uD} [Category.{uD', uD} D] {F G : Functor W.Localization D} (τ : W.Q.comp F ⟶ W.Q.comp G) : CategoryStruct.id W.Q ◫ natTransExtension τ = τ

theorem CategoryTheory.Localization.Construction.natTrans_hcomp_injective {C : Type uC} [Category.{uC', uC} C] {W : MorphismProperty C} {D : Type uD} [Category.{uD', uD} D] {F G : Functor W.Localization D} {τ₁ τ₂ : F ⟶ G} (h : CategoryStruct.id W.Q ◫ τ₁ = CategoryStruct.id W.Q ◫ τ₂) : τ₁ = τ₂

def CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor {C : Type uC} [Category.{uC', uC} C] (W : MorphismProperty C) (D : Type uD) [Category.{uD', uD} D] : Functor (Functor W.Localization D) (W.FunctorsInverting D)

The functor (W.Localization ⥤ D) ⥤ (W.FunctorsInverting D) induced by the composition with W.Q : C ⥤ W.Localization.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor_obj_obj_map {C : Type uC} [Category.{uC', uC} C] (W : MorphismProperty C) (D : Type uD) [Category.{uD', uD} D] (X : Functor W.Localization D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((functor W D).obj X).obj.map f = X.map (W.Q.map f)

@[simp]

theorem CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor_map_app {C : Type uC} [Category.{uC', uC} C] (W : MorphismProperty C) (D : Type uD) [Category.{uD', uD} D] {X✝ Y✝ : Functor W.Localization D} (f : X✝ ⟶ Y✝) (X : C) : ((functor W D).map f).app X = f.app (W.Q.obj X)

@[simp]

theorem CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor_obj_obj_obj {C : Type uC} [Category.{uC', uC} C] (W : MorphismProperty C) (D : Type uD) [Category.{uD', uD} D] (X : Functor W.Localization D) (X✝ : C) : ((functor W D).obj X).obj.obj X✝ = X.obj (W.Q.obj X✝)

def CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse {C : Type uC} [Category.{uC', uC} C] (W : MorphismProperty C) (D : Type uD) [Category.{uD', uD} D] : Functor (W.FunctorsInverting D) (Functor W.Localization D)

The function (W.FunctorsInverting D) ⥤ (W.Localization ⥤ D) induced by Construction.lift.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_obj_obj {C : Type uC} [Category.{uC', uC} C] (W : MorphismProperty C) (D : Type uD) [Category.{uD', uD} D] (G : W.FunctorsInverting D) (a : Quotient (relations W)) : ((inverse W D).obj G).obj a = G.obj.obj a.as.obj

@[simp]

theorem CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_obj_map {C : Type uC} [Category.{uC', uC} C] (W : MorphismProperty C) (D : Type uD) [Category.{uD', uD} D] (G : W.FunctorsInverting D) (a b : Quotient (relations W)) (hf : a ⟶ b) : ((inverse W D).obj G).map hf = Quot.liftOn hf (fun (f : a.as ⟶ b.as) => composePath ({ obj := fun (X : LocQuiver W) => G.obj.obj X.obj, map := fun {X Y : LocQuiver W} (a : X ⟶ Y) => Sum.rec (fun (val : X.obj ⟶ Y.obj) => G.obj.map val) (fun (val : { f : Y.obj ⟶ X.obj // W f }) => inv (G.obj.map ↑val)) a }.mapPath f)) ⋯

@[simp]

theorem CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_map_app {C : Type uC} [Category.{uC', uC} C] (W : MorphismProperty C) (D : Type uD) [Category.{uD', uD} D] {X✝ Y✝ : W.FunctorsInverting D} (τ : X✝ ⟶ Y✝) (X : W.Localization) : ((inverse W D).map τ).app X = NatTransExtension.app (CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp τ (eqToHom ⋯))) X

def CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.unitIso {C : Type uC} [Category.{uC', uC} C] (W : MorphismProperty C) (D : Type uD) [Category.{uD', uD} D] : Functor.id (Functor W.Localization D) ≅ (functor W D).comp (inverse W D)

The unit isomorphism of the equivalence of categories whiskeringLeftEquivalence W D.

Equations

• CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.unitIso W D = CategoryTheory.eqToIso ⋯

@[simp]

theorem CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.unitIso_hom {C : Type uC} [Category.{uC', uC} C] (W : MorphismProperty C) (D : Type uD) [Category.{uD', uD} D] : (unitIso W D).hom = eqToHom ⋯

@[simp]

theorem CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.unitIso_inv {C : Type uC} [Category.{uC', uC} C] (W : MorphismProperty C) (D : Type uD) [Category.{uD', uD} D] : (unitIso W D).inv = eqToHom ⋯

def CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.counitIso {C : Type uC} [Category.{uC', uC} C] (W : MorphismProperty C) (D : Type uD) [Category.{uD', uD} D] : (inverse W D).comp (functor W D) ≅ Functor.id (W.FunctorsInverting D)

The counit isomorphism of the equivalence of categories WhiskeringLeftEquivalence W D.

Equations

• CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.counitIso W D = CategoryTheory.eqToIso ⋯

@[simp]

theorem CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.counitIso_inv {C : Type uC} [Category.{uC', uC} C] (W : MorphismProperty C) (D : Type uD) [Category.{uD', uD} D] : (counitIso W D).inv = eqToHom ⋯

@[simp]

theorem CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.counitIso_hom {C : Type uC} [Category.{uC', uC} C] (W : MorphismProperty C) (D : Type uD) [Category.{uD', uD} D] : (counitIso W D).hom = eqToHom ⋯

def CategoryTheory.Localization.Construction.whiskeringLeftEquivalence {C : Type uC} [Category.{uC', uC} C] (W : MorphismProperty C) (D : Type uD) [Category.{uD', uD} D] : Functor W.Localization D ≌ W.FunctorsInverting D

The equivalence of categories (W.localization ⥤ D) ≌ (W.FunctorsInverting D) induced by the composition with W.Q : C ⥤ W.localization.

Equations

• One or more equations did not get rendered due to their size.