Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Pullback.pullbackP1Iso

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

Defined in

Mathlib.AlgebraicGeometry.Pullbacks

Cited by

10 results in Mathlib

Foundations

Depth 158 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Limits.HasPullback