Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Cover.pullbackHom_map_assoc

∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] {X W : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) (f : W ⟶ X)
  [inst_2 : ∀ (x : 𝒰.I₀), CategoryTheory.Limits.HasPullback f (𝒰.f x)] (i : 𝒰.toPreZeroHypercover.1)
  {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (𝒰.pullbackHom f i) (CategoryTheory.CategoryStruct.comp (𝒰.f i) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i)
      (CategoryTheory.CategoryStruct.comp f h)

Defined in

Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.MorphismProperty.IsStableUnderBaseChangeAlgebraicGeometry.Scheme.IsJointlySurjectivePreservingCategoryTheory.Limits.HasPullback