Theorems · Definition · category theory

CategoryTheory.PreZeroHypercover.inter

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {T : C} →
      (E : CategoryTheory.PreZeroHypercover T) →
        (F : CategoryTheory.PreZeroHypercover T) →
          [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] →
            CategoryTheory.PreZeroHypercover T

Pairwise intersection of two pre-0-hypercovers.

Defined in

Mathlib.CategoryTheory.Sites.Hypercover.Zero

Cited by

18 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasPullback