English
For a Grothendieck topology J on C, and a concrete category A with the stated structure, the construction provides a local-bijectivity instance on the category D, i.e., J.WEqualsLocallyBijective D holds under the given hypotheses.
Русский
Для топологии Гротенидка J на C и конкретной категории D с указанной структурой, конструируется локальная биективность: J.WEqualsLocallyBijective D выполняется при заданных гипотезах.
LaTeX
$$$J\text{-}WEqualsLocallyBijective(D)\quad\text{holds under the stated hypotheses.}$$$
Lean4
instance {D : Type w} [Category.{w'} D] {FD : D → D → Type*} {CD : D → Type (max u v)}
[∀ X Y, FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory.{max u v} D FD] [HasWeakSheafify J D]
[J.HasSheafCompose (forget D)] [J.PreservesSheafification (forget D)] [(forget D).ReflectsIsomorphisms] :
J.WEqualsLocallyBijective D := by apply WEqualsLocallyBijective.mk'
