Base changes of base changes

Let P be a property of morphisms stable under base change. If the base change pullback.snd f k of f along k has P, then so does every further base change of f along a morphism factoring through k: this file records the forms of this used when reducing a property of morphisms of schemes to an affine base. Mathlib's MorphismProperty.pullback_snd is the case where f itself has P.

Main results

• CategoryTheory.MorphismProperty.pullback_snd_comp: P (pullback.snd f k) implies P (pullback.snd f (e ≫ k)); pullback_snd_of_comp_eq is the same for a morphism equal to e ≫ k.
• CategoryTheory.MorphismProperty.pullback_snd_pullback_fst_comp: the base change of f along Y ×_S T ⟶ Y passes its property to the base change along Y ×_S T' ⟶ Y for any T' ⟶ T.
• CategoryTheory.MorphismProperty.pullback_snd_pullback_snd: P (pullback.snd f k) implies P (pullback.snd (pullback.snd f v) a) whenever a ≫ v factors through k.
• CategoryTheory.MorphismProperty.pullback_snd_comp_left: if P is moreover stable under composition, P e and P (pullback.snd f k) imply P (pullback.snd (e ≫ f) k).

theorem CategoryTheory.MorphismProperty.pullback_snd_comp {C : Type u_1} [Category.{v_1, u_1} C] {P : MorphismProperty C} [P.IsStableUnderBaseChange] {X Y W W' : C} (f : X ⟶ Y) (k : W ⟶ Y) (e : W' ⟶ W) [Limits.HasPullback f k] [Limits.HasPullback f (CategoryStruct.comp e k)] (h : P (Limits.pullback.snd f k)) : P (Limits.pullback.snd f (CategoryStruct.comp e k))

A base change of pullback.snd f k along e is the base change of f along e ≫ k, so it inherits every property stable under base change.

theorem CategoryTheory.MorphismProperty.pullback_snd_of_comp_eq {C : Type u_1} [Category.{v_1, u_1} C] {P : MorphismProperty C} [P.IsStableUnderBaseChange] {X Y W W' : C} (f : X ⟶ Y) (k : W ⟶ Y) (e : W' ⟶ W) {a : W' ⟶ Y} [Limits.HasPullback f k] [Limits.HasPullback f a] (hfac : CategoryStruct.comp e k = a) (h : P (Limits.pullback.snd f k)) : P (Limits.pullback.snd f a)

A form of pullback_snd_comp for a morphism a known to factor as e ≫ k. Its conclusion does not mention the composite, so it can be applied where rewriting with the factorisation inside pullback is not possible.

theorem CategoryTheory.MorphismProperty.pullback_snd_pullback_fst_comp {C : Type u_1} [Category.{v_1, u_1} C] {P : MorphismProperty C} [P.IsStableUnderBaseChange] {X Y S T T' : C} (f : X ⟶ Y) (g : Y ⟶ S) (r : T ⟶ S) (t : T' ⟶ T) [Limits.HasPullback g r] [Limits.HasPullback g (CategoryStruct.comp t r)] [Limits.HasPullback f (Limits.pullback.fst g r)] [Limits.HasPullback f (Limits.pullback.fst g (CategoryStruct.comp t r))] (h : P (Limits.pullback.snd f (Limits.pullback.fst g r))) : P (Limits.pullback.snd f (Limits.pullback.fst g (CategoryStruct.comp t r)))

If the base change of f along Y ×_S T ⟶ Y has P, then so does its base change along Y ×_S T' ⟶ Y for every t : T' ⟶ T, since the latter factors through the former.

theorem CategoryTheory.MorphismProperty.pullback_snd_pullback_snd {C : Type u_1} [Category.{v_1, u_1} C] {P : MorphismProperty C} [P.IsStableUnderBaseChange] {X Y W Y' T : C} (f : X ⟶ Y) (v : Y' ⟶ Y) (a : T ⟶ Y') (k : W ⟶ Y) (e : T ⟶ W) [Limits.HasPullback f v] [Limits.HasPullback (Limits.pullback.snd f v) a] [Limits.HasPullback f k] (hfac : CategoryStruct.comp a v = CategoryStruct.comp e k) (h : P (Limits.pullback.snd f k)) : P (Limits.pullback.snd (Limits.pullback.snd f v) a)

If a ≫ v factors as e ≫ k, then the base change of pullback.snd f v along a inherits from pullback.snd f k every property stable under base change.

theorem CategoryTheory.MorphismProperty.pullback_snd_comp_left {C : Type u_1} [Category.{v_1, u_1} C] {P : MorphismProperty C} [P.IsStableUnderBaseChange] {X Y W : C} [P.IsStableUnderComposition] {X' : C} (f : X ⟶ Y) (k : W ⟶ Y) (e : X' ⟶ X) [Limits.HasPullback f k] [Limits.HasPullback (CategoryStruct.comp e f) k] (he : P e) (h : P (Limits.pullback.snd f k)) : P (Limits.pullback.snd (CategoryStruct.comp e f) k)

For a property stable under base change and composition, precomposing f with a morphism having the property keeps the property of pullback.snd f k.