Theorems · Definition · category theory

CategoryTheory.Precoverage.ZeroHypercover.singleton

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Precoverage C} →
      {S T : C} → (f : S ⟶ T) → CategoryTheory.Presieve.singleton f ∈ J.coverings T → J.ZeroHypercover T

The 0-hypercover defined by a single covering morphism.

Defined in

Mathlib.CategoryTheory.Sites.Hypercover.Zero

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category