Lean4
/-- The lift of a presheaf morphism onto the sheafification subpresheaf. -/
noncomputable def sheafifyLift (f : G.toPresheaf ⟶ F') (h : Presieve.IsSheaf J F') : (G.sheafify J).toPresheaf ⟶ F'
where
app _ s := (h (G.sieveOfSection s.1) s.prop).amalgamate (_) ((G.family_of_elements_compatible s.1).map f)
naturality := by
intro U V i
ext s
apply (h _ ((Subpresheaf.sheafify J G).toPresheaf.map i s).prop).isSeparatedFor.ext
intro W j hj
refine
(Presieve.IsSheafFor.valid_glue (h _ ((G.sheafify J).toPresheaf.map i s).2)
((G.family_of_elements_compatible _).map _) _ hj).trans
?_
dsimp
conv_rhs => rw [← FunctorToTypes.map_comp_apply]
change _ = F'.map (j ≫ i.unop).op _
refine
Eq.trans ?_
(Presieve.IsSheafFor.valid_glue (h _ s.2) ((G.family_of_elements_compatible s.1).map f) (j ≫ i.unop) ?_).symm
· dsimp [Presieve.FamilyOfElements.map]
exact congr_arg _ (Subtype.ext (FunctorToTypes.map_comp_apply _ _ _ _).symm)
· dsimp [Presieve.FamilyOfElements.map] at hj ⊢
rwa [FunctorToTypes.map_comp_apply]
