English
The diagram of opens LeCover is cofinal in the diagram of opens contained in some U_i; hence, there is a final functor from pairwise to OpensLeCover U.
Русский
Диаграмма OpensLeCover является кофинальной в диаграмме открытых множеств, содержащихся в некотором U_i; отсюда следует, что существует окончательный функтор из парной диаграммы в OpensLeCover U.
LaTeX
$$$\text{OpensLeCover U}$ является конечной над $\text{Pairwise diagram}$, то есть существует.final$$
Lean4
/-- Given a family of opens `U` and an open `Y` equal to the union of opens in `U`, we may
take the presieve on `Y` associated to `U` and the sieve generated by it, and form the
full subcategory (subposet) of opens contained in `Y` (`over Y`) consisting of arrows
in the sieve. This full subcategory is equivalent to `OpensLeCover U`, the (poset)
category of opens contained in some `U i`. -/
@[simps]
def generateEquivalenceOpensLe_functor' :
(ObjectProperty.FullSubcategory fun f : Over Y => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom) ⥤
OpensLeCover U :=
{ obj := fun f =>
⟨f.1.left,
let ⟨_, h, _, ⟨i, hY⟩, _⟩ := f.2
⟨i, hY ▸ h.le⟩⟩
map := fun {_ _} g => g.left }
