English
The map under presheafToPresheaf corresponds to the inv of a sheafifyIso in the presence of adjunctions.
Русский
Отображение presheafToPresheaf соответствует обратному значению изоморфа шарирования.
LaTeX
$$$(\text{sheafToPresheaf } J E).map ((\text{sheafComposeNatTrans } J F (plusPlusAdjunction J D) (plusPlusAdjunction J E)).app P) = (\text{sheafifyCompIso } J F P).inv$$$
Lean4
theorem sheafToPresheaf_map_sheafComposeNatTrans_eq_sheafifyCompIso_inv (P : Cᵒᵖ ⥤ D) :
(sheafToPresheaf J E).map ((sheafComposeNatTrans J F (plusPlusAdjunction J D) (plusPlusAdjunction J E)).app P) =
(sheafifyCompIso J F P).inv :=
by
suffices
(sheafComposeNatTrans J F (plusPlusAdjunction J D) (plusPlusAdjunction J E)).app P = ⟨(sheafifyCompIso J F P).inv⟩
by
rw [this]
rfl
apply ((plusPlusAdjunction J E).homEquiv _ _).injective
convert sheafComposeNatTrans_fac J F (plusPlusAdjunction J D) (plusPlusAdjunction J E) P
dsimp [plusPlusAdjunction]
simp
