Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Pullback.openCoverOfBase

{X Y Z : AlgebraicGeometry.Scheme} →
  Z.OpenCover → (f : X ⟶ Z) → (g : Y ⟶ Z) → (CategoryTheory.Limits.pullback f g).OpenCover

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.

Defined in

Mathlib.AlgebraicGeometry.Pullbacks

Cited by

6 results in Mathlib

Foundations

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