CategoryTheory.MorphismProperty.id_mem
theorem CategoryTheory.MorphismProperty.id_mem :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C)
[inst_1 : W.ContainsIdentities] (X : C), W (CategoryTheory.CategoryStruct.id X)
This theorem states that for any category `C` and for any `MorphismProperty` `W` that contains identity morphisms, the identity morphism of any object `X` in `C` is an element of `W`. In other words, if `W` is a property that all identity morphisms possess in the category `C`, then the identity morphism on any object `X` in `C` has the property `W`.
More concisely: In any category `C` and for any morphism property `W` containing identity morphisms, the identity morphism of every object `X` in `C` belongs to `W`.
|
CategoryTheory.MorphismProperty.comp_mem
theorem CategoryTheory.MorphismProperty.comp_mem :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C)
[inst_1 : W.IsStableUnderComposition] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z),
W f → W g → W (CategoryTheory.CategoryStruct.comp f g)
The theorem `CategoryTheory.MorphismProperty.comp_mem` states that for any given category `C`, if a property `W` holds for morphisms in `C`, and if `W` is multiplicative, then for any three objects `X`, `Y`, and `Z` in `C`, if `f` is a morphism from `X` to `Y` and `g` is a morphism from `Y` to `Z` such that both `f` and `g` have property `W`, then the composite morphism `f ≫ g` (from `X` to `Z` via `Y`) also has property `W`.
More concisely: If `C` is a category, `W` is a multiplicative property of morphisms in `C`, and `f : X → Y` and `g : Y → Z` are morphisms with property `W`, then their composite `f ≫ g : X → Z` also has property `W`.
|