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.

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 ⊤ = ⊤

@[simp]

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

@[simp]

theorem CategoryTheory.Sieve.overEquiv_symm_bot {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 (Over.Hom.left f) ((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 (Over.Hom.left f) 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 (Over.Hom.left f)

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_ofArrows {C : Type u} [Category.{v, u} C] {X : C} {Y : Over X} {I : Type u_1} (Z : I → Over X) (g : (i : I) → Z i ⟶ Y) : (overEquiv Y) (ofArrows Z g) = ofArrows (fun (i : I) => (Z i).left) fun (i : I) => Over.Hom.left (g i)

theorem CategoryTheory.Sieve.overEquiv_preOneHypercover_sieve₁ {C : Type u} [Category.{v, u} C] {X : C} {Y : Over X} (E : PreOneHypercover Y) {i₁ i₂ : E.I₀} {W : Over X} (p₁ : W ⟶ E.X i₁) (p₂ : W ⟶ E.X i₂) : (overEquiv W) (E.sieve₁ p₁ p₂) = (E.map (Over.forget X)).sieve₁ (Over.Hom.left p₁) (Over.Hom.left p₂)

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

theorem CategoryTheory.Sieve.overEquiv_functorPullback_map {C : Type u} [Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (U : Over X) (S : Sieve ((Over.map f).obj U)) : (overEquiv U) (functorPullback (Over.map f) S) = (overEquiv ((Over.map f).obj U)) S

theorem CategoryTheory.Sieve.overEquiv_functorPullback_post {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] (F : Functor C D) {X : C} (U : Over X) (S : Sieve ((Over.post F).obj U)) : (overEquiv U) (functorPullback (Over.post F) S) = functorPullback F ((overEquiv ((Over.post F).obj U)) S)

theorem CategoryTheory.Sieve.overEquiv_functorPushforward_post {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] (F : Functor C D) {X : C} (U : Over X) (S : Sieve U) : (overEquiv ((Over.post F).obj U)) (functorPushforward (Over.post F) S) = functorPushforward F ((overEquiv U) 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

• J.over X = { sieves := fun (Y : CategoryTheory.Over X) => ⇑(CategoryTheory.Sieve.overEquiv Y) ⁻¹' J Y.left, top_mem' := ⋯, pullback_stable' := ⋯, transitive' := ⋯ }

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)

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

instance CategoryTheory.GrothendieckTopology.instIsCocontinuousOverObjPostOver {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {D : Type u_1} [Category.{v_1, u_1} D] (K : GrothendieckTopology D) (F : Functor C D) (X : C) [F.IsCocontinuous J K] : (Over.post F).IsCocontinuous (J.over X) (K.over (F.obj X))

theorem CategoryTheory.CoverPreserving.overPost {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {D : Type u_1} [Category.{v_1, u_1} D] {K : GrothendieckTopology D} {F : Functor C D} (X : C) (h : CoverPreserving J K F) : CoverPreserving (J.over X) (K.over (F.obj X)) (Over.post F)

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

instance CategoryTheory.GrothendieckTopology.instPreservesOneHypercoversOverObjPostOver {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] {J : GrothendieckTopology C} {K : GrothendieckTopology D} (F : Functor C D) (X : C) [F.PreservesOneHypercovers J K] : (Over.post F).PreservesOneHypercovers (J.over X) (K.over (F.obj X))

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

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

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.

Equations

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

Equations

• J.overMapPullbackCongr A h = CategoryTheory.Functor.sheafPushforwardContinuousIso (CategoryTheory.Over.mapCongr f g h) A (J.over X) (J.over Y)

@[simp]

theorem CategoryTheory.GrothendieckTopology.overMapPullbackCongr_inv_app_hom_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).hom.app X✝ = M.obj.map ((Over.mapCongr f g h).hom.app (Opposite.unop X✝)).op

@[simp]

theorem CategoryTheory.GrothendieckTopology.overMapPullbackCongr_hom_app_hom_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).hom.app X✝ = M.obj.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.

Equations

• J.overMapPullbackId A X = CategoryTheory.Functor.sheafPushforwardContinuousId' (CategoryTheory.Over.mapId X) A (J.over X)

@[simp]

theorem CategoryTheory.GrothendieckTopology.overMapPullbackId_hom_app_hom_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✝).hom.app X✝¹ = X✝.obj.map ((Over.mapId X).inv.app (Opposite.unop X✝¹)).op

@[simp]

theorem CategoryTheory.GrothendieckTopology.overMapPullbackId_inv_app_hom_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✝).hom.app X✝¹ = X✝.obj.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.

Equations

• J.overMapPullbackComp A f g = CategoryTheory.Functor.sheafPushforwardContinuousComp' (CategoryTheory.Over.mapComp f g).symm A (J.over X) (J.over Y) (J.over Z)

@[simp]

theorem CategoryTheory.GrothendieckTopology.overMapPullbackComp_inv_app_hom_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✝).hom.app X✝¹ = X✝.obj.map ((Over.mapComp f g).inv.app (Opposite.unop X✝¹)).op

@[simp]

theorem CategoryTheory.GrothendieckTopology.overMapPullbackComp_hom_app_hom_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✝).hom.app X✝¹ = X✝.obj.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.

Equations

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

def CategoryTheory.Sheaf.pushforwardOverMapIso {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] (F : Sheaf J A) {X Y : C} (f : X ⟶ Y) : ((Over.map f).sheafPushforwardContinuous A (J.over X) (J.over Y)).obj (F.over Y) ≅ F.over X

For f : X ⟶ Y, F.over Y viewed as a sheaf on Over X is isomorphic to F.Over X.

Equations

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

@[simp]

theorem CategoryTheory.Sheaf.pushforwardOverMapIso_inv_hom_app {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] (F : Sheaf J A) {X Y : C} (f : X ⟶ Y) (X✝ : (Over X)ᵒᵖ) : (F.pushforwardOverMapIso f).inv.hom.app X✝ = CategoryStruct.id (F.obj.obj (Opposite.op (Opposite.unop X✝).left))

@[simp]

theorem CategoryTheory.Sheaf.pushforwardOverMapIso_hom_hom_app {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] (F : Sheaf J A) {X Y : C} (f : X ⟶ Y) (X✝ : (Over X)ᵒᵖ) : (F.pushforwardOverMapIso f).hom.hom.app X✝ = CategoryStruct.id (F.obj.obj (Opposite.op (Opposite.unop X✝).left))

noncomputable def CategoryTheory.Sheaf.toPushforwardOverPullback {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [Limits.HasPullbacks C] (F : Sheaf J A) {X Y : C} (f : X ⟶ Y) : F.over Y ⟶ ((Over.pullback f).sheafPushforwardContinuous A (J.over Y) (J.over X)).obj (F.over X)

For f : X ⟶ Y, this is the morphism from F.over Y to the pushforward of F.over X along Over.pullback f induced by Limits.pullback.fst.

Equations

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

@[simp]

theorem CategoryTheory.Sheaf.toPushforwardOverPullback_hom_app {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [Limits.HasPullbacks C] (F : Sheaf J A) {X Y : C} (f : X ⟶ Y) (U : (Over Y)ᵒᵖ) : (F.toPushforwardOverPullback f).hom.app U = F.obj.map (Limits.pullback.fst (Opposite.unop U).hom f).op

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.instIsDenseSubsiteOverLeftOverInverseIteratedSliceEquiv {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.instIsContinuousOverLeftIteratedSliceForwardOver {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.instIsCocontinuousOverLeftIteratedSliceForwardOver {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.instIsContinuousOverLeftIteratedSliceBackwardOver {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.instIsCocontinuousOverLeftIteratedSliceBackwardOver {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)