Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_f

∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : Z.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z) (i : 𝒰.I₀),
  (AlgebraicGeometry.Scheme.Pullback.openCoverOfBase 𝒰 f g).f i =
    CategoryTheory.Limits.pullback.map (CategoryTheory.Limits.pullback.snd f (𝒰.f i))
      (CategoryTheory.Limits.pullback.snd g (𝒰.f i)) f g (CategoryTheory.Limits.pullback.fst f (𝒰.f i))
      (CategoryTheory.Limits.pullback.fst g (𝒰.f i)) (𝒰.f i) ⋯ ⋯

Defined in

Mathlib.AlgebraicGeometry.Pullbacks

Cited by

0 results in Mathlib

Foundations

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