Lean4
/-- Isomorphic `PresheafedSpace`s have naturally isomorphic presheaves. -/
@[simps]
def sheafIsoOfIso (H : X ≅ Y) : Y.2 ≅ H.hom.base _* X.2
where
hom := H.hom.c
inv := Presheaf.pushforwardToOfIso ((forget _).mapIso H).symm H.inv.c
hom_inv_id := by
ext U
rw [NatTrans.comp_app]
simpa using congr_arg (fun f => f ≫ eqToHom _) (congr_app H.inv_hom_id (op U))
inv_hom_id := by
ext U
dsimp
rw [NatTrans.id_app]
simp only [Presheaf.pushforwardToOfIso_app, Iso.symm_inv, mapIso_hom, forget_map, Iso.symm_hom, mapIso_inv,
eqToHom_map, assoc]
have eq₁ := congr_app H.hom_inv_id (op ((Opens.map H.hom.base).obj U))
have eq₂ :=
H.hom.c.naturality (eqToHom (congr_obj (congr_arg Opens.map ((forget C).congr_map H.inv_hom_id.symm)) U)).op
rw [id_c, NatTrans.id_app, id_comp, eqToHom_map, comp_c_app] at eq₁
rw [eqToHom_op, eqToHom_map] at eq₂
erw [eq₂, reassoc_of% eq₁]
simp
