Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Pullback.t_snd

∀ {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₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t 𝒰 f g i j)
      (CategoryTheory.Limits.pullback.snd
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) (𝒰.f j))
        (𝒰.f i)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
        (𝒰.f j))
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g)

Defined in

Mathlib.AlgebraicGeometry.Pullbacks

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Limits.HasPullback