Theorems · Definition · category theory

CategoryTheory.GrothendieckTopology.toCoverage

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.GrothendieckTopology C → CategoryTheory.Coverage C

Associate a coverage to any Grothendieck topology. If J is a Grothendieck topology, and K is the associated coverage, then a presieve S is a covering presieve for K if and only if the sieve that it generates is a covering sieve for J.

Defined in

Mathlib.CategoryTheory.Sites.Coverage

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category