Theorems · Definition · category theory

CategoryTheory.GrothendieckTopology.over

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.GrothendieckTopology C → (X : C) → CategoryTheory.GrothendieckTopology (CategoryTheory.Over X)

The Grothendieck topology on the category Over X for any X : C that is induced by a Grothendieck topology on C.

Defined in

Mathlib.CategoryTheory.Sites.Over

Cited by

115 results in Mathlib

Foundations

Depth 40 from the axioms, rests on 372 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category