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 : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
:
C
The product of the sections of a presheaf over a family of open sets.
Equations
- TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens F U = ∏ fun (i : ι) => F.obj (Opposite.op (U i))
Instances For
def
TopCat.Presheaf.SheafConditionEqualizerProducts.piInters
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.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.
Equations
- TopCat.Presheaf.SheafConditionEqualizerProducts.piInters F U = ∏ fun (p : ι × ι) => F.obj (Opposite.op (U p.1 ⊓ U p.2))
Instances For
def
TopCat.Presheaf.SheafConditionEqualizerProducts.leftRes
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
TopCat.Presheaf.SheafConditionEqualizerProducts.rightRes
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
TopCat.Presheaf.SheafConditionEqualizerProducts.res
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
:
F.obj (Opposite.op (iSup U)) ⟶ TopCat.Presheaf.SheafConditionEqualizerProducts.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.
Equations
- TopCat.Presheaf.SheafConditionEqualizerProducts.res F U = CategoryTheory.Limits.Pi.lift fun (i : ι) => F.map (TopologicalSpace.Opens.leSupr U i).op
Instances For
theorem
TopCat.Presheaf.SheafConditionEqualizerProducts.res_π_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
(i : ι)
[inst : CategoryTheory.ConcreteCategory C]
(x : (CategoryTheory.forget C).obj (F.obj (Opposite.op (iSup U))))
:
(CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun (i : ι) => F.obj (Opposite.op (U i))) { as := i })
((TopCat.Presheaf.SheafConditionEqualizerProducts.res F U) x) = (F.map (TopologicalSpace.Opens.leSupr U i).op) x
@[simp]
theorem
TopCat.Presheaf.SheafConditionEqualizerProducts.res_π
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
(i : ι)
:
CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.SheafConditionEqualizerProducts.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.w_apply
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
[inst : CategoryTheory.ConcreteCategory C]
(x : (CategoryTheory.forget C).obj (F.obj (Opposite.op (iSup U))))
:
theorem
TopCat.Presheaf.SheafConditionEqualizerProducts.w
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
:
CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.SheafConditionEqualizerProducts.res F U)
(TopCat.Presheaf.SheafConditionEqualizerProducts.leftRes F U) = CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.SheafConditionEqualizerProducts.res F U)
(TopCat.Presheaf.SheafConditionEqualizerProducts.rightRes F U)
@[reducible]
def
TopCat.Presheaf.SheafConditionEqualizerProducts.diagram
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
:
The equalizer diagram for the sheaf condition.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
TopCat.Presheaf.SheafConditionEqualizerProducts.fork
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
:
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.
Equations
Instances For
@[simp]
theorem
TopCat.Presheaf.SheafConditionEqualizerProducts.fork_pt
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
:
(TopCat.Presheaf.SheafConditionEqualizerProducts.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 : TopCat.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 : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
:
@[simp]
theorem
TopCat.Presheaf.SheafConditionEqualizerProducts.fork_π_app_walkingParallelPair_one
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
:
def
TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens.isoOfIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
{F : TopCat.Presheaf C X}
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
{G : TopCat.Presheaf C X}
(α : F ≅ G)
:
Isomorphic presheaves have isomorphic piOpens for any cover U.
Equations
- TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens.isoOfIso U α = CategoryTheory.Limits.Pi.mapIso fun (x : ι) => α.app (Opposite.op (U x))
Instances For
def
TopCat.Presheaf.SheafConditionEqualizerProducts.piInters.isoOfIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
{F : TopCat.Presheaf C X}
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
{G : TopCat.Presheaf C X}
(α : F ≅ G)
:
Isomorphic presheaves have isomorphic piInters for any cover U.
Equations
- TopCat.Presheaf.SheafConditionEqualizerProducts.piInters.isoOfIso U α = CategoryTheory.Limits.Pi.mapIso fun (x : ι × ι) => α.app (Opposite.op (U x.1 ⊓ U x.2))
Instances For
def
TopCat.Presheaf.SheafConditionEqualizerProducts.diagram.isoOfIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
{F : TopCat.Presheaf C X}
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
{G : TopCat.Presheaf C X}
(α : F ≅ G)
:
Isomorphic presheaves have isomorphic sheaf condition diagrams.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
TopCat.Presheaf.SheafConditionEqualizerProducts.fork.isoOfIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
{F : TopCat.Presheaf C X}
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
{G : TopCat.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.
Equations
Instances For
def
TopCat.Presheaf.IsSheafEqualizerProducts
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.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).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The remainder of this file shows that the "equalizer products" sheaf condition is equivalent to the "pairwise intersections" sheaf condition.
@[simp]
theorem
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_π_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
(c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp (CategoryTheory.Pairwise.diagram U).op F))
(Z : CategoryTheory.Limits.WalkingParallelPair)
:
(TopCat.Presheaf.SheafConditionPairwiseIntersections.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)))
@[simp]
theorem
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj_pt
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
(c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp (CategoryTheory.Pairwise.diagram U).op F))
:
def
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctorObj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
(c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp (CategoryTheory.Pairwise.diagram U).op F))
:
Implementation of SheafConditionPairwiseIntersections.coneEquiv.
Equations
- One or more equations did not get rendered due to their size.
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 : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
(c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp (CategoryTheory.Pairwise.diagram U).op F))
(Z : CategoryTheory.Limits.WalkingParallelPair)
:
((TopCat.Presheaf.SheafConditionPairwiseIntersections.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 : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
{c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp (CategoryTheory.Pairwise.diagram U).op F)}
{c' : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp (CategoryTheory.Pairwise.diagram U).op F)}
(f : c ⟶ c')
:
((TopCat.Presheaf.SheafConditionPairwiseIntersections.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 : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
(c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp (CategoryTheory.Pairwise.diagram U).op F))
:
((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor F U).obj c).pt = c.pt
def
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
:
Implementation of SheafConditionPairwiseIntersections.coneEquiv.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_pt
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
(c : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U))
:
@[simp]
theorem
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj_π_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
(c : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U))
(x : (CategoryTheory.Pairwise ι)ᵒᵖ)
:
(TopCat.Presheaf.SheafConditionPairwiseIntersections.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.coneEquivInverseObj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
(c : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U))
:
Implementation of SheafConditionPairwiseIntersections.coneEquiv.
Equations
- One or more equations did not get rendered due to their size.
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 : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
(c : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U))
(x : (CategoryTheory.Pairwise ι)ᵒᵖ)
:
((TopCat.Presheaf.SheafConditionPairwiseIntersections.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 (TopCat.Presheaf.SheafConditionEqualizerProducts.leftRes F U)
(CategoryTheory.Limits.Pi.π (fun (p : ι × ι) => F.obj (Opposite.op (U p.1 ⊓ U p.2))) (a, a_1))))
x.unop
@[simp]
theorem
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_pt
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
(c : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U))
:
((TopCat.Presheaf.SheafConditionPairwiseIntersections.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 : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
{c : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U)}
{c' : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U)}
(f : c ⟶ c')
:
((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse F U).map f).hom = f.hom
def
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
:
Implementation of SheafConditionPairwiseIntersections.coneEquiv.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp_inv_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
(c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp (CategoryTheory.Pairwise.diagram U).op F))
:
(TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp F U c).inv.hom = CategoryTheory.CategoryStruct.id
((CategoryTheory.Functor.comp (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor F U)
(TopCat.Presheaf.SheafConditionPairwiseIntersections.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 : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
(c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp (CategoryTheory.Pairwise.diagram U).op F))
:
def
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
(c : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp (CategoryTheory.Pairwise.diagram U).op F))
:
(CategoryTheory.Functor.id
(CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp (CategoryTheory.Pairwise.diagram U).op F))).obj
c ≅ (CategoryTheory.Functor.comp (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor F U)
(TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse F U)).obj
c
Implementation of SheafConditionPairwiseIntersections.coneEquiv.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso_inv_app_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.Presheaf C X✝)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X✝)
(X : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp (CategoryTheory.Pairwise.diagram U).op F))
:
((TopCat.Presheaf.SheafConditionPairwiseIntersections.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 : TopCat.Presheaf C X✝)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X✝)
(X : CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp (CategoryTheory.Pairwise.diagram U).op F))
:
((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso F U).hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
def
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
:
CategoryTheory.Functor.id
(CategoryTheory.Limits.Cone (CategoryTheory.Functor.comp (CategoryTheory.Pairwise.diagram U).op F)) ≅ CategoryTheory.Functor.comp (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor F U)
(TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse F U)
Implementation of SheafConditionPairwiseIntersections.coneEquiv.
Equations
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 : TopCat.Presheaf C X✝)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X✝)
(X : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U))
:
((TopCat.Presheaf.SheafConditionPairwiseIntersections.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 : TopCat.Presheaf C X✝)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X✝)
(X : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U))
:
((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivCounitIso F U).inv.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 : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
:
Implementation of SheafConditionPairwiseIntersections.coneEquiv.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_unitIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
:
@[simp]
theorem
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_inverse
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
:
@[simp]
theorem
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_counitIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
:
@[simp]
theorem
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv_functor
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
:
def
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquiv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
TopCat.Presheaf.SheafConditionPairwiseIntersections.isLimitMapConeOfIsLimitSheafConditionFork
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
(P : CategoryTheory.Limits.IsLimit (TopCat.Presheaf.SheafConditionEqualizerProducts.fork F U))
:
If SheafConditionEqualizerProducts.fork is an equalizer,
then F.mapCone (cone U) is a limit cone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
TopCat.Presheaf.SheafConditionPairwiseIntersections.isLimitSheafConditionForkOfIsLimitMapCone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.Presheaf C X)
{ι : Type v'}
(U : ι → TopologicalSpace.Opens ↑X)
(Q : CategoryTheory.Limits.IsLimit (F.mapCone (CategoryTheory.Limits.Cocone.op (CategoryTheory.Pairwise.cocone U))))
:
If F.mapCone (cone U) is a limit cone,
then SheafConditionEqualizerProducts.fork is an equalizer.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
TopCat.Presheaf.isSheaf_iff_isSheafEqualizerProducts
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasProducts C]
{X : TopCat}
(F : TopCat.Presheaf C X)
:
The sheaf condition in terms of an equalizer diagram is equivalent to the default sheaf condition.