mathlib3 documentation

category_theory.localization.construction

Construction of the localized category #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

We first construct a quiver loc_quiver 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 loc_quiver 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.is_inverted_by 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 #

source
@[nolint]
structure category_theory.localization.construction.loc_quiver {C : Type u_1} [category_theory.category C] (W : category_theory.morphism_property C) :
Type u_1
  • obj : C

If W : morphism_property C, loc_quiver 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.

Instances for category_theory.localization.construction.loc_quiver
source
@[protected, instance]
def category_theory.localization.construction.loc_quiver.quiver {C : Type u_1} [category_theory.category C] (W : category_theory.morphism_property C) :
quiver (category_theory.localization.construction.loc_quiver W)
Equations
source
def category_theory.localization.construction.ι_paths {C : Type u_1} [category_theory.category C] (W : category_theory.morphism_property C) (X : C) :
category_theory.paths (category_theory.localization.construction.loc_quiver W)

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

Equations
source
@[simp]
def category_theory.localization.construction.ψ₁ {C : Type u_1} [category_theory.category C] (W : category_theory.morphism_property C) {X Y : C} (f : X ⟶ Y) :
category_theory.localization.construction.ι_paths W X ⟶ category_theory.localization.construction.ι_paths W Y

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

Equations
source
@[simp]
def category_theory.localization.construction.ψ₂ {C : Type u_1} [category_theory.category C] (W : category_theory.morphism_property C) {X Y : C} (w : X ⟶ Y) (hw : W w) :
category_theory.localization.construction.ι_paths W Y ⟶ category_theory.localization.construction.ι_paths W X

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

Equations
source
inductive category_theory.localization.construction.relations {C : Type u_1} [category_theory.category C] (W : category_theory.morphism_property C) :
hom_rel (category_theory.paths (category_theory.localization.construction.loc_quiver W))

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

source
@[nolint]
def category_theory.morphism_property.localization {C : Type u_1} [category_theory.category C] (W : category_theory.morphism_property C) :
Type u_1

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

Equations
Instances for category_theory.morphism_property.localization
source
@[protected, instance]
def category_theory.morphism_property.localization.category {C : Type u_1} [category_theory.category C] (W : category_theory.morphism_property C) :
category_theory.category W.localization
source
def category_theory.morphism_property.Q {C : Type u_1} [category_theory.category C] (W : category_theory.morphism_property C) :
C ⥤ W.localization

The obvious functor C ⥤ W.localization

Equations
Instances for category_theory.morphism_property.Q
source
def category_theory.localization.construction.Wiso {C : Type u_1} [category_theory.category C] {W : category_theory.morphism_property 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
source
@[reducible]
def category_theory.localization.construction.Winv {C : Type u_1} [category_theory.category C] {W : category_theory.morphism_property C} {X Y : C} (w : X ⟶ Y) (hw : W w) :
(category_theory.morphism_property.Q (λ {X Y : C} (w : X ⟶ Y), W w)).obj Y ⟶ (category_theory.morphism_property.Q (λ {X Y : C} (w : X ⟶ Y), W w)).obj X

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

source
theorem category_theory.morphism_property.Q_inverts {C : Type u_1} [category_theory.category C] (W : category_theory.morphism_property C) :
W.is_inverted_by W.Q
source
noncomputable def category_theory.localization.construction.lift_to_path_category {C : Type u_1} [category_theory.category C] {W : category_theory.morphism_property C} {D : Type u_3} [category_theory.category D] (G : C ⥤ D) (hG : W.is_inverted_by G) :
category_theory.paths (category_theory.localization.construction.loc_quiver W) ⥤ D

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

Equations
source
@[simp]
theorem category_theory.localization.construction.lift_to_path_category_obj {C : Type u_1} [category_theory.category C] {W : category_theory.morphism_property C} {D : Type u_3} [category_theory.category D] (G : C ⥤ D) (hG : W.is_inverted_by G) (X : category_theory.paths (category_theory.localization.construction.loc_quiver W)) :
(category_theory.localization.construction.lift_to_path_category G hG).obj X = G.obj X.obj
source
@[simp]
theorem category_theory.localization.construction.lift_to_path_category_map {C : Type u_1} [category_theory.category C] {W : category_theory.morphism_property C} {D : Type u_3} [category_theory.category D] (G : C ⥤ D) (hG : W.is_inverted_by G) (X Y : category_theory.paths (category_theory.localization.construction.loc_quiver W)) (f : X ⟶ Y) :
(category_theory.localization.construction.lift_to_path_category G hG).map f = category_theory.compose_path ({obj := λ (X : category_theory.localization.construction.loc_quiver W), G.obj X.obj, map := λ (X Y : category_theory.localization.construction.loc_quiver W), sum.rec G.map (subtype.rec (λ (g : Y.obj ⟶ X.obj) (hg : W g), category_theory.inv (G.map g)))}.map_path f)
source
@[simp]
theorem category_theory.localization.construction.lift_obj {C : Type u_1} [category_theory.category C] {W : category_theory.morphism_property C} {D : Type u_3} [category_theory.category D] (G : C ⥤ D) (hG : W.is_inverted_by G) (a : category_theory.quotient (category_theory.localization.construction.relations W)) :
(category_theory.localization.construction.lift G hG).obj a = G.obj a.as.obj
source
@[simp]
theorem category_theory.localization.construction.lift_map {C : Type u_1} [category_theory.category C] {W : category_theory.morphism_property C} {D : Type u_3} [category_theory.category D] (G : C ⥤ D) (hG : W.is_inverted_by G) (a b : category_theory.quotient (category_theory.localization.construction.relations W)) (hf : a ⟶ b) :
(category_theory.localization.construction.lift G hG).map hf = quot.lift_on hf (category_theory.localization.construction.lift_to_path_category G hG).map _
source
noncomputable def category_theory.localization.construction.lift {C : Type u_1} [category_theory.category C] {W : category_theory.morphism_property C} {D : Type u_3} [category_theory.category D] (G : C ⥤ D) (hG : W.is_inverted_by G) :
W.localization ⥤ D

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

Equations
Instances for category_theory.localization.construction.lift
source
@[simp]
theorem category_theory.localization.construction.fac {C : Type u_1} [category_theory.category C] {W : category_theory.morphism_property C} {D : Type u_3} [category_theory.category D] (G : C ⥤ D) (hG : W.is_inverted_by G) :
W.Q ⋙ category_theory.localization.construction.lift G hG = G
source
theorem category_theory.localization.construction.uniq {C : Type u_1} [category_theory.category C] {W : category_theory.morphism_property C} {D : Type u_3} [category_theory.category D] (G₁ G₂ : W.localization ⥤ D) (h : W.Q ⋙ G₁ = W.Q ⋙ G₂) :
G₁ = G₂
source
@[simp]
theorem category_theory.localization.construction.obj_equiv_symm_apply {C : Type u_1} [category_theory.category C] (W : category_theory.morphism_property C) (X : W.localization) :
⇑((category_theory.localization.construction.obj_equiv W).symm) X = X.as.obj
source
@[simp]
theorem category_theory.localization.construction.obj_equiv_apply {C : Type u_1} [category_theory.category C] (W : category_theory.morphism_property C) (ᾰ : C) :
⇑(category_theory.localization.construction.obj_equiv W) ᾰ = W.Q.obj ᾰ
source
def category_theory.localization.construction.obj_equiv {C : Type u_1} [category_theory.category C] (W : category_theory.morphism_property C) :
C ≃ W.localization

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

Equations
source
theorem category_theory.localization.construction.morphism_property_is_top {C : Type u_1} [category_theory.category C] {W : category_theory.morphism_property C} (P : category_theory.morphism_property W.localization) (hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)) (hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (category_theory.localization.construction.Winv w hw)) (hP₃ : P.stable_under_composition) :
P = ⊤

A morphism_property 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

source
theorem category_theory.localization.construction.morphism_property_is_top' {C : Type u_1} [category_theory.category C] {W : category_theory.morphism_property C} (P : category_theory.morphism_property W.localization) (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) (hP₃ : P.stable_under_composition) :
P = ⊤

A morphism_property 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.

source
def category_theory.localization.construction.nat_trans_extension.app {C : Type u_1} [category_theory.category C] {W : category_theory.morphism_property C} {D : Type u_3} [category_theory.category D] {F₁ F₂ : W.localization ⥤ D} (τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ 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
source
@[simp]
theorem category_theory.localization.construction.nat_trans_extension.app_eq {C : Type u_1} [category_theory.category C] {W : category_theory.morphism_property C} {D : Type u_3} [category_theory.category D] {F₁ F₂ : W.localization ⥤ D} (τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂) (X : C) :
category_theory.localization.construction.nat_trans_extension.app τ (W.Q.obj X) = τ.app X
source
def category_theory.localization.construction.nat_trans_extension {C : Type u_1} [category_theory.category C] {W : category_theory.morphism_property C} {D : Type u_3} [category_theory.category D] {F₁ F₂ : W.localization ⥤ D} (τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ 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
source
@[simp]
theorem category_theory.localization.construction.nat_trans_extension_app {C : Type u_1} [category_theory.category C] {W : category_theory.morphism_property C} {D : Type u_3} [category_theory.category D] {F₁ F₂ : W.localization ⥤ D} (τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂) (X : W.localization) :
(category_theory.localization.construction.nat_trans_extension τ).app X = category_theory.localization.construction.nat_trans_extension.app τ X
source
@[simp]
theorem category_theory.localization.construction.nat_trans_extension_hcomp {C : Type u_1} [category_theory.category C] {W : category_theory.morphism_property C} {D : Type u_3} [category_theory.category D] {F G : W.localization ⥤ D} (τ : W.Q ⋙ F ⟶ W.Q ⋙ G) :
𝟙 W.Q ◫ category_theory.localization.construction.nat_trans_extension τ = τ
source
theorem category_theory.localization.construction.nat_trans_hcomp_injective {C : Type u_1} [category_theory.category C] {W : category_theory.morphism_property C} {D : Type u_3} [category_theory.category D] {F G : W.localization ⥤ D} {τ₁ τ₂ : F ⟶ G} (h : 𝟙 W.Q ◫ τ₁ = 𝟙 W.Q ◫ τ₂) :
τ₁ = τ₂
source
@[simp]
theorem category_theory.localization.construction.whiskering_left_equivalence.functor_obj_obj_obj {C : Type u_1} [category_theory.category C] (W : category_theory.morphism_property C) (D : Type u_3) [category_theory.category D] (X : W.localization ⥤ D) (X_1 : C) :
((category_theory.localization.construction.whiskering_left_equivalence.functor W D).obj X).obj.obj X_1 = X.obj (W.Q.obj X_1)
source
def category_theory.localization.construction.whiskering_left_equivalence.functor {C : Type u_1} [category_theory.category C] (W : category_theory.morphism_property C) (D : Type u_3) [category_theory.category D] :
(W.localization ⥤ D) ⥤ W.functors_inverting D

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

Equations
source
@[simp]
theorem category_theory.localization.construction.whiskering_left_equivalence.functor_obj_obj_map {C : Type u_1} [category_theory.category C] (W : category_theory.morphism_property C) (D : Type u_3) [category_theory.category D] (X : W.localization ⥤ D) (_x _x_1 : C) (f : _x ⟶ _x_1) :
((category_theory.localization.construction.whiskering_left_equivalence.functor W D).obj X).obj.map f = X.map (W.Q.map f)
source
@[simp]
theorem category_theory.localization.construction.whiskering_left_equivalence.functor_map_app {C : Type u_1} [category_theory.category C] (W : category_theory.morphism_property C) (D : Type u_3) [category_theory.category D] (X Y : W.localization ⥤ D) (f : X ⟶ Y) (X_1 : C) :
((category_theory.localization.construction.whiskering_left_equivalence.functor W D).map f).app X_1 = f.app (W.Q.obj X_1)
source
@[simp]
theorem category_theory.localization.construction.whiskering_left_equivalence.inverse_obj {C : Type u_1} [category_theory.category C] (W : category_theory.morphism_property C) (D : Type u_3) [category_theory.category D] (G : W.functors_inverting D) :
(category_theory.localization.construction.whiskering_left_equivalence.inverse W D).obj G = category_theory.localization.construction.lift G.obj _
source
@[simp]
theorem category_theory.localization.construction.whiskering_left_equivalence.inverse_map {C : Type u_1} [category_theory.category C] (W : category_theory.morphism_property C) (D : Type u_3) [category_theory.category D] (G₁ G₂ : W.functors_inverting D) (τ : G₁ ⟶ G₂) :
(category_theory.localization.construction.whiskering_left_equivalence.inverse W D).map τ = category_theory.localization.construction.nat_trans_extension (category_theory.eq_to_hom _ ≫ τ ≫ category_theory.eq_to_hom _)
source
noncomputable def category_theory.localization.construction.whiskering_left_equivalence.inverse {C : Type u_1} [category_theory.category C] (W : category_theory.morphism_property C) (D : Type u_3) [category_theory.category D] :
W.functors_inverting D ⥤ W.localization ⥤ D

The function (W.functors_inverting D) ⥤ (W.localization ⥤ D) induced by construction.lift.

Equations
source
@[simp]
theorem category_theory.localization.construction.whiskering_left_equivalence.unit_iso_inv {C : Type u_1} [category_theory.category C] (W : category_theory.morphism_property C) (D : Type u_3) [category_theory.category D] :
(category_theory.localization.construction.whiskering_left_equivalence.unit_iso W D).inv = category_theory.eq_to_hom _
source
noncomputable def category_theory.localization.construction.whiskering_left_equivalence.unit_iso {C : Type u_1} [category_theory.category C] (W : category_theory.morphism_property C) (D : Type u_3) [category_theory.category D] :
𝟭 (W.localization ⥤ D) ≅ category_theory.localization.construction.whiskering_left_equivalence.functor W D ⋙ category_theory.localization.construction.whiskering_left_equivalence.inverse W D

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

Equations
source
@[simp]
theorem category_theory.localization.construction.whiskering_left_equivalence.unit_iso_hom {C : Type u_1} [category_theory.category C] (W : category_theory.morphism_property C) (D : Type u_3) [category_theory.category D] :
(category_theory.localization.construction.whiskering_left_equivalence.unit_iso W D).hom = category_theory.eq_to_hom _
source
@[simp]
theorem category_theory.localization.construction.whiskering_left_equivalence.counit_iso_inv {C : Type u_1} [category_theory.category C] (W : category_theory.morphism_property C) (D : Type u_3) [category_theory.category D] :
(category_theory.localization.construction.whiskering_left_equivalence.counit_iso W D).inv = category_theory.eq_to_hom _
source
noncomputable def category_theory.localization.construction.whiskering_left_equivalence.counit_iso {C : Type u_1} [category_theory.category C] (W : category_theory.morphism_property C) (D : Type u_3) [category_theory.category D] :
category_theory.localization.construction.whiskering_left_equivalence.inverse W D ⋙ category_theory.localization.construction.whiskering_left_equivalence.functor W D ≅ 𝟭 (W.functors_inverting D)

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

Equations
source
@[simp]
theorem category_theory.localization.construction.whiskering_left_equivalence.counit_iso_hom {C : Type u_1} [category_theory.category C] (W : category_theory.morphism_property C) (D : Type u_3) [category_theory.category D] :
(category_theory.localization.construction.whiskering_left_equivalence.counit_iso W D).hom = category_theory.eq_to_hom _
source
noncomputable def category_theory.localization.construction.whiskering_left_equivalence {C : Type u_1} [category_theory.category C] (W : category_theory.morphism_property C) (D : Type u_3) [category_theory.category D] :
W.localization ⥤ D ≌ W.functors_inverting D

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

Equations