English
For any f: G.toPresheaf ⟶ F' and a sheaf condition h on F', the canonical lift satisfies a compatibly equation with the map from G to its sheafification.
Русский
Для любого f: G.toPresheaf ⟶ F' и условия шарфа h на F' канонический лифт удовлетворяет совместимости с отображением из G в её шейфайфикацию.
LaTeX
$$$ Subpresheaf.homOfLe (G.le_sheafify J) \\gg G.sheafifyLift f h = f $$$
Lean4
theorem to_sheafifyLift (f : G.toPresheaf ⟶ F') (h : Presieve.IsSheaf J F') :
Subpresheaf.homOfLe (G.le_sheafify J) ≫ G.sheafifyLift f h = f :=
by
ext U s
apply (h _ ((Subpresheaf.homOfLe (G.le_sheafify J)).app U s).prop).isSeparatedFor.ext
intro V i hi
have := elementwise_of% f.naturality
exact
(Presieve.IsSheafFor.valid_glue (h _ ((homOfLe (_ : _ ≤ sheafify _ _)).app _ _).2)
((G.family_of_elements_compatible _).map _) _ _).trans
(this _ _)
