CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.of_isLocalization_of_isLocalization
theorem CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.of_isLocalization_of_isLocalization :
∀ {C₁ : Type u₁} {C₂ : Type u₂} {D₂ : Type u₅} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
[inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₆, u₅} D₂]
{W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂}
(Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₂ : CategoryTheory.Functor C₂ D₂) [inst_3 : L₂.IsLocalization W₂]
[inst_4 : (Φ.functor.comp L₂).IsLocalization W₁], Φ.IsLocalizedEquivalence
The theorem `CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.of_isLocalization_of_isLocalization` states that for any two types `C₁` and `C₂` representing categories and another type `D₂`, also representing a category, if we have a `LocalizerMorphism` `Φ` from a morphism property `W₁` to a morphism property `W₂`, and a functor `L₂` from `C₂` to `D₂` such that `L₂` is a localization for `W₂` and the composition of `Φ.functor` and `L₂` is also a localization for `W₁`, then `Φ` is a localized equivalence. In other words, if the composition of a localizer morphism and a functor provides a localization, then the localizer morphism itself can be considered as a localized equivalence under the given conditions.
More concisely: If a Localizer Morphism Φ from morphism property W₁ to W₂ together with a functor L₂ from category C₂ to D₂ satisfy Φ.functor \* L₂ being a localization for W₁, then Φ is a localized equivalence between C₁ and C₂.
|
CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.of_equivalence
theorem CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.of_equivalence :
∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
[inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
[inst_2 : Φ.functor.IsEquivalence], W₂ ≤ W₁.map Φ.functor → Φ.IsLocalizedEquivalence
This theorem states that, given two types `C₁` and `C₂` with category structures, and morphism properties `W₁` and `W₂` on these categories respectively, if we have a localizer morphism (`Φ : CategoryTheory.LocalizerMorphism W₁ W₂`) whose underlying functor (`Φ.functor`) is an equivalence of categories, and `W₁` and `W₂` essentially correspond to each other via this equivalence (meaning `W₂` is a subset of `W₁` mapped by `Φ.functor`), then `Φ` is a localized equivalence. This theorem bridges the abstract concept of an equivalence of categories with the concrete concept of a localized equivalence.
More concisely: Given localizer morphisms `Φ : C₁ → C₂` between categories with essential surjective underlying functors, if `Φ.functor` is an equivalence of categories and `W₂ ⊆ W₁` with `Φ.functor W₁ = W₂`, then `Φ` is a localized equivalence.
|
CategoryTheory.LocalizerMorphism.map
theorem CategoryTheory.LocalizerMorphism.map :
∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
[inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂} (self : CategoryTheory.LocalizerMorphism W₁ W₂),
W₁ ≤ W₂.inverseImage self.functor
The theorem `CategoryTheory.LocalizerMorphism.map` states that for any two categories `C₁` and `C₂` and morphism properties `W₁` in `C₁` and `W₂` in `C₂`, a given `LocalizerMorphism` between `W₁` and `W₂` ensures that the `functor` is compatible with these morphism properties. In other words, any morphism in `C₁` that satisfies `W₁` is mapped by the `functor` to a morphism in `C₂` that satisfies `W₂`. This is formalized by the statement that `W₁` is a subset (or, less formally, "sits inside") of the inverse image of `W₂` under the functor associated with the `LocalizerMorphism`. In essence, this theorem asserts a type of commutativity property for the `LocalizerMorphism` with respect to the `MorphismProperty`.
More concisely: Given LocalizerMorphisms between morphism properties W₁ in category C₁ and W₂ in category C₂, the LocalizerMorphism maps morphisms satisfying W₁ to morphisms satisfying W₂, i.e., W₁ ⊆ (functor inverse-image W₂).
|
CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.nonempty_isEquivalence
theorem CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.nonempty_isEquivalence :
∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
[inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
{W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂}
[self : Φ.IsLocalizedEquivalence], Nonempty (Φ.localizedFunctor W₁.Q W₂.Q).IsEquivalence
The theorem `CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.nonempty_isEquivalence` states that for any two categories `C₁` and `C₂` with morphism properties `W₁` and `W₂` respectively, and a localizer morphism `Φ` between them, if `Φ` is an equivalence of localized categories, then there exists an equivalence of functors induced by `Φ` between the localizations of `C₁` and `C₂`. In other words, the process of localization does not prevent `Φ` from inducing an equivalence between the localized categories.
More concisely: Given categories `C₁` and `C₂` with morphism properties `W₁` and `W₂`, and a localizer morphism `Φ` between them that is an equivalence of localized categories, there exists an equivalence of functors induced by `Φ` between the localizations of `C₁` and `C₂`.
|