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.

@[simp]

theorem CategoryTheory.Presieve.map_functorPullback_overForget {C : Type u} [Category.{v, u} C] {X : C} {Y : Over X} (R : Presieve Y.left) : map (Over.forget X) (functorPullback (Over.forget X) R) = R

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.

@[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)

theorem CategoryTheory.Sieve.overEquiv_symm_pullback {C : Type u} [Category.{v, u} C] {X : C} {Y₁ Y₂ : Over X} (f : Y₁ ⟶ Y₂) (S : Sieve Y₂.left) : (overEquiv Y₁).symm (pullback f.left S) = pullback f ((overEquiv Y₂).symm 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 ⋯)

theorem CategoryTheory.Sieve.overEquiv_generate {C : Type u} [Category.{v, u} C] {X : C} {Y : Over X} (R : Presieve Y) : (overEquiv Y) (generate R) = generate (Presieve.functorPushforward (Over.forget X) R)

theorem CategoryTheory.Sieve.overEquiv_symm_generate {C : Type u} [Category.{v, u} C] {X : C} {Y : Over X} (R : Presieve Y.left) : (overEquiv Y).symm (generate R) = generate (Presieve.functorPullback (Over.forget X) R)

@[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.

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

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)

theorem CategoryTheory.GrothendieckTopology.coverPreserving_over_star {C : Type u'} [Category.{v_1, u'} C] [Limits.HasBinaryProducts C] {J : GrothendieckTopology C} (X : C) : CoverPreserving J (J.over X) (Over.star X)

instance CategoryTheory.GrothendieckTopology.instIsContinuousOverStarOver {C : Type u'} [Category.{v_1, u'} C] [Limits.HasBinaryProducts C] {J : GrothendieckTopology C} (X : C) : (Over.star X).IsContinuous J (J.over X)

@[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.

def CategoryTheory.GrothendieckTopology.overMapPullbackCongr {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] {X Y : C} {f g : X ⟶ Y} (h : f = g) : J.overMapPullback A f ≅ J.overMapPullback A g

Two identical morphisms give isomorphic overMapPullback functors on sheaves.

@[simp]

theorem CategoryTheory.GrothendieckTopology.overMapPullbackCongr_inv_app_val_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] {X Y : C} {f g : X ⟶ Y} (h : f = g) (M : Sheaf (J.over Y) A) (X✝ : (Over X)ᵒᵖ) : ((J.overMapPullbackCongr A h).inv.app M).val.app X✝ = M.val.map ((Over.mapCongr f g h).hom.app (Opposite.unop X✝)).op

@[simp]

theorem CategoryTheory.GrothendieckTopology.overMapPullbackCongr_hom_app_val_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] {X Y : C} {f g : X ⟶ Y} (h : f = g) (M : Sheaf (J.over Y) A) (X✝ : (Over X)ᵒᵖ) : ((J.overMapPullbackCongr A h).hom.app M).val.app X✝ = M.val.map ((Over.mapCongr f g h).inv.app (Opposite.unop X✝)).op

theorem CategoryTheory.GrothendieckTopology.overMapPullbackCongr_eq_eqToIso {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] {X Y : C} {f g : X ⟶ Y} (h : f = g) : J.overMapPullbackCongr A h = eqToIso ⋯

def CategoryTheory.GrothendieckTopology.overMapPullbackId {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] (X : C) : J.overMapPullback A (CategoryStruct.id X) ≅ Functor.id (Sheaf (J.over X) A)

Applying overMapPullback to the identity map gives the identity functor.

@[simp]

theorem CategoryTheory.GrothendieckTopology.overMapPullbackId_hom_app_val_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] (X : C) (X✝ : Sheaf (J.over X) A) (X✝¹ : (Over X)ᵒᵖ) : ((J.overMapPullbackId A X).hom.app X✝).val.app X✝¹ = X✝.val.map ((Over.mapId X).inv.app (Opposite.unop X✝¹)).op

@[simp]

theorem CategoryTheory.GrothendieckTopology.overMapPullbackId_inv_app_val_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] (X : C) (X✝ : Sheaf (J.over X) A) (X✝¹ : (Over X)ᵒᵖ) : ((J.overMapPullbackId A X).inv.app X✝).val.app X✝¹ = X✝.val.map ((Over.mapId X).hom.app (Opposite.unop X✝¹)).op

def CategoryTheory.GrothendieckTopology.overMapPullbackComp {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : (J.overMapPullback A g).comp (J.overMapPullback A f) ≅ J.overMapPullback A (CategoryStruct.comp f g)

The composition of two overMapPullback functors identifies to overMapPullback for the composition.

@[simp]

theorem CategoryTheory.GrothendieckTopology.overMapPullbackComp_inv_app_val_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (X✝ : Sheaf (J.over Z) A) (X✝¹ : (Over X)ᵒᵖ) : ((J.overMapPullbackComp A f g).inv.app X✝).val.app X✝¹ = X✝.val.map ((Over.mapComp f g).inv.app (Opposite.unop X✝¹)).op

@[simp]

theorem CategoryTheory.GrothendieckTopology.overMapPullbackComp_hom_app_val_app {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (X✝ : Sheaf (J.over Z) A) (X✝¹ : (Over X)ᵒᵖ) : ((J.overMapPullbackComp A f g).hom.app X✝).val.app X✝¹ = X✝.val.map ((Over.mapComp f g).hom.app (Opposite.unop X✝¹)).op

theorem CategoryTheory.GrothendieckTopology.overMapPullback_comp_id {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp (J.overMapPullbackComp A f (CategoryStruct.id Y)).inv (CategoryStruct.comp (Functor.whiskerRight (J.overMapPullbackId A Y).hom (J.overMapPullback A f)) (J.overMapPullback A f).leftUnitor.hom) = (J.overMapPullbackCongr A ⋯).hom

theorem CategoryTheory.GrothendieckTopology.overMapPullback_comp_id_assoc {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] {X Y : C} (f : X ⟶ Y) {Z : Functor (Sheaf (J.over Y) A) (Sheaf (J.over X) A)} (h : J.overMapPullback A f ⟶ Z) : CategoryStruct.comp (J.overMapPullbackComp A f (CategoryStruct.id Y)).inv (CategoryStruct.comp (Functor.whiskerRight (J.overMapPullbackId A Y).hom (J.overMapPullback A f)) (CategoryStruct.comp (J.overMapPullback A f).leftUnitor.hom h)) = CategoryStruct.comp (J.overMapPullbackCongr A ⋯).hom h

theorem CategoryTheory.GrothendieckTopology.overMapPullback_id_comp {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp (J.overMapPullbackComp A (CategoryStruct.id X) f).inv (CategoryStruct.comp ((J.overMapPullback A f).whiskerLeft (J.overMapPullbackId A X).hom) (J.overMapPullback A f).rightUnitor.hom) = (J.overMapPullbackCongr A ⋯).hom

theorem CategoryTheory.GrothendieckTopology.overMapPullback_id_comp_assoc {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] {X Y : C} (f : X ⟶ Y) {Z : Functor (Sheaf (J.over Y) A) (Sheaf (J.over X) A)} (h : J.overMapPullback A f ⟶ Z) : CategoryStruct.comp (J.overMapPullbackComp A (CategoryStruct.id X) f).inv (CategoryStruct.comp ((J.overMapPullback A f).whiskerLeft (J.overMapPullbackId A X).hom) (CategoryStruct.comp (J.overMapPullback A f).rightUnitor.hom h)) = CategoryStruct.comp (J.overMapPullbackCongr A ⋯).hom h

theorem CategoryTheory.GrothendieckTopology.overMapPullback_assoc {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] {X Y Z T : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ T) : CategoryStruct.comp (J.overMapPullbackComp A f (CategoryStruct.comp g h)).inv (CategoryStruct.comp (Functor.whiskerRight (J.overMapPullbackComp A g h).inv (J.overMapPullback A f)) (CategoryStruct.comp ((J.overMapPullback A h).associator (J.overMapPullback A g) (J.overMapPullback A f)).hom (CategoryStruct.comp ((J.overMapPullback A h).whiskerLeft (J.overMapPullbackComp A f g).hom) (J.overMapPullbackComp A (CategoryStruct.comp f g) h).hom))) = (J.overMapPullbackCongr A ⋯).hom

theorem CategoryTheory.GrothendieckTopology.overMapPullback_assoc_assoc {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (A : Type u') [Category.{v', u'} A] {X Y Z T : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ T) {Z✝ : Functor (Sheaf (J.over T) A) (Sheaf (J.over X) A)} (h✝ : J.overMapPullback A (CategoryStruct.comp (CategoryStruct.comp f g) h) ⟶ Z✝) : CategoryStruct.comp (J.overMapPullbackComp A f (CategoryStruct.comp g h)).inv (CategoryStruct.comp (Functor.whiskerRight (J.overMapPullbackComp A g h).inv (J.overMapPullback A f)) (CategoryStruct.comp ((J.overMapPullback A h).associator (J.overMapPullback A g) (J.overMapPullback A f)).hom (CategoryStruct.comp ((J.overMapPullback A h).whiskerLeft (J.overMapPullbackComp A f g).hom) (CategoryStruct.comp (J.overMapPullbackComp A (CategoryStruct.comp f g) h).hom h✝)))) = CategoryStruct.comp (J.overMapPullbackCongr A ⋯).hom h✝

@[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.

theorem CategoryTheory.over_toGrothendieck_eq_toGrothendieck_comap_forget {C : Type u} [Category.{v, u} C] (K : Precoverage C) [K.HasPullbacks] [K.IsStableUnderBaseChange] (X : C) : K.toGrothendieck.over X = (Precoverage.comap (Over.forget X) K).toGrothendieck

The Grothendieck topology on Over X, obtained from localizing the topology generated by the precoverage K, is generated by the preimage of K.

instance CategoryTheory.instIsDenseSubsiteOverLeftDiscretePUnitOverInverseIteratedSliceEquiv {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} (f : Over X) : Functor.IsDenseSubsite (J.over f.left) ((J.over X).over f) f.iteratedSliceEquiv.inverse

instance CategoryTheory.instIsContinuousOverLeftDiscretePUnitIteratedSliceForwardOver {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} (f : Over X) : f.iteratedSliceForward.IsContinuous ((J.over X).over f) (J.over f.left)

instance CategoryTheory.instIsCocontinuousOverLeftDiscretePUnitIteratedSliceForwardOver {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} (f : Over X) : f.iteratedSliceForward.IsCocontinuous ((J.over X).over f) (J.over f.left)

instance CategoryTheory.instIsContinuousOverLeftDiscretePUnitIteratedSliceBackwardOver {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} (f : Over X) : f.iteratedSliceBackward.IsContinuous (J.over f.left) ((J.over X).over f)

instance CategoryTheory.instIsCocontinuousOverLeftDiscretePUnitIteratedSliceBackwardOver {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} (f : Over X) : f.iteratedSliceBackward.IsCocontinuous (J.over f.left) ((J.over X).over f)