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.
noncomputable 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.
Instances For
noncomputable 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.
Instances For
noncomputable 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)
:
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.
Instances For
noncomputable 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)
:
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.
Instances For
noncomputable 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)
:
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.
Instances For
@[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 : carrier (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) = (CategoryTheory.ConcreteCategory.hom (F.map (TopologicalSpace.Opens.leSupr U i).op)) x
theorem
TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens.hom_ext
{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✝ : C}
{f f' : X✝ ⟶ piOpens F U}
(w :
∀ (j : CategoryTheory.Discrete ι),
CategoryTheory.CategoryStruct.comp f
(CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun (i : ι) => F.obj (Opposite.op (U i))) j) = CategoryTheory.CategoryStruct.comp f'
(CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun (i : ι) => F.obj (Opposite.op (U i))) j))
:
f = f'
Copy of limit.hom_ext, specialized to piOpens for use by the ext tactic.
theorem
TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens.hom_ext_iff
{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✝ : C}
{f f' : X✝ ⟶ piOpens F U}
:
f = f' ↔ ∀ (j : CategoryTheory.Discrete ι),
CategoryTheory.CategoryStruct.comp f
(CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun (i : ι) => F.obj (Opposite.op (U i))) j) = CategoryTheory.CategoryStruct.comp f'
(CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun (i : ι) => F.obj (Opposite.op (U i))) j)
theorem
TopCat.Presheaf.SheafConditionEqualizerProducts.piInters.hom_ext
{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✝ : C}
{f f' : X✝ ⟶ piInters F U}
(w :
∀ (j : CategoryTheory.Discrete (ι × ι)),
CategoryTheory.CategoryStruct.comp f
(CategoryTheory.Limits.limit.π
(CategoryTheory.Discrete.functor fun (p : ι × ι) => F.obj (Opposite.op (U p.1 ⊓ U p.2))) j) = CategoryTheory.CategoryStruct.comp f'
(CategoryTheory.Limits.limit.π
(CategoryTheory.Discrete.functor fun (p : ι × ι) => F.obj (Opposite.op (U p.1 ⊓ U p.2))) j))
:
f = f'
Copy of limit.hom_ext, specialized to piInters for use by the ext tactic.
theorem
TopCat.Presheaf.SheafConditionEqualizerProducts.piInters.hom_ext_iff
{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✝ : C}
{f f' : X✝ ⟶ piInters F U}
:
f = f' ↔ ∀ (j : CategoryTheory.Discrete (ι × ι)),
CategoryTheory.CategoryStruct.comp f
(CategoryTheory.Limits.limit.π
(CategoryTheory.Discrete.functor fun (p : ι × ι) => F.obj (Opposite.op (U p.1 ⊓ U p.2))) j) = CategoryTheory.CategoryStruct.comp f'
(CategoryTheory.Limits.limit.π
(CategoryTheory.Discrete.functor fun (p : ι × ι) => F.obj (Opposite.op (U p.1 ⊓ U p.2))) j)
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 : carrier (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]
noncomputable 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)
:
The equalizer diagram for the sheaf condition.
Instances For
noncomputable 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.
Instances For
@[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)
:
@[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)
noncomputable 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)
:
Isomorphic presheaves have isomorphic piOpens for any cover U.
Instances For
noncomputable 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)
:
Isomorphic presheaves have isomorphic piInters for any cover U.
Instances For
noncomputable 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)
:
Isomorphic presheaves have isomorphic sheaf condition diagrams.
Instances For
noncomputable 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)
:
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.
Instances For
def
TopCat.Presheaf.IsSheafEqualizerProducts
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : Presheaf C X)
:
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).
Instances For
The remainder of this file shows that the "equalizer products" sheaf condition is equivalent to the "pairwise intersections" sheaf condition.
noncomputable 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))
:
Implementation of SheafConditionPairwiseIntersections.coneEquiv.
Instances For
@[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)))
noncomputable 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)
:
Implementation of SheafConditionPairwiseIntersections.coneEquiv.
Instances For
@[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
@[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_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
noncomputable 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))
:
Implementation of SheafConditionPairwiseIntersections.coneEquiv.
Instances For
@[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
noncomputable 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)
:
Implementation of SheafConditionPairwiseIntersections.coneEquiv.
Instances For
@[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)
@[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
noncomputable 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.
Instances For
@[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))
:
@[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
noncomputable 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)
:
Implementation of SheafConditionPairwiseIntersections.coneEquiv.
Instances For
@[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
@[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
noncomputable 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)
:
Implementation of SheafConditionPairwiseIntersections.coneEquiv.
Instances For
@[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
@[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
noncomputable 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)
:
Cones over diagram U ⋙ F are the same as a cones over the usual sheaf condition equalizer diagram.
Instances For
@[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_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_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
@[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
noncomputable 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))
:
If SheafConditionEqualizerProducts.fork is an equalizer,
then F.mapCone (cone U) is a limit cone.
Instances For
noncomputable 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))
:
If F.mapCone (cone U) is a limit cone,
then SheafConditionEqualizerProducts.fork is an equalizer.
Instances For
theorem
TopCat.Presheaf.isSheaf_iff_isSheafEqualizerProducts
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : Presheaf C X)
:
The sheaf condition in terms of an equalizer diagram is equivalent to the default sheaf condition.