Documentation

Mathlib.AlgebraicGeometry.Pullbacks

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

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

Equations
Instances For

    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.
    Instances For
      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
      @[reducible, inline]

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

      Equations
      Instances For

        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.
        Instances For
          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
          @[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) :
          @[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]
          @[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

          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.
          Instances For

            The first projection from the glued scheme into X.

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

              The second projection from the glued scheme into Y.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                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.
                Instances For
                  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

                  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.
                  Instances For
                    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) :

                    (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.
                    Instances For
                      @[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

                      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.
                      Instances For
                        @[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
                        @[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

                        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.
                        Instances For

                          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.
                          Instances For

                            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.
                            Instances For
                              @[simp]
                              @[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) :
                              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) :

                              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.
                              Instances For
                                @[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)); 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) , isLimit := this }).inv (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) )))

                                (Implementation). Use openCoverOfBase instead.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[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)

                                  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.
                                  Instances For