# 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 : ) :
S (J.over X).sieves Y J.sieves Y.left
theorem CategoryTheory.GrothendieckTopology.overEquiv_symm_mem_over {C : Type u} {X : C} (Y : ) (S : CategoryTheory.Sieve Y.left) (hS : S J.sieves Y.left) :
.symm S (J.over X).sieves Y
instance CategoryTheory.GrothendieckTopology.instIsCocontinuousOverForgetOver {C : Type u} (X : C) :
.IsCocontinuous (J.over X) J
Equations
• =
instance CategoryTheory.GrothendieckTopology.instIsContinuousOverForgetOver {C : Type u} (X : C) :
.IsContinuous (J.over X) J
Equations
• =
@[reducible, inline]

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

Equations
• J.overPullback A X = .sheafPushforwardContinuous A (J.over X) J
Instances For
theorem CategoryTheory.GrothendieckTopology.over_map_coverPreserving {C : Type u} {X : C} {Y : C} (f : X Y) :
CategoryTheory.CoverPreserving (J.over X) (J.over Y)
instance CategoryTheory.GrothendieckTopology.instIsContinuousOverMapOver {C : Type u} {X : C} {Y : C} (f : X Y) :
.IsContinuous (J.over X) (J.over Y)
Equations
• =
@[reducible, inline]
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
• J.overMapPullback A f = .sheafPushforwardContinuous A (J.over X) (J.over Y)
Instances For