English
A presheaf P is a sheaf for the Grothendieck topology generated by a pretopology K iff for every X and R ∈ K X the associated cone is a limit cone.
Русский
Прешефикс P является sheaf в топологии, порождённой препотопологией K, если для каждого X и R ∈ K X соответствующий конус является пределом.
LaTeX
$$$IsSheaf K.toGrothendieck P \iff \forall X(R: Presieve X), R \in K X \rightarrow Nonempty(IsLimit (P.mapCone (generate R).arrows.cocone.op))$$$
Lean4
/-- Given a sieve `S` on `X : C`, a presheaf `P : Cᵒᵖ ⥤ A`, and an object `E` of `A`,
the cones over the natural diagram `S.arrows.diagram.op ⋙ P` associated to `S` and `P`
with cone point `E` are in 1-1 correspondence with sieve_compatible family of elements
for the sieve `S` and the presheaf of types `Hom (E, P -)`. -/
def conesEquivSieveCompatibleFamily :
(S.arrows.diagram.op ⋙ P).cones.obj E ≃
{ x : FamilyOfElements (P ⋙ coyoneda.obj E) (S : Presieve X) // x.SieveCompatible }
where
toFun
π :=
⟨fun _ f h => π.app (op ⟨Over.mk f, h⟩), fun X Y f g hf =>
by
apply (id_comp _).symm.trans
dsimp
exact π.naturality (Quiver.Hom.op (Over.homMk _ (by rfl)))⟩
invFun
x :=
{ app := fun f => x.1 f.unop.1.hom f.unop.2
naturality := fun f f' g =>
by
refine Eq.trans ?_ (x.2 f.unop.1.hom g.unop.left f.unop.2)
dsimp
rw [id_comp]
convert rfl
rw [Over.w] }
