Theorems · Theorem · category theory

CategoryTheory.Precoverage.ZeroHypercover.isPullback_of_forall_isPullback

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C}
  [J.toGrothendieck.Subcanonical] [inst_2 : CategoryTheory.Limits.HasPullbacks C] [J.IsStableUnderBaseChange]
  {P X Y Z : C} (fst : P ⟶ X) (snd : P ⟶ Y) (f : X ⟶ Z) (g : Y ⟶ Z) (𝒰 : J.ZeroHypercover X),
  (∀ (i : 𝒰.I₀),
      CategoryTheory.IsPullback (CategoryTheory.Limits.pullback.snd fst (𝒰.f i))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst fst (𝒰.f i)) snd)
        (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) →
    CategoryTheory.IsPullback fst snd f g

To show that `` P > X | | v v Y > Z ` is a pullback square, it suffices to check that ` P ×[X] Uᵢ > Uᵢ | | v v Y --> Z ` is a pullback square for all Uᵢ in a cover of X` for some subcanonical topology.

Defined in

Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.GrothendieckTopology.SubcanonicalCategoryTheory.Limits.HasPullbacksCategoryTheory.Precoverage.IsStableUnderBaseChange