Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Pullback.t

{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 j : 𝒰.I₀) → 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.

Defined in

Mathlib.AlgebraicGeometry.Pullbacks

Cited by

15 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Limits.HasPullback