English
There is a natural isomorphism between a whiskered cocone and a sieve-generated cocone via generateEquivalence.
Русский
Существует естественное изоморфизм между взбитой (заводимой) верхушечной конусной структурой и коконом, порождаемым решеткой через generateEquivalence.
LaTeX
$$$\text{whiskerIsoMapGenerateCocone}: \text{...} \cong \text{...}$$$
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_inverse' (hY : Y = iSup U) :
OpensLeCover U ⥤
(ObjectProperty.FullSubcategory fun f : Over Y => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom)
where
obj := fun V =>
⟨⟨V.obj, ⟨⟨⟩⟩, homOfLE <| hY ▸ (V.2.choose_spec.trans (le_iSup U (V.2.choose)))⟩,
⟨U V.2.choose, V.2.choose_spec.hom, homOfLE <| hY ▸ le_iSup U V.2.choose, ⟨V.2.choose, rfl⟩, rfl⟩⟩
map {_ _} g := Over.homMk g
map_id
_ := by
refine Over.OverMorphism.ext ?_
simp only [Functor.id_obj, Sieve.generate_apply, Functor.const_obj_obj, Over.homMk_left,
eq_iff_true_of_subsingleton]
map_comp {_ _ _} f
g := by
refine Over.OverMorphism.ext ?_
simp only [Functor.id_obj, Sieve.generate_apply, Functor.const_obj_obj, Over.homMk_left,
eq_iff_true_of_subsingleton]
