Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Pullback.t_snd_assoc

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

Defined in

Mathlib.AlgebraicGeometry.Pullbacks

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Limits.HasPullback