Theorems · Definition · category theory

CategoryTheory.PreZeroHypercover.restrictIndex

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {T : C} → (E : CategoryTheory.PreZeroHypercover T) → {ι : Type w'} → (ι → E.I₀) → CategoryTheory.PreZeroHypercover T

Restrict the indexing type to ι by precomposing with a function ι → E.I₀.

Defined in

Mathlib.CategoryTheory.Sites.Hypercover.Zero

Cited by

11 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

CategoryTheory.Category