Theorems · Inductive type · category theory

CategoryTheory.GrothendieckTopology

(C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max u v)

The definition of a Grothendieck topology: a set of sieves J X on each object X satisfying three axioms: 1. For every object X, the maximal sieve is in J X. 2. If S ∈ J X then its pullback along any h : Y ⟶ X is in J Y. 3. If S ∈ J X and R is a sieve on X, then provided that the pullback of R along any arrow f : Y ⟶ X in S is in J Y, we have that R itself is in J X. A sieve S on X is referred to as J-covering, (or just covering), if S ∈ J X. See also [nlab] or [MM92] Chapter III, Section 2, Definition 1.

Defined in

Mathlib.CategoryTheory.Sites.Grothendieck

Cited by

1,415 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

CategoryTheory.Category