Theorems · Inductive type · category theory

CategoryTheory.Coverage

(C : Type u_1) → [CategoryTheory.Category.{v_1, u_1} C] → Type (max u_1 v_1)

The type Coverage C of coverages on C. A coverage is a collection of covering presieves on every object X : C, which satisfies a pullback compatibility condition. Explicitly, this condition says that whenever S is a covering presieve for X and f : Y ⟶ X is a morphism, then there exists some covering presieve T for Y such that T factors through S along f.

Defined in

Mathlib.CategoryTheory.Sites.Coverage

Cited by

31 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

CategoryTheory.Category