English
If a morphism of presheaves is mono, then its image under the forgetful functor preserves mono-ness on the corresponding sheaf level.
Русский
Если морфизм прехешафов моно, то его образ под забывающим функтором сохраняет моно-ность на уровне шейфа.
LaTeX
$$$\\text{presheaf\\_mono\\_of\\_mono}: \\text{Mono}(f) \\Rightarrow \\text{Mono}(f.1)$$$
Lean4
/-- The sheafification functor is left adjoint to the forgetful functor. -/
@[simps! unit_app counit_app_val]
noncomputable def plusPlusAdjunction : plusPlusSheaf J D ⊣ sheafToPresheaf J D :=
Adjunction.mkOfHomEquiv
{ homEquiv := fun P Q =>
{ toFun := fun e => J.toSheafify P ≫ e.val
invFun := fun e => ⟨J.sheafifyLift e Q.2⟩
left_inv := fun _ => Sheaf.Hom.ext <| (J.sheafifyLift_unique _ _ _ rfl).symm
right_inv := fun _ => J.toSheafify_sheafifyLift _ _ }
homEquiv_naturality_left_symm := by
intro P Q R η γ; ext1; dsimp; symm
apply J.sheafifyMap_sheafifyLift
homEquiv_naturality_right := fun η γ => by
dsimp
rw [Category.assoc] }
