Theorems · Definition · category theory

CategoryTheory.PreOneHypercover.inter

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      (E : CategoryTheory.PreOneHypercover S) →
        (F : CategoryTheory.PreOneHypercover S) →
          [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] →
            [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b),
                  CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i))
                    (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))] →
              CategoryTheory.PreOneHypercover S

Intersection of two pre-1-hypercovers.

Defined in

Mathlib.CategoryTheory.Sites.Hypercover.One

Cited by

12 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasPullbackCategoryTheory.Limits.HasPullback