English
Let J be a Grothendieck topology on a category C, and A a concrete category with a weak sheafification, along with suitable hypotheses on forgetful functors and local injectivity/surjectivity. Then A satisfies a local-bijection principle: for presheaves P, Q valued in A, a morphism f: P → Q is a local isomorphism exactly when its associated local data (via sheafification) yields an isomorphism, equivalently when f is locally injective and locally surjective in the prescribed sense.
Русский
Пусть J — топология Гротендикка на категорию C, A — конкретная категория с слабой Sheafification, при этом выполняются нужные условия относительно забывающего функтору и локальной инъективности и сюръективности. Тогда A удовлетворяет локальный принцип биективности: для преповес P, Q, значения в A, морфизм f: P → Q является локальной изоморфизмом тогда и только тогда, когда его локальные данные через sheafification дают изоморфизм; эквивалентно условию локальной инъективности и локальной сюръективности.
LaTeX
$$$J\text{-}WEqualsLocallyBijective(A) \quad\text{iff}\quad (\forall P,Q : C^{\mathrm{op}} \to A),\; (f: P \to Q) \,:\; f\text{ locally bijective }\iff \text{(toSheafify }J\,P \to toSheafify }J\,Q) \text{ is an isomorphism}.$$$
Lean4
theorem mk' [HasWeakSheafify J A] [(forget A).ReflectsIsomorphisms] [J.HasSheafCompose (forget A)]
[∀ (P : Cᵒᵖ ⥤ A), Presheaf.IsLocallyInjective J (CategoryTheory.toSheafify J P)]
[∀ (P : Cᵒᵖ ⥤ A), Presheaf.IsLocallySurjective J (CategoryTheory.toSheafify J P)] : J.WEqualsLocallyBijective A
where
iff {P Q}
f := by
rw [W_iff, ← Sheaf.isLocallyBijective_iff_isIso (A := A), ←
Presheaf.isLocallyInjective_comp_iff J f (CategoryTheory.toSheafify J Q), ←
Presheaf.isLocallySurjective_comp_iff J f (CategoryTheory.toSheafify J Q), CategoryTheory.toSheafify_naturality,
Presheaf.comp_isLocallyInjective_iff, Presheaf.comp_isLocallySurjective_iff]
