CategoryTheory.MorphismProperty.RespectsIso.cancel_left_isIso
theorem CategoryTheory.MorphismProperty.RespectsIso.cancel_left_isIso :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C},
P.RespectsIso →
∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [inst_1 : CategoryTheory.IsIso f],
P (CategoryTheory.CategoryStruct.comp f g) ↔ P g
The theorem `CategoryTheory.MorphismProperty.RespectsIso.cancel_left_isIso` states that for any category `C` and any morphism property `P` that respects isomorphisms, for any objects `X`, `Y`, and `Z` in `C` and any morphisms `f` from `X` to `Y` and `g` from `Y` to `Z`, where `f` is an isomorphism, the property `P` holds for the composition of `f` and `g` if and only if `P` holds for `g`. In other words, if `P` respects isomorphisms, then the property `P` of a composition of an isomorphism and another morphism can be "cancelled" to just the property of the latter morphism.
More concisely: For any category, morphism property respecting isomorphisms, and composable morphisms where the first is an isomorphism, the morphism property holds for their composition if and only if it holds for the right morphism.
|
CategoryTheory.MorphismProperty.RespectsIso.epimorphisms
theorem CategoryTheory.MorphismProperty.RespectsIso.epimorphisms :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
(CategoryTheory.MorphismProperty.epimorphisms C).RespectsIso
This theorem states that in any category `C`, the property of being an epimorphism (a morphism such that any two morphisms that compose with it to equal morphisms are themselves equal) is preserved under composition with isomorphisms. More specifically, if a morphism `f` is an epimorphism, then for any isomorphism `e`, the morphisms obtained by composing `e` and `f` either on the left or on the right are also epimorphisms.
More concisely: In any category, if a morphism is an epimorphism, then so is its composition with any isomorphism.
|
CategoryTheory.MorphismProperty.RespectsIso.cancel_right_isIso
theorem CategoryTheory.MorphismProperty.RespectsIso.cancel_right_isIso :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C},
P.RespectsIso →
∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [inst_1 : CategoryTheory.IsIso g],
P (CategoryTheory.CategoryStruct.comp f g) ↔ P f
The theorem `CategoryTheory.MorphismProperty.RespectsIso.cancel_right_isIso` states that for any category `C` and a morphism property `P` that respects isomorphisms, given three objects `X`, `Y`, and `Z` in `C` and two morphisms `f : X ⟶ Y` and `g : Y ⟶ Z` where `g` is an isomorphism, the property `P` holds for the composition `f ≫ g` if and only if `P` holds for `f`. In other words, if we have a property of morphisms that is preserved under post-composition with an isomorphism, then testing that property on a composition is equivalent to testing it on the first morphism in the composition where the second morphism is an isomorphism.
More concisely: For any category C and morphism property P respecting isomorphisms, if isomorphism g : Y ⟶ Z and morphisms f : X ⟶ Y and f ≫ g hold property P, then f also holds property P.
|
CategoryTheory.MorphismProperty.map_respectsIso
theorem CategoryTheory.MorphismProperty.map_respectsIso :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1}
[inst_1 : CategoryTheory.Category.{u_2, u_1} D] (P : CategoryTheory.MorphismProperty C)
(F : CategoryTheory.Functor C D), (P.map F).RespectsIso
The theorem `CategoryTheory.MorphismProperty.map_respectsIso` states that for any categories `C` and `D`, given a morphism property `P` on `C` and a functor `F` from `C` to `D`, the property `P` mapped to `D` by the functor `F` respects isomorphisms. In other words, if a morphism in `D` is obtained by applying the functor `F` on a morphism in `C` that satisfies property `P`, and it is composed with an isomorphism, then the resulting morphism still satisfies the mapped property. This theorem is important in category theory as it ensures that certain properties of morphisms are preserved under functors when dealing with isomorphisms.
More concisely: If `F : C -> D` is a functor, `P : Pproperty C` is a morphism property on `C`, and `f : C -> Ob D` is a morphism in `C` with `P f`, then for any isomorphism `g : Ob D -> Ob D`, `P (F g . F) f` holds.
|
CategoryTheory.MorphismProperty.RespectsIso.isomorphisms
theorem CategoryTheory.MorphismProperty.RespectsIso.isomorphisms :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
(CategoryTheory.MorphismProperty.isomorphisms C).RespectsIso
The theorem `CategoryTheory.MorphismProperty.RespectsIso.isomorphisms` states that for any type `C` that forms a category, the property of being an isomorphism is preserved when composed with an isomorphism. In other words, if a morphism in the category `C` is an isomorphism, then its composition with any isomorphism (either on the left or on the right) also has the property of being an isomorphism.
More concisely: In any category, the composition of an isomorphism with another isomorphism is an isomorphism.
|
CategoryTheory.MorphismProperty.map_mem_map
theorem CategoryTheory.MorphismProperty.map_mem_map :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1}
[inst_1 : CategoryTheory.Category.{u_2, u_1} D] (P : CategoryTheory.MorphismProperty C)
(F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y), P f → P.map F (F.map f)
This theorem is a statement about morphism properties and functors in category theory. It says that for any category `C`, any morphism property `P` on `C`, any functor `F` from `C` to some category `D`, and any morphism `f` from `X` to `Y` in `C`, if `f` has property `P`, then the image of `f` under the functor `F` also has the property `P` when it is considered in the category `D`. In other words, if a morphism in the source category has some property, then its image under a functor into the target category also has that property, where the property is being appropriately transformed along with the morphism by the functor.
More concisely: For any category `C`, functor `F` from `C` to a category `D`, morphism property `P`, and morphism `f` in `C`, if `f` has property `P`, then `F(f)` has property `P` in `D`.
|
CategoryTheory.MorphismProperty.map_map
theorem CategoryTheory.MorphismProperty.map_map :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1}
[inst_1 : CategoryTheory.Category.{u_3, u_1} D] (P : CategoryTheory.MorphismProperty C)
(F : CategoryTheory.Functor C D) {E : Type u_2} [inst_2 : CategoryTheory.Category.{u_4, u_2} E]
(G : CategoryTheory.Functor D E), (P.map F).map G = P.map (F.comp G)
The theorem `CategoryTheory.MorphismProperty.map_map` states that for any two categories `C` and `D`, and any property `P` of morphisms in `C`, if we first apply a functor `F` from `C` to `D` to `P`, obtaining a property of morphisms in `D`, and then apply a functor `G` from `D` to a third category `E`, the result is the same as if we had first formed the composite functor `F ∘ G` from `C` to `E` and then applied it to `P`. This is essentially a statement about the commutativity of the process of applying functors to morphism properties.
More concisely: For any categories C, D, E, functors F : C -> D and G : D -> E, and property P of morphisms in C, the composition of functors F and G preserves the property P, i.e., (F ∘ G)(P) = F(G(P)).
|
CategoryTheory.MorphismProperty.inverseImage_equivalence_inverse_eq_map_functor
theorem CategoryTheory.MorphismProperty.inverseImage_equivalence_inverse_eq_map_functor :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1}
[inst_1 : CategoryTheory.Category.{u_2, u_1} D] (P : CategoryTheory.MorphismProperty D),
P.RespectsIso → ∀ (E : C ≌ D), P.inverseImage E.functor = P.map E.inverse
This theorem states that, for any two categories `C` and `D`, and for a property `P` that applies to morphisms in `D` and respects isomorphisms, the inverse image of the property `P` under the functor from `C` to `D` is the same as the image of the property `P` under the inverse of the equivalence from `C` to `D`. In other words, under the conditions of this theorem, taking the inverse image with respect to a functor and taking the image with respect to the inverse functor yield the same morphism property in `C`.
More concisely: For any functors F : C -> D and G : D -> C between categories, and property P on D that is invariant under isomorphism, the inverse image of P under F is equal to the image of P under G^(-1).
|
CategoryTheory.MorphismProperty.RespectsIso.isoClosure_eq
theorem CategoryTheory.MorphismProperty.RespectsIso.isoClosure_eq :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C},
P.RespectsIso → P.isoClosure = P
The theorem `CategoryTheory.MorphismProperty.RespectsIso.isoClosure_eq` states that for any `MorphismProperty` P in a category C, if P respects isomorphisms (meaning that if a morphism has property P, then composing that morphism with any isomorphism will still result in a morphism with property P), then the "closure by isomorphisms" of P is P itself. The "closure by isomorphisms" of a property P is the property where a morphism f has the property if there exist some other morphisms and an isomorphism between f and another morphism that has property P.
More concisely: If a morphism property P in a category respects isomorphisms, then the closure of P by isomorphisms equals P.
|
CategoryTheory.MorphismProperty.RespectsIso.of_respects_arrow_iso
theorem CategoryTheory.MorphismProperty.RespectsIso.of_respects_arrow_iso :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C),
(∀ (f g : CategoryTheory.Arrow C), (f ≅ g) → P f.hom → P g.hom) → P.RespectsIso
The theorem `CategoryTheory.MorphismProperty.RespectsIso.of_respects_arrow_iso` states that for any category `C` and any morphism property `P` in `C`, if for every pair of objects `f` and `g` in the arrow category of `C`, the property `P` is preserved under isomorphism (that is, whenever `f` is isomorphic to `g`, the property `P` holding for the homomorphism of `f` implies that it also holds for the homomorphism of `g`), then the morphism property `P` respects isomorphisms in the original category `C`. In other words, if a property of morphisms holds when we move to isomorphic objects in the arrow category, then it will also hold when we compose with isomorphisms in the original category.
More concisely: If a morphism property in a category is preserved under isomorphisms in the arrow category, then it is a morphism property in the original category.
|
CategoryTheory.MorphismProperty.RespectsIso.monomorphisms
theorem CategoryTheory.MorphismProperty.RespectsIso.monomorphisms :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
(CategoryTheory.MorphismProperty.monomorphisms C).RespectsIso
This theorem states that in any category `C`, the property of being a monomorphism is preserved under composition with an isomorphism. More concretely, if we have morphisms in `C` such that one is a monomorphism and the other is an isomorphism, the composition of these two morphisms (in any order) is also a monomorphism. This result is a fundamental property in category theory that connects the concepts of monomorphisms and isomorphisms.
More concisely: In any category, the composition of a monomorphism and an isomorphism is a monomorphism.
|
CategoryTheory.MorphismProperty.RespectsIso.arrow_mk_iso_iff
theorem CategoryTheory.MorphismProperty.RespectsIso.arrow_mk_iso_iff :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C},
P.RespectsIso →
∀ {W X Y Z : C} {f : W ⟶ X} {g : Y ⟶ Z},
(CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g) → (P f ↔ P g)
This theorem states that for any category `C` and a morphism property `P` that respects isomorphisms, if we have four objects `W`, `X`, `Y`, and `Z` in `C` and two morphisms `f: W ⟶ X` and `g: Y ⟶ Z`, then if the arrows created by `f` and `g` (i.e., `CategoryTheory.Arrow.mk f` and `CategoryTheory.Arrow.mk g`) are isomorphic, then `P f` holds if and only if `P g` holds. In other words, if `f` and `g` give rise to isomorphic objects in the arrow category, then `f` and `g` either both have the property `P` or both do not have the property `P`.
More concisely: If morphisms `f: W ⟶ X` and `g: Y ⟶ Z` in a category `C` with isomorphism-respecting property `P` have isomorphic arrows, then `P(f)` if and only if `P(g)`.
|