Theorems · Definition · category theory

CategoryTheory.PreZeroHypercover.sectionsEquivOfHasPullbacks

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {S : C} →
      (E : CategoryTheory.PreZeroHypercover S) →
        [inst_1 : E.HasPullbacks] →
          (F : CategoryTheory.Functor Cᵒᵖ (Type u_2)) →
            (E.toPreOneHypercover.multicospanIndex F).sections ≃
              Subtype (CategoryTheory.Presieve.Arrows.Compatible F E.f)

If the pre-0-hypercover E has pairwise pullbacks, the sections over the multifork associated to a presheaf of types are equivalent to the compatible families on E.

Defined in

Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.PreZeroHypercover.HasPullbacks