Lean4
/-- The mono factorization given by `image_sheaf` for a morphism is an image. -/
noncomputable def imageFactorization {F F' : Sheaf J (Type (max v u))} (f : F ⟶ F') : Limits.ImageFactorisation f
where
F := imageMonoFactorization f
isImage :=
{ lift := fun I => by
haveI M := (Sheaf.Hom.mono_iff_presheaf_mono J (Type (max v u)) _).mp I.m_mono
refine ⟨Subpresheaf.homOfLe ?_ ≫ inv (Subpresheaf.toRange I.m.1)⟩
apply Subpresheaf.sheafify_le
· conv_lhs => rw [← I.fac]
apply Subpresheaf.range_comp_le
· rw [← isSheaf_iff_isSheaf_of_type]
exact F'.2
· apply Presieve.isSheaf_iso J (asIso <| Subpresheaf.toRange I.m.1)
rw [← isSheaf_iff_isSheaf_of_type]
exact I.I.2
lift_fac := fun I => by
ext1
dsimp [imageMonoFactorization]
generalize_proofs h
rw [← Subpresheaf.homOfLe_ι h, Category.assoc]
congr 1
rw [IsIso.inv_comp_eq, Subpresheaf.toRange_ι] }
