English
The isLimitOpensLeEquivGenerate₂ yields an equivalence of IsLimit structures between the opens-le-cover cocone and the sieve-generated cocone.
Русский
Изоморфия из IsLimit происходит между коконом OpensLeCover и коконом, порождаемым сидом.
LaTeX
$$$\text{isLimitOpensLeEquivGenerate₂}(R,hR): IsLimit( F.mapCone (opensLeCoverCocone Y R)^{op}) \cong IsLimit( F.mapCone (Sieve.generate R).arrows.cocone^{op} ).$$$
Lean4
/-- Given a presheaf `F` on the topological space `X` and a presieve `R` whose generated sieve
is covering for the associated Grothendieck topology (equivalently, the presieve is covering
for the associated pretopology), the natural cone associated to `F` and the family of opens
associated to `R` is a limit cone iff the natural cone associated to `F` and the generated
sieve is a limit cone.
Since only the existence of a 1-1 correspondence will be used, the exact definition does
not matter, so tactics are used liberally. -/
def isLimitOpensLeEquivGenerate₂ (R : Presieve Y) (hR : Sieve.generate R ∈ Opens.grothendieckTopology X Y) :
IsLimit (F.mapCone (opensLeCoverCocone (coveringOfPresieve Y R)).op) ≃
IsLimit (F.mapCone (Sieve.generate R).arrows.cocone.op) :=
by
convert
isLimitOpensLeEquivGenerate₁ F (coveringOfPresieve Y R)
(coveringOfPresieve.iSup_eq_of_mem_grothendieck Y R hR).symm using
1
rw [covering_presieve_eq_self R]
