Theorems · Theorem · category theory

CategoryTheory.Precoverage.mem_coverings_of_isPullback

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.IsStableUnderBaseChange]
  {ι : Type w} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S),
  CategoryTheory.Presieve.ofArrows X f ∈ J.coverings S →
    ∀ {Y : C} (g : Y ⟶ S) {P : ι → C} (p₁ : (i : ι) → P i ⟶ Y) (p₂ : (i : ι) → P i ⟶ X i),
      (∀ (i : ι), CategoryTheory.IsPullback (p₁ i) (p₂ i) g (f i)) →
        CategoryTheory.Presieve.ofArrows P p₁ ∈ J.coverings Y

Defined in

Mathlib.CategoryTheory.Sites.Precoverage

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Precoverage.IsStableUnderBaseChange