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

@[simp]

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

theorem CategoryTheory.Sieve.overEquiv_le_overEquiv_iff {C : Type u} [Category.{v, u} C] {X : C} {Y : Over X} (R₁ R₂ : Sieve Y) : (overEquiv Y) R₁ ≤ (overEquiv Y) R₂ ↔ R₁ ≤ R₂

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

@[simp]

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

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

@[simp]

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

def CategoryTheory.GrothendieckTopology.over {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (X : C) : GrothendieckTopology (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} [Category.{v, u} C] (J : GrothendieckTopology C) {X : C} {Y : Over X} (S : Sieve Y) : S ∈ (J.over X) Y ↔ (Sieve.overEquiv Y) S ∈ J Y.left

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

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

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

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

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

@[reducible, inline]

abbrev CategoryTheory.GrothendieckTopology.overPullback {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] (X : C) : Functor (Sheaf J A) (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} [Category.{v, u} C] (J : GrothendieckTopology C) {X Y : C} (f : X ⟶ Y) : CoverPreserving (J.over X) (J.over Y) (Over.map f)

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

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

@[reducible, inline]

abbrev CategoryTheory.GrothendieckTopology.overMapPullback {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] {X Y : C} (f : X ⟶ Y) : Functor (Sheaf (J.over Y) A) (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} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] (F : Sheaf J A) (X : C) : 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