Theorems · Definition · category theory

CategoryTheory.PreZeroHypercover.toPreOneHypercover

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} → (E : CategoryTheory.PreZeroHypercover S) → [E.HasPullbacks] → CategoryTheory.PreOneHypercover S

If the pairwise pullbacks exist, this is the pre-1-hypercover where the covers by the pullbacks are given by the pullbacks themselves.

Defined in

Mathlib.CategoryTheory.Sites.Hypercover.One

Cited by

23 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.PreZeroHypercover.HasPullbacks