CategoryTheory.Functor.IsLocalization.of_equivalence_target
theorem CategoryTheory.Functor.IsLocalization.of_equivalence_target :
∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_6, u_1} C]
[inst_1 : CategoryTheory.Category.{u_7, u_2} D] (L : CategoryTheory.Functor C D)
(W : CategoryTheory.MorphismProperty C) {E : Type u_4} [inst_2 : CategoryTheory.Category.{u_5, u_4} E]
(L' : CategoryTheory.Functor C E) (eq : D ≌ E) [inst_3 : L.IsLocalization W],
(L.comp eq.functor ≅ L') → L'.IsLocalization W
The theorem `CategoryTheory.Functor.IsLocalization.of_equivalence_target` states that if a functor `L : C ⥤ D` is a localization for a MorphismProperty `W` in a category `C`, then this property also holds for a functor obtained by post-composing `L` with an equivalence of categories, provided that the composition of `L` and this equivalence functor is naturally isomorphic to another functor `L' : C ⥤ E`. In other words, if `L` has a certain localization property with respect to `W`, this property is preserved when we map the category `D` to another category `E` via an equivalence of categories.
More concisely: If functor `L : C -> D` is a localization for property `W` in category `C`, and there exists an equivalence of categories `F : D -> E` such that `L` is naturally isomorphic to `L' : C -> E`, then `L'` also localizes `W`.
|
CategoryTheory.Functor.IsLocalization.inverts
theorem CategoryTheory.Functor.IsLocalization.inverts :
∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_4, u_1} C]
[inst_1 : CategoryTheory.Category.{u_5, u_2} D] {L : CategoryTheory.Functor C D}
{W : CategoryTheory.MorphismProperty C} [self : L.IsLocalization W], W.IsInvertedBy L
The theorem `CategoryTheory.Functor.IsLocalization.inverts` states that, given a category `C`, another category `D`, a functor `L` from `C` to `D`, and a `MorphismProperty` `W` in `C`, if `L` is an instance of localization with respect to `W`, then the functor `L` inverts the morphism property `W`. In other words, for every morphism in `C` that has the property `W`, there exists a morphism in `D` which is its inverse under the action of the functor `L`.
More concisely: Given a functor `L` from category `C` to category `D` that is a localization with respect to morphism property `W` in `C`, every morphism in `C` with property `W` has an inverse in `D` under the action of `L`.
|
CategoryTheory.Functor.IsLocalization.nonempty_isEquivalence
theorem CategoryTheory.Functor.IsLocalization.nonempty_isEquivalence :
∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_4, u_1} C]
[inst_1 : CategoryTheory.Category.{u_5, u_2} D] {L : CategoryTheory.Functor C D}
{W : CategoryTheory.MorphismProperty C} [self : L.IsLocalization W],
Nonempty (CategoryTheory.Localization.Construction.lift L ⋯).IsEquivalence
The theorem `CategoryTheory.Functor.IsLocalization.nonempty_isEquivalence` states that for any categories `C` and `D`, given a functor `L` from `C` to `D` and a class of morphisms `W` in `C`, if `L` is a localization with respect to `W`, then there exists an equivalence of categories between the localizations of `C` and `D` constructed via `L`. In layman's terms, the localized category constructed by functor `L` is equivalent to the original category.
More concisely: If functor `L` from category `C` to category `D` is a localization with respect to morphisms `W` in `C`, then the localizations of `C` and `D` constructed via `L` are equivalent categories.
|
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.inverts
theorem CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.inverts :
∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_4, u_1} C]
[inst_1 : CategoryTheory.Category.{u_5, u_2} D] {L : CategoryTheory.Functor C D}
{W : CategoryTheory.MorphismProperty C} {E : Type u_3} [inst_2 : CategoryTheory.Category.{u_6, u_3} E],
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L W E → W.IsInvertedBy L
The theorem `CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.inverts` states that for any categories `C`, `D`, and `E`, given a functor `L` from `C` to `D`, and a `MorphismProperty` `W` on `C`, if `L` satisfies the strict universal property with fixed target for `W` and `E`, then `L` inverts `W`. In simpler terms, this says that if any morphism in `C` that has the property `W` can be lifted through `L` to a morphism in `E` in a unique way, then `L` necessarily "inverts" `W`, i.e., it transforms any morphism with the property `W` into an isomorphism in `D`.
More concisely: If a functor `L` from category `C` to category `D` satisfies the strict universal property with fixed target for a morphism property `W` on `C` and a category `E`, then `L` inverts `W`, i.e., `L(w)` is an isomorphism in `D` for every `w` in `C` with property `W`.
|
CategoryTheory.Functor.IsLocalization.mk'
theorem CategoryTheory.Functor.IsLocalization.mk' :
∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_4, u_1} C]
[inst_1 : CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D)
(W : CategoryTheory.MorphismProperty C),
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L W D →
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L W W.Localization → L.IsLocalization W
This theorem states that for any two types `C` and `D`, which have category structures, and a functor `L` from `C` to `D`, together with the morphism property `W` on `C`, if `L` satisfies the strict universal property with fixed target `D` and `W`, and also the strict universal property with fixed target being the localization of `W`, then `L` is an isomorphism on the localization of `W`, i.e., `L` is a localization functor.
In simpler terms, this theorem provides a criterion to determine when a functor is a localization functor. It says that a functor is a localization functor if it preserves certain morphism properties and is universal in a certain sense.
More concisely: A functor between two categorically structured types with given morphism property is a localization functor if it strictly preserves the universal property with respect to that property and its localization.
|
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.fac
theorem CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.fac :
∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_4, u_1} C]
[inst_1 : CategoryTheory.Category.{u_5, u_2} D] {L : CategoryTheory.Functor C D}
{W : CategoryTheory.MorphismProperty C} {E : Type u_3} [inst_2 : CategoryTheory.Category.{u_6, u_3} E]
(self : CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L W E) (F : CategoryTheory.Functor C E)
(hF : W.IsInvertedBy F), L.comp (self.lift F hF) = F
The theorem `CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.fac` states that for any two categories `C` and `D`, given a functor `L` from `C` to `D`, a MorphismProperty `W` in `C`, and a category `E`, if we have a functor `F` from `C` to `E` such that `W` is inverted by `F`, then the composition of functor `L` with the lifting of functor `F` using the strict universal property for the fixed target localization is equal to `F`. In other words, this theorem establishes the strict universal property of the fixed target localization in Category Theory.
More concisely: Given functors F : C -> E and L : C -> D, if W is a MorphismProperty in C inverted by L and F preserves W, then L o (lifting of F to L-localization) = F.
|
CategoryTheory.Localization.inverts
theorem CategoryTheory.Localization.inverts :
∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_4, u_1} C]
[inst_1 : CategoryTheory.Category.{u_5, u_2} D] (L : CategoryTheory.Functor C D)
(W : CategoryTheory.MorphismProperty C) [inst_2 : L.IsLocalization W], W.IsInvertedBy L
The theorem `CategoryTheory.Localization.inverts` states that for any category `C` and `D`, a functor `L` from `C` to `D`, and a morphism property `W` in `C`, if the functor `L` is a localization of `W`, then all morphisms in `W` are mapped to isomorphisms in `D` by `L`. In other words, if `L` is a localization of `W`, then `W` is inverted by `L`.
More concisely: If functor `L` is a localization of morphism property `W` in category `C`, then for any morphism `f` in `W`, `L(f)` is an isomorphism in category `D`.
|
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.uniq
theorem CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.uniq :
∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_4, u_1} C]
[inst_1 : CategoryTheory.Category.{u_5, u_2} D] {L : CategoryTheory.Functor C D}
{W : CategoryTheory.MorphismProperty C} {E : Type u_3} [inst_2 : CategoryTheory.Category.{u_6, u_3} E],
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget L W E →
∀ (F₁ F₂ : CategoryTheory.Functor D E), L.comp F₁ = L.comp F₂ → F₁ = F₂
This theorem, the "uniqueness of the lifted functor", states that for any categories `C`, `D`, and `E`, a functor `L` from `C` to `D`, and a MorphismProperty `W` of `C`, if `L` satisfies the strict universal property with a fixed target `E`, then for any two functors `F1` and `F2` from `D` to `E`, if the composition of `L` and `F1` equals the composition of `L` and `F2`, then `F1` must equal `F2`. In other words, given the strict universal property, the functor `L` composed with any functor from `D` to `E` determines that functor uniquely.
More concisely: Given categories `C`, `D`, `E`, a functor `L: C -> D`, a MorphismProperty `W` of `C`, and functors `F1, F2: D -> E`, if `L` satisfies the strict universal property for `W` and `L ∘ F1 = L ∘ F2`, then `F1 = F2`.
|