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₁ : CategoryTheory.Over X} {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 : C} {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).toPrefunctor.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 ∈ (CategoryTheory.GrothendieckTopology.over J X).sieves Y ↔ (CategoryTheory.Sieve.overEquiv Y) S ∈ J.sieves 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.sieves Y.left) : (CategoryTheory.Sieve.overEquiv Y).symm S ∈ (CategoryTheory.GrothendieckTopology.over J X).sieves Y

theorem CategoryTheory.GrothendieckTopology.over_forget_coverPreserving {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (X : C) : CategoryTheory.CoverPreserving (CategoryTheory.GrothendieckTopology.over J 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.instIsCocontinuousOverInstCategoryOverForgetOver {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (X : C) : CategoryTheory.Functor.IsCocontinuous (CategoryTheory.Over.forget X) (CategoryTheory.GrothendieckTopology.over J X) J

Equations

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

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

Equations

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

@[inline, reducible]

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 (CategoryTheory.GrothendieckTopology.over J X) A)

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

Equations

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

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

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

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

Equations

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

@[inline, reducible]

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 : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.Functor (CategoryTheory.Sheaf (CategoryTheory.GrothendieckTopology.over J Y) A) (CategoryTheory.Sheaf (CategoryTheory.GrothendieckTopology.over J X) A)

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.