Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap

{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] →
          (s : CategoryTheory.Limits.PullbackCone f g) →
            (i j : 𝒰.I₀) →
              CategoryTheory.Limits.pullback ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
                  ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j) ⟶
                (AlgebraicGeometry.Scheme.Pullback.gluing 𝒰 f g).V (i, j)

(Implementation) The canonical map (s.X ×[X] Uᵢ) ×[s.X] (s.X ×[X] Uⱼ) ⟶ (Uᵢ ×[Z] Y) ×[X] Uⱼ This is used in gluedLift.

Defined in

Mathlib.AlgebraicGeometry.Pullbacks

Cited by

4 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Limits.HasPullback