Theorems · Definition · category theory

CategoryTheory.Coverage.toGrothendieck

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

The Grothendieck topology associated to a coverage K. It is defined inductively as follows: 1. If S is a covering presieve for K, then the sieve generated by S is a covering sieve for the associated Grothendieck topology. 2. The top sieves are in the associated Grothendieck topology. 3. Add all sieves required by the local character axiom of a Grothendieck topology. The pullback compatibility condition for a coverage ensures that the associated Grothendieck topology is pullback stable, and so an additional constructor in the inductive construction is not needed.

Defined in

Mathlib.CategoryTheory.Sites.Coverage

Cited by

15 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category