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]
structure
category_theory.functor.is_localization
{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) :
Prop
- inverts : W.is_inverted_by L
- nonempty_is_equivalence : nonempty (category_theory.is_equivalence (category_theory.localization.construction.lift L category_theory.functor.is_localization.inverts))
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.
@[protected, instance]
def
category_theory.functor.Q_is_localization
{C : Type u_1}
[category_theory.category C]
(W : category_theory.morphism_property C) :
W.Q.is_localization W
structure
category_theory.localization.strict_universal_property_fixed_target
{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] :
Type (max u_1 u_2 u_3 u_4 u_5 u_6)
- inverts : W.is_inverted_by L
- lift : Π (F : C ⥤ E), W.is_inverted_by F → D ⥤ E
- fac : ∀ (F : C ⥤ E) (hF : W.is_inverted_by F), L ⋙ self.lift F hF = F
- uniq : ∀ (F₁ F₂ : D ⥤ E), L ⋙ F₁ = L ⋙ F₂ → F₁ = F₂
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
- category_theory.localization.strict_universal_property_fixed_target.has_sizeof_inst
- category_theory.localization.strict_universal_property_fixed_target.inhabited
@[simp]
theorem
category_theory.localization.strict_universal_property_fixed_target_Q_lift
{C : Type u_1}
[category_theory.category C]
(W : category_theory.morphism_property C)
(E : Type u_5)
[category_theory.category E]
(G : C ⥤ E)
(hG : W.is_inverted_by G) :
noncomputable
def
category_theory.localization.strict_universal_property_fixed_target_Q
{C : Type u_1}
[category_theory.category C]
(W : category_theory.morphism_property C)
(E : Type u_5)
[category_theory.category E] :
The localized category W.localization that was constructed satisfies
the universal property of the localization.
Equations
- category_theory.localization.strict_universal_property_fixed_target_Q W E = {inverts := _, lift := category_theory.localization.construction.lift _inst_3, fac := _, uniq := _}
@[protected, instance]
noncomputable
def
category_theory.localization.strict_universal_property_fixed_target.inhabited
{C : Type u_1}
[category_theory.category C]
(W : category_theory.morphism_property C)
(E : Type u_5)
[category_theory.category E] :
@[simp]
theorem
category_theory.localization.strict_universal_property_fixed_target_id_lift
{C : Type u_1}
[category_theory.category C]
(W : category_theory.morphism_property C)
(E : Type u_5)
[category_theory.category E]
(hW : W ⊆ category_theory.morphism_property.isomorphisms C)
(F : C ⥤ E)
(hF : W.is_inverted_by F) :
def
category_theory.localization.strict_universal_property_fixed_target_id
{C : Type u_1}
[category_theory.category C]
(W : category_theory.morphism_property C)
(E : Type u_5)
[category_theory.category E]
(hW : W ⊆ category_theory.morphism_property.isomorphisms C) :
When W consists of isomorphisms, the identity satisfies the universal property
of the localization.
Equations
- category_theory.localization.strict_universal_property_fixed_target_id W E hW = {inverts := _, lift := λ (F : C ⥤ E) (hF : W.is_inverted_by F), F, fac := _, uniq := _}
theorem
category_theory.functor.is_localization.mk'
{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)
(h₁ : category_theory.localization.strict_universal_property_fixed_target L W D)
(h₂ : category_theory.localization.strict_universal_property_fixed_target L W W.localization) :
L.is_localization W
theorem
category_theory.functor.is_localization.for_id
{C : Type u_1}
[category_theory.category C]
(W : category_theory.morphism_property C)
(hW : W ⊆ category_theory.morphism_property.isomorphisms C) :
(𝟭 C).is_localization W
theorem
category_theory.localization.inverts
{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] :
W.is_inverted_by L
@[simp]
theorem
category_theory.localization.iso_of_hom_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)
[L.is_localization W]
{X Y : C}
(f : X ⟶ Y)
(hf : W f) :
(category_theory.localization.iso_of_hom L W f hf).inv = category_theory.inv (L.map f)
@[simp]
theorem
category_theory.localization.iso_of_hom_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) :
(category_theory.localization.iso_of_hom L W f hf).hom = L.map f
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) :
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
- category_theory.localization.iso_of_hom L W f hf = category_theory.as_iso (L.map f)
@[protected, instance]
noncomputable
def
category_theory.localization.construction.lift.category_theory.is_equivalence
{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] :
noncomputable
def
category_theory.localization.equivalence_from_model
{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] :
W.localization ≌ D
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.
noncomputable
def
category_theory.localization.Q_comp_equivalence_from_model_functor_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)
[L.is_localization W] :
Via the equivalence of categories equivalence_from_model L W : W.localization ≌ D,
one may identify the functors W.Q and L.
noncomputable
def
category_theory.localization.comp_equivalence_from_model_inverse_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)
[L.is_localization W] :
Via the equivalence of categories equivalence_from_model L W : W.localization ≌ D,
one may identify the functors L and W.Q.
Equations
- category_theory.localization.comp_equivalence_from_model_inverse_iso L W = ((category_theory.iso_whisker_right (category_theory.localization.Q_comp_equivalence_from_model_functor_iso L W).symm (category_theory.localization.equivalence_from_model L W).inverse ≪≫ W.Q.associator (category_theory.localization.equivalence_from_model L W).functor (category_theory.localization.equivalence_from_model L W).inverse) ≪≫ category_theory.iso_whisker_left W.Q (category_theory.localization.equivalence_from_model L W).unit_iso.symm) ≪≫ W.Q.right_unitor
theorem
category_theory.localization.ess_surj
{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] :
def
category_theory.localization.whiskering_left_functor
{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] :
(D ⥤ E) ⥤ W.functors_inverting E
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
- category_theory.localization.whiskering_left_functor L W E = category_theory.full_subcategory.lift (λ (F : C ⥤ E), W.is_inverted_by F) ((category_theory.whiskering_left C D E).obj L) _
Instances for category_theory.localization.whiskering_left_functor
@[protected, instance]
noncomputable
def
category_theory.localization.whiskering_left_functor.category_theory.is_equivalence
{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] :
Equations
- category_theory.localization.whiskering_left_functor.category_theory.is_equivalence L W E = category_theory.is_equivalence.of_iso (category_theory.nat_iso.of_components (λ (F : D ⥤ E), category_theory.eq_to_iso _) _) (category_theory.is_equivalence.of_equivalence ((category_theory.localization.equivalence_from_model L W).symm.congr_left.trans (category_theory.localization.construction.whiskering_left_equivalence W E)))
noncomputable
def
category_theory.localization.functor_equivalence
{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] :
D ⥤ E ≌ W.functors_inverting E
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.
@[nolint]
def
category_theory.localization.whiskering_left_functor'
{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] :
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.whiskering_left_functor'_eq
{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] :
@[simp]
theorem
category_theory.localization.whiskering_left_functor'_obj
{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 : D ⥤ E) :
(category_theory.localization.whiskering_left_functor' L W E).obj F = L ⋙ F
@[protected, instance]
noncomputable
def
category_theory.localization.whiskering_left_functor'.category_theory.full
{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] :
@[protected, instance]
def
category_theory.localization.whiskering_left_functor'.category_theory.faithful
{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] :
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
- category_theory.localization.lift F hF L = (category_theory.localization.functor_equivalence L W E).inverse.obj {obj := F, property := hF}
Instances for category_theory.localization.lift
@[protected, instance]
noncomputable
def
category_theory.localization.lifting_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] :
Equations
@[simp]
theorem
category_theory.localization.fac_hom_app
{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]
(X : C) :
(category_theory.localization.fac F hF L).hom.app X = (category_theory.eq_to_hom _).app X ≫ (category_theory.is_equivalence.counit_iso.hom.app {obj := F, property := hF}).app X
noncomputable
def
category_theory.localization.fac
{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] :
L ⋙ category_theory.localization.lift F hF L ≅ F
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
@[simp]
theorem
category_theory.localization.fac_inv_app
{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]
(X : C) :
(category_theory.localization.fac F hF L).inv.app X = (category_theory.is_equivalence.counit_iso.inv.app {obj := F, property := hF}).app X ≫ (category_theory.eq_to_hom _).app X
@[protected, instance]
noncomputable
def
category_theory.localization.lifting_construction_lift
{C : Type u_1}
{D : Type u_2}
[category_theory.category C]
[category_theory.category D]
{W : category_theory.morphism_property C}
(F : C ⥤ D)
(hF : W.is_inverted_by F) :
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
- category_theory.localization.lift_nat_trans L W F₁ F₂ F₁' F₂' τ = (category_theory.localization.whiskering_left_functor' L W E).preimage ((category_theory.localization.lifting.iso L W F₁ F₁').hom ≫ τ ≫ (category_theory.localization.lifting.iso L W F₂ F₂').inv)
@[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) :
(category_theory.localization.lift_nat_trans L W F₁ F₂ F₁' F₂' τ).app (L.obj X) = (category_theory.localization.lifting.iso L W F₁ F₁').hom.app X ≫ τ.app X ≫ (category_theory.localization.lifting.iso L W F₂ F₂').inv.app X
@[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'
@[simp]
theorem
category_theory.localization.lift_nat_trans_id
{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)
[h : category_theory.localization.lifting L W F F'] :
category_theory.localization.lift_nat_trans L W F 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
- 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, inv := category_theory.localization.lift_nat_trans L W F₂ F₁ F₂' F₁' e.inv, hom_inv_id' := _, inv_hom_id' := _}
@[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
@[simp]
theorem
category_theory.localization.lifting.comp_right_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]
{E' : Type u_7}
[category_theory.category E']
(F : C ⥤ E)
(F' : D ⥤ E)
[category_theory.localization.lifting L W F F']
(G : E ⥤ E') :
category_theory.localization.lifting.iso L W (F ⋙ G) (F' ⋙ G) = category_theory.iso_whisker_right (category_theory.localization.lifting.iso L W F F') G
@[protected, instance]
def
category_theory.localization.lifting.comp_right
{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]
{E' : Type u_7}
[category_theory.category E']
(F : C ⥤ E)
(F' : D ⥤ E)
[category_theory.localization.lifting L W F F']
(G : E ⥤ E') :
category_theory.localization.lifting L W (F ⋙ G) (F' ⋙ G)
Equations
- category_theory.localization.lifting.comp_right L W F F' G = {iso := category_theory.iso_whisker_right (category_theory.localization.lifting.iso L W F F') G}
@[protected, instance]
def
category_theory.localization.lifting.id
{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] :
category_theory.localization.lifting L W L (𝟭 D)
Equations
@[simp]
theorem
category_theory.localization.lifting.id_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)
[L.is_localization W] :
category_theory.localization.lifting.iso L W L (𝟭 D) = L.right_unitor
@[simp]
theorem
category_theory.localization.lifting.of_isos_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}
(e : F₁ ≅ F₂)
(e' : F₁' ≅ F₂')
[category_theory.localization.lifting L W F₁ F₁'] :
category_theory.localization.lifting.iso L W F₂ F₂' = category_theory.iso_whisker_left L e'.symm ≪≫ category_theory.localization.lifting.iso L W F₁ F₁' ≪≫ e
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₁'] :
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
- category_theory.localization.lifting.of_isos L W e e' = {iso := category_theory.iso_whisker_left L e'.symm ≪≫ category_theory.localization.lifting.iso L W F₁ F₁' ≪≫ e}
theorem
category_theory.functor.is_localization.of_iso
{C : Type u_1}
{D : Type u_2}
[category_theory.category C]
[category_theory.category D]
(W : category_theory.morphism_property C)
{L₁ L₂ : C ⥤ D}
(e : L₁ ≅ L₂)
[L₁.is_localization W] :
L₂.is_localization W
theorem
category_theory.functor.is_localization.of_equivalence_target
{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' : C ⥤ E)
(eq : D ≌ E)
[L.is_localization W]
(e : L ⋙ eq.functor ≅ L') :
L'.is_localization W
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.