Fibred products of schemes

In this file we construct the fibred product of schemes via gluing. We roughly follow [har77] Theorem 3.3.

In particular, the main construction is to show that for an open cover { Uᵢ } of X, if there exist fibred products Uᵢ ×[Z] Y for each i, then there exists a fibred product X ×[Z] Y.

Then, for constructing the fibred product for arbitrary schemes X, Y, Z, we can use the construction to reduce to the case where X, Y, Z are all affine, where fibred products are constructed via tensor products.

def AlgebraicGeometry.Scheme.Pullback.v {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j : 𝒰.J) : Scheme

The intersection of Uᵢ ×[Z] Y and Uⱼ ×[Z] Y is given by (Uᵢ ×[Z] Y) ×[X] Uⱼ

def AlgebraicGeometry.Scheme.Pullback.t {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j : 𝒰.J) : v 𝒰 f g i j ⟶ v 𝒰 f g j i

The canonical transition map (Uᵢ ×[Z] Y) ×[X] Uⱼ ⟶ (Uⱼ ×[Z] Y) ×[X] Uᵢ given by the fact that pullbacks are associative and symmetric.

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.t_fst_fst {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j : 𝒰.J) : CategoryTheory.CategoryStruct.comp (t 𝒰 f g i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) (𝒰.map j)) (𝒰.map i)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g)) = CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j)

theorem AlgebraicGeometry.Scheme.Pullback.t_fst_fst_assoc {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j : 𝒰.J) {Z✝ : Scheme} (h : 𝒰.obj j ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (t 𝒰 f g i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) (𝒰.map j)) (𝒰.map i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j)) h

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.t_fst_snd {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j : 𝒰.J) : CategoryTheory.CategoryStruct.comp (t 𝒰 f g i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) (𝒰.map j)) (𝒰.map i)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g)

theorem AlgebraicGeometry.Scheme.Pullback.t_fst_snd_assoc {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j : 𝒰.J) {Z✝ : Scheme} (h : Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (t 𝒰 f g i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) (𝒰.map j)) (𝒰.map i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) h)

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.t_snd {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j : 𝒰.J) : CategoryTheory.CategoryStruct.comp (t 𝒰 f g i j) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) (𝒰.map j)) (𝒰.map i)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g)

theorem AlgebraicGeometry.Scheme.Pullback.t_snd_assoc {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j : 𝒰.J) {Z✝ : Scheme} (h : 𝒰.obj i ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (t 𝒰 f g i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) (𝒰.map j)) (𝒰.map i)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) h)

theorem AlgebraicGeometry.Scheme.Pullback.t_id {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) : t 𝒰 f g i i = CategoryTheory.CategoryStruct.id (v 𝒰 f g i i)

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.Pullback.fV {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j : 𝒰.J) : v 𝒰 f g i j ⟶ CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g

The inclusion map of V i j = (Uᵢ ×[Z] Y) ×[X] Uⱼ ⟶ Uᵢ ×[Z] Y

def AlgebraicGeometry.Scheme.Pullback.t' {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j k : 𝒰.J) : CategoryTheory.Limits.pullback (fV 𝒰 f g i j) (fV 𝒰 f g i k) ⟶ CategoryTheory.Limits.pullback (fV 𝒰 f g j k) (fV 𝒰 f g j i)

The map ((Xᵢ ×[Z] Y) ×[X] Xⱼ) ×[Xᵢ ×[Z] Y] ((Xᵢ ×[Z] Y) ×[X] Xₖ) ⟶ ((Xⱼ ×[Z] Y) ×[X] Xₖ) ×[Xⱼ ×[Z] Y] ((Xⱼ ×[Z] Y) ×[X] Xᵢ) needed for gluing

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_fst {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j k : 𝒰.J) : CategoryTheory.CategoryStruct.comp (t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (fV 𝒰 f g j k) (fV 𝒰 f g j i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) (𝒰.map j)) (𝒰.map k)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j))

theorem AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_fst_assoc {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j k : 𝒰.J) {Z✝ : Scheme} (h : 𝒰.obj j ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (fV 𝒰 f g j k) (fV 𝒰 f g j i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) (𝒰.map j)) (𝒰.map k)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) h))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j)) h)

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_snd {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j k : 𝒰.J) : CategoryTheory.CategoryStruct.comp (t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (fV 𝒰 f g j k) (fV 𝒰 f g j i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) (𝒰.map j)) (𝒰.map k)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g))

theorem AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_snd_assoc {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j k : 𝒰.J) {Z✝ : Scheme} (h : Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (fV 𝒰 f g j k) (fV 𝒰 f g j i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) (𝒰.map j)) (𝒰.map k)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) h))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) h))

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.t'_fst_snd {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j k : 𝒰.J) : CategoryTheory.CategoryStruct.comp (t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (fV 𝒰 f g j k) (fV 𝒰 f g j i)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) (𝒰.map j)) (𝒰.map k))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map k))

theorem AlgebraicGeometry.Scheme.Pullback.t'_fst_snd_assoc {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j k : 𝒰.J) {Z✝ : Scheme} (h : 𝒰.obj k ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (fV 𝒰 f g j k) (fV 𝒰 f g j i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) (𝒰.map j)) (𝒰.map k)) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map k)) h)

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_fst {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j k : 𝒰.J) : CategoryTheory.CategoryStruct.comp (t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (fV 𝒰 f g j k) (fV 𝒰 f g j i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) (𝒰.map j)) (𝒰.map i)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j))

theorem AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_fst_assoc {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j k : 𝒰.J) {Z✝ : Scheme} (h : 𝒰.obj j ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (fV 𝒰 f g j k) (fV 𝒰 f g j i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) (𝒰.map j)) (𝒰.map i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) h))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j)) h)

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_snd {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j k : 𝒰.J) : CategoryTheory.CategoryStruct.comp (t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (fV 𝒰 f g j k) (fV 𝒰 f g j i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) (𝒰.map j)) (𝒰.map i)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g))

theorem AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_snd_assoc {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j k : 𝒰.J) {Z✝ : Scheme} (h : Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (fV 𝒰 f g j k) (fV 𝒰 f g j i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) (𝒰.map j)) (𝒰.map i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) h))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) h))

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.t'_snd_snd {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j k : 𝒰.J) : CategoryTheory.CategoryStruct.comp (t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (fV 𝒰 f g j k) (fV 𝒰 f g j i)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) (𝒰.map j)) (𝒰.map i))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g))

theorem AlgebraicGeometry.Scheme.Pullback.t'_snd_snd_assoc {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j k : 𝒰.J) {Z✝ : Scheme} (h : 𝒰.obj i ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (fV 𝒰 f g j k) (fV 𝒰 f g j i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) (𝒰.map j)) (𝒰.map i)) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) h))

theorem AlgebraicGeometry.Scheme.Pullback.cocycle_fst_fst_fst {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j k : 𝒰.J) : CategoryTheory.CategoryStruct.comp (t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp (t' 𝒰 f g j k i) (CategoryTheory.CategoryStruct.comp (t' 𝒰 f g k i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g))))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g))

theorem AlgebraicGeometry.Scheme.Pullback.cocycle_fst_fst_snd {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j k : 𝒰.J) : CategoryTheory.CategoryStruct.comp (t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp (t' 𝒰 f g j k i) (CategoryTheory.CategoryStruct.comp (t' 𝒰 f g k i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g))))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g))

theorem AlgebraicGeometry.Scheme.Pullback.cocycle_fst_snd {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j k : 𝒰.J) : CategoryTheory.CategoryStruct.comp (t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp (t' 𝒰 f g j k i) (CategoryTheory.CategoryStruct.comp (t' 𝒰 f g k i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j))))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (fV 𝒰 f g i j) (fV 𝒰 f g i k)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j))

theorem AlgebraicGeometry.Scheme.Pullback.cocycle_snd_fst_fst {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j k : 𝒰.J) : CategoryTheory.CategoryStruct.comp (t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp (t' 𝒰 f g j k i) (CategoryTheory.CategoryStruct.comp (t' 𝒰 f g k i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map k)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g))))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map k)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g))

theorem AlgebraicGeometry.Scheme.Pullback.cocycle_snd_fst_snd {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j k : 𝒰.J) : CategoryTheory.CategoryStruct.comp (t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp (t' 𝒰 f g j k i) (CategoryTheory.CategoryStruct.comp (t' 𝒰 f g k i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map k)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g))))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map k)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g))

theorem AlgebraicGeometry.Scheme.Pullback.cocycle_snd_snd {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j k : 𝒰.J) : CategoryTheory.CategoryStruct.comp (t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp (t' 𝒰 f g j k i) (CategoryTheory.CategoryStruct.comp (t' 𝒰 f g k i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map k))))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map k))

theorem AlgebraicGeometry.Scheme.Pullback.cocycle {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j k : 𝒰.J) : CategoryTheory.CategoryStruct.comp (t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp (t' 𝒰 f g j k i) (t' 𝒰 f g k i j)) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback (fV 𝒰 f g i j) (fV 𝒰 f g i k))

def AlgebraicGeometry.Scheme.Pullback.gluing {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] : GlueData

Given Uᵢ ×[Z] Y, this is the glued fibred product X ×[Z] Y.

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.gluing_t {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j : 𝒰.J) : (gluing 𝒰 f g).t i j = t 𝒰 f g i j

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.gluing_U {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) : (gluing 𝒰 f g).U i = CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.gluing_f {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (x✝ x✝¹ : 𝒰.J) : (gluing 𝒰 f g).f x✝ x✝¹ = CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map x✝) f) g) (𝒰.map x✝)) (𝒰.map x✝¹)

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.gluing_V {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (x✝ : 𝒰.J × 𝒰.J) : (gluing 𝒰 f g).V x✝ = match x✝ with | (i, j) => v 𝒰 f g i j

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.gluing_t' {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j k : 𝒰.J) : (gluing 𝒰 f g).t' i j k = t' 𝒰 f g i j k

theorem AlgebraicGeometry.Scheme.Pullback.gluing_J {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] : (gluing 𝒰 f g).J = 𝒰.J

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.gluing_ι {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (j : 𝒰.J) : (gluing 𝒰 f g).ι j = CategoryTheory.Limits.Multicoequalizer.π (gluing 𝒰 f g).diagram j

def AlgebraicGeometry.Scheme.Pullback.p1 {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] : (gluing 𝒰 f g).glued ⟶ X

The first projection from the glued scheme into X.

def AlgebraicGeometry.Scheme.Pullback.p2 {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] : (gluing 𝒰 f g).glued ⟶ Y

The second projection from the glued scheme into Y.

theorem AlgebraicGeometry.Scheme.Pullback.p_comm {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] : CategoryTheory.CategoryStruct.comp (p1 𝒰 f g) f = CategoryTheory.CategoryStruct.comp (p2 𝒰 f g) g

def AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (s : CategoryTheory.Limits.PullbackCone f g) (i j : 𝒰.J) : CategoryTheory.Limits.pullback ((Cover.pullbackCover 𝒰 s.fst).map i) ((Cover.pullbackCover 𝒰 s.fst).map j) ⟶ (gluing 𝒰 f g).V (i, j)

(Implementation) The canonical map (s.X ×[X] Uᵢ) ×[s.X] (s.X ×[X] Uⱼ) ⟶ (Uᵢ ×[Z] Y) ×[X] Uⱼ

This is used in gluedLift.

theorem AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (s : CategoryTheory.Limits.PullbackCone f g) (i j : 𝒰.J) : CategoryTheory.CategoryStruct.comp (gluedLiftPullbackMap 𝒰 f g s i j) (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst ((Cover.pullbackCover 𝒰 s.fst).map i) ((Cover.pullbackCover 𝒰 s.fst).map j)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry s.fst (𝒰.map i)).hom (CategoryTheory.Limits.pullback.map (𝒰.map i) s.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g (CategoryTheory.CategoryStruct.id (𝒰.obj i)) s.snd f ⋯ ⋯))

theorem AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst_assoc {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (s : CategoryTheory.Limits.PullbackCone f g) (i j : 𝒰.J) {Z✝ : Scheme} (h : CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (gluedLiftPullbackMap 𝒰 f g s i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst ((Cover.pullbackCover 𝒰 s.fst).map i) ((Cover.pullbackCover 𝒰 s.fst).map j)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry s.fst (𝒰.map i)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map (𝒰.map i) s.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g (CategoryTheory.CategoryStruct.id (𝒰.obj i)) s.snd f ⋯ ⋯) h))

theorem AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (s : CategoryTheory.Limits.PullbackCone f g) (i j : 𝒰.J) : CategoryTheory.CategoryStruct.comp (gluedLiftPullbackMap 𝒰 f g s i j) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd ((Cover.pullbackCover 𝒰 s.fst).map i) ((Cover.pullbackCover 𝒰 s.fst).map j)) (CategoryTheory.Limits.pullback.snd s.fst (𝒰.map j))

theorem AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_snd_assoc {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (s : CategoryTheory.Limits.PullbackCone f g) (i j : 𝒰.J) {Z✝ : Scheme} (h : 𝒰.obj j ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (gluedLiftPullbackMap 𝒰 f g s i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) (𝒰.map i)) (𝒰.map j)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd ((Cover.pullbackCover 𝒰 s.fst).map i) ((Cover.pullbackCover 𝒰 s.fst).map j)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd s.fst (𝒰.map j)) h)

def AlgebraicGeometry.Scheme.Pullback.gluedLift {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (s : CategoryTheory.Limits.PullbackCone f g) : s.pt ⟶ (gluing 𝒰 f g).glued

The lifted map s.X ⟶ (gluing 𝒰 f g).glued in order to show that (gluing 𝒰 f g).glued is indeed the pullback.

Given a pullback cone s, we have the maps s.fst ⁻¹' Uᵢ ⟶ Uᵢ and s.fst ⁻¹' Uᵢ ⟶ s.X ⟶ Y that we may lift to a map s.fst ⁻¹' Uᵢ ⟶ Uᵢ ×[Z] Y.

to glue these into a map s.X ⟶ Uᵢ ×[Z] Y, we need to show that the maps agree on (s.fst ⁻¹' Uᵢ) ×[s.X] (s.fst ⁻¹' Uⱼ) ⟶ Uᵢ ×[Z] Y. This is achieved by showing that both of these maps factors through gluedLiftPullbackMap.

theorem AlgebraicGeometry.Scheme.Pullback.gluedLift_p1 {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (s : CategoryTheory.Limits.PullbackCone f g) : CategoryTheory.CategoryStruct.comp (gluedLift 𝒰 f g s) (p1 𝒰 f g) = s.fst

theorem AlgebraicGeometry.Scheme.Pullback.gluedLift_p2 {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (s : CategoryTheory.Limits.PullbackCone f g) : CategoryTheory.CategoryStruct.comp (gluedLift 𝒰 f g s) (p2 𝒰 f g) = s.snd

def AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j : 𝒰.J) : CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.fst (p1 𝒰 f g) (𝒰.map i)) ((gluing 𝒰 f g).ι j) ⟶ v 𝒰 f g j i

(Implementation) The canonical map (W ×[X] Uᵢ) ×[W] (Uⱼ ×[Z] Y) ⟶ (Uⱼ ×[Z] Y) ×[X] Uᵢ = V j i where W is the glued fibred product.

This is used in lift_comp_ι.

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_fst {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j : 𝒰.J) : CategoryTheory.CategoryStruct.comp (pullbackFstιToV 𝒰 f g i j) (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) (𝒰.map j)) (𝒰.map i)) = CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (p1 𝒰 f g) (𝒰.map i)) ((gluing 𝒰 f g).ι j)

theorem AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_fst_assoc {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j : 𝒰.J) {Z✝ : Scheme} (h : CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (pullbackFstιToV 𝒰 f g i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) (𝒰.map j)) (𝒰.map i)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (p1 𝒰 f g) (𝒰.map i)) ((gluing 𝒰 f g).ι j)) h

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_snd {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j : 𝒰.J) : CategoryTheory.CategoryStruct.comp (pullbackFstιToV 𝒰 f g i j) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) (𝒰.map j)) (𝒰.map i)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (p1 𝒰 f g) (𝒰.map i)) ((gluing 𝒰 f g).ι j)) (CategoryTheory.Limits.pullback.snd (p1 𝒰 f g) (𝒰.map i))

theorem AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_snd_assoc {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i j : 𝒰.J) {Z✝ : Scheme} (h : 𝒰.obj i ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (pullbackFstιToV 𝒰 f g i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map j) f) g) (𝒰.map j)) (𝒰.map i)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (p1 𝒰 f g) (𝒰.map i)) ((gluing 𝒰 f g).ι j)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (p1 𝒰 f g) (𝒰.map i)) h)

theorem AlgebraicGeometry.Scheme.Pullback.lift_comp_ι {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift (CategoryTheory.Limits.pullback.snd (p1 𝒰 f g) (𝒰.map i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (p1 𝒰 f g) (𝒰.map i)) (p2 𝒰 f g)) ⋯) ((gluing 𝒰 f g).ι i) = CategoryTheory.Limits.pullback.fst (p1 𝒰 f g) (𝒰.map i)

We show that the map W ×[X] Uᵢ ⟶ Uᵢ ×[Z] Y ⟶ W is the first projection, where the first map is given by the lift of W ×[X] Uᵢ ⟶ Uᵢ and W ×[X] Uᵢ ⟶ W ⟶ Y.

It suffices to show that the two map agrees when restricted onto Uⱼ ×[Z] Y. In this case, both maps factor through V j i via pullback_fst_ι_to_V

def AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) : CategoryTheory.Limits.pullback (p1 𝒰 f g) (𝒰.map i) ≅ CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g

The canonical isomorphism between W ×[X] Uᵢ and Uᵢ ×[X] Y. That is, the preimage of Uᵢ in W along p1 is indeed Uᵢ ×[X] Y.

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_fst {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) : CategoryTheory.CategoryStruct.comp (pullbackP1Iso 𝒰 f g i).hom (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) = CategoryTheory.Limits.pullback.snd (p1 𝒰 f g) (𝒰.map i)

theorem AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_fst_assoc {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) {Z✝ : Scheme} (h : 𝒰.obj i ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (pullbackP1Iso 𝒰 f g i).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (p1 𝒰 f g) (𝒰.map i)) h

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_snd {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) : CategoryTheory.CategoryStruct.comp (pullbackP1Iso 𝒰 f g i).hom (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (p1 𝒰 f g) (𝒰.map i)) (p2 𝒰 f g)

theorem AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_snd_assoc {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) {Z✝ : Scheme} (h : Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (pullbackP1Iso 𝒰 f g i).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (p1 𝒰 f g) (𝒰.map i)) (CategoryTheory.CategoryStruct.comp (p2 𝒰 f g) h)

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_fst {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) : CategoryTheory.CategoryStruct.comp (pullbackP1Iso 𝒰 f g i).inv (CategoryTheory.Limits.pullback.fst (p1 𝒰 f g) (𝒰.map i)) = (gluing 𝒰 f g).ι i

theorem AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_fst_assoc {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) {Z✝ : Scheme} (h : (gluing 𝒰 f g).glued ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (pullbackP1Iso 𝒰 f g i).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (p1 𝒰 f g) (𝒰.map i)) h) = CategoryTheory.CategoryStruct.comp ((gluing 𝒰 f g).ι i) h

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_snd {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) : CategoryTheory.CategoryStruct.comp (pullbackP1Iso 𝒰 f g i).inv (CategoryTheory.Limits.pullback.snd (p1 𝒰 f g) (𝒰.map i)) = CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g

theorem AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_snd_assoc {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) {Z✝ : Scheme} (h : 𝒰.obj i ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (pullbackP1Iso 𝒰 f g i).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (p1 𝒰 f g) (𝒰.map i)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g) h

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_ι {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) : CategoryTheory.CategoryStruct.comp (pullbackP1Iso 𝒰 f g i).hom (CategoryTheory.Limits.Multicoequalizer.π (gluing 𝒰 f g).diagram i) = CategoryTheory.Limits.pullback.fst (p1 𝒰 f g) (𝒰.map i)

theorem AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_hom_ι_assoc {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) {Z✝ : Scheme} (h : CategoryTheory.Limits.multicoequalizer (gluing 𝒰 f g).diagram ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (pullbackP1Iso 𝒰 f g i).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicoequalizer.π (gluing 𝒰 f g).diagram i) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (p1 𝒰 f g) (𝒰.map i)) h

def AlgebraicGeometry.Scheme.Pullback.gluedIsLimit {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk (p1 𝒰 f g) (p2 𝒰 f g) ⋯)

The glued scheme ((gluing 𝒰 f g).glued) is indeed the pullback of f and g.

theorem AlgebraicGeometry.Scheme.Pullback.hasPullback_of_cover {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] : CategoryTheory.Limits.HasPullback f g

instance AlgebraicGeometry.Scheme.Pullback.affine_hasPullback {A B C : CommRingCat} (f : Spec A ⟶ Spec C) (g : Spec B ⟶ Spec C) : CategoryTheory.Limits.HasPullback f g

theorem AlgebraicGeometry.Scheme.Pullback.affine_affine_hasPullback {B C : CommRingCat} {X : Scheme} (f : X ⟶ Spec C) (g : Spec B ⟶ Spec C) : CategoryTheory.Limits.HasPullback f g

instance AlgebraicGeometry.Scheme.Pullback.base_affine_hasPullback {C : CommRingCat} {X Y : Scheme} (f : X ⟶ Spec C) (g : Y ⟶ Spec C) : CategoryTheory.Limits.HasPullback f g

instance AlgebraicGeometry.Scheme.Pullback.left_affine_comp_pullback_hasPullback {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) (i : Z.affineCover.J) : CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp ((Cover.pullbackCover Z.affineCover f).map i) f) g

instance AlgebraicGeometry.Scheme.Pullback.instHasPullback {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryTheory.Limits.HasPullback f g

instance AlgebraicGeometry.Scheme.Pullback.instHasPullbacks : CategoryTheory.Limits.HasPullbacks Scheme

instance AlgebraicGeometry.Scheme.Pullback.isAffine_of_isAffine_isAffine_isAffine {X Y Z : Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [IsAffine X] [IsAffine Y] [IsAffine Z] : IsAffine (CategoryTheory.Limits.pullback f g)

theorem AlgebraicGeometry.Scheme.isEmpty_pullback {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) (H : Disjoint (Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base))) : IsEmpty ↥(CategoryTheory.Limits.pullback f g)

def AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) : (CategoryTheory.Limits.pullback f g).OpenCover

Given an open cover { Xᵢ } of X, then X ×[Z] Y is covered by Xᵢ ×[Z] Y.

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft_J {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) : (openCoverOfLeft 𝒰 f g).J = 𝒰.J

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft_obj {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (i : 𝒰.J) : (openCoverOfLeft 𝒰 f g).obj i = CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft_map {X Y Z : Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (i : 𝒰.J) : (openCoverOfLeft 𝒰 f g).map i = CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g f g (𝒰.map i) (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯

def AlgebraicGeometry.Scheme.Pullback.openCoverOfRight {X Y Z : Scheme} (𝒰 : Y.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) : (CategoryTheory.Limits.pullback f g).OpenCover

Given an open cover { Yᵢ } of Y, then X ×[Z] Y is covered by X ×[Z] Yᵢ.

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.openCoverOfRight_J {X Y Z : Scheme} (𝒰 : Y.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) : (openCoverOfRight 𝒰 f g).J = 𝒰.J

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.openCoverOfRight_map {X Y Z : Scheme} (𝒰 : Y.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (i : 𝒰.J) : (openCoverOfRight 𝒰 f g).map i = CategoryTheory.Limits.pullback.map f (CategoryTheory.CategoryStruct.comp (𝒰.map i) g) f g (CategoryTheory.CategoryStruct.id X) (𝒰.map i) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.openCoverOfRight_obj {X Y Z : Scheme} (𝒰 : Y.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (i : 𝒰.J) : (openCoverOfRight 𝒰 f g).obj i = CategoryTheory.Limits.pullback f (CategoryTheory.CategoryStruct.comp (𝒰.map i) g)

def AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight {X Y Z : Scheme} (𝒰X : X.OpenCover) (𝒰Y : Y.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) : (CategoryTheory.Limits.pullback f g).OpenCover

Given an open cover { Xᵢ } of X and an open cover { Yⱼ } of Y, then X ×[Z] Y is covered by Xᵢ ×[Z] Yⱼ.

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_map {X Y Z : Scheme} (𝒰X : X.OpenCover) (𝒰Y : Y.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (ij : 𝒰X.J × 𝒰Y.J) : (openCoverOfLeftRight 𝒰X 𝒰Y f g).map ij = CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (𝒰X.map ij.1) f) (CategoryTheory.CategoryStruct.comp (𝒰Y.map ij.2) g) f g (𝒰X.map ij.1) (𝒰Y.map ij.2) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_obj {X Y Z : Scheme} (𝒰X : X.OpenCover) (𝒰Y : Y.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (ij : 𝒰X.J × 𝒰Y.J) : (openCoverOfLeftRight 𝒰X 𝒰Y f g).obj ij = CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (𝒰X.map ij.1) f) (CategoryTheory.CategoryStruct.comp (𝒰Y.map ij.2) g)

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_J {X Y Z : Scheme} (𝒰X : X.OpenCover) (𝒰Y : Y.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) : (openCoverOfLeftRight 𝒰X 𝒰Y f g).J = (𝒰X.J × 𝒰Y.J)

def AlgebraicGeometry.Scheme.Pullback.openCoverOfBase' {X Y Z : Scheme} (𝒰 : Z.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) : (CategoryTheory.Limits.pullback f g).OpenCover

(Implementation). Use openCoverOfBase instead.

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.openCoverOfBase'_map {X Y Z : Scheme} (𝒰 : Z.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (x : (i : (openCoverOfLeft (Cover.pullbackCover 𝒰 f) f g).J) × ((fun (i : (openCoverOfLeft (Cover.pullbackCover 𝒰 f) f g).J) => coverOfIsIso (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry (CategoryTheory.Limits.pullback.snd f (𝒰.map i)) (CategoryTheory.Limits.pullback.snd g (𝒰.map i))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.isoLimitCone { cone := ⋯.cone, isLimit := ⋯.isLimit }).inv (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f (𝒰.map i)) (𝒰.map i)) g (CategoryTheory.CategoryStruct.comp ((Cover.pullbackCover 𝒰 f).map i) f) g (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback f (𝒰.map i))) (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯)))) i).J) : (openCoverOfBase' 𝒰 f g).map x = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry (CategoryTheory.Limits.pullback.snd f (𝒰.map x.fst)) (CategoryTheory.Limits.pullback.snd g (𝒰.map x.fst))).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.isoLimitCone { cone := ⋯.cone, isLimit := ⋯.isLimit }).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f (𝒰.map x.fst)) (𝒰.map x.fst)) g (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f (𝒰.map x.fst)) f) g (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback f (𝒰.map x.fst))) (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f (𝒰.map x.fst)) f) g f g (CategoryTheory.Limits.pullback.fst f (𝒰.map x.fst)) (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯)))

def AlgebraicGeometry.Scheme.Pullback.openCoverOfBase {X Y Z : Scheme} (𝒰 : Z.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) : (CategoryTheory.Limits.pullback f g).OpenCover

Given an open cover { Zᵢ } of Z, then X ×[Z] Y is covered by Xᵢ ×[Zᵢ] Yᵢ, where Xᵢ = X ×[Z] Zᵢ and Yᵢ = Y ×[Z] Zᵢ is the preimage of Zᵢ in X and Y.

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_obj {X Y Z : Scheme} (𝒰 : Z.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (i : 𝒰.J) : (openCoverOfBase 𝒰 f g).obj i = CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.snd f (𝒰.map i)) (CategoryTheory.Limits.pullback.snd g (𝒰.map i))

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_J {X Y Z : Scheme} (𝒰 : Z.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) : (openCoverOfBase 𝒰 f g).J = 𝒰.J

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_map {X Y Z : Scheme} (𝒰 : Z.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (i : 𝒰.J) : (openCoverOfBase 𝒰 f g).map i = CategoryTheory.Limits.pullback.map (CategoryTheory.Limits.pullback.snd f (𝒰.map i)) (CategoryTheory.Limits.pullback.snd g (𝒰.map i)) f g (CategoryTheory.Limits.pullback.fst f (𝒰.map i)) (CategoryTheory.Limits.pullback.fst g (𝒰.map i)) (𝒰.map i) ⋯ ⋯

noncomputable def AlgebraicGeometry.Scheme.Pullback.diagonalCover {X Y : Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (𝒱 : (i : (Cover.pullbackCover 𝒰 f).J) → ((Cover.pullbackCover 𝒰 f).obj i).OpenCover) : (CategoryTheory.Limits.pullback.diagonalObj f).OpenCover

Given 𝒰 i covering Y and 𝒱 i j covering 𝒰 i, this is the open cover 𝒱 i j₁ ×[𝒰 i] 𝒱 i j₂ ranging over all i, j₁, j₂.

noncomputable def AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange {X Y : Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (𝒱 : (i : (Cover.pullbackCover 𝒰 f).J) → ((Cover.pullbackCover 𝒰 f).obj i).OpenCover) : (CategoryTheory.Limits.pullback.diagonalObj f).Opens

The image of 𝒱 i j₁ ×[𝒰 i] 𝒱 i j₂ in diagonalCover with j₁ = j₂

theorem AlgebraicGeometry.Scheme.Pullback.diagonalCover_map {X Y : Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (𝒱 : (i : (Cover.pullbackCover 𝒰 f).J) → ((Cover.pullbackCover 𝒰 f).obj i).OpenCover) (I : (diagonalCover f 𝒰 𝒱).J) : (diagonalCover f 𝒰 𝒱).map I = CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp ((𝒱 I.fst).map I.snd.1) (Cover.pullbackHom 𝒰 f I.fst)) (CategoryTheory.CategoryStruct.comp ((𝒱 I.fst).map I.snd.2) (Cover.pullbackHom 𝒰 f I.fst)) f f (CategoryTheory.CategoryStruct.comp ((𝒱 I.fst).map I.snd.1) (CategoryTheory.Limits.pullback.fst f (𝒰.map I.fst))) (CategoryTheory.CategoryStruct.comp ((𝒱 I.fst).map I.snd.2) (CategoryTheory.Limits.pullback.fst f (𝒰.map I.fst))) (𝒰.map I.fst) ⋯ ⋯

noncomputable def AlgebraicGeometry.Scheme.Pullback.diagonalRestrictIsoDiagonal {X Y : Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (𝒱 : (i : (Cover.pullbackCover 𝒰 f).J) → ((Cover.pullbackCover 𝒰 f).obj i).OpenCover) (i : (openCoverOfBase 𝒰 f f).J) (j : (𝒱 i).J) : CategoryTheory.Arrow.mk (CategoryTheory.Limits.pullback.diagonal f ∣_ Hom.opensRange ((diagonalCover f 𝒰 𝒱).map ⟨i, (j, j)⟩)) ≅ CategoryTheory.Arrow.mk (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.CategoryStruct.comp ((𝒱 i).map j) (CategoryTheory.Limits.pullback.snd f (𝒰.map i))))

The restriction of the diagonal X ⟶ X ×ₛ X to 𝒱 i j ×[𝒰 i] 𝒱 i j is the diagonal 𝒱 i j ⟶ 𝒱 i j ×[𝒰 i] 𝒱 i j.

instance AlgebraicGeometry.Scheme.pullback_map_isOpenImmersion {X Y S X' Y' S' : Scheme} (f : X ⟶ S) (g : Y ⟶ S) (f' : X' ⟶ S') (g' : Y' ⟶ S') (i₁ : X ⟶ X') (i₂ : Y ⟶ Y') (i₃ : S ⟶ S') (e₁ : CategoryTheory.CategoryStruct.comp f i₃ = CategoryTheory.CategoryStruct.comp i₁ f') (e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₂ g') [IsOpenImmersion i₁] [IsOpenImmersion i₂] [CategoryTheory.Mono i₃] : IsOpenImmersion (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)

noncomputable def AlgebraicGeometry.pullbackSpecIso (R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] : CategoryTheory.Limits.pullback (Spec.map (CommRingCat.ofHom (algebraMap R S))) (Spec.map (CommRingCat.ofHom (algebraMap R T))) ≅ Spec (CommRingCat.of (TensorProduct R S T))

The isomorphism between the fibred product of two schemes Spec S and Spec T over a scheme Spec R and the Spec of the tensor product S ⊗[R] T.

@[simp]

theorem AlgebraicGeometry.pullbackSpecIso_inv_fst (R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] : CategoryTheory.CategoryStruct.comp (pullbackSpecIso R S T).inv (CategoryTheory.Limits.pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap R S))) (Spec.map (CommRingCat.ofHom (algebraMap R T)))) = Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom)

The composition of the inverse of the isomorphism pullbackSpecIso R S T (from the pullback of Spec S ⟶ Spec R and Spec T ⟶ Spec R to Spec (S ⊗[R] T)) with the first projection is the morphism Spec (S ⊗[R] T) ⟶ Spec S obtained by applying Spec.map to the ring morphism s ↦ s ⊗ₜ[R] 1.

@[simp]

theorem AlgebraicGeometry.pullbackSpecIso_inv_fst_assoc (R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] {Z : Scheme} (h : Spec (CommRingCat.of S) ⟶ Z) : CategoryTheory.CategoryStruct.comp (pullbackSpecIso R S T).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap R S))) (Spec.map (CommRingCat.ofHom (algebraMap R T)))) h) = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom)) h

@[simp]

theorem AlgebraicGeometry.pullbackSpecIso_inv_snd (R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] : CategoryTheory.CategoryStruct.comp (pullbackSpecIso R S T).inv (CategoryTheory.Limits.pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap R S))) (Spec.map (CommRingCat.ofHom (algebraMap R T)))) = Spec.map (CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight)

The composition of the inverse of the isomorphism pullbackSpecIso R S T (from the pullback of Spec S ⟶ Spec R and Spec T ⟶ Spec R to Spec (S ⊗[R] T)) with the second projection is the morphism Spec (S ⊗[R] T) ⟶ Spec T obtained by applying Spec.map to the ring morphism t ↦ 1 ⊗ₜ[R] t.

@[simp]

theorem AlgebraicGeometry.pullbackSpecIso_inv_snd_assoc (R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] {Z : Scheme} (h : Spec (CommRingCat.of T) ⟶ Z) : CategoryTheory.CategoryStruct.comp (pullbackSpecIso R S T).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap R S))) (Spec.map (CommRingCat.ofHom (algebraMap R T)))) h) = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight)) h

@[simp]

theorem AlgebraicGeometry.pullbackSpecIso_hom_fst (R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] : CategoryTheory.CategoryStruct.comp (pullbackSpecIso R S T).hom (Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom)) = CategoryTheory.Limits.pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap R S))) (Spec.map (CommRingCat.ofHom (algebraMap R T)))

The composition of the isomorphism pullbackSpecIso R S T (from the pullback of Spec S ⟶ Spec R and Spec T ⟶ Spec R to Spec (S ⊗[R] T)) with the morphism Spec (S ⊗[R] T) ⟶ Spec S obtained by applying Spec.map to the ring morphism s ↦ s ⊗ₜ[R] 1 is the first projection.

@[simp]

theorem AlgebraicGeometry.pullbackSpecIso_hom_fst_assoc (R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] {Z : Scheme} (h : Spec (CommRingCat.of S) ⟶ Z) : CategoryTheory.CategoryStruct.comp (pullbackSpecIso R S T).hom (CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap R S))) (Spec.map (CommRingCat.ofHom (algebraMap R T)))) h

@[simp]

theorem AlgebraicGeometry.pullbackSpecIso_hom_snd (R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] : CategoryTheory.CategoryStruct.comp (pullbackSpecIso R S T).hom (Spec.map (CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight)) = CategoryTheory.Limits.pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap R S))) (Spec.map (CommRingCat.ofHom (algebraMap R T)))

The composition of the isomorphism pullbackSpecIso R S T (from the pullback of Spec S ⟶ Spec R and Spec T ⟶ Spec R to Spec (S ⊗[R] T)) with the morphism Spec (S ⊗[R] T) ⟶ Spec T obtained by applying Spec.map to the ring morphism t ↦ 1 ⊗ₜ[R] t is the second projection.

@[simp]

theorem AlgebraicGeometry.pullbackSpecIso_hom_snd_assoc (R S T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] {Z : Scheme} (h : Spec (CommRingCat.of T) ⟶ Z) : CategoryTheory.CategoryStruct.comp (pullbackSpecIso R S T).hom (CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (Spec.map (CommRingCat.ofHom (algebraMap R S))) (Spec.map (CommRingCat.ofHom (algebraMap R T)))) h

theorem AlgebraicGeometry.isPullback_Spec_map_isPushout {A B C P : CommRingCat} (f : A ⟶ B) (g : A ⟶ C) (inl : B ⟶ P) (inr : C ⟶ P) (h : CategoryTheory.IsPushout f g inl inr) : CategoryTheory.IsPullback (Spec.map inl) (Spec.map inr) (Spec.map f) (Spec.map g)

theorem AlgebraicGeometry.isPullback_Spec_map_pushout {A B C : CommRingCat} (f : A ⟶ B) (g : A ⟶ C) : CategoryTheory.IsPullback (Spec.map (CategoryTheory.Limits.pushout.inl f g)) (Spec.map (CategoryTheory.Limits.pushout.inr f g)) (Spec.map f) (Spec.map g)

theorem AlgebraicGeometry.diagonal_Spec_map (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] : CategoryTheory.Limits.pullback.diagonal (Spec.map (CommRingCat.ofHom (algebraMap R S))) = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.lmul' R).toRingHom)) (pullbackSpecIso R S S).inv

instance AlgebraicGeometry.instCartesianMonoidalCategoryOverScheme {S : Scheme} : CategoryTheory.CartesianMonoidalCategory (CategoryTheory.Over S)

instance AlgebraicGeometry.instBraidedCategoryOverScheme {S : Scheme} : CategoryTheory.BraidedCategory (CategoryTheory.Over S)