English
The restriction equality sheafHom_restrict_eq states that the whiskered morphism equals α after restricting to C: whiskerLeft G.op (sheafHom α) = α.
Русский
Равенство ограниченного гомоморфизма: whiskerLeft G.op (sheafHom α) = α.
LaTeX
$$$\mathrm{whiskerLeft}(G^{op},\mathrm{sheafHom}(\alpha)) = \alpha.$$$
Lean4
/-- The constructed `sheafHom α` is equal to `α` when restricted onto `C`. -/
theorem sheafHom_restrict_eq (α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val) : whiskerLeft G.op (sheafHom α) = α :=
by
ext X
apply yoneda.map_injective
ext U
erw [yoneda.map_preimage]
symm
change (show (ℱ'.val ⋙ coyoneda.obj (op (unop U))).obj (op (G.obj (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]
simp only [pushforwardFamily, Functor.comp_map, yoneda_map_app, coyoneda_obj_map, op_comp,
FunctorToTypes.map_comp_apply, homOver_app]
congr 1
simp only [Category.assoc]
congr 1
have :=
naturality_apply (G := G) (ℱ := ℱ ⋙ coyoneda.obj (op <| (G.op ⋙ ℱ).obj X)) (ℱ' :=
⟨_, Presheaf.isSheaf_comp_of_isSheaf K ℱ'.val (coyoneda.obj (op ((G.op ⋙ ℱ).obj X))) ℱ'.cond⟩)
(whiskerRight α (coyoneda.obj _)) hf.some.map (𝟙 _)
simpa using this
