Base change of a fibre product

Let X ⟶ S and Y ⟶ S be two objects over S, and let X' ⟶ S' and Y' ⟶ S' be their base changes along f : S' ⟶ S. Then the fibre product X' ×_{S'} Y' is the base change of X ×_S Y along f, through the morphism pullback.map induced by X' ⟶ X and Y' ⟶ Y (CategoryTheory.IsPullback.pullback_map). In other words, base change preserves fibre products over the base. The canonical comparison isomorphism CategoryTheory.Limits.pullbackBaseChangeIso has explicit projection formulas and is natural in both objects over the base.

Fibre products over a common base also commute with each other: if T is the fibre product of T₁ and T₂ over S, and X that of X₁ and X₂, then T ×_S X is the fibre product of T₁ ×_S X₁ and T₂ ×_S X₂ over S, through the morphisms pullback.map induced by the projections (CategoryTheory.IsPullback.pullback_map_pullback_map). This is the middle-four interchange of fibre products, (T₁ ×_S T₂) ×_S (X₁ ×_S X₂) ≅ (T₁ ×_S X₁) ×_S (T₂ ×_S X₂).

The canonical identification of an iterated fibre product with a direct fibre product commutes with maps in the first factor (CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_naturality).

theorem CategoryTheory.IsPullback.pullback_map {C : Type u_1} [Category.{v_1, u_1} C] {S S' X Y X' Y' : C} {f : S' ⟶ S} {pX : X ⟶ S} {pY : Y ⟶ S} {pX' : X' ⟶ S'} {pY' : Y' ⟶ S'} {iX : X' ⟶ X} {iY : Y' ⟶ Y} [Limits.HasPullback pX pY] [Limits.HasPullback pX' pY'] (hX : IsPullback pX' iX f pX) (hY : IsPullback pY' iY f pY) : IsPullback (CategoryStruct.comp (Limits.pullback.fst pX' pY') pX') (Limits.pullback.map pX' pY' pX pY iX iY f ⋯ ⋯) f (CategoryStruct.comp (Limits.pullback.fst pX pY) pX)

Base change preserves fibre products. If X' ⟶ S' and Y' ⟶ S' are the base changes of X ⟶ S and Y ⟶ S along f : S' ⟶ S, then X' ×_{S'} Y', as an object over S', is the base change of X ×_S Y along f.

theorem CategoryTheory.IsPullback.pullback_map_pullback_map {C : Type u_1} [Category.{v_1, u_1} C] {S X T T₁ T₂ X₁ X₂ : C} {t : T ⟶ S} {t₁ : T₁ ⟶ S} {t₂ : T₂ ⟶ S} {x : X ⟶ S} {x₁ : X₁ ⟶ S} {x₂ : X₂ ⟶ S} {p₁ : T ⟶ T₁} {p₂ : T ⟶ T₂} {q₁ : X ⟶ X₁} {q₂ : X ⟶ X₂} [Limits.HasPullback t x] [Limits.HasPullback t₁ x₁] [Limits.HasPullback t₂ x₂] (hT : IsPullback p₁ p₂ t₁ t₂) (hX : IsPullback q₁ q₂ x₁ x₂) (ht₁ : CategoryStruct.comp p₁ t₁ = t) (hx₁ : CategoryStruct.comp q₁ x₁ = x) : IsPullback (Limits.pullback.map t x t₁ x₁ p₁ q₁ (CategoryStruct.id S) ⋯ ⋯) (Limits.pullback.map t x t₂ x₂ p₂ q₂ (CategoryStruct.id S) ⋯ ⋯) (CategoryStruct.comp (Limits.pullback.snd t₁ x₁) x₁) (CategoryStruct.comp (Limits.pullback.snd t₂ x₂) x₂)

Fibre products commute with fibre products. If T is the fibre product of T₁ and T₂ over S, and X is the fibre product of X₁ and X₂ over S, then T ×_S X is the fibre product of T₁ ×_S X₁ and T₂ ×_S X₂ over S, with the projections induced by those of T and X.

noncomputable def CategoryTheory.Limits.pullbackBaseChangeIso {C : Type u_1} [Category.{v_1, u_1} C] [HasPullbacks C] {X Y S S' : C} (f : X ⟶ S) (g : Y ⟶ S) (φ : S' ⟶ S) : pullback (CategoryStruct.comp (pullback.fst f g) f) φ ≅ pullback (pullback.snd f φ) (pullback.snd g φ)

Base change of a fibre product is the fibre product of the base changes, with both base-changed factors regarded as objects over S' through their second projections.

@[simp]

theorem CategoryTheory.Limits.pullbackBaseChangeIso_hom_fst {C : Type u_1} [Category.{v_1, u_1} C] [HasPullbacks C] {X Y S S' : C} (f : X ⟶ S) (g : Y ⟶ S) (φ : S' ⟶ S) : CategoryStruct.comp (pullbackBaseChangeIso f g φ).hom (pullback.fst (pullback.snd f φ) (pullback.snd g φ)) = pullback.map (CategoryStruct.comp (pullback.fst f g) f) φ f φ (pullback.fst f g) (CategoryStruct.id S') (CategoryStruct.id S) ⋯ ⋯

The first projection of the base-change comparison is the base change of the first projection.

@[simp]

theorem CategoryTheory.Limits.pullbackBaseChangeIso_hom_fst_assoc {C : Type u_1} [Category.{v_1, u_1} C] [HasPullbacks C] {X Y S S' : C} (f : X ⟶ S) (g : Y ⟶ S) (φ : S' ⟶ S) {Z : C} (h : pullback f φ ⟶ Z) : CategoryStruct.comp (pullbackBaseChangeIso f g φ).hom (CategoryStruct.comp (pullback.fst (pullback.snd f φ) (pullback.snd g φ)) h) = CategoryStruct.comp (pullback.map (CategoryStruct.comp (pullback.fst f g) f) φ f φ (pullback.fst f g) (CategoryStruct.id S') (CategoryStruct.id S) ⋯ ⋯) h

The first projection of the base-change comparison is the base change of the first projection.

@[simp]

theorem CategoryTheory.Limits.pullbackBaseChangeIso_hom_snd {C : Type u_1} [Category.{v_1, u_1} C] [HasPullbacks C] {X Y S S' : C} (f : X ⟶ S) (g : Y ⟶ S) (φ : S' ⟶ S) : CategoryStruct.comp (pullbackBaseChangeIso f g φ).hom (pullback.snd (pullback.snd f φ) (pullback.snd g φ)) = pullback.map (CategoryStruct.comp (pullback.fst f g) f) φ g φ (pullback.snd f g) (CategoryStruct.id S') (CategoryStruct.id S) ⋯ ⋯

The second projection of the base-change comparison is the base change of the second projection.

@[simp]

theorem CategoryTheory.Limits.pullbackBaseChangeIso_hom_snd_assoc {C : Type u_1} [Category.{v_1, u_1} C] [HasPullbacks C] {X Y S S' : C} (f : X ⟶ S) (g : Y ⟶ S) (φ : S' ⟶ S) {Z : C} (h : pullback g φ ⟶ Z) : CategoryStruct.comp (pullbackBaseChangeIso f g φ).hom (CategoryStruct.comp (pullback.snd (pullback.snd f φ) (pullback.snd g φ)) h) = CategoryStruct.comp (pullback.map (CategoryStruct.comp (pullback.fst f g) f) φ g φ (pullback.snd f g) (CategoryStruct.id S') (CategoryStruct.id S) ⋯ ⋯) h

The second projection of the base-change comparison is the base change of the second projection.

@[simp]

theorem CategoryTheory.Limits.pullbackBaseChangeIso_inv_fst {C : Type u_1} [Category.{v_1, u_1} C] [HasPullbacks C] {X Y S S' : C} (f : X ⟶ S) (g : Y ⟶ S) (φ : S' ⟶ S) : CategoryStruct.comp (pullbackBaseChangeIso f g φ).inv (pullback.fst (CategoryStruct.comp (pullback.fst f g) f) φ) = pullback.map (pullback.snd f φ) (pullback.snd g φ) f g (pullback.fst f φ) (pullback.fst g φ) φ ⋯ ⋯

The inverse base-change comparison projects to the original fibre product by the projections from both base changes.

@[simp]

theorem CategoryTheory.Limits.pullbackBaseChangeIso_inv_fst_assoc {C : Type u_1} [Category.{v_1, u_1} C] [HasPullbacks C] {X Y S S' : C} (f : X ⟶ S) (g : Y ⟶ S) (φ : S' ⟶ S) {Z : C} (h : pullback f g ⟶ Z) : CategoryStruct.comp (pullbackBaseChangeIso f g φ).inv (CategoryStruct.comp (pullback.fst (CategoryStruct.comp (pullback.fst f g) f) φ) h) = CategoryStruct.comp (pullback.map (pullback.snd f φ) (pullback.snd g φ) f g (pullback.fst f φ) (pullback.fst g φ) φ ⋯ ⋯) h

The inverse base-change comparison projects to the original fibre product by the projections from both base changes.

@[simp]

theorem CategoryTheory.Limits.pullbackBaseChangeIso_inv_snd {C : Type u_1} [Category.{v_1, u_1} C] [HasPullbacks C] {X Y S S' : C} (f : X ⟶ S) (g : Y ⟶ S) (φ : S' ⟶ S) : CategoryStruct.comp (pullbackBaseChangeIso f g φ).inv (pullback.snd (CategoryStruct.comp (pullback.fst f g) f) φ) = CategoryStruct.comp (pullback.fst (pullback.snd f φ) (pullback.snd g φ)) (pullback.snd f φ)

The base-change comparison is an isomorphism over the new base.

@[simp]

theorem CategoryTheory.Limits.pullbackBaseChangeIso_inv_snd_assoc {C : Type u_1} [Category.{v_1, u_1} C] [HasPullbacks C] {X Y S S' : C} (f : X ⟶ S) (g : Y ⟶ S) (φ : S' ⟶ S) {Z : C} (h : S' ⟶ Z) : CategoryStruct.comp (pullbackBaseChangeIso f g φ).inv (CategoryStruct.comp (pullback.snd (CategoryStruct.comp (pullback.fst f g) f) φ) h) = CategoryStruct.comp (pullback.fst (pullback.snd f φ) (pullback.snd g φ)) (CategoryStruct.comp (pullback.snd f φ) h)

The base-change comparison is an isomorphism over the new base.

theorem CategoryTheory.Limits.pullbackBaseChangeIso_naturality {C : Type u_1} [Category.{v_1, u_1} C] [HasPullbacks C] {X Y S S' : C} (f : X ⟶ S) (g : Y ⟶ S) (φ : S' ⟶ S) {X' Y' : C} (f' : X' ⟶ S) (g' : Y' ⟶ S) (a : X ⟶ X') (b : Y ⟶ Y') (ha : CategoryStruct.comp a f' = f) (hb : CategoryStruct.comp b g' = g) : CategoryStruct.comp (pullback.map (CategoryStruct.comp (pullback.fst f g) f) φ (CategoryStruct.comp (pullback.fst f' g') f') φ (pullback.map f g f' g' a b (CategoryStruct.id S) ⋯ ⋯) (CategoryStruct.id S') (CategoryStruct.id S) ⋯ ⋯) (pullbackBaseChangeIso f' g' φ).hom = CategoryStruct.comp (pullbackBaseChangeIso f g φ).hom (pullback.map (pullback.snd f φ) (pullback.snd g φ) (pullback.snd f' φ) (pullback.snd g' φ) (pullback.map f φ f' φ a (CategoryStruct.id S') (CategoryStruct.id S) ⋯ ⋯) (pullback.map g φ g' φ b (CategoryStruct.id S') (CategoryStruct.id S) ⋯ ⋯) (CategoryStruct.id S') ⋯ ⋯)

The base-change comparison is natural in both objects over the base.

theorem CategoryTheory.Limits.pullbackBaseChangeIso_naturality_assoc {C : Type u_1} [Category.{v_1, u_1} C] [HasPullbacks C] {X Y S S' : C} (f : X ⟶ S) (g : Y ⟶ S) (φ : S' ⟶ S) {X' Y' : C} (f' : X' ⟶ S) (g' : Y' ⟶ S) (a : X ⟶ X') (b : Y ⟶ Y') (ha : CategoryStruct.comp a f' = f) (hb : CategoryStruct.comp b g' = g) {Z : C} (h : pullback (pullback.snd f' φ) (pullback.snd g' φ) ⟶ Z) : CategoryStruct.comp (pullback.map (CategoryStruct.comp (pullback.fst f g) f) φ (CategoryStruct.comp (pullback.fst f' g') f') φ (pullback.map f g f' g' a b (CategoryStruct.id S) ⋯ ⋯) (CategoryStruct.id S') (CategoryStruct.id S) ⋯ ⋯) (CategoryStruct.comp (pullbackBaseChangeIso f' g' φ).hom h) = CategoryStruct.comp (pullbackBaseChangeIso f g φ).hom (CategoryStruct.comp (pullback.map (pullback.snd f φ) (pullback.snd g φ) (pullback.snd f' φ) (pullback.snd g' φ) (pullback.map f φ f' φ a (CategoryStruct.id S') (CategoryStruct.id S) ⋯ ⋯) (pullback.map g φ g' φ b (CategoryStruct.id S') (CategoryStruct.id S) ⋯ ⋯) (CategoryStruct.id S') ⋯ ⋯) h)

The base-change comparison is natural in both objects over the base.

theorem CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_naturality {C : Type u_1} [Category.{v_1, u_1} C] {S T U X Y : C} (a : X ⟶ S) (b : Y ⟶ S) (g : T ⟶ S) (h : U ⟶ T) [HasPullback a g] [HasPullback b g] [HasPullback (pullback.snd a g) h] [HasPullback (pullback.snd b g) h] (φ : X ⟶ Y) (hφ : CategoryStruct.comp φ b = a) : CategoryStruct.comp (pullback.map a (CategoryStruct.comp h g) b (CategoryStruct.comp h g) φ (CategoryStruct.id U) (CategoryStruct.id S) ⋯ ⋯) (pullbackLeftPullbackSndIso b g h).inv = CategoryStruct.comp (pullbackLeftPullbackSndIso a g h).inv (pullback.map (pullback.snd a g) h (pullback.snd b g) h (pullback.map a g b g φ (CategoryStruct.id T) (CategoryStruct.id S) ⋯ ⋯) (CategoryStruct.id U) (CategoryStruct.id T) ⋯ ⋯)

The inverse canonical isomorphism between a direct and an iterated pullback is natural in morphisms of the first factor over the common base.

theorem CategoryTheory.Limits.pullbackLeftPullbackSndIso_inv_naturality_assoc {C : Type u_1} [Category.{v_1, u_1} C] {S T U X Y : C} (a : X ⟶ S) (b : Y ⟶ S) (g : T ⟶ S) (h : U ⟶ T) [HasPullback a g] [HasPullback b g] [HasPullback (pullback.snd a g) h] [HasPullback (pullback.snd b g) h] (φ : X ⟶ Y) (hφ : CategoryStruct.comp φ b = a) {Z : C} (h✝ : pullback (pullback.snd b g) h ⟶ Z) : CategoryStruct.comp (pullback.map a (CategoryStruct.comp h g) b (CategoryStruct.comp h g) φ (CategoryStruct.id U) (CategoryStruct.id S) ⋯ ⋯) (CategoryStruct.comp (pullbackLeftPullbackSndIso b g h).inv h✝) = CategoryStruct.comp (pullbackLeftPullbackSndIso a g h).inv (CategoryStruct.comp (pullback.map (pullback.snd a g) h (pullback.snd b g) h (pullback.map a g b g φ (CategoryStruct.id T) (CategoryStruct.id S) ⋯ ⋯) (CategoryStruct.id U) (CategoryStruct.id T) ⋯ ⋯) h✝)

The inverse canonical isomorphism between a direct and an iterated pullback is natural in morphisms of the first factor over the common base.