English
If P is a sheaf, and S is a cover with a sieve-compatible family of elements, then there exists a unique amalgamation producing a morphism E → P(X).
Русский
Если P — онащная оболочка, и S — покрытие с совместимым семейством элементов, то существует единственный амальгамируемый морфизм E → P(X).
LaTeX
$$$\\text{amalgamate}: (P\\text{IsSheaf})\\Rightarrow (E\\to P(X))$$$
Lean4
/-- Given sieve `S` and presheaf `P : Cᵒᵖ ⥤ A`, their natural associated cone admits at most one
morphism from every cone in the same category (i.e. over the same diagram),
iff `Hom (E, P -)`is separated for the sieve `S` and all `E : A`. -/
theorem subsingleton_iff_isSeparatedFor :
(∀ c, Subsingleton (c ⟶ P.mapCone S.arrows.cocone.op)) ↔ ∀ E : Aᵒᵖ, IsSeparatedFor (P ⋙ coyoneda.obj E) S.arrows :=
by
constructor
· intro hs E x t₁ t₂ h₁ h₂
have hx := is_compatible_of_exists_amalgamation x ⟨t₁, h₁⟩
rw [compatible_iff_sieveCompatible] at hx
specialize hs hx.cone
rcases hs with ⟨hs⟩
simpa only [Subtype.mk.injEq] using
(show Subtype.mk t₁ h₁ = ⟨t₂, h₂⟩ from (homEquivAmalgamation hx).symm.injective (hs _ _))
· rintro h ⟨E, π⟩
let eqv := conesEquivSieveCompatibleFamily P S (op E)
constructor
rw [← eqv.left_inv π]
intro f₁ f₂
let eqv' := homEquivAmalgamation (eqv π).2
apply eqv'.injective
ext
apply h _ (eqv π).1 <;> exact (eqv' _).2
