English
There is an equivalence between the diagram over U and the mapped diagram through the equivalence OpensLeCover and pairwise.
Русский
Существует эквивалентность между диаграммой над U и отображаемой диаграммой через эквивалентности OpensLeCover и пары.
LaTeX
$$$\text{pairwiseDiagramIso} : \text{Pairwise.diagram } U \cong \text{OpensLeCover } U$$$
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 (hY : Y = iSup U) :
(ObjectProperty.FullSubcategory fun f : Over Y => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom) ≌
OpensLeCover U
where
functor := generateEquivalenceOpensLe_functor' _
inverse := generateEquivalenceOpensLe_inverse' _ hY
unitIso :=
eqToIso <|
CategoryTheory.Functor.ext (by rintro ⟨⟨_, _⟩, _⟩; dsimp; congr)
(by intros; refine Over.OverMorphism.ext ?_; simp)
counitIso :=
eqToIso <|
CategoryTheory.Functor.hext (by intro; refine ObjectProperty.FullSubcategory.ext ?_; rfl) (by intros; rfl)
