limitFlipCompLimIsoLimitCompLim — Mathlib

English

The inverse of the limit isomorphism composes with the pair of projections to recover the pair projections: (limitUncurryIsoLimitCompLim F).inv ∘ π_(j,k) = π_j ∘ π_k.

Русский

Обратный изоморфизм предела композитной структуры восстанавливает пару проекций: (limitUncurryIsoLimitCompLim F).inv ∘ π_(j,k) = π_j ∘ π_k.

LaTeX

$$$(\text{limitUncurryIsoLimitCompLim } F)^{-1} \circ \text{limit.π}_{(j,k)} = \text{limit.π}_j \circ \text{limit.π}_k$$$

Lean4

/-- The limit of `F.flip ⋙ lim` is isomorphic to the limit of `F ⋙ lim`. -/
noncomputable def limitFlipCompLimIsoLimitCompLim : limit (F.flip ⋙ lim) ≅ limit (F ⋙ lim) :=
  (limitUncurryIsoLimitCompLim _).symm ≪≫
    HasLimit.isoOfNatIso (uncurryObjFlip _) ≪≫
      HasLimit.isoOfEquivalence (Prod.braiding _ _) (NatIso.ofComponents fun _ => by rfl) ≪≫
        limitUncurryIsoLimitCompLim _

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