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} [CategoryTheory.Category.{v, u} C] {X : C} (Y : CategoryTheory.Over X) : CategoryTheory.Sieve Y ≃ CategoryTheory.Sieve Y.left

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.

@[simp]

theorem CategoryTheory.Sieve.overEquiv_top {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (Y : CategoryTheory.Over X) : (CategoryTheory.Sieve.overEquiv Y) ⊤ = ⊤

@[simp]

theorem CategoryTheory.Sieve.overEquiv_symm_top {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} (Y : CategoryTheory.Over X) : (CategoryTheory.Sieve.overEquiv Y).symm ⊤ = ⊤

theorem CategoryTheory.Sieve.overEquiv_pullback {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y₁ Y₂ : CategoryTheory.Over X} (f : Y₁ ⟶ Y₂) (S : CategoryTheory.Sieve Y₂) : (CategoryTheory.Sieve.overEquiv Y₁) (CategoryTheory.Sieve.pullback f S) = CategoryTheory.Sieve.pullback f.left ((CategoryTheory.Sieve.overEquiv Y₂) S)

@[simp]

theorem CategoryTheory.Sieve.overEquiv_symm_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : CategoryTheory.Over X} (S : CategoryTheory.Sieve Y.left) {Z : CategoryTheory.Over X} (f : Z ⟶ Y) : ((CategoryTheory.Sieve.overEquiv Y).symm S).arrows f ↔ S.arrows f.left

theorem CategoryTheory.Sieve.overEquiv_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : CategoryTheory.Over X} (S : CategoryTheory.Sieve Y) {Z : C} (f : Z ⟶ Y.left) : ((CategoryTheory.Sieve.overEquiv Y) S).arrows f ↔ S.arrows (CategoryTheory.Over.homMk f ⋯)

@[simp]

theorem CategoryTheory.Sieve.functorPushforward_over_map {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : CategoryTheory.Over X) (S : CategoryTheory.Sieve Z.left) : CategoryTheory.Sieve.functorPushforward (CategoryTheory.Over.map f) ((CategoryTheory.Sieve.overEquiv Z).symm S) = (CategoryTheory.Sieve.overEquiv ((CategoryTheory.Over.map f).obj Z)).symm S

def CategoryTheory.GrothendieckTopology.over {C : Type u} [CategoryTheory.Category.{v, u} C] (J : 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.

Equations

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

theorem CategoryTheory.GrothendieckTopology.mem_over_iff {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {X : C} {Y : CategoryTheory.Over X} (S : CategoryTheory.Sieve Y) : S ∈ (J.over X) Y ↔ (CategoryTheory.Sieve.overEquiv Y) S ∈ J Y.left

theorem CategoryTheory.GrothendieckTopology.overEquiv_symm_mem_over {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {X : C} (Y : CategoryTheory.Over X) (S : CategoryTheory.Sieve Y.left) (hS : S ∈ J Y.left) : (CategoryTheory.Sieve.overEquiv Y).symm S ∈ (J.over X) Y

theorem CategoryTheory.GrothendieckTopology.over_forget_coverPreserving {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (X : C) : CategoryTheory.CoverPreserving (J.over X) J (CategoryTheory.Over.forget X)

theorem CategoryTheory.GrothendieckTopology.over_forget_compatiblePreserving {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (X : C) : CategoryTheory.CompatiblePreserving J (CategoryTheory.Over.forget X)

instance CategoryTheory.GrothendieckTopology.instIsCocontinuousOverForgetOver {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (X : C) : (CategoryTheory.Over.forget X).IsCocontinuous (J.over X) J

Equations

• ⋯ = ⋯

instance CategoryTheory.GrothendieckTopology.instIsContinuousOverForgetOver {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (X : C) : (CategoryTheory.Over.forget X).IsContinuous (J.over X) J

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev CategoryTheory.GrothendieckTopology.overPullback {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u') [CategoryTheory.Category.{v', u'} A] (X : C) : CategoryTheory.Functor (CategoryTheory.Sheaf J A) (CategoryTheory.Sheaf (J.over X) A)

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

Equations

• J.overPullback A X = (CategoryTheory.Over.forget X).sheafPushforwardContinuous A (J.over X) J

theorem CategoryTheory.GrothendieckTopology.over_map_coverPreserving {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {X Y : C} (f : X ⟶ Y) : CategoryTheory.CoverPreserving (J.over X) (J.over Y) (CategoryTheory.Over.map f)

theorem CategoryTheory.GrothendieckTopology.over_map_compatiblePreserving {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {X Y : C} (f : X ⟶ Y) : CategoryTheory.CompatiblePreserving (J.over Y) (CategoryTheory.Over.map f)

instance CategoryTheory.GrothendieckTopology.instIsContinuousOverMapOver {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {X Y : C} (f : X ⟶ Y) : (CategoryTheory.Over.map f).IsContinuous (J.over X) (J.over Y)

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev CategoryTheory.GrothendieckTopology.overMapPullback {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u') [CategoryTheory.Category.{v', u'} A] {X Y : C} (f : X ⟶ Y) : CategoryTheory.Functor (CategoryTheory.Sheaf (J.over Y) A) (CategoryTheory.Sheaf (J.over X) A)

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 = (CategoryTheory.Over.map f).sheafPushforwardContinuous A (J.over X) (J.over Y)

@[reducible, inline]

abbrev CategoryTheory.Sheaf.over {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] (F : CategoryTheory.Sheaf J A) (X : C) : CategoryTheory.Sheaf (J.over X) A

Given F : Sheaf J A and X : C, this is the pullback of F on J.over X.

Equations

• F.over X = (J.overPullback A X).obj F