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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f) g] (i : 𝒰.J) (j : 𝒰.J) : AlgebraicGeometry.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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f) g] (i : 𝒰.J) (j : 𝒰.J) : AlgebraicGeometry.Scheme.Pullback.v 𝒰 f g i j ⟶ AlgebraicGeometry.Scheme.Pullback.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.

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[inline, reducible]

abbrev AlgebraicGeometry.Scheme.Pullback.fV {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f) g] (i : 𝒰.J) (j : 𝒰.J) : AlgebraicGeometry.Scheme.Pullback.v 𝒰 f g i j ⟶ CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f) g] (i : 𝒰.J) (j : 𝒰.J) (k : 𝒰.J) : CategoryTheory.Limits.pullback (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j) (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k) ⟶ CategoryTheory.Limits.pullback (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g j k) (AlgebraicGeometry.Scheme.Pullback.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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

The first projection from the glued scheme into X.

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

The second projection from the glued scheme into Y.

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

def AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f) g] (s : CategoryTheory.Limits.PullbackCone f g) (i : 𝒰.J) (j : 𝒰.J) : CategoryTheory.Limits.pullback (AlgebraicGeometry.Scheme.OpenCover.map (AlgebraicGeometry.Scheme.OpenCover.pullbackCover 𝒰 (CategoryTheory.Limits.PullbackCone.fst s)) i) (AlgebraicGeometry.Scheme.OpenCover.map (AlgebraicGeometry.Scheme.OpenCover.pullbackCover 𝒰 (CategoryTheory.Limits.PullbackCone.fst s)) j) ⟶ CategoryTheory.GlueData.V (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).toGlueData (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_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f) g] (s : CategoryTheory.Limits.PullbackCone f g) (i : 𝒰.J) (j : 𝒰.J) {Z : AlgebraicGeometry.Scheme} (h : CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f) g ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap 𝒰 f g s i j) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry (CategoryTheory.Limits.PullbackCone.fst s) (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) (CategoryTheory.Limits.PullbackCone.fst s) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f) g (CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i)) (CategoryTheory.Limits.PullbackCone.snd s) f (_ : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Scheme.OpenCover.obj 𝒰 i)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f)) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PullbackCone.fst s) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PullbackCone.snd s) g)) h))

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

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

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

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

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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f) g] (s : CategoryTheory.Limits.PullbackCone f g) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.gluedLift 𝒰 f g s) (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) = CategoryTheory.Limits.PullbackCone.fst s

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

def AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f) g] (i : 𝒰.J) (j : 𝒰.J) : CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.GlueData.ι (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g) j) ⟶ AlgebraicGeometry.Scheme.Pullback.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_ι.

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

@[simp]

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

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

@[simp]

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

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

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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f) g] (i : 𝒰.J) : CategoryTheory.Limits.pullback (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) ≅ CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.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.

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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.openCoverOfBase'_map {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover Z) (f : X ⟶ Z) (g : Y ⟶ Z) (x : (i : (AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft (AlgebraicGeometry.Scheme.OpenCover.pullbackCover 𝒰 f) f g).J) × ((fun i => let Xᵢ := CategoryTheory.Limits.pullback f (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i); let Yᵢ := CategoryTheory.Limits.pullback g (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i); let W := CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd; let_fun this := CategoryTheory.Limits.bigSquareIsPullback CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd g (_ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd) (_ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst g) (CategoryTheory.Limits.PullbackCone.flipIsLimit (CategoryTheory.Limits.pullbackIsPullback g (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i))) (CategoryTheory.Limits.PullbackCone.flipIsLimit (CategoryTheory.Limits.pullbackIsPullback CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd)); AlgebraicGeometry.Scheme.openCoverOfIsIso (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.isoLimitCone { cone := CategoryTheory.Limits.PullbackCone.mk CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst) (_ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst) g), isLimit := this }).inv (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i)) g (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map (AlgebraicGeometry.Scheme.OpenCover.pullbackCover 𝒰 f) i) f) g (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback f (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i))) (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i)) (CategoryTheory.CategoryStruct.id Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback f (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i))) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map (AlgebraicGeometry.Scheme.OpenCover.pullbackCover 𝒰 f) i) f)) (_ : CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id Y) g))))) i).J) : AlgebraicGeometry.Scheme.OpenCover.map (AlgebraicGeometry.Scheme.Pullback.openCoverOfBase' 𝒰 f g) x = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.isoLimitCone { cone := CategoryTheory.Limits.PullbackCone.mk CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd) (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 x.fst) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst) g), isLimit := CategoryTheory.Limits.bigSquareIsPullback CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 x.fst) CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd g (_ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd) (_ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 x.fst) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst g) (CategoryTheory.Limits.PullbackCone.flipIsLimit (CategoryTheory.Limits.pullbackIsPullback g (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 x.fst))) (CategoryTheory.Limits.PullbackCone.flipIsLimit (CategoryTheory.Limits.pullbackIsPullback CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd)) }).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 x.fst)) g (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f) g (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback f (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 x.fst))) (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 x.fst)) (CategoryTheory.CategoryStruct.id Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback f (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 x.fst))) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f)) (_ : CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id Y) g)) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f) g f g CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map (AlgebraicGeometry.Scheme.OpenCover.pullbackCover 𝒰 f) x.fst) f) (CategoryTheory.CategoryStruct.id Z) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map (AlgebraicGeometry.Scheme.OpenCover.pullbackCover 𝒰 f) x.fst) f) (_ : CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id Y) g))))

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

(Implementation). Use openCoverOfBase instead.

@[simp]

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

@[simp]

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

@[simp]

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

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

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.

instance AlgebraicGeometry.Scheme.pullback_map_isOpenImmersion {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme} {X' : AlgebraicGeometry.Scheme} {Y' : AlgebraicGeometry.Scheme} {S' : AlgebraicGeometry.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') [AlgebraicGeometry.IsOpenImmersion i₁] [AlgebraicGeometry.IsOpenImmersion i₂] [CategoryTheory.Mono i₃] : AlgebraicGeometry.IsOpenImmersion (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂)