English
The natural transformation sheafComposeNatTrans J F (plusPlusAdjunction J D) (plusPlusAdjunction J E) is an isomorphism.
Русский
Естественная трансформация sheafComposeNatTrans является изоморфизмом.
LaTeX
$$$IsIso\left(\text{sheafComposeNatTrans } J F (plusPlusAdjunction J D) (plusPlusAdjunction J E)\right)$$$
Lean4
theorem preservesSheafification_iff_of_adjunctions_of_hasSheafCompose :
J.PreservesSheafification F ↔ IsIso (sheafComposeNatTrans J F adj₁ adj₂) :=
by
rw [J.preservesSheafification_iff_of_adjunctions F adj₁ adj₂, NatTrans.isIso_iff_isIso_app]
apply forall_congr'
intro P
rw [← J.W_iff_isIso_map_of_adjunction adj₂, ← J.W_sheafToPresheaf_map_iff_isIso, ←
sheafComposeNatTrans_fac J F adj₁ adj₂, (W _).precomp_iff _ _ (J.W_adj_unit_app adj₂ (P ⋙ F))]
