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.toPrefunctor.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.toPrefunctor.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.toPrefunctor.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.toPrefunctor.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).toPrefunctor.obj (F.toPrefunctor.obj (Opposite.op (iSup U))))
:
(CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun (i : ι) => F.toPrefunctor.obj (Opposite.op (U i)))
{ as := i })
((TopCat.Presheaf.SheafConditionEqualizerProducts.res F U) x) = (F.toPrefunctor.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.toPrefunctor.obj (Opposite.op (U i))) { as := i }) = F.toPrefunctor.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).toPrefunctor.obj (F.toPrefunctor.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
- One or more equations did not get rendered due to their size.
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.toPrefunctor.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).toPrefunctor.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).toPrefunctor.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).toPrefunctor.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.toPrefunctor.obj (Opposite.op (U i))) i))
fun (i j : ι) =>
CategoryTheory.CategoryStruct.comp (c.π.app CategoryTheory.Limits.WalkingParallelPair.one)
(CategoryTheory.Limits.Pi.π (fun (p : ι × ι) => F.toPrefunctor.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).toPrefunctor.obj c).π.app x = CategoryTheory.Pairwise.rec
(fun (a : ι) =>
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c)
(CategoryTheory.Limits.Pi.π (fun (i : ι) => F.toPrefunctor.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.toPrefunctor.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).toPrefunctor.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).toPrefunctor.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)).toPrefunctor.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))
:
(TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp F U c).hom.hom = CategoryTheory.CategoryStruct.id
((CategoryTheory.Functor.id
(CategoryTheory.Limits.Cone
(CategoryTheory.Functor.comp (CategoryTheory.Pairwise.diagram U).op F))).toPrefunctor.obj
c).pt
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))).toPrefunctor.obj
c ≅ (CategoryTheory.Functor.comp (TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivFunctor F U)
(TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse F U)).toPrefunctor.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.