mathlib3 documentation

category_theory.localization.predicate

Predicate for localized categories #

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

In this file, a predicate L.is_localization W is introduced for a functor L : C ⥤ D and W : morphism_property C: it expresses that L identifies D with the localized category of C with respect to W (up to equivalence).

We introduce a universal property strict_universal_property_fixed_target L W E which states that L inverts the morphisms in W and that all functors C ⥤ E inverting W uniquely factors as a composition of L ⋙ G with G : D ⥤ E. Such universal properties are inputs for the constructor is_localization.mk' for L.is_localization W.

When L : C ⥤ D is a localization functor for W : morphism_property (i.e. when [L.is_localization W] holds), for any category E, there is an equivalence functor_equivalence L W E : (D ⥤ E) ≌ (W.functors_inverting E) that is induced by the composition with the functor L. When two functors F : C ⥤ E and F' : D ⥤ E correspond via this equivalence, we shall say that F' lifts F, and the associated isomorphism L ⋙ F' ≅ F is the datum that is part of the class lifting L W F F'. The functions lift_nat_trans and lift_nat_iso can be used to lift natural transformations and natural isomorphisms between functors.

@[class]

The predicate expressing that, up to equivalence, a functor L : C ⥤ D identifies the category D with the localized category of C with respect to W : morphism_property C.

Instances of this typeclass

This universal property states that a functor L : C ⥤ D inverts morphisms in W and the all functors D ⥤ E (for a fixed category E) uniquely factors through L.

Instances for category_theory.localization.strict_universal_property_fixed_target
noncomputable def category_theory.localization.iso_of_hom {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] (L : C D) (W : category_theory.morphism_property C) [L.is_localization W] {X Y : C} (f : X Y) (hf : W f) :
L.obj X L.obj Y

The isomorphism L.obj X ≅ L.obj Y that is deduced from a morphism f : X ⟶ Y which belongs to W, when L.is_localization W.

Equations

A chosen equivalence of categories W.localization ≅ D for a functor L : C ⥤ D which satisfies L.is_localization W. This shall be used in order to deduce properties of L from properties of W.Q.

Equations

Via the equivalence of categories equivalence_from_model L W : W.localization ≌ D, one may identify the functors W.Q and L.

Equations

The functor (D ⥤ E) ⥤ W.functors_inverting E induced by the composition with a localization functor L : C ⥤ D with respect to W : morphism_property C.

Equations
Instances for category_theory.localization.whiskering_left_functor

The equivalence of categories (D ⥤ E) ≌ (W.functors_inverting E) induced by the composition with a localization functor L : C ⥤ D with respect to W : morphism_property C.

Equations
@[nolint]

The functor (D ⥤ E) ⥤ (C ⥤ E) given by the composition with a localization functor L : C ⥤ D with respect to W : morphism_property C.

Equations
Instances for category_theory.localization.whiskering_left_functor'
theorem category_theory.localization.nat_trans_ext {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] (L : C D) (W : category_theory.morphism_property C) {E : Type u_5} [category_theory.category E] [L.is_localization W] {F₁ F₂ : D E} (τ τ' : F₁ F₂) (h : (X : C), τ.app (L.obj X) = τ'.app (L.obj X)) :
τ = τ'
@[class]
structure category_theory.localization.lifting {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] (L : C D) (W : category_theory.morphism_property C) {E : Type u_5} [category_theory.category E] [L.is_localization W] (F : C E) (F' : D E) :
Type (max u_1 u_6)

When L : C ⥤ D is a localization functor for W : morphism_property C and F : C ⥤ E is a functor, we shall say that F' : D ⥤ E lifts F if the obvious diagram is commutative up to an isomorphism.

Instances of this typeclass
Instances of other typeclasses for category_theory.localization.lifting
  • category_theory.localization.lifting.has_sizeof_inst
noncomputable def category_theory.localization.lift {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] {W : category_theory.morphism_property C} {E : Type u_5} [category_theory.category E] (F : C E) (hF : W.is_inverted_by F) (L : C D) [hL : L.is_localization W] :
D E

Given a localization functor L : C ⥤ D for W : morphism_property C and a functor F : C ⥤ E which inverts W, this is a choice of functor D ⥤ E which lifts F.

Equations
Instances for category_theory.localization.lift

The canonical isomorphism L ⋙ lift F hF L ≅ F for any functor F : C ⥤ E which inverts W, when L : C ⥤ D is a localization functor for W.

Equations
noncomputable def category_theory.localization.lift_nat_trans {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] (L : C D) (W : category_theory.morphism_property C) {E : Type u_5} [category_theory.category E] [L.is_localization W] (F₁ F₂ : C E) (F₁' F₂' : D E) [category_theory.localization.lifting L W F₁ F₁'] [h₂ : category_theory.localization.lifting L W F₂ F₂'] (τ : F₁ F₂) :
F₁' F₂'

Given a localization functor L : C ⥤ D for W : morphism_property C, if (F₁' F₂' : D ⥤ E) are functors which lifts functors (F₁ F₂ : C ⥤ E), a natural transformation τ : F₁ ⟶ F₂ uniquely lifts to a natural transformation F₁' ⟶ F₂'.

Equations
@[simp]
theorem category_theory.localization.lift_nat_trans_app {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] (L : C D) (W : category_theory.morphism_property C) {E : Type u_5} [category_theory.category E] [L.is_localization W] (F₁ F₂ : C E) (F₁' F₂' : D E) [category_theory.localization.lifting L W F₁ F₁'] [category_theory.localization.lifting L W F₂ F₂'] (τ : F₁ F₂) (X : C) :
@[simp]
theorem category_theory.localization.comp_lift_nat_trans {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] (L : C D) (W : category_theory.morphism_property C) {E : Type u_5} [category_theory.category E] [L.is_localization W] (F₁ F₂ F₃ : C E) (F₁' F₂' F₃' : D E) [h₁ : category_theory.localization.lifting L W F₁ F₁'] [h₂ : category_theory.localization.lifting L W F₂ F₂'] [h₃ : category_theory.localization.lifting L W F₃ F₃'] (τ : F₁ F₂) (τ' : F₂ F₃) :
category_theory.localization.lift_nat_trans L W F₁ F₂ F₁' F₂' τ category_theory.localization.lift_nat_trans L W F₂ F₃ F₂' F₃' τ' = category_theory.localization.lift_nat_trans L W F₁ F₃ F₁' F₃' τ')
@[simp]
theorem category_theory.localization.comp_lift_nat_trans_assoc {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] (L : C D) (W : category_theory.morphism_property C) {E : Type u_5} [category_theory.category E] [L.is_localization W] (F₁ F₂ F₃ : C E) (F₁' F₂' F₃' : D E) [h₁ : category_theory.localization.lifting L W F₁ F₁'] [h₂ : category_theory.localization.lifting L W F₂ F₂'] [h₃ : category_theory.localization.lifting L W F₃ F₃'] (τ : F₁ F₂) (τ' : F₂ F₃) {X' : D E} (f' : F₃' X') :
category_theory.localization.lift_nat_trans L W F₁ F₂ F₁' F₂' τ category_theory.localization.lift_nat_trans L W F₂ F₃ F₂' F₃' τ' f' = category_theory.localization.lift_nat_trans L W F₁ F₃ F₁' F₃' τ') f'
noncomputable def category_theory.localization.lift_nat_iso {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] (L : C D) (W : category_theory.morphism_property C) {E : Type u_5} [category_theory.category E] [L.is_localization W] (F₁ F₂ : C E) (F₁' F₂' : D E) [h₁ : category_theory.localization.lifting L W F₁ F₁'] [h₂ : category_theory.localization.lifting L W F₂ F₂'] (e : F₁ F₂) :
F₁' F₂'

Given a localization functor L : C ⥤ D for W : morphism_property C, if (F₁' F₂' : D ⥤ E) are functors which lifts functors (F₁ F₂ : C ⥤ E), a natural isomorphism τ : F₁ ⟶ F₂ lifts to a natural isomorphism F₁' ⟶ F₂'.

Equations
@[simp]
theorem category_theory.localization.lift_nat_iso_hom {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] (L : C D) (W : category_theory.morphism_property C) {E : Type u_5} [category_theory.category E] [L.is_localization W] (F₁ F₂ : C E) (F₁' F₂' : D E) [h₁ : category_theory.localization.lifting L W F₁ F₁'] [h₂ : category_theory.localization.lifting L W F₂ F₂'] (e : F₁ F₂) :
(category_theory.localization.lift_nat_iso L W F₁ F₂ F₁' F₂' e).hom = category_theory.localization.lift_nat_trans L W F₁ F₂ F₁' F₂' e.hom
@[simp]
theorem category_theory.localization.lift_nat_iso_inv {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] (L : C D) (W : category_theory.morphism_property C) {E : Type u_5} [category_theory.category E] [L.is_localization W] (F₁ F₂ : C E) (F₁' F₂' : D E) [h₁ : category_theory.localization.lifting L W F₁ F₁'] [h₂ : category_theory.localization.lifting L W F₂ F₂'] (e : F₁ F₂) :
(category_theory.localization.lift_nat_iso L W F₁ F₂ F₁' F₂' e).inv = category_theory.localization.lift_nat_trans L W F₂ F₁ F₂' F₁' e.inv
def category_theory.localization.lifting.of_isos {C : Type u_1} {D : Type u_2} [category_theory.category C] [category_theory.category D] (L : C D) (W : category_theory.morphism_property C) {E : Type u_5} [category_theory.category E] [L.is_localization W] {F₁ F₂ : C E} {F₁' F₂' : D E} (e : F₁ F₂) (e' : F₁' F₂') [category_theory.localization.lifting L W F₁ F₁'] :

Given a localization functor L : C ⥤ D for W : morphism_property C, if F₁' : D ⥤ E lifts a functor F₁ : C ⥤ D, then a functor F₂' which is isomorphic to F₁' also lifts a functor F₂ that is isomorphic to F₁.

Equations

If L : C ⥤ D is a localization for W : morphism_property C, then it is also the case of a functor obtained by post-composing L with an equivalence of categories.