CategoryTheory.MorphismProperty.StableUnderBaseChange.fst
theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.fst :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C},
P.StableUnderBaseChange →
∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst_1 : CategoryTheory.Limits.HasPullback f g],
P g → P CategoryTheory.Limits.pullback.fst
This theorem states that for any category `C`, if a property `P` of morphisms in `C` is stable under base change, then for any objects `X`, `Y`, and `S` in `C`, and morphisms `f : X ⟶ S` and `g : Y ⟶ S` that have a pullback, if `P` holds for the morphism `g`, then it also holds for the first projection of the pullback of `f` and `g`. In terms of category theory, this means that the property of morphisms being examined is preserved under the operation of forming pullbacks and projecting onto the first factor.
More concisely: If a property of morphisms in a category is stable under base change, then for any morphisms with a pullback and having the property, the first projection of their pullback also possesses the property.
|
CategoryTheory.MorphismProperty.StableUnderBaseChange.snd
theorem CategoryTheory.MorphismProperty.StableUnderBaseChange.snd :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C},
P.StableUnderBaseChange →
∀ {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst_1 : CategoryTheory.Limits.HasPullback f g],
P f → P CategoryTheory.Limits.pullback.snd
This theorem states that, given a category `C` and a morphism property `P` on `C` which is stable under base change, for any three objects `X`, `Y`, and `S` in `C` and two morphisms `f : X ⟶ S` and `g : Y ⟶ S` such that a pullback of `f` and `g` exists, if morphism `f` has the property `P`, then the second projection of the pullback (denoted `CategoryTheory.Limits.pullback.snd`) also has the property `P`. In other words, the property `P` is preserved in the pullback operation.
More concisely: If `C` is a category, `P` is a stable under base change morphism property on `C`, and `f : X ⟶ S` and `g : Y ⟶ S` are morphisms in `C` with a pullback, then if `f` has property `P`, so does the second projection of the pullback of `f` and `g`.
|