Theorems · Theorem · category theory

CategoryTheory.over_toGrothendieck_eq_toGrothendieck_comap_forget

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (K : CategoryTheory.Precoverage C) [K.HasPullbacks]
  [K.IsStableUnderBaseChange] (X : C),
  K.toGrothendieck.over X = (CategoryTheory.Precoverage.comap (CategoryTheory.Over.forget X) K).toGrothendieck

The Grothendieck topology on Over X, obtained from localizing the topology generated by the precoverage K, is generated by the preimage of K.

Defined in

Mathlib.CategoryTheory.Sites.Over

Cited by

3 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Precoverage.HasPullbacksCategoryTheory.Precoverage.IsStableUnderBaseChange