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.

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

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.

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

      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

      Instances For
        @[simp]
        theorem AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_fst {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f) g] (i : 𝒰.J) (j : 𝒰.J) (k : 𝒰.J) :
        CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd
        theorem AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_snd_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f) g] (i : 𝒰.J) (j : 𝒰.J) (k : 𝒰.J) {Z : AlgebraicGeometry.Scheme} (h : Y Z) :
        CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h))) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h))
        @[simp]
        theorem AlgebraicGeometry.Scheme.Pullback.t'_fst_fst_snd {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f) g] (i : 𝒰.J) (j : 𝒰.J) (k : 𝒰.J) :
        CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd)
        @[simp]
        theorem AlgebraicGeometry.Scheme.Pullback.t'_fst_snd {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f) g] (i : 𝒰.J) (j : 𝒰.J) (k : 𝒰.J) :
        CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd
        @[simp]
        theorem AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_fst {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f) g] (i : 𝒰.J) (j : 𝒰.J) (k : 𝒰.J) :
        CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd
        theorem AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_snd_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f) g] (i : 𝒰.J) (j : 𝒰.J) (k : 𝒰.J) {Z : AlgebraicGeometry.Scheme} (h : Y Z) :
        CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h))) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h))
        @[simp]
        theorem AlgebraicGeometry.Scheme.Pullback.t'_snd_fst_snd {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f) g] (i : 𝒰.J) (j : 𝒰.J) (k : 𝒰.J) :
        CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd)
        @[simp]
        theorem AlgebraicGeometry.Scheme.Pullback.t'_snd_snd {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f) g] (i : 𝒰.J) (j : 𝒰.J) (k : 𝒰.J) :
        CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst)
        theorem AlgebraicGeometry.Scheme.Pullback.cocycle_fst_fst_fst {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f) g] (i : 𝒰.J) (j : 𝒰.J) (k : 𝒰.J) :
        CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g j k i) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g k i j) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst)))) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst)
        theorem AlgebraicGeometry.Scheme.Pullback.cocycle_fst_fst_snd {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f) g] (i : 𝒰.J) (j : 𝒰.J) (k : 𝒰.J) :
        CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g j k i) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g k i j) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd)))) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd)
        theorem AlgebraicGeometry.Scheme.Pullback.cocycle_snd_fst_fst {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f) g] (i : 𝒰.J) (j : 𝒰.J) (k : 𝒰.J) :
        CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g j k i) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g k i j) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst)))) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst)
        theorem AlgebraicGeometry.Scheme.Pullback.cocycle_snd_fst_snd {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f) g] (i : 𝒰.J) (j : 𝒰.J) (k : 𝒰.J) :
        CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g j k i) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g k i j) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd)))) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd)
        theorem AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst_assoc {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f) g] (s : CategoryTheory.Limits.PullbackCone f g) (i : 𝒰.J) (j : 𝒰.J) {Z : AlgebraicGeometry.Scheme} (h : CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f) g Z) :
        theorem AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover X) (f : X Z) (g : Y Z) [∀ (i : 𝒰.J), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) f) g] (s : CategoryTheory.Limits.PullbackCone f g) (i : 𝒰.J) (j : 𝒰.J) :

        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.

        Instances For

          (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_ι.

          Instances For

            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

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

            Instances For

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

              Instances For

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

                Instances For
                  @[simp]
                  theorem AlgebraicGeometry.Scheme.Pullback.openCoverOfBase'_map {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover Z) (f : X Z) (g : Y Z) (x : (i : (AlgebraicGeometry.Scheme.Pullback.openCoverOfLeft (AlgebraicGeometry.Scheme.OpenCover.pullbackCover 𝒰 f) f g).J) × ((fun i => let Xᵢ := CategoryTheory.Limits.pullback f (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i); let Yᵢ := CategoryTheory.Limits.pullback g (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i); let W := CategoryTheory.Limits.pullback CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd; let_fun this := CategoryTheory.Limits.bigSquareIsPullback CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd g (_ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd) (_ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst g) (CategoryTheory.Limits.PullbackCone.flipIsLimit (CategoryTheory.Limits.pullbackIsPullback g (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i))) (CategoryTheory.Limits.PullbackCone.flipIsLimit (CategoryTheory.Limits.pullbackIsPullback CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd)); AlgebraicGeometry.Scheme.openCoverOfIsIso (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.isoLimitCone { cone := CategoryTheory.Limits.PullbackCone.mk CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst) (_ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst) g), isLimit := this }).inv (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i)) g (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map (AlgebraicGeometry.Scheme.OpenCover.pullbackCover 𝒰 f) i) f) g (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback f (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i))) (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i)) (CategoryTheory.CategoryStruct.id Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback f (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i))) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map (AlgebraicGeometry.Scheme.OpenCover.pullbackCover 𝒰 f) i) f)) (_ : CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id Y) g))))) i).J) :
                  AlgebraicGeometry.Scheme.OpenCover.map (AlgebraicGeometry.Scheme.Pullback.openCoverOfBase' 𝒰 f g) x = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.isoLimitCone { cone := CategoryTheory.Limits.PullbackCone.mk CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd) (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 x.fst) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst) g), isLimit := CategoryTheory.Limits.bigSquareIsPullback CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 x.fst) CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd g (_ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd) (_ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 x.fst) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst g) (CategoryTheory.Limits.PullbackCone.flipIsLimit (CategoryTheory.Limits.pullbackIsPullback g (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 x.fst))) (CategoryTheory.Limits.PullbackCone.flipIsLimit (CategoryTheory.Limits.pullbackIsPullback CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd)) }).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 x.fst)) g (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f) g (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback f (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 x.fst))) (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 x.fst)) (CategoryTheory.CategoryStruct.id Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback f (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 x.fst))) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f)) (_ : CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id Y) g)) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f) g f g CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.CategoryStruct.id Z) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map (AlgebraicGeometry.Scheme.OpenCover.pullbackCover 𝒰 f) x.fst) f) (CategoryTheory.CategoryStruct.id Z) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.map (AlgebraicGeometry.Scheme.OpenCover.pullbackCover 𝒰 f) x.fst) f) (_ : CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id Z) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id Y) g))))
                  @[simp]
                  theorem AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_map {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.OpenCover Z) (f : X Z) (g : Y Z) (i : 𝒰.J) :
                  AlgebraicGeometry.Scheme.OpenCover.map (AlgebraicGeometry.Scheme.Pullback.openCoverOfBase 𝒰 f g) i = CategoryTheory.Limits.pullback.map CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd f g CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) (_ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f) (_ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.OpenCover.map 𝒰 i) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst g)

                  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.

                  Instances For