Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap_fst

∀ {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.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.gluedLiftPullbackMap 𝒰 f g s i j)
      (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.Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f i)
        ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ s.fst 𝒰).f j))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry s.fst (𝒰.f i)).hom
        (CategoryTheory.Limits.pullback.map (𝒰.f i) s.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g
          (CategoryTheory.CategoryStruct.id (𝒰.X i)) s.snd f ⋯ ⋯))

Defined in

Mathlib.AlgebraicGeometry.Pullbacks

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Limits.HasPullback