English
If a presheaf P satisfies the sheaf condition with respect to the Grothendieck topology J, then the canonical map P → P⁺ is an isomorphism.
Русский
Если пресефейф P удовлетворяет условию шейфа относительно топологии Дж, то каноническое отображение P → P⁺ является изоморфизмом.
LaTeX
$$$\\text{Presheaf.IsSheaf } J P \\;\\Rightarrow\\; \\text{IsIso} (J.toPlus P)$$$
Lean4
theorem isIso_toPlus_of_isSheaf (hP : Presheaf.IsSheaf J P) : IsIso (J.toPlus P) :=
by
rw [Presheaf.isSheaf_iff_multiequalizer] at hP
suffices ∀ X, IsIso ((J.toPlus P).app X) from NatIso.isIso_of_isIso_app _
intro X
refine IsIso.comp_isIso' inferInstance ?_
suffices ∀ (S T : (J.Cover X.unop)ᵒᵖ) (f : S ⟶ T), IsIso ((J.diagram P X.unop).map f) from
isIso_ι_of_isInitial (initialOpOfTerminal isTerminalTop) _
intro S T e
have : S.unop.toMultiequalizer P ≫ (J.diagram P X.unop).map e = T.unop.toMultiequalizer P :=
Multiequalizer.hom_ext _ _ _ (fun II => by simp)
have : (J.diagram P X.unop).map e = inv (S.unop.toMultiequalizer P) ≫ T.unop.toMultiequalizer P := by simp [← this]
rw [this]
infer_instance
