English
The diagram over pairwise opens is isomorphic to the corresponding mapped diagram after transporting along the equivalence.
Русский
Диаграмма по парным открытым множествам изомормична соответствующей отображаемой диаграмме после переноса по эквивалентности.
LaTeX
$$$\text{pairwiseDiagramIso }(U) : \text{Pairwise.diagram } U \cong (\text{pairwiseToOpensLeCover } U) \circ \iota$$$
Lean4
/-- Given a family of opens `opensLeCoverCocone U` is essentially the natural cocone
associated to the sieve generated by the presieve associated to `U` with indexing
category changed using the above equivalence. -/
@[simps]
def whiskerIsoMapGenerateCocone (hY : Y = iSup U) :
(F.mapCone (opensLeCoverCocone U).op).whisker (generateEquivalenceOpensLe U hY).op.functor ≅
F.mapCone (Sieve.generate (presieveOfCoveringAux U Y)).arrows.cocone.op
where
hom :=
{ hom := F.map (eqToHom (congr_arg op hY.symm))
w := fun j => by
erw [← F.map_comp]
dsimp
congr 1 }
inv :=
{ hom := F.map (eqToHom (congr_arg op hY))
w := fun j => by
erw [← F.map_comp]
dsimp
congr 1 }
hom_inv_id := by
ext
simp [eqToHom_map]
inv_hom_id := by
ext
simp [eqToHom_map]
