Sheafification section is amalgamation

Stream: Is there code for X?

[Andrew Yang]

Do we know that every section of the sheafification (of a sheaf of types) is the amalgamation of some sections from the original sheaf?
For example

example {C : Type v} [category.{v} C] (J : grothendieck_topology C) {F : Cᵒᵖ ⥤ Type v}
  (U : C) (s : (J.sheafify F).obj (op U)) :
  ∃ (S : sieve U) (H : S ∈ J U) (x : presieve.family_of_elements F S),
    (x.comp_presheaf_map $ J.to_sheafify F).is_amalgamation s := sorry

Tagging @Adam Topaz since sheafification is your work.

[Adam Topaz]

No we don't have this. Do you have a proof?

[Andrew Yang]

I could prove that the subset of sections satisfying the condition (image_sheaf (J.to_sheafify F)) is a subsheaf of J.sheafify F, so that there is a map J.sheafify F ⟶ image_sheaf (J.to_sheafify F) which should show that they are equal.

[Adam Topaz]

Where is image_sheaf?

[Andrew Yang]

Sorry about the confusion. I just defined it.

def image_sheaf {C : Type v} [category.{v} C] (J : grothendieck_topology C) {F G : Cᵒᵖ ⥤ Type v}
  (f : F ⟶ G) : Cᵒᵖ ⥤ Type v :=
{ obj := λ U, { s : G.obj U // ∃ (S : sieve (unop U)) (H : S ∈ J (unop U))
    (x : presieve.family_of_elements F S), (x.comp_presheaf_map f).is_amalgamation s },
  map := λ U V i s, ⟨G.map i s, begin
    obtain ⟨S, hS, x, hx⟩ := s.prop,
    exact ⟨_, J.pullback_stable i.unop hS, x.pullback i.unop,
      λ W j hj, (functor_to_types.map_comp_apply G i j.op _).symm.trans (hx _ hj)⟩,
  end⟩,
  map_id' := λ U, funext $ λ x, subtype.ext (functor_to_types.map_id_apply G ↑x),
  map_comp' := λ U V W i j, funext $ λ x, subtype.ext (functor_to_types.map_comp_apply G i j x) }

[Andrew Yang]

And there is also

lemma image_sheaf_is_sheaf {C : Type v} [category.{v} C] (J : grothendieck_topology C)
  {F G : Cᵒᵖ ⥤ Type v} (f : F ⟶ G) (hG : presieve.is_sheaf J G) :
    presieve.is_sheaf J (image_sheaf J f) := sorry

where I have a proof already.

[Adam Topaz]

Ah, I see. Anyway that would be a useful lemma to add!

[Andrew Yang]

Ok. I'll make it into a PR. Thanks!