Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Pullback.diagonalCover_map

∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover)
  (𝒱 :
    (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).I₀) →
      ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i).OpenCover)
  (I : (AlgebraicGeometry.Scheme.Pullback.diagonalCover f 𝒰 𝒱).I₀),
  (AlgebraicGeometry.Scheme.Pullback.diagonalCover f 𝒰 𝒱).f I =
    CategoryTheory.Limits.pullback.map
      (CategoryTheory.CategoryStruct.comp ((𝒱 I.fst).f I.snd.1) (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f I.fst))
      (CategoryTheory.CategoryStruct.comp ((𝒱 I.fst).f I.snd.2) (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f I.fst))
      f f (CategoryTheory.CategoryStruct.comp ((𝒱 I.fst).f I.snd.1) (CategoryTheory.Limits.pullback.fst f (𝒰.f I.fst)))
      (CategoryTheory.CategoryStruct.comp ((𝒱 I.fst).f I.snd.2) (CategoryTheory.Limits.pullback.fst f (𝒰.f I.fst)))
      (𝒰.f I.fst) ⋯ ⋯

Defined in

Mathlib.AlgebraicGeometry.Pullbacks

Cited by

2 results in Mathlib

Foundations

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