The sheaf condition in terms of an equalizer of products #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
Top.presheaf.sheaf_condition_equalizer_products.pi_opens
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X) :
C
The product of the sections of a presheaf over a family of open sets.
Equations
- Top.presheaf.sheaf_condition_equalizer_products.pi_opens F U = ∏ λ (i : ι), F.obj (opposite.op (U i))
noncomputable
def
Top.presheaf.sheaf_condition_equalizer_products.pi_inters
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X) :
C
The product of the sections of a presheaf over the pairwise intersections of a family of open sets.
Equations
- Top.presheaf.sheaf_condition_equalizer_products.pi_inters F U = ∏ λ (p : ι × ι), F.obj (opposite.op (U p.fst ⊓ U p.snd))
noncomputable
def
Top.presheaf.sheaf_condition_equalizer_products.left_res
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.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
- Top.presheaf.sheaf_condition_equalizer_products.left_res F U = category_theory.limits.pi.lift (λ (p : ι × ι), category_theory.limits.pi.π (λ (i : ι), F.obj (opposite.op (U i))) p.fst ≫ F.map ((U p.fst).inf_le_left (U p.snd)).op)
noncomputable
def
Top.presheaf.sheaf_condition_equalizer_products.right_res
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.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
- Top.presheaf.sheaf_condition_equalizer_products.right_res F U = category_theory.limits.pi.lift (λ (p : ι × ι), category_theory.limits.pi.π (λ (i : ι), F.obj (opposite.op (U i))) p.snd ≫ F.map ((U p.fst).inf_le_right (U p.snd)).op)
noncomputable
def
Top.presheaf.sheaf_condition_equalizer_products.res
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.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.
Equations
- Top.presheaf.sheaf_condition_equalizer_products.res F U = category_theory.limits.pi.lift (λ (i : ι), F.map (topological_space.opens.le_supr U i).op)
@[simp]
theorem
Top.presheaf.sheaf_condition_equalizer_products.res_π_apply
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X)
(i : ι)
[I : category_theory.concrete_category C]
(x : ↥(F.obj (opposite.op (supr U)))) :
⇑(category_theory.limits.limit.π (category_theory.discrete.functor (λ (i : ι), F.obj (opposite.op (U i)))) {as := i}) (⇑(Top.presheaf.sheaf_condition_equalizer_products.res F U) x) = ⇑(F.map (topological_space.opens.le_supr U i).op) x
@[simp]
theorem
Top.presheaf.sheaf_condition_equalizer_products.res_π
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X)
(i : ι) :
Top.presheaf.sheaf_condition_equalizer_products.res F U ≫ category_theory.limits.limit.π (category_theory.discrete.functor (λ (i : ι), F.obj (opposite.op (U i)))) {as := i} = F.map (topological_space.opens.le_supr U i).op
theorem
Top.presheaf.sheaf_condition_equalizer_products.w_apply
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X)
[I : category_theory.concrete_category C]
(x : ↥(F.obj (opposite.op (supr U)))) :
theorem
Top.presheaf.sheaf_condition_equalizer_products.w
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X) :
@[reducible]
noncomputable
def
Top.presheaf.sheaf_condition_equalizer_products.diagram
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X) :
The equalizer diagram for the sheaf condition.
noncomputable
def
Top.presheaf.sheaf_condition_equalizer_products.fork
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.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.
@[simp]
theorem
Top.presheaf.sheaf_condition_equalizer_products.fork_X
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X) :
(Top.presheaf.sheaf_condition_equalizer_products.fork F U).X = F.obj (opposite.op (supr U))
@[simp]
theorem
Top.presheaf.sheaf_condition_equalizer_products.fork_ι
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X) :
@[simp]
theorem
Top.presheaf.sheaf_condition_equalizer_products.fork_π_app_walking_parallel_pair_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X) :
@[simp]
theorem
Top.presheaf.sheaf_condition_equalizer_products.fork_π_app_walking_parallel_pair_one
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X) :
@[simp]
noncomputable
def
Top.presheaf.sheaf_condition_equalizer_products.pi_opens.iso_of_iso
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
{F : Top.presheaf C X}
{ι : Type v'}
(U : ι → topological_space.opens ↥X)
{G : Top.presheaf C X}
(α : F ≅ G) :
Isomorphic presheaves have isomorphic pi_opens for any cover U.
Equations
- Top.presheaf.sheaf_condition_equalizer_products.pi_opens.iso_of_iso U α = category_theory.limits.pi.map_iso (λ (X_1 : ι), α.app (opposite.op (U X_1)))
@[simp]
noncomputable
def
Top.presheaf.sheaf_condition_equalizer_products.pi_inters.iso_of_iso
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
{F : Top.presheaf C X}
{ι : Type v'}
(U : ι → topological_space.opens ↥X)
{G : Top.presheaf C X}
(α : F ≅ G) :
Isomorphic presheaves have isomorphic pi_inters for any cover U.
Equations
- Top.presheaf.sheaf_condition_equalizer_products.pi_inters.iso_of_iso U α = category_theory.limits.pi.map_iso (λ (X_1 : ι × ι), α.app (opposite.op (U X_1.fst ⊓ U X_1.snd)))
noncomputable
def
Top.presheaf.sheaf_condition_equalizer_products.diagram.iso_of_iso
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
{F : Top.presheaf C X}
{ι : Type v'}
(U : ι → topological_space.opens ↥X)
{G : Top.presheaf C X}
(α : F ≅ G) :
Isomorphic presheaves have isomorphic sheaf condition diagrams.
Equations
- Top.presheaf.sheaf_condition_equalizer_products.diagram.iso_of_iso U α = category_theory.nat_iso.of_components (λ (X_1 : category_theory.limits.walking_parallel_pair), X_1.cases_on (Top.presheaf.sheaf_condition_equalizer_products.pi_opens.iso_of_iso U α) (Top.presheaf.sheaf_condition_equalizer_products.pi_inters.iso_of_iso U α)) _
noncomputable
def
Top.presheaf.sheaf_condition_equalizer_products.fork.iso_of_iso
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
{F : Top.presheaf C X}
{ι : Type v'}
(U : ι → topological_space.opens ↥X)
{G : Top.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
def
Top.presheaf.is_sheaf_equalizer_products
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.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).
Equations
- F.is_sheaf_equalizer_products = ∀ ⦃ι : Type v'⦄ (U : ι → topological_space.opens ↥X), nonempty (category_theory.limits.is_limit (Top.presheaf.sheaf_condition_equalizer_products.fork F U))
The remainder of this file shows that the equalizer_products sheaf condition is equivalent to the pariwise_intersections sheaf condition.
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor_obj_X
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X)
(c : category_theory.limits.cone ((category_theory.pairwise.diagram U).op ⋙ F)) :
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor_obj_π_app
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X)
(c : category_theory.limits.cone ((category_theory.pairwise.diagram U).op ⋙ F))
(Z : category_theory.limits.walking_parallel_pair) :
(Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor_obj F U c).π.app Z = Z.cases_on (category_theory.limits.pi.lift (λ (i : ι), c.π.app (opposite.op (category_theory.pairwise.single i)))) (category_theory.limits.pi.lift (λ (b : ι × ι), c.π.app (opposite.op (category_theory.pairwise.pair b.fst b.snd))))
noncomputable
def
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor_obj
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X)
(c : category_theory.limits.cone ((category_theory.pairwise.diagram U).op ⋙ F)) :
Implementation of sheaf_condition_pairwise_intersections.cone_equiv.
Equations
- Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor_obj F U c = {X := c.X, π := {app := λ (Z : category_theory.limits.walking_parallel_pair), Z.cases_on (category_theory.limits.pi.lift (λ (i : ι), c.π.app (opposite.op (category_theory.pairwise.single i)))) (category_theory.limits.pi.lift (λ (b : ι × ι), c.π.app (opposite.op (category_theory.pairwise.pair b.fst b.snd)))), naturality' := _}}
noncomputable
def
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X) :
Implementation of sheaf_condition_pairwise_intersections.cone_equiv.
Equations
- Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor F U = {obj := λ (c : category_theory.limits.cone ((category_theory.pairwise.diagram U).op ⋙ F)), Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor_obj F U c, map := λ (c c' : category_theory.limits.cone ((category_theory.pairwise.diagram U).op ⋙ F)) (f : c ⟶ c'), {hom := f.hom, w' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor_obj_2
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X)
(c : category_theory.limits.cone ((category_theory.pairwise.diagram U).op ⋙ F)) :
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor_map_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X)
(c c' : category_theory.limits.cone ((category_theory.pairwise.diagram U).op ⋙ F))
(f : c ⟶ c') :
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse_obj_X
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X)
(c : category_theory.limits.cone (Top.presheaf.sheaf_condition_equalizer_products.diagram F U)) :
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse_obj_π_app
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X)
(c : category_theory.limits.cone (Top.presheaf.sheaf_condition_equalizer_products.diagram F U))
(x : (category_theory.pairwise ι)ᵒᵖ) :
(Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse_obj F U c).π.app x = opposite.rec (λ (x : category_theory.pairwise ι), x.cases_on (λ (i : ι), c.π.app category_theory.limits.walking_parallel_pair.zero ≫ category_theory.limits.pi.π (λ (i : ι), F.obj (opposite.op (U i))) i) (λ (i j : ι), c.π.app category_theory.limits.walking_parallel_pair.one ≫ category_theory.limits.pi.π (λ (p : ι × ι), F.obj (opposite.op (U p.fst ⊓ U p.snd))) (i, j))) x
noncomputable
def
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse_obj
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X)
(c : category_theory.limits.cone (Top.presheaf.sheaf_condition_equalizer_products.diagram F U)) :
Implementation of sheaf_condition_pairwise_intersections.cone_equiv.
Equations
- Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse_obj F U c = {X := c.X, π := {app := λ (x : (category_theory.pairwise ι)ᵒᵖ), opposite.rec (λ (x : category_theory.pairwise ι), x.cases_on (λ (i : ι), c.π.app category_theory.limits.walking_parallel_pair.zero ≫ category_theory.limits.pi.π (λ (i : ι), F.obj (opposite.op (U i))) i) (λ (i j : ι), c.π.app category_theory.limits.walking_parallel_pair.one ≫ category_theory.limits.pi.π (λ (p : ι × ι), F.obj (opposite.op (U p.fst ⊓ U p.snd))) (i, j))) x, naturality' := _}}
noncomputable
def
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X) :
Implementation of sheaf_condition_pairwise_intersections.cone_equiv.
Equations
- Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse F U = {obj := λ (c : category_theory.limits.cone (Top.presheaf.sheaf_condition_equalizer_products.diagram F U)), Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse_obj F U c, map := λ (c c' : category_theory.limits.cone (Top.presheaf.sheaf_condition_equalizer_products.diagram F U)) (f : c ⟶ c'), {hom := f.hom, w' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse_map_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X)
(c c' : category_theory.limits.cone (Top.presheaf.sheaf_condition_equalizer_products.diagram F U))
(f : c ⟶ c') :
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse_obj_2
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X)
(c : category_theory.limits.cone (Top.presheaf.sheaf_condition_equalizer_products.diagram F U)) :
noncomputable
def
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_unit_iso_app
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X)
(c : category_theory.limits.cone ((category_theory.pairwise.diagram U).op ⋙ F)) :
Implementation of sheaf_condition_pairwise_intersections.cone_equiv.
Equations
- Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_unit_iso_app F U c = {hom := {hom := 𝟙 ((𝟭 (category_theory.limits.cone ((category_theory.pairwise.diagram U).op ⋙ F))).obj c).X, w' := _}, inv := {hom := 𝟙 ((Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor F U ⋙ Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse F U).obj c).X, w' := _}, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_unit_iso_app_inv_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X)
(c : category_theory.limits.cone ((category_theory.pairwise.diagram U).op ⋙ F)) :
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_unit_iso_app_hom_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X)
(c : category_theory.limits.cone ((category_theory.pairwise.diagram U).op ⋙ F)) :
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_unit_iso_inv_app_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X)
(X_1 : category_theory.limits.cone ((category_theory.pairwise.diagram U).op ⋙ F)) :
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_unit_iso_hom_app_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X)
(X_1 : category_theory.limits.cone ((category_theory.pairwise.diagram U).op ⋙ F)) :
noncomputable
def
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_unit_iso
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X) :
Implementation of sheaf_condition_pairwise_intersections.cone_equiv.
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_counit_iso_inv_app_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X)
(X_1 : category_theory.limits.cone (Top.presheaf.sheaf_condition_equalizer_products.diagram F U)) :
noncomputable
def
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_counit_iso
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X) :
Implementation of sheaf_condition_pairwise_intersections.cone_equiv.
Equations
- Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_counit_iso F U = category_theory.nat_iso.of_components (λ (c : category_theory.limits.cone (Top.presheaf.sheaf_condition_equalizer_products.diagram F U)), {hom := {hom := 𝟙 ((Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse F U ⋙ Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor F U).obj c).X, w' := _}, inv := {hom := 𝟙 ((𝟭 (category_theory.limits.cone (Top.presheaf.sheaf_condition_equalizer_products.diagram F U))).obj c).X, w' := _}, hom_inv_id' := _, inv_hom_id' := _}) _
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_counit_iso_hom_app_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X)
(X_1 : category_theory.limits.cone (Top.presheaf.sheaf_condition_equalizer_products.diagram F U)) :
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_counit_iso_2
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X) :
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor_2
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X) :
noncomputable
def
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X) :
Cones over diagram U ⋙ F are the same as a cones over the usual sheaf condition equalizer diagram.
Equations
- Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv F U = {functor := Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_functor F U, inverse := Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse F U, unit_iso := Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_unit_iso F U, counit_iso := Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_counit_iso F U, functor_unit_iso_comp' := _}
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_unit_iso_2
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X) :
@[simp]
theorem
Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_inverse_2
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X) :
noncomputable
def
Top.presheaf.sheaf_condition_pairwise_intersections.is_limit_map_cone_of_is_limit_sheaf_condition_fork
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X)
(P : category_theory.limits.is_limit (Top.presheaf.sheaf_condition_equalizer_products.fork F U)) :
If sheaf_condition_equalizer_products.fork is an equalizer,
then F.map_cone (cone U) is a limit cone.
Equations
- Top.presheaf.sheaf_condition_pairwise_intersections.is_limit_map_cone_of_is_limit_sheaf_condition_fork F U P = (⇑((category_theory.limits.is_limit.of_cone_equiv (Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv F U).symm).symm) P).of_iso_limit {hom := {hom := 𝟙 ((Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv F U).symm.functor.obj (Top.presheaf.sheaf_condition_equalizer_products.fork F U)).X, w' := _}, inv := {hom := 𝟙 (category_theory.functor.map_cone F (category_theory.pairwise.cocone U).op).X, w' := _}, hom_inv_id' := _, inv_hom_id' := _}
noncomputable
def
Top.presheaf.sheaf_condition_pairwise_intersections.is_limit_sheaf_condition_fork_of_is_limit_map_cone
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X)
{ι : Type v'}
(U : ι → topological_space.opens ↥X)
(Q : category_theory.limits.is_limit (category_theory.functor.map_cone F (category_theory.pairwise.cocone U).op)) :
If F.map_cone (cone U) is a limit cone,
then sheaf_condition_equalizer_products.fork is an equalizer.
Equations
- Top.presheaf.sheaf_condition_pairwise_intersections.is_limit_sheaf_condition_fork_of_is_limit_map_cone F U Q = (⇑((category_theory.limits.is_limit.of_cone_equiv (Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv F U)).symm) Q).of_iso_limit {hom := {hom := 𝟙 ((Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv F U).functor.obj (category_theory.functor.map_cone F (category_theory.pairwise.cocone U).op)).X, w' := _}, inv := {hom := 𝟙 (Top.presheaf.sheaf_condition_equalizer_products.fork F U).X, w' := _}, hom_inv_id' := _, inv_hom_id' := _}
theorem
Top.presheaf.is_sheaf_iff_is_sheaf_equalizer_products
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_products C]
{X : Top}
(F : Top.presheaf C X) :
The sheaf condition in terms of an equalizer diagram is equivalent to the default sheaf condition.