CategoryTheory.Localization.Construction.fac
theorem CategoryTheory.Localization.Construction.fac :
∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C} {D : Type uD}
[inst_1 : CategoryTheory.Category.{uD', uD} D] (G : CategoryTheory.Functor C D) (hG : W.IsInvertedBy G),
W.Q.comp (CategoryTheory.Localization.Construction.lift G hG) = G
This theorem states that, given a category `C` with a morphism property `W` and another category `D`, if we have a functor `G` from `C` to `D` that inverts all morphisms in `W` (i.e., maps them to isomorphisms in `D`), then composing the functor `Q` associated with `W` with the localization lift of `G` (given by `CategoryTheory.Localization.Construction.lift G hG`) yields the original functor `G`. This localization construction is a key concept in category theory and this theorem formalizes one of its fundamental properties.
More concisely: Given a category `C` with a morphism property `W`, a functor `G: C -> D`, and a localization of `C` at `W`, the functor `Q` associated with `W` and the lift `lift G hG` commute, i.e., `Q ∘ lift G hG = G`.
|
CategoryTheory.Localization.Construction.morphismProperty_is_top
theorem CategoryTheory.Localization.Construction.morphismProperty_is_top :
∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C}
(P : CategoryTheory.MorphismProperty W.Localization) [inst_1 : P.IsStableUnderComposition],
(∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)) →
(∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (CategoryTheory.Localization.Construction.winv w hw)) → P = ⊤
The theorem `CategoryTheory.Localization.Construction.morphismProperty_is_top` states that for any category `C` and a `MorphismProperty` `W` in the localization of `C`, if we have a `MorphismProperty` `P` in the localization of `W` which is stable under composition, then `P` is satisfied by all morphisms in the localized category if it contains the image of the morphisms in the original category and the inverses of the morphisms in `W`. In other words, this theorem states that `P` is the top element (represented as `⊤`) in the set of all MorphismProperties, provided that it meets these conditions of containing image of original morphisms, their inverses and being stable under composition.
More concisely: In a category localization, a stable under composition MorphismProperty `P` that contains the images of morphisms from the original category and their inverses satisfies `P = ⊤`, the top element of MorphismProperties.
|
CategoryTheory.Localization.Construction.morphismProperty_is_top'
theorem CategoryTheory.Localization.Construction.morphismProperty_is_top' :
∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C}
(P : CategoryTheory.MorphismProperty W.Localization) [inst_1 : P.IsStableUnderComposition],
(∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)) → (∀ ⦃X Y : W.Localization⦄ (e : X ≅ Y), P e.hom → P e.inv) → P = ⊤
This theorem, `CategoryTheory.Localization.Construction.morphismProperty_is_top'`, is about the properties of morphisms in a localized category. It states that for any category `C` and any morphism property `P` in the localization of `C`, if `P` is stable under composition, and it contains the image of the morphisms in the original category `C`, and also if `P` is stable by passing to inverses, then `P` is equal to the top element, implying that `P` holds for all morphisms in the localized category.
In other words, all morphisms in the localized category satisfy a given property if this property holds for all images of morphisms from the original category, and this property is preserved under composition and inversion of morphisms.
More concisely: If a morphism property in a localized category is stable under composition, contains the images of morphisms from the original category, and is stable under taking inverses, then it holds for all morphisms in the localized category.
|