isLimitOpensLeCoverEquivPairwise — Mathlib

English

The morphisms on the pairwise level map to corresponding morphisms in OpensLeCover via hom maps defined by inf-le relations.

Русский

Морфизмы на уровне пары отображаются в OpensLeCover соответствующими морфизмами через определения для inf-relations.

LaTeX

$$$\text{pairwiseToOpensLeCoverMap} : (V ⟶ W) \mapsto (\text{hom } V W)$ with $(V,W)$ mapped by inf relations.$$

Lean4

/-- The diagram over all `{ V : Opens X // ∃ i, V ≤ U i }` is a limit iff the diagram
over `U i` and `U i ⊓ U j` is a limit. -/
def isLimitOpensLeCoverEquivPairwise :
    IsLimit (F.mapCone (opensLeCoverCocone U).op) ≃ IsLimit (F.mapCone (Pairwise.cocone U).op) :=
  calc
    IsLimit (F.mapCone (opensLeCoverCocone U).op) ≃
        IsLimit ((F.mapCone (opensLeCoverCocone U).op).whisker (pairwiseToOpensLeCover U).op) :=
      (Functor.Initial.isLimitWhiskerEquiv (pairwiseToOpensLeCover U).op _).symm
    _ ≃ IsLimit (F.mapCone ((opensLeCoverCocone U).op.whisker (pairwiseToOpensLeCover U).op)) :=
      (IsLimit.equivIsoLimit F.mapConeWhisker.symm)
    _ ≃
        IsLimit
          ((Cones.postcomposeEquivalence _).functor.obj
            (F.mapCone ((opensLeCoverCocone U).op.whisker (pairwiseToOpensLeCover U).op))) :=
      (IsLimit.postcomposeHomEquiv _ _).symm
    _ ≃
        IsLimit
          (F.mapCone
            ((Cones.postcomposeEquivalence _).functor.obj
              ((opensLeCoverCocone U).op.whisker (pairwiseToOpensLeCover U).op))) :=
      (IsLimit.equivIsoLimit (Functor.mapConePostcomposeEquivalenceFunctor _).symm)
    _ ≃ IsLimit (F.mapCone (Pairwise.cocone U).op) :=
      IsLimit.equivIsoLimit ((Cones.functoriality _ _).mapIso (pairwiseCoconeIso U :).symm)

Похожие утверждения