Lean4
/-- Given a functorial surjective/injective factorizations of morphisms in a concrete
category `A`, this is the induced functorial locally surjective/locally injective
factorization of morphisms in the category `Sheaf J A`. -/
noncomputable def functorialLocallySurjectiveInjectiveFactorization :
(locallySurjective J A).FunctorialFactorizationData (locallyInjective J A)
where
Z := (sheafToPresheaf J A).mapArrow ⋙ (data.functorCategory Cᵒᵖ).Z ⋙ presheafToSheaf J A
i :=
whiskerLeft Arrow.leftFunc (inv (sheafificationAdjunction J A).counit) ≫
whiskerLeft (sheafToPresheaf J A).mapArrow (whiskerRight (data.functorCategory Cᵒᵖ).i (presheafToSheaf J A))
p :=
whiskerLeft (sheafToPresheaf J A).mapArrow (whiskerRight (data.functorCategory Cᵒᵖ).p (presheafToSheaf J A)) ≫
whiskerLeft Arrow.rightFunc (sheafificationAdjunction J A).counit
fac := by
ext f : 2
dsimp
simp only [assoc, ← Functor.map_comp_assoc, MorphismProperty.FunctorialFactorizationData.fac_app,
NatIso.isIso_inv_app, IsIso.inv_comp_eq]
exact (sheafificationAdjunction J A).counit.naturality f.hom
hi
_ := by
dsimp [locallySurjective]
rw [← isLocallySurjective_sheafToPresheaf_map_iff, Functor.map_comp, Presheaf.comp_isLocallySurjective_iff,
isLocallySurjective_sheafToPresheaf_map_iff, Presheaf.isLocallySurjective_presheafToSheaf_map_iff]
apply Presheaf.isLocallySurjective_of_surjective
apply (data.functorCategory Cᵒᵖ).hi
hp
_ := by
dsimp [locallyInjective]
rw [← isLocallyInjective_sheafToPresheaf_map_iff, Functor.map_comp, Presheaf.isLocallyInjective_comp_iff,
isLocallyInjective_sheafToPresheaf_map_iff, Presheaf.isLocallyInjective_presheafToSheaf_map_iff]
apply Presheaf.isLocallyInjective_of_injective
apply (data.functorCategory Cᵒᵖ).hp
