Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Pullback.v

{X Y Z : AlgebraicGeometry.Scheme} →
  (𝒰 : X.OpenCover) →
    (f : X ⟶ Z) →
      (g : Y ⟶ Z) →
        [∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] →
          𝒰.I₀ → 𝒰.I₀ → AlgebraicGeometry.Scheme

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

Defined in

Mathlib.AlgebraicGeometry.Pullbacks

Cited by

34 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Limits.HasPullback