Theorems · Inductive type · category theory

CategoryTheory.Precoverage.ZeroHypercover.Small

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {J : CategoryTheory.Precoverage C} → {S : C} → J.ZeroHypercover S → Prop

A w-0-hypercover E is w'-small if there exists an indexing type ι in Type w' and a restriction map ι → E.I₀ such that the restriction of E to ι is still covering. Note: This is weaker than E.I₀ being w'-small. For example, every Zariski cover of X : Scheme.{u} is u-small, because X itself suffices as indexing type.

Defined in

Mathlib.CategoryTheory.Sites.Hypercover.Zero

Cited by

7 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

CategoryTheory.Category