English
The components of appIso provide an isomorphism on fibers that is inverse to appHom on each X.
Русский
Компоненты appIso дают изоморфизм волокон, обратный appHom на каждом X.
LaTeX
$$$\mathrm{appIso}(\alpha,X): \mathcal{F}.\mathrm{val}.obj(\mathrm{op} X) \cong \mathcal{F}'.\mathrm{val}.obj(\mathrm{op} X) \quad\text{with }$$
Lean4
/-- If the pullback map is obtained via whiskering,
then the result `sheaf_hom (whisker_left G.op α)` is equal to `α`.
-/
theorem sheafHom_eq (α : ℱ ⟶ ℱ'.val) : sheafHom (whiskerLeft G.op α) = α :=
by
ext X
apply yoneda.map_injective
ext U
erw [yoneda.map_preimage]
symm
change (show (ℱ'.val ⋙ coyoneda.obj (op (unop U))).obj (op (unop X)) from _) = _
apply
sheaf_eq_amalgamation ℱ'
(G.is_cover_of_isCoverDense _ _)
-- Porting note: next line was not needed in mathlib3
· exact (pushforwardFamily_compatible _ _)
intro Y f hf
conv_lhs => rw [← hf.some.fac]
dsimp; simp
