Theorems · Theorem · category theory

CategoryTheory.Precoverage.ZeroHypercover.singleton_toPreZeroHypercover

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

Defined in

Mathlib.CategoryTheory.Sites.Hypercover.Zero

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category