Lean4
/-- (Implementation). The sheaf map given in `types.sheaf_hom` is natural in terms of `X`. -/
@[simps]
noncomputable def sheafCoyonedaHom (α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val) :
coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type _)).obj ℱ ⟶ coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type _)).obj ℱ'.val
where
app X := presheafHom (homOver α (unop X))
naturality X Y
f := by
ext U x
change appHom (homOver α (unop Y)) (unop U) (f.unop ≫ x) = f.unop ≫ appHom (homOver α (unop X)) (unop U) x
symm
apply sheaf_eq_amalgamation
· apply G.is_cover_of_isCoverDense
· exact pushforwardFamily_compatible (homOver α Y.unop) (f.unop ≫ x)
intro Y' f' hf'
change unop X ⟶ ℱ.obj (op (unop _)) at x
dsimp
simp only [Category.assoc]
congr 1
conv_lhs => rw [← hf'.some.fac]
simp only [← Category.assoc, op_comp, Functor.map_comp]
congr 1
exact (appHom_restrict (homOver α (unop X)) hf'.some.map.op x).trans (by simp)
