Theorems · Definition · category theory

CategoryTheory.Precoverage.toGrothendieck

{C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] → CategoryTheory.Precoverage C → CategoryTheory.GrothendieckTopology C

The Grothendieck topology associated to a precoverage J. It is defined inductively as follows: 1. If S is a covering presieve for J, 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 pullback stability condition of a Grothendieck topology. 4. Add all sieves required by the local character axiom of a Grothendieck topology.

Defined in

Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Cited by

41 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category