# Documentation

Mathlib.CategoryTheory.Sites.Over

Localization

In this file, given a Grothendieck topology J on a category C and X : C, we construct a Grothendieck topology J.over X on the category Over X. In order to do this, we first construct a bijection Sieve.overEquiv Y : Sieve Y ≃ Sieve Y.left for all Y : Over X. Then, as it is stated in SGA 4 III 5.2.1, a sieve of Y : Over X is covering for J.over X if and only if the corresponding sieve of Y.left is covering for J. As a result, the forgetful functor Over.forget X : Over X ⥤ X is both cover-preserving and cover-lifting.

def CategoryTheory.Sieve.overEquiv {C : Type u} {X : C} (Y : ) :

The equivalence Sieve Y ≃ Sieve Y.left for all Y : Over X.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Sieve.overEquiv_top {C : Type u} {X : C} (Y : ) :
@[simp]
theorem CategoryTheory.Sieve.overEquiv_symm_top {C : Type u} {X : C} (Y : ) :
.symm =
theorem CategoryTheory.Sieve.overEquiv_pullback {C : Type u} {X : C} {Y₁ : } {Y₂ : } (f : Y₁ Y₂) (S : ) :
@[simp]
theorem CategoryTheory.Sieve.overEquiv_symm_iff {C : Type u} {X : C} {Y : } (S : CategoryTheory.Sieve Y.left) {Z : } (f : Z Y) :
(.symm S).arrows f S.arrows f.left
theorem CategoryTheory.Sieve.overEquiv_iff {C : Type u} {X : C} {Y : } (S : ) {Z : C} (f : Z Y.left) :
().arrows f S.arrows
@[simp]
theorem CategoryTheory.Sieve.functorPushforward_over_map {C : Type u} {X : C} {Y : C} (f : X Y) (Z : ) (S : CategoryTheory.Sieve Z.left) :
= ().symm S

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.GrothendieckTopology.mem_over_iff {C : Type u} {X : C} {Y : } (S : ) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
@[inline, reducible]
abbrev CategoryTheory.GrothendieckTopology.overPullback {C : Type u} (A : Type u') [] (X : C) :

The pullback functor Sheaf J A ⥤ Sheaf (J.over X) A

Equations
Instances For
Equations
• One or more equations did not get rendered due to their size.
@[inline, reducible]
abbrev CategoryTheory.GrothendieckTopology.overMapPullback {C : Type u} (A : Type u') [] {X : C} {Y : C} (f : X Y) :

The pullback functor Sheaf (J.over Y) A ⥤ Sheaf (J.over X) A induced by a morphism f : X ⟶ Y.

Equations
• One or more equations did not get rendered due to their size.
Instances For