English
For presheaves valued in a concrete category with appropriate forgetful properties, the usual sheaf condition coincides with the unique gluing formulation.
Русский
Для прешейфов, значения которых лежат в абсолютной категории и у которых в нужной ситуации отражаются изоморфизмы, обычное условие шейфа совпадает с формулировкой уникальной слепки.
LaTeX
$$$$\text{IsSheaf } F \iff \text{IsSheafUniqueGluing } F,$$$$
Lean4
/-- In this version of the lemma, the inclusion homs `iUV` can be specified directly by the user,
which can be more convenient in practice.
-/
theorem existsUnique_gluing' (V : Opens X) (iUV : ∀ i : ι, U i ⟶ V) (hcover : V ≤ iSup U)
(sf : ∀ i : ι, ToType (F.1.obj (op (U i)))) (h : IsCompatible F.1 U sf) :
∃! s : ToType (F.1.obj (op V)), ∀ i : ι, F.1.map (iUV i).op s = sf i :=
by
have V_eq_supr_U : V = iSup U := le_antisymm hcover (iSup_le fun i => (iUV i).le)
obtain ⟨gl, gl_spec, gl_uniq⟩ := F.existsUnique_gluing U sf h
refine ⟨F.1.map (eqToHom V_eq_supr_U).op gl, ?_, ?_⟩
· intro i
rw [← ConcreteCategory.comp_apply, ← F.1.map_comp]
exact gl_spec i
· intro gl' gl'_spec
convert congr_arg _ (gl_uniq (F.1.map (eqToHom V_eq_supr_U.symm).op gl') fun i => _) <;>
rw [← ConcreteCategory.comp_apply, ← F.1.map_comp]
· rw [eqToHom_op, eqToHom_op, eqToHom_trans, eqToHom_refl, F.1.map_id, ConcreteCategory.id_apply]
· exact gl'_spec i
