Locally surjective morphisms #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Main definitions #
is_locally_surjective: A morphism of presheaves valued in a concrete category is locally surjective with respect to a grothendieck topology if every section in the target is locally in the set-theoretic image, i.e. the image sheaf coincides with the target.
Main results #
to_sheafify_is_locally_surjective:to_sheafifyis locally surjective.
theorem
category_theory.image_sieve_apply
{C : Type u}
[category_theory.category C]
{A : Type u'}
[category_theory.category A]
[category_theory.concrete_category A]
{F G : Cᵒᵖ ⥤ A}
(f : F ⟶ G)
{U : C}
(s : ↥(G.obj (opposite.op U)))
(V : C)
(i : V ⟶ U) :
⇑(category_theory.image_sieve f s) i = ∃ (t : ↥(F.obj (opposite.op V))), ⇑(f.app (opposite.op V)) t = ⇑(G.map i.op) s
def
category_theory.image_sieve
{C : Type u}
[category_theory.category C]
{A : Type u'}
[category_theory.category A]
[category_theory.concrete_category A]
{F G : Cᵒᵖ ⥤ A}
(f : F ⟶ G)
{U : C}
(s : ↥(G.obj (opposite.op U))) :
Given f : F ⟶ G, a morphism between presieves, and s : G.obj (op U), this is the sieve
of U consisting of the i : V ⟶ U such that s restricted along i is in the image of f.
Equations
- category_theory.image_sieve f s = {arrows := λ (V : C) (i : V ⟶ U), ∃ (t : ↥(F.obj (opposite.op V))), ⇑(f.app (opposite.op V)) t = ⇑(G.map i.op) s, downward_closed' := _}
theorem
category_theory.image_sieve_eq_sieve_of_section
{C : Type u}
[category_theory.category C]
{A : Type u'}
[category_theory.category A]
[category_theory.concrete_category A]
{F G : Cᵒᵖ ⥤ A}
(f : F ⟶ G)
{U : C}
(s : ↥(G.obj (opposite.op U))) :
theorem
category_theory.image_sieve_whisker_forget
{C : Type u}
[category_theory.category C]
{A : Type u'}
[category_theory.category A]
[category_theory.concrete_category A]
{F G : Cᵒᵖ ⥤ A}
(f : F ⟶ G)
{U : C}
(s : ↥(G.obj (opposite.op U))) :
theorem
category_theory.image_sieve_app
{C : Type u}
[category_theory.category C]
{A : Type u'}
[category_theory.category A]
[category_theory.concrete_category A]
{F G : Cᵒᵖ ⥤ A}
(f : F ⟶ G)
{U : C}
(s : ↥(F.obj (opposite.op U))) :
category_theory.image_sieve f (⇑(f.app (opposite.op U)) s) = ⊤
def
category_theory.is_locally_surjective
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{A : Type u'}
[category_theory.category A]
[category_theory.concrete_category A]
{F G : Cᵒᵖ ⥤ A}
(f : F ⟶ G) :
Prop
A morphism of presheaves f : F ⟶ G is locally surjective with respect to a grothendieck
topology if every section of G is locally in the image of f.
Equations
- category_theory.is_locally_surjective J f = ∀ (U : C) (s : ↥(G.obj (opposite.op U))), category_theory.image_sieve f s ∈ ⇑J U
theorem
category_theory.is_locally_surjective_iff_image_presheaf_sheafify_eq_top
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{A : Type u'}
[category_theory.category A]
[category_theory.concrete_category A]
{F G : Cᵒᵖ ⥤ A}
(f : F ⟶ G) :
theorem
category_theory.is_locally_surjective_iff_image_presheaf_sheafify_eq_top'
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{F G : Cᵒᵖ ⥤ Type w}
(f : F ⟶ G) :
theorem
category_theory.is_locally_surjective_iff_is_iso
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{F G : category_theory.Sheaf J (Type w)}
(f : F ⟶ G) :
theorem
category_theory.is_locally_surjective_iff_whisker_forget
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{A : Type u'}
[category_theory.category A]
[category_theory.concrete_category A]
{F G : Cᵒᵖ ⥤ A}
(f : F ⟶ G) :
theorem
category_theory.is_locally_surjective_of_surjective
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{A : Type u'}
[category_theory.category A]
[category_theory.concrete_category A]
{F G : Cᵒᵖ ⥤ A}
(f : F ⟶ G)
(H : ∀ (U : Cᵒᵖ), function.surjective ⇑(f.app U)) :
theorem
category_theory.is_locally_surjective_of_iso
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{A : Type u'}
[category_theory.category A]
[category_theory.concrete_category A]
{F G : Cᵒᵖ ⥤ A}
(f : F ⟶ G)
[category_theory.is_iso f] :
theorem
category_theory.is_locally_surjective.comp
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{A : Type u'}
[category_theory.category A]
[category_theory.concrete_category A]
{F₁ F₂ F₃ : Cᵒᵖ ⥤ A}
{f₁ : F₁ ⟶ F₂}
{f₂ : F₂ ⟶ F₃}
(h₁ : category_theory.is_locally_surjective J f₁)
(h₂ : category_theory.is_locally_surjective J f₂) :
category_theory.is_locally_surjective J (f₁ ≫ f₂)
noncomputable
def
category_theory.sheafification_iso_image_presheaf
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
(F : Cᵒᵖ ⥤ Type (max u v)) :
The image of F in J.sheafify F is isomorphic to the sheafification.
Equations
- category_theory.sheafification_iso_image_presheaf J F = {hom := J.sheafify_lift (J.to_image_presheaf_sheafify (J.to_sheafify F)) _, inv := (category_theory.grothendieck_topology.subpresheaf.sheafify J (category_theory.grothendieck_topology.image_presheaf (J.to_sheafify F))).ι, hom_inv_id' := _, inv_hom_id' := _}
theorem
category_theory.to_sheafify_is_locally_surjective
{C : Type u}
[category_theory.category C]
(J : category_theory.grothendieck_topology C)
{B : Type w}
[category_theory.category B]
[category_theory.concrete_category B]
[∀ (X : C), category_theory.limits.has_colimits_of_shape (J.cover X)ᵒᵖ B]
[∀ (P : Cᵒᵖ ⥤ B) (X : C) (S : J.cover X), category_theory.limits.has_multiequalizer (S.index P)]
[Π (X : C) (W : J.cover X) (P : Cᵒᵖ ⥤ B), category_theory.limits.preserves_limit (W.index P).multicospan (category_theory.forget B)]
[Π (X : C), category_theory.limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (category_theory.forget B)]
[∀ (α β : Type (max u v)) (fst snd : β → α), category_theory.limits.has_limits_of_shape (category_theory.limits.walking_multicospan fst snd) B]
(F : Cᵒᵖ ⥤ B) :