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} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.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ⱼ

Equations

• AlgebraicGeometry.Scheme.Pullback.v 𝒰 f g i j = CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (𝒰.map i)) (𝒰.map j)

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

Equations

• One or more equations did not get rendered due to their size.

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

@[reducible, inline]

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

Equations

• AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j = CategoryTheory.Limits.pullback.fst

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

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_fst_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z✝) (g : Y ⟶ Z✝) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) (j : 𝒰.J) (k : 𝒰.J) {Z : AlgebraicGeometry.Scheme} (h : 𝒰.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} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.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} (𝒰 : X.OpenCover) (f : X ⟶ Z✝) (g : Y ⟶ Z✝) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.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} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.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} (𝒰 : X.OpenCover) (f : X ⟶ Z✝) (g : Y ⟶ Z✝) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) (j : 𝒰.J) (k : 𝒰.J) {Z : AlgebraicGeometry.Scheme} (h : 𝒰.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} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.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} (𝒰 : X.OpenCover) (f : X ⟶ Z✝) (g : Y ⟶ Z✝) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) (j : 𝒰.J) (k : 𝒰.J) {Z : AlgebraicGeometry.Scheme} (h : 𝒰.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} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.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} (𝒰 : X.OpenCover) (f : X ⟶ Z✝) (g : Y ⟶ Z✝) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.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} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.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} (𝒰 : X.OpenCover) (f : X ⟶ Z✝) (g : Y ⟶ Z✝) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) (j : 𝒰.J) (k : 𝒰.J) {Z : AlgebraicGeometry.Scheme} (h : 𝒰.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} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.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} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.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} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.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} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.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} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.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} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.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} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.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} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.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_V {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] : ∀ (x : 𝒰.J × 𝒰.J), (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).V x = match x with | (i, j) => AlgebraicGeometry.Scheme.Pullback.v 𝒰 f g i j

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

The first projection from the glued scheme into X.

Equations

• One or more equations did not get rendered due to their size.

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

The second projection from the glued scheme into Y.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.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 : 𝒰.J) {Z : AlgebraicGeometry.Scheme} (h : CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (𝒰.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 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_fst {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.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 : 𝒰.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 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_snd_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.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 : 𝒰.J) {Z : AlgebraicGeometry.Scheme} (h : 𝒰.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} (𝒰 : 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 : 𝒰.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} (𝒰 : 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 ⟶ (AlgebraicGeometry.Scheme.Pullback.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.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.Pullback.gluedLift_p1 {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.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 (AlgebraicGeometry.Scheme.Pullback.gluedLift 𝒰 f g s) (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) = s.fst

theorem AlgebraicGeometry.Scheme.Pullback.gluedLift_p2 {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.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 (AlgebraicGeometry.Scheme.Pullback.gluedLift 𝒰 f g s) (AlgebraicGeometry.Scheme.Pullback.p2 𝒰 f g) = s.snd

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

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.Pullback.pullbackFstιToV_fst_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z✝) (g : Y ⟶ Z✝) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) (j : 𝒰.J) {Z : AlgebraicGeometry.Scheme} (h : CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (𝒰.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} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.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} (𝒰 : X.OpenCover) (f : X ⟶ Z✝) (g : Y ⟶ Z✝) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) (j : 𝒰.J) {Z : AlgebraicGeometry.Scheme} (h : 𝒰.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} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.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} (𝒰 : 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 (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.p2 𝒰 f g)) ⋯) ((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} (𝒰 : 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 (AlgebraicGeometry.Scheme.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.

Equations

• One or more equations did not get rendered due to their size.

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

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_fst {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.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 (AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso 𝒰 f g i).inv CategoryTheory.Limits.pullback.fst = (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).ι i

theorem AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso_inv_snd_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z✝) (g : Y ⟶ Z✝) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) {Z : AlgebraicGeometry.Scheme} (h : 𝒰.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} (𝒰 : 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 (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} (𝒰 : X.OpenCover) (f : X ⟶ Z✝) (g : Y ⟶ Z✝) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) g] (i : 𝒰.J) {Z : AlgebraicGeometry.Scheme} (h : (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).glued ⟶ Z) : CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso 𝒰 f g i).hom (CategoryTheory.CategoryStruct.comp ((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} (𝒰 : 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 (AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso 𝒰 f g i).hom ((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} (𝒰 : 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 (AlgebraicGeometry.Scheme.Pullback.p1 𝒰 f g) (AlgebraicGeometry.Scheme.Pullback.p2 𝒰 f g) ⋯)

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

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.Pullback.hasPullback_of_cover {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.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 : 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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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 : Z.affineCover.J) : CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp ((Z.affineCover.pullbackCover f).map i) f) g

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• AlgebraicGeometry.Scheme.Pullback.instHasPullbacks = ⋯

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)

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

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

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft_map {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (i : 𝒰.J) : (AlgebraicGeometry.Scheme.Pullback.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.openCoverOfLeft {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.openCoverOfRight_map {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : Y.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (i : 𝒰.J) : (AlgebraicGeometry.Scheme.Pullback.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) ⋯ ⋯

def AlgebraicGeometry.Scheme.Pullback.openCoverOfRight {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.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ᵢ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight_obj {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰X : X.OpenCover) (𝒰Y : Y.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (ij : 𝒰X.J × 𝒰Y.J) : (AlgebraicGeometry.Scheme.Pullback.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 : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰X : X.OpenCover) (𝒰Y : Y.OpenCover) (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 : X.OpenCover) (𝒰Y : Y.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (ij : 𝒰X.J × 𝒰Y.J) : (AlgebraicGeometry.Scheme.Pullback.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) ⋯ ⋯

def AlgebraicGeometry.Scheme.Pullback.openCoverOfLeftRight {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.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ⱼ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

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

(Implementation). Use openCoverOfBase instead.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

def AlgebraicGeometry.Scheme.Pullback.openCoverOfBase {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.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.

Equations

• One or more equations did not get rendered due to their size.

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₂)

Equations

• ⋯ = ⋯