The sheaf condition in terms of an equalizer of products

Here we set up the machinery for the "usual" definition of the sheaf condition, e.g. as in https://stacks.math.columbia.edu/tag/0072 in terms of an equalizer diagram where the two objects are ∏ᶜ F.obj (U i) and ∏ᶜ F.obj (U i) ⊓ (U j).

We show that this sheaf condition is equivalent to the "pairwise intersections" sheaf condition when the presheaf is valued in a category with products, and thereby equivalent to the default sheaf condition.

def TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : C

The product of the sections of a presheaf over a family of open sets.

def TopCat.Presheaf.SheafConditionEqualizerProducts.piInters {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : C

The product of the sections of a presheaf over the pairwise intersections of a family of open sets.

def TopCat.Presheaf.SheafConditionEqualizerProducts.leftRes {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : piOpens F U ⟶ piInters F U

The morphism Π F.obj (U i) ⟶ Π F.obj (U i) ⊓ (U j) whose components are given by the restriction maps from U i to U i ⊓ U j.

def TopCat.Presheaf.SheafConditionEqualizerProducts.rightRes {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : piOpens F U ⟶ piInters F U

The morphism Π F.obj (U i) ⟶ Π F.obj (U i) ⊓ (U j) whose components are given by the restriction maps from U j to U i ⊓ U j.

def TopCat.Presheaf.SheafConditionEqualizerProducts.res {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : F.obj (Opposite.op (iSup U)) ⟶ piOpens F U

The morphism F.obj U ⟶ Π F.obj (U i) whose components are given by the restriction maps from U j to U i ⊓ U j.

@[simp]

theorem TopCat.Presheaf.SheafConditionEqualizerProducts.res_π {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (i : ι) : CategoryTheory.CategoryStruct.comp (res F U) (CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun (i : ι) => F.obj (Opposite.op (U i))) { as := i }) = F.map (TopologicalSpace.Opens.leSupr U i).op

theorem TopCat.Presheaf.SheafConditionEqualizerProducts.res_π_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (i : ι) {F✝ : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F✝ X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F✝] (x : CategoryTheory.ToType (F.obj (Opposite.op (iSup U)))) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun (i : ι) => F.obj (Opposite.op (U i))) { as := i })) ((CategoryTheory.ConcreteCategory.hom (res F U)) x) = (F.map (TopologicalSpace.Opens.leSupr U i).op) x

theorem TopCat.Presheaf.SheafConditionEqualizerProducts.w {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : CategoryTheory.CategoryStruct.comp (res F U) (leftRes F U) = CategoryTheory.CategoryStruct.comp (res F U) (rightRes F U)

theorem TopCat.Presheaf.SheafConditionEqualizerProducts.w_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) {F✝ : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F✝ X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F✝] (x : CategoryTheory.ToType (F.obj (Opposite.op (iSup U)))) : (CategoryTheory.ConcreteCategory.hom (leftRes F U)) ((CategoryTheory.ConcreteCategory.hom (res F U)) x) = (CategoryTheory.ConcreteCategory.hom (rightRes F U)) ((CategoryTheory.ConcreteCategory.hom (res F U)) x)

@[reducible, inline]

abbrev TopCat.Presheaf.SheafConditionEqualizerProducts.diagram {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C

The equalizer diagram for the sheaf condition.

def TopCat.Presheaf.SheafConditionEqualizerProducts.fork {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : CategoryTheory.Limits.Fork (leftRes F U) (rightRes F U)

The restriction map F.obj U ⟶ Π F.obj (U i) gives a cone over the equalizer diagram for the sheaf condition. The sheaf condition asserts this cone is a limit cone.

@[simp]

theorem TopCat.Presheaf.SheafConditionEqualizerProducts.fork_pt {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : (fork F U).pt = F.obj (Opposite.op (iSup U))

@[simp]

theorem TopCat.Presheaf.SheafConditionEqualizerProducts.fork_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : (fork F U).ι = res F U

@[simp]

theorem TopCat.Presheaf.SheafConditionEqualizerProducts.fork_π_app_walkingParallelPair_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : (fork F U).π.app CategoryTheory.Limits.WalkingParallelPair.zero = res F U

@[simp]

theorem TopCat.Presheaf.SheafConditionEqualizerProducts.fork_π_app_walkingParallelPair_one {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : (fork F U).π.app CategoryTheory.Limits.WalkingParallelPair.one = CategoryTheory.CategoryStruct.comp (res F U) (leftRes F U)

def TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens.isoOfIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} {F : Presheaf C X} {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) {G : Presheaf C X} (α : F ≅ G) : piOpens F U ≅ piOpens G U

Isomorphic presheaves have isomorphic piOpens for any cover U.

def TopCat.Presheaf.SheafConditionEqualizerProducts.piInters.isoOfIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} {F : Presheaf C X} {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) {G : Presheaf C X} (α : F ≅ G) : piInters F U ≅ piInters G U

Isomorphic presheaves have isomorphic piInters for any cover U.

def TopCat.Presheaf.SheafConditionEqualizerProducts.diagram.isoOfIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} {F : Presheaf C X} {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) {G : Presheaf C X} (α : F ≅ G) : diagram F U ≅ diagram G U

Isomorphic presheaves have isomorphic sheaf condition diagrams.

def TopCat.Presheaf.SheafConditionEqualizerProducts.fork.isoOfIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} {F : Presheaf C X} {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) {G : Presheaf C X} (α : F ≅ G) : fork F U ≅ (CategoryTheory.Limits.Cones.postcompose (diagram.isoOfIso U α).inv).obj (fork G U)

If F G : Presheaf C X are isomorphic presheaves, then the fork F U, the canonical cone of the sheaf condition diagram for F, is isomorphic to fork F G postcomposed with the corresponding isomorphism between sheaf condition diagrams.

def TopCat.Presheaf.IsSheafEqualizerProducts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) : Prop

The sheaf condition for a F : Presheaf C X requires that the morphism F.obj U ⟶ ∏ᶜ F.obj (U i) (where U is some open set which is the union of the U i) is the equalizer of the two morphisms ∏ᶜ F.obj (U i) ⟶ ∏ᶜ F.obj (U i) ⊓ (U j).

The remainder of this file shows that the "equalizer products" sheaf condition is equivalent to the "pairwise intersections" sheaf condition.

def TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)) : CategoryTheory.Limits.Cone (SheafConditionEqualizerProducts.diagram F U)

Implementation of SheafConditionPairwiseIntersections.coneEquiv.

@[simp]

theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_pt {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)) : (coneEquivFunctorObj F U c).pt = c.pt

@[simp]

theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_π_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)) (Z : CategoryTheory.Limits.WalkingParallelPair) : (coneEquivFunctorObj F U c).π.app Z = CategoryTheory.Limits.WalkingParallelPair.casesOn Z (CategoryTheory.Limits.Pi.lift fun (i : ι) => c.π.app (Opposite.op (CategoryTheory.Pairwise.single i))) (CategoryTheory.Limits.Pi.lift fun (b : ι × ι) => c.π.app (Opposite.op (CategoryTheory.Pairwise.pair b.1 b.2)))

def TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : CategoryTheory.Functor (CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)) (CategoryTheory.Limits.Cone (SheafConditionEqualizerProducts.diagram F U))

Implementation of SheafConditionPairwiseIntersections.coneEquiv.

@[simp]

theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_pt {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)) : ((coneEquivFunctor F U).obj c).pt = c.pt

@[simp]

theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_map_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) {c c' : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)} (f : c ⟶ c') : ((coneEquivFunctor F U).map f).hom = f.hom

@[simp]

theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor_obj_π_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)) (Z : CategoryTheory.Limits.WalkingParallelPair) : ((coneEquivFunctor F U).obj c).π.app Z = CategoryTheory.Limits.WalkingParallelPair.rec (CategoryTheory.Limits.Pi.lift fun (i : ι) => c.π.app (Opposite.op (CategoryTheory.Pairwise.single i))) (CategoryTheory.Limits.Pi.lift fun (b : ι × ι) => c.π.app (Opposite.op (CategoryTheory.Pairwise.pair b.1 b.2))) Z

def TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (c : CategoryTheory.Limits.Cone (SheafConditionEqualizerProducts.diagram F U)) : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)

Implementation of SheafConditionPairwiseIntersections.coneEquiv.

@[simp]

theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_pt {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (c : CategoryTheory.Limits.Cone (SheafConditionEqualizerProducts.diagram F U)) : (coneEquivInverseObj F U c).pt = c.pt

@[simp]

theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_π_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (c : CategoryTheory.Limits.Cone (SheafConditionEqualizerProducts.diagram F U)) (x : (CategoryTheory.Pairwise ι)ᵒᵖ) : (coneEquivInverseObj F U c).π.app x = Opposite.rec (fun (x : CategoryTheory.Pairwise ι) => CategoryTheory.Pairwise.casesOn x (fun (i : ι) => CategoryTheory.CategoryStruct.comp (c.π.app CategoryTheory.Limits.WalkingParallelPair.zero) (CategoryTheory.Limits.Pi.π (fun (i : ι) => F.obj (Opposite.op (U i))) i)) fun (i j : ι) => CategoryTheory.CategoryStruct.comp (c.π.app CategoryTheory.Limits.WalkingParallelPair.one) (CategoryTheory.Limits.Pi.π (fun (p : ι × ι) => F.obj (Opposite.op (U p.1 ⊓ U p.2))) (i, j))) x

def TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : CategoryTheory.Functor (CategoryTheory.Limits.Cone (SheafConditionEqualizerProducts.diagram F U)) (CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F))

Implementation of SheafConditionPairwiseIntersections.coneEquiv.

@[simp]

theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_pt {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (c : CategoryTheory.Limits.Cone (SheafConditionEqualizerProducts.diagram F U)) : ((coneEquivInverse F U).obj c).pt = c.pt

@[simp]

theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_map_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) {c c' : CategoryTheory.Limits.Cone (SheafConditionEqualizerProducts.diagram F U)} (f : c ⟶ c') : ((coneEquivInverse F U).map f).hom = f.hom

@[simp]

theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_π_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (c : CategoryTheory.Limits.Cone (SheafConditionEqualizerProducts.diagram F U)) (x : (CategoryTheory.Pairwise ι)ᵒᵖ) : ((coneEquivInverse F U).obj c).π.app x = CategoryTheory.Pairwise.rec (fun (a : ι) => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c) (CategoryTheory.Limits.Pi.π (fun (i : ι) => F.obj (Opposite.op (U i))) a)) (fun (a a_1 : ι) => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c) (CategoryTheory.CategoryStruct.comp (SheafConditionEqualizerProducts.leftRes F U) (CategoryTheory.Limits.Pi.π (fun (p : ι × ι) => F.obj (Opposite.op (U p.1 ⊓ U p.2))) (a, a_1)))) (Opposite.unop x)

def TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)) : (CategoryTheory.Functor.id (CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F))).obj c ≅ ((coneEquivFunctor F U).comp (coneEquivInverse F U)).obj c

Implementation of SheafConditionPairwiseIntersections.coneEquiv.

@[simp]

theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_inv_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)) : (coneEquivUnitIsoApp F U c).inv.hom = CategoryTheory.CategoryStruct.id (((coneEquivFunctor F U).comp (coneEquivInverse F U)).obj c).pt

@[simp]

theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_hom_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (c : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)) : (coneEquivUnitIsoApp F U c).hom.hom = CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F))).obj c).pt

def TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : CategoryTheory.Functor.id (CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)) ≅ (coneEquivFunctor F U).comp (coneEquivInverse F U)

Implementation of SheafConditionPairwiseIntersections.coneEquiv.

@[simp]

theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_inv_app_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (X✝ : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)) : ((coneEquivUnitIso F U).inv.app X✝).hom = CategoryTheory.CategoryStruct.id X✝.pt

@[simp]

theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_hom_app_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (X✝ : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)) : ((coneEquivUnitIso F U).hom.app X✝).hom = CategoryTheory.CategoryStruct.id X✝.pt

def TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : (coneEquivInverse F U).comp (coneEquivFunctor F U) ≅ CategoryTheory.Functor.id (CategoryTheory.Limits.Cone (SheafConditionEqualizerProducts.diagram F U))

Implementation of SheafConditionPairwiseIntersections.coneEquiv.

@[simp]

theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_inv_app_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (X✝ : CategoryTheory.Limits.Cone (SheafConditionEqualizerProducts.diagram F U)) : ((coneEquivCounitIso F U).inv.app X✝).hom = CategoryTheory.CategoryStruct.id X✝.pt

@[simp]

theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso_hom_app_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (X✝ : CategoryTheory.Limits.Cone (SheafConditionEqualizerProducts.diagram F U)) : ((coneEquivCounitIso F U).hom.app X✝).hom = CategoryTheory.CategoryStruct.id X✝.pt

def TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F) ≌ CategoryTheory.Limits.Cone (SheafConditionEqualizerProducts.diagram F U)

Cones over diagram U ⋙ F are the same as a cones over the usual sheaf condition equalizer diagram.

@[simp]

theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_inverse {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : (coneEquiv F U).inverse = coneEquivInverse F U

@[simp]

theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_unitIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : (coneEquiv F U).unitIso = coneEquivUnitIso F U

@[simp]

theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_counitIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : (coneEquiv F U).counitIso = coneEquivCounitIso F U

@[simp]

theorem TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_functor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) : (coneEquiv F U).functor = coneEquivFunctor F U

def TopCat.Presheaf.SheafConditionPairwiseIntersections.isLimitMapConeOfIsLimitSheafConditionFork {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (P : CategoryTheory.Limits.IsLimit (SheafConditionEqualizerProducts.fork F U)) : CategoryTheory.Limits.IsLimit (CategoryTheory.Functor.mapCone F (CategoryTheory.Pairwise.cocone U).op)

If SheafConditionEqualizerProducts.fork is an equalizer, then F.mapCone (cone U) is a limit cone.

def TopCat.Presheaf.SheafConditionPairwiseIntersections.isLimitSheafConditionForkOfIsLimitMapCone {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (Q : CategoryTheory.Limits.IsLimit (CategoryTheory.Functor.mapCone F (CategoryTheory.Pairwise.cocone U).op)) : CategoryTheory.Limits.IsLimit (SheafConditionEqualizerProducts.fork F U)

If F.mapCone (cone U) is a limit cone, then SheafConditionEqualizerProducts.fork is an equalizer.

theorem TopCat.Presheaf.isSheaf_iff_isSheafEqualizerProducts {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] {X : TopCat} (F : Presheaf C X) : F.IsSheaf ↔ F.IsSheafEqualizerProducts

The sheaf condition in terms of an equalizer diagram is equivalent to the default sheaf condition.